Homotopy invariance of vector-bundle pullback

For each $x\in X$, compactness of $I$ gives a partition $0=t_0<\cdots <t_r=1$ and neighborhoods $U_{x,j}$ of $x$ such that $\xi$ is trivial on $U_{x,j}\times [t_{j-1},t_j]$. After shrinking to $U_x={\bigcap }_j{U}_{x,j}$, modify each later strip trivialization by its transition matrix at the common endpoint; consecutive trivializations then agree there and paste. Thus $\xi {\mathrm{\mid }}_{U_x\times I}$ is trivial.

Apply [A1] and [F2] to the cover $(U_x)$. Apply the countabilization [F3] to obtain a countable open cover $(V_m)$ and a locally finite partition $({\lambda }_m)$ with $\mathrm{supp}{\lambda }_m\subseteq V_m$, where each $V_m$ is a disjoint union of open sets contained in members of the original cover. Pasting the corresponding trivializations over those disjoint pieces makes $\xi {\mathrm{\mid }}_{V_m\times I}$ trivial.

Put ${\psi }_0=0$, ${\psi }_m={\sum }_{j\le m}{\lambda }_j$, and let $X_m\subseteq X\times I$ be the graph of ${\psi }_m$. Over $V_m\times I$, its chosen trivialization transports a vector vertically from $(x,{\psi }_m(x))$ to $(x,{\psi }_{m-1}(x))$. Outside $\mathrm{supp}{\lambda }_m$ the two graph points agree, so extending by the identity gives a continuous bundle isomorphism $h_m:\xi {\mathrm{\mid }}_{X_m}\to \xi {\mathrm{\mid }}_{X_{m-1}}$.

Near any $x$, choose $M$ so every ${\lambda }_m$ with $m>M$ vanishes there. On that neighborhood ${\psi }_M=1$, and $h_1\circ \cdots \circ h_M$ carries the restriction over the graph of $1$ to the graph of $0$. Enlarging $M$ does not change this map locally because the added $h_m$ are identities. These local formulas therefore define a continuous fiberwise-linear isomorphism $\xi {\mathrm{\mid }}_{X\times \{1\}}\to \xi {\mathrm{\mid }}_{X\times \{0\}}$. Reversing the finite local composites gives its continuous inverse.

By [F1] the two endpoint restrictions are precisely $f_1^{\ast }E$ and $f_0^{\ast }E$, so step 4.1 proves the assertion. AC was used in step 2.1 to supply DC and countabilize the arbitrary partition; the finite strip constructions are choice-free once their data are supplied. Different partitions and charts can give different endpoint maps, which is why no canonical isomorphism is claimed.