A fixed leafwise cap gives a joint transverse product with exact collar data

Independence of the path. Let $q,q^{\mathrm{\prime }}$ be two paths in $W$ from $x_{\ast }$ to $x$; then $q\ast q^{\mathrm{\prime }-1}$ is a based loop at $x_{\ast }$, null-homotopic in the disk $W$ by [F1]. Composing the null-homotopy with the $C^2$ map $B$ gives a leafwise homotopy in $L$ relative to endpoints between the corresponding leafwise paths, so by [F2] the holonomy germs agree: the transported transversal at $B(x)$ is independent of $q$ near $t=0$. By [F3] each finite transport is a $C^2$ local diffeomorphism germ, so in each fixed local endpoint transversal the finite chart formulas are $C^2$. Subdivide the compact parameter disk into finitely many cells mapping into boxes, and use their finitely many edge-loop relations to choose one common interval $J_0=(-{\delta }_0,{\delta }_0)$; label transitions agree on open cell neighborhoods as in [F4].

Use the fixed smooth field V of any prescribed collar data. When no collar data are prescribed, construct such a field near the compact image: in smooth ambient charts choose constant fields with positive transverse evaluation on smaller domains, and sum finitely many nonnegative compact-set bumps from [F5] whose cores cover the image. Positivity is an open convex condition and coorientation fixes its sign. A field obtained this way is smooth in the ambient smooth charts; no C² foliation-coordinate field is called smooth. If τ is negatively oriented, apply the positive-transversal construction to $t\mapsto \tau (-t)$ and reverse the parameter again in the final product.

Finite continuation data. Because $B(W)$ is compact and covered by finitely many flat boxes, a finite subdivision of the disk $W$ into closed cells carries each cell into one box; combined with step 1.1 this is exactly the finite holonomy-trivial cap continuation required as a hypothesis of [F4].

The product. Applying [F4] to the compact disk $W$, the cap $B$, the field $V$ of step 2.1 and the continuation data of step 3.1 produces a uniform interval $J=(-r,r)\subseteq J_0$ and a jointly $C^2$ map $P:W\times J\to M$ with $P(x,0)=B(x)$, leaf-valued slices, transverse tracks and $d{P}^{-1}(TF)=TW=\ker (dt)$; the interval $J$ is fixed by the finitely many flow-root data of the cap before any collar section is examined.

Exact collar range bookkeeping. Let $C_0\subseteq C$ be a closed collar with $S=t_C(C_0)⋐J$. The set $S$ is compact, because $C_0$ is compact and $t_C$ is continuous, and $S$ is contained in the open interval $J$ with positive distance from its endpoints; hence there is an open interval $I$ with $S⋐I⋐J$. For $x\in C_0$ one has $t_C(x)\in S\subseteq I\subseteq J$, so $P(x,t_C(x))$ is defined, and $f_C(x)=T_x(t_C(x))$ lies in the transported leaf with label $t_C(x)$; the exact collar clause of [F4], whose projection hypothesis on $f_C$ is part of the data, therefore gives $P(x,t_C(x))=f_C(x)$ for every $x\in C_0$, hence also on the interior of $C_0$.

Boundary-zero special case. If $C$ is a collar of $\mathrm{\partial }W$ and $t_C=0$ on the boundary collar, then by continuity of $t_C$ the section range of a sufficiently thin closed collar $C_0\subseteq C$ around $\mathrm{\partial }W$ is arbitrarily close to $0$; since $J$ is an open interval about $0$, such a $C_0$ satisfies $t_C(C_0)⋐J$, so step 5.1 applies.

The construction of $P$ and of the range interval used finitely many boxes, cells, bumps and local roots, so no choice beyond the standing hypothesis [F8] is invoked; steps 4.1–6.1 prove the statement.