Transverse preimages carry the pulled-back normal structure

Around $x\in P$ choose a bundle chart of $E$ over $U\subseteq B$ and use [F1] to view it as a smooth chart of the target near $f(x)$; on $W$ write $f=(g,h)$ with $h$ valued in ${\mathbb{R}}^r$ and $g$ valued in $U$, so that $P\cap W=h^{-1}(0)$ and the normal space of the zero section at $f(x)$ is identified with the fibre $E_{g(x)}={\mathbb{R}}^r$. By [F2] applied to the smooth map $f{\mathrm{\mid }}_W$ and the embedded zero section, transversality at $x$ is exactly surjectivity of $d{h}_x$. If another trivialization replaces $h$ by $T(g(x))h(x)$ with $T$ a smooth invertible matrix function, then at $h=0$ its derivative is $T(g(x))d{h}_x$, so surjectivity is chart-independent and the transition acts on the normal quotient by the same matrix.

Restricted to $W\cap \mathrm{Int}X$, the map $f$ takes values in the smooth stratum and, by step 1.1, is transverse to the embedded zero section there. The published transverse preimage theorem [F3] therefore makes $P$ an embedded submanifold of codimension $r$ of that open set, with $T_{x}P=\{v\in T_{x}X:d{f}_x(v)\in T_{f(x)}{0}_B\}=\ker d{h}_x$. Since the interior points of $P$ are covered by these open sets, the interior part of $P$ is an embedded submanifold with the asserted tangent space.

The differential $d{h}_x$ factors through the quotient to a linear isomorphism $T_{x}X\mathrm{/}{T}_{x}P\to E_{g(x)}$. Step 1.1 shows that these local isomorphisms transform by exactly the transition matrices of $E$, so they glue to a smooth bundle isomorphism $\nu (P\subset X)\to (g{\mathrm{\mid }}_P{)}^{\ast }E$ over $P\cap \mathrm{Int}X$; smoothness of the normal bundle is [F5].

Let $x\in P\cap \mathrm{\partial }X$ and use boundary coordinates $(u,t)$ with $t\ge 0$. By [F7], the fibre coordinate $h(u,t)$ extends smoothly across $t=0$ near $x$. Boundary transversality says $d_{u}h(u,0)$ is surjective at $x$; hence, after reordering the $n-1$ tangential coordinates, an $r\times r$ minor in the first $r$ coordinates of $u$ is invertible. The map $(u,t)\mapsto (h(u,t),u_{r+1},\dots ,u_{n-1},t)$ has invertible derivative, so [F6] makes it a local diffeomorphism. Its last coordinate is exactly the original $t$, so it maps the source half-space to $\{t\ge 0\}$, without assuming an arbitrary nonlinear image of a half-space is linear. In these coordinates $P$ is precisely $\{h=0,t\ge 0\}$, with boundary $\{h=0,t=0\}$, and its tangent space is $\ker dh$. These charts prove neateness. The same local normal quotient map as step 3.1 is a smooth bundle isomorphism at boundary points, and $T_x\mathrm{\partial }X\mathrm{/}{T}_x\mathrm{\partial }P\to T_{x}X\mathrm{/}{T}_{x}P$ is an isomorphism since $dh{\mathrm{\mid }}_{T_x\mathrm{\partial }X}$ is surjective. Thus its restriction is exactly the boundary normal identification. When $r=0$, the coordinate map is the identity and the same conclusion holds.

For $r>0$ and nonempty $B$, the zero section is closed in $D(E)$ and disjoint from $S(E)$; its saturation under the sphere collapse is itself, so the quotient topology makes its image closed. Passing to the compactly generated topology preserves this closed set. If $r=0$, [F1] uses the based empty-subspace quotient $B\mathrm{/}\mathrm{\varnothing }=B_{+}$, so $B$ and its added isolated basepoint are separate clopen pieces. Thus $0_B$ is closed for every rank, and $P=f^{-1}(0_B)$ is closed and therefore compact for compact $X$; in rank zero it is also open. For empty $B$, $0_B=\mathrm{\varnothing }$ and every conclusion is vacuous. No choice beyond [A1] is used.