[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)]$.
[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]
[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]
