[proofplan] We first verify that the formula $[p,f]\mapsto[p,a(f)]$ is independent of the representative of the associated-bundle equivalence class. Then we prove that the map preserves the base point in $M$. Smoothness is checked in associated-bundle local trivializations, where the map becomes the product map $(x,f)\mapsto(x,a(f))$. Finally, identity and composition are verified directly on representatives. [/proofplan]

[step:Check that the formula is independent of representatives]Let $q:P\times F\to P\times_G F$ and $q':P\times F'\to P\times_G F'$ denote the quotient maps. Define a map $\widetilde A:P\times F\to P\times_G F'$ by \begin{align*} \widetilde A(p,f):=[p,a(f)]. \end{align*} We prove that $\widetilde A$ is constant on the equivalence classes defining $P\times_G F$. Suppose $(p_1,f_1),(p_2,f_2)\in P\times F$ satisfy $(p_2,f_2)=(p_1g,g^{-1}\cdot f_1)$ for some $g\in G$. Since $a$ is $G$-equivariant, \begin{align*} a(g^{-1}\cdot f_1)=g^{-1}\cdot a(f_1). \end{align*} Therefore \begin{align*} \widetilde A(p_2,f_2)=[p_1g,a(g^{-1}\cdot f_1)]. \end{align*} Using equivariance in the preceding display, \begin{align*} [p_1g,a(g^{-1}\cdot f_1)]=[p_1g,g^{-1}\cdot a(f_1)]. \end{align*} By the [equivalence relation](/page/Equivalence%20Relation) defining $P\times_G F'$, this last class equals $[p_1,a(f_1)]$. Hence \begin{align*} \widetilde A(p_2,f_2)=\widetilde A(p_1,f_1). \end{align*} Thus there is a unique map $A:P\times_G F\to P\times_G F'$ satisfying \begin{align*} A(q(p,f))=\widetilde A(p,f) \end{align*} for every $(p,f)\in P\times F$, namely $A([p,f])=[p,a(f)]$.[/step]

[guided]The only possible obstruction to defining $A([p,f])=[p,a(f)]$ is that the same point of $P\times_G F$ may have many representatives. We therefore compare two representatives that are related by the defining equivalence relation. Let $q:P\times F\to P\times_G F$ and $q':P\times F'\to P\times_G F'$ denote the quotient maps. Define $\widetilde A:P\times F\to P\times_G F'$ by \begin{align*} \widetilde A(p,f):=[p,a(f)]. \end{align*} To descend $\widetilde A$ to the quotient, we must show that $\widetilde A(p,f)$ has the same value after replacing $(p,f)$ by an equivalent pair. Assume $(p_2,f_2)=(p_1g,g^{-1}\cdot f_1)$ for some $p_1\in P$, $f_1\in F$, and $g\in G$. The equivariance hypothesis on $a:F\to F'$ says precisely that $a(h\cdot f)=h\cdot a(f)$ for every $h\in G$ and $f\in F$. Applying this with $h=g^{-1}$ gives \begin{align*} a(g^{-1}\cdot f_1)=g^{-1}\cdot a(f_1). \end{align*} Therefore \begin{align*} \widetilde A(p_2,f_2)=[p_1g,a(g^{-1}\cdot f_1)]. \end{align*} Substituting the equivariance identity gives \begin{align*} [p_1g,a(g^{-1}\cdot f_1)]=[p_1g,g^{-1}\cdot a(f_1)]. \end{align*} Now the right-hand side is exactly one of the pairs identified with $(p_1,a(f_1))$ in the associated bundle $P\times_G F'$, because the equivalence relation there identifies $(p',f')$ with $(p'g,h^{-1}\cdot f')$ for group elements acting on the fibre. Thus \begin{align*} [p_1g,g^{-1}\cdot a(f_1)]=[p_1,a(f_1)]. \end{align*} Hence $\widetilde A(p_2,f_2)=\widetilde A(p_1,f_1)$. This proves that $\widetilde A$ is constant on equivalence classes, so it descends uniquely to a map $A:P\times_G F\to P\times_G F'$ with $A([p,f])=[p,a(f)]$.[/guided]

[step:Verify that the induced map lies over the identity on $M$] Let $\pi_F:P\times_G F\to M$ and $\pi_{F'}:P\times_G F'\to M$ denote the associated-bundle projections, defined by \begin{align*} \pi_F([p,f])=\pi(p) \end{align*} and \begin{align*} \pi_{F'}([p,f'])=\pi(p). \end{align*} These formulas are well-defined because $\pi(pg)=\pi(p)$ for the right principal action of $G$ on $P$. For every $[p,f]\in P\times_G F$, \begin{align*} \pi_{F'}(A([p,f]))=\pi_{F'}([p,a(f)]). \end{align*} By the definition of $\pi_{F'}$, \begin{align*} \pi_{F'}([p,a(f)])=\pi(p). \end{align*} By the definition of $\pi_F$, \begin{align*} \pi(p)=\pi_F([p,f]). \end{align*} Therefore \begin{align*} \pi_{F'}\circ A=\pi_F. \end{align*} So $A$ is a map over $M$. [/step]

[step:Check smoothness in associated local trivializations] Let $U\subset M$ be an [open set](/page/Open%20Set) over which $P$ admits a smooth local section $s:U\to P$. The associated-bundle trivializations determined by $s$ are the maps $\Phi_U:U\times F\to \pi_F^{-1}(U)$ and $\Phi'_U:U\times F'\to \pi_{F'}^{-1}(U)$ defined by \begin{align*} \Phi_U(x,f)=[s(x),f] \end{align*} and \begin{align*} \Phi'_U(x,f')=[s(x),f']. \end{align*} Their inverses are smooth by the standard smooth structure on associated bundles. In these local coordinates, the conjugated map $(\Phi'_U)^{-1}\circ A\circ \Phi_U:U\times F\to U\times F'$ satisfies \begin{align*} ((\Phi'_U)^{-1}\circ A\circ \Phi_U)(x,f)=(x,a(f)). \end{align*} The map $\operatorname{id}_U:U\to U$ is smooth, and $a:F\to F'$ is smooth by hypothesis. Hence the product map $U\times F\to U\times F'$ given by $(x,f)\mapsto(x,a(f))$ is smooth. Since smoothness is local on the source and these associated-bundle trivializations cover $P\times_G F$, the map $A:P\times_G F\to P\times_G F'$ is smooth. [/step]

[step:Verify identity and composition on representatives] If $a=\operatorname{id}_F:F\to F$, then for every $[p,f]\in P\times_G F$, \begin{align*} A([p,f])=[p,\operatorname{id}_F(f)]. \end{align*} Since $\operatorname{id}_F(f)=f$, this gives \begin{align*} A([p,f])=[p,f]. \end{align*} Thus the identity map on $F$ induces $\operatorname{id}_{P\times_G F}$. Now let $F''$ be a smooth left $G$-manifold, and let $b:F'\to F''$ be a smooth $G$-equivariant map. Let $B:P\times_G F'\to P\times_G F''$ denote the map induced by $b$, and let $C:P\times_G F\to P\times_G F''$ denote the map induced by $b\circ a$. For every $[p,f]\in P\times_G F$, \begin{align*} (B\circ A)([p,f])=B([p,a(f)]). \end{align*} By the definition of $B$, \begin{align*} B([p,a(f)])=[p,b(a(f))]. \end{align*} By the definition of $C$, \begin{align*} [p,b(a(f))]=C([p,f]). \end{align*} Therefore $B\circ A=C$. This proves functoriality in the fibre and completes the proof. [/step]