A bundle embedding produces its Grassmannian classifying map

In a local frame of $E$, write $j_x$ as a continuous full-rank $N\times n$ matrix $A(x)$. The orthogonal projection onto its image is $P(x)=A(x)(A(x{)}^{\ast }A(x){)}^{-1}A(x{)}^{\ast }$. Invertibility of the positive matrix $A^{\ast }A$ and continuity of matrix inversion make $P$ continuous. The graph chart of [F1] identifies a plane continuously from its projection, so $x\mapsto j(E_x)$ is continuous.

For supplied numerating charts ${\varphi }_s:E{\mathrm{\mid }}_{U_s}\to U_s\times {\mathbb{F}}^n$ and partition $({\rho }_s)$ from [F2], define $J(e)=(\sqrt{{\rho }_s(p(e))}{\varphi }_s(e){)}_{s\in S}$, with a zero coordinate off $U_s$. Support containment makes each zero extension continuous, and local finiteness makes $J$ locally land in a finite coordinate subspace. Some ${\rho }_s(x)>0$ at every $x$, so $J_x$ is injective. This proves the locally finite-coordinate assertion without any choice beyond the supplied data.

The map $\mathrm{\Theta }:E\to c_j^{\ast }{\gamma }_n^N$, $e\mapsto (p(e),j(e))$, is continuous and linear and bijective on every fiber. In the same local frame, its inverse on the image plane is represented by $(A^{\ast }A{)}^{-1}{A}^{\ast }$, which varies continuously. Hence $\mathrm{\Theta }$ is a bundle isomorphism.

Apply the countabilization [F3] to an arbitrary numeration. Using its countable chart domains in step 1.2 gives an embedding into ${\mathbb{F}}^{\mathrm{\infty }}$, continuous for the weak direct-limit topology because it locally lands in a finite stage. This is the exact AC use in the countable clause.

If $X$ is compact Hausdorff, [F4] gives $E\oplus E^{\mathrm{\prime }}\cong X\times {\mathbb{F}}^N$ for finite $N$. Restricting this isomorphism to the first summand gives a finite-dimensional bundle embedding, and steps 1.1–2.1 give its finite Grassmannian map and tautological pullback. The empty base and rank-zero cases use $N=0$ as in [F4].