The Smale–Hirsch immersion theorem

For a connected noncompact source, [F1] applies because such a boundaryless component is open in the no-compact-component sense. Suppose the connected source is closed. For any fixed normal-bundle type $E$ of rank $n-m>0$, its open disk-bundle interior has dimension $n$ and every component is noncompact. Apply [F1] there. The dimension-preserving collar and enriched restriction comparisons of [F2] show that the derivative map on the enriched spaces ${\mathcal{I}}_E\to {\mathcal{F}}_E$ is a weak equivalence.

The enriched spaces are not ordinary formal components. Their forgetful maps over the loci of normal type $E$ are Serre fibrations, with fibre the actual isomorphisms $E\cong \nu$, which after one identification form $\mathrm{Aut}(E)$. The derivative induces the identity on that common fibre. The exact-sequence and component-action comparison in [F2] therefore descends the enriched equivalence to the ordinary locus, at every genuine basepoint. Every formal component meets some such locus, taking $E$ to be the datum's own normal bundle; all compact based homotopies and paths in that locus have their identifications transported by the forgetful lifting comparison. This accounts for their monodromy rather than discarding the identification fibre. Consequently the ordinary closed-source derivative map is a weak equivalence on all components and at every basepoint.

For disconnected $M$, its second-countable component set is at most countable. The weak mapping spaces are products over source components: every tested compact source set meets only finitely many components. Componentwise maps and homotopies therefore compute homotopy groups and components of the product. The component comparisons of steps 1.1–2.1 give all higher isomorphisms, and countable choice gives the product component bijection. Empty sources give singleton spaces. Thus the ordinary derivative map is a weak equivalence for all the stated sources.

Fix one compact collared parameter neighbourhood $R$ with $Q\subset \mathrm{int}R\subset R\subset W$, where the original data on $W\times M$ are smooth and holonomic. For every closed source component $X$, compactness and the ordinary derivative weak equivalence of steps 1.1–2.1 satisfy exactly the compact-source transfer hypothesis in [F3]. It gives a formal deformation to genuine families, fixed on $R$ before smoothing and hence fixed on a common smaller neighbourhood of $Q$ afterward; smooth original data give a smooth deformation. The finite pair model of $(P,R)$ can be fixed once for all these components. For each noncompact source component apply the direct relative construction of [F1], fixing that same smaller parameter neighbourhood. The at-most-countably many component constructions may be selected by countable choice. Their product homotopy is weakly continuous because every compact source set meets finitely many components; smoothness is local on those open components. This proves the relative conclusions on all of $M$. The compact-source transfer is applied only after ordinary weak equivalence is established by the normal-identification fibration descent, so varying normal-bundle identifications and their monodromy are retained.