A handle decomposition gives a relative CW complex

Record the attachment comparison explicitly. If $e:Y\to Z$ is a homotopy equivalence and $\alpha :S^{k-1}\to Y$, attach a disk to its mapping cylinder $M_e$ along $\alpha$ in the source end. By [F6], $M_e$ retracts to $Y$ fixing $Y$, so this enlarged space retracts to $Y{\cup }_{\alpha }{D}^k$. Inside $M_e$, the source attaching map is homotopic along its cylinder tracks to the target map $e\alpha$. For a homotopy $H$ of attaching maps, the space formed by attaching $D^k\times I$ along $H$ retracts to either endpoint attachment: use the disk-cylinder retraction onto $(D^k\times \{0\})\cup (S^{k-1}\times I)$, or its reversed version, from [F4]. Hence the enlarged space is also equivalent to the disk attached at the target end, which retracts to $Z{\cup }_{e\alpha }{D}^k$. This proves invariance under replacing the base by a homotopy equivalent model. For equivalences of pairs, carry the base pair through its mapping cylinder; the same retractions restrict to those of the base cylinder, giving equivalences of pairs. If the original base is retained pointwise and the initial equivalence is relative to it, the relative form of [F6] makes all these equivalences relative to it. The case $k=0$ is a disjoint point.

Suppose a CW model $A$ for $M_0$ is available. The initial collar retracts to $M_0$, hence has pair model $(A,A)$. Inductively replace a handle by its core using [F1], transport its attaching map by the current equivalence, and apply step 1.1. By [F2] homotope the resulting map $S^{k_i-1}\to X_{i-1}$ to a cellular one; the attaching sphere has a finite CW structure (two hemispheres, with the usual lower-dimensional cells), so the finite-source clause applies. Step 1.1 also proves invariance under this homotopy. Attaching its disk therefore gives a genuine CW complex $X_i$ with one additional cell of dimension $k_i$ and with base subcomplex $A$. Finite attachments have the quotient weak topology and closure finiteness. Thus the induction gives $(X,A)\simeq (W,M_0)$, and retains the supplied base pointwise when $A=M_0$.

Supply the finite model of $M_0$ without circularity by dimension induction, simultaneously proving that every compact smooth manifold has finite CW homotopy type. In dimension zero, compactness and discreteness give finitely many points, with their zero-cell structure. In dimension $d>0$, present any compact smooth $d$-manifold relative to the empty face by [F5]. Step 2.1 uses the empty CW base and produces an absolute finite CW model, without assuming any model in dimension $d$. For a general $d$-triad, $M_0$ is a compact boundaryless $(d-1)$-manifold and has a finite CW model by the already established lower-dimensional case. Step 2.1 then supplies the asserted model of pairs. This induction uses only the explicit finite attachment comparisons and finite-source cellular approximation, in addition to the ${\mathrm{A}\mathrm{C}}_{\omega }$ Morse and handle suppliers.

There is one relative cell for every original handle, including a disjoint point for index zero and the full-dimensional core cell for index $n$. An empty handle list gives the collar equivalence to the base model. The equivalence is relative to the actual $M_0$ only when its CW structure is supplied; in general it is an equivalence of pairs to $(X,A)$. This proves all the stated assertions and the dimension-induction conclusion.