Associated bundle is locally trivial and functorial under pullback

If $q_0:X\to Y$ is any quotient and $V\subseteq Y$ is open, its restriction $q_0^{-1}(V)\to V$ is quotient. Indeed an inverse image open in $q_0^{-1}(V)$ is open in $X$, since this domain is open; it equals the full inverse image of the tested subset of $V$, which is therefore open in $Y$ and in $V$. Conversely any open in $V$ is open in $Y$ and pulls back to an open. Apply this to $V=r^{-1}(U)$ for a principal chart domain $U$; F1 makes $V$ open, and its preimage is ${\pi }^{-1}(U)\times F$.

In a principal chart write $\theta (p)=(\pi (p),a(p))$ and $s(b)={\theta }^{-1}(b,1)$. Then $p=s(\pi (p))a(p)$ and $a(pg)=a(p)g$. The functions $a,s$ are continuous. Hence $(p,x)\mapsto (\pi (p),a(p)x)$ is continuous and constant on each orbit, since $a(pg)g^{-1}x=a(p)x$. By step 1.1 and F2 it descends to a continuous $\chi :r^{-1}(U)\to U\times F$. Its inverse is $\psi (b,y)=[s(b),y]$, continuous by F3–F4 and the quotient map. The identities are $\chi \psi (b,y)=(b,y)$ and $\psi \chi [p,x]=[s(\pi (p)),a(p)x]=[p,x]$. This proves local triviality.

On a chart overlap, write $s_j(b)=s_i(b)c_{ij}(b)$, so $c_{ij}=a_i\circ s_j$ is continuous. The associated transition is $(b,y)\mapsto (b,c_{ij}(b)y)$. Uniqueness of principal coordinates gives $c_{ii}=1$ and $c_{ik}=c_{ij}{c}_{jk}$, so the action law gives exactly the bundle cocycle identities, even if different group elements act identically on $F$.

The principal pullback $h^{\ast }P=\{(a,p):h(a)=\pi (p)\}$ has action $(a,p)g=(a,pg)$. Over $h^{-1}(U)$ its equivariant chart is $(a,p)\mapsto (a,a(p))$, where the second $a(p)$ denotes the principal coordinate from step 2.1, not the base variable. Its continuous inverse is $(a,g)\mapsto (a,{\theta }^{-1}(h(a),g))$. These coordinate formulas and F3–F4 prove it is a principal bundle. The prequotient map $((a,p),x)\mapsto (a,[p,x])$ is continuous into $A\times Q$, lands in $h^{\ast }Q$, and is invariant under the diagonal action. It therefore descends continuously to $\mathrm{\Phi }$ by F2.

Over $h^{-1}(U)$ both sides of $\mathrm{\Phi }$ have associated coordinates $(a,a(p)x)$, and $\mathrm{\Phi }$ becomes the identity on $h^{-1}(U)\times F$. Thus it is bijective on every fiber, and its inverse is continuous on the open cover of the target by these chart domains. F5 makes the inverse globally continuous. This proves the asserted bundle isomorphism without claiming that products preserve arbitrary quotient maps.

For $k:T\to A$, the canonical principal pullback identification sends $(t,(k(t),p))$ to $(t,p)$, with continuous inverse inserting $k(t)$. The associated and ordinary pullback identifications are analogous. Starting from $[(t,(k(t),p)),x]$, either order of the comparisons gives $(t,[p,x])$. The two maps are therefore equal on all points. The identity base map similarly deletes the redundant coordinate $\pi (p)$ and gives identity compatibility. Repeated compositions forget the same redundant coordinates regardless of parentheses, proving the promised naturality.

Empty $A$ gives empty pullbacks; empty $B$ forces $P$ and any domain $A$ of $h$ empty. Empty $F$ gives empty associated total spaces, and every chart is the empty homeomorphism. Singleton $F$ gives the base, and the trivial group gives the ordinary product formulas. No numerical time or homotopy endpoints occur. Each chart is examined one at a time and every descended map is uniquely determined before its continuity check; no simultaneous representative or chart choices are used. This completes the proof.