ecause \pi_K is G-equivariant, such a map e exists. Because \pi_G is onto, such a map e is unique. Because the preimage under \pi_K of a G-orbit in N/K is a single G-orbit in N, the map e is one-to-one. Because the maps \pi_{G/K} and \pi_K are onto, the map e is onto.
Thus, the map e is a bijection. To show that it is a diffeomorphism, it remains to show, for every parametrisation p \colon U \to N/G, that p is a plot of N/G if and only if e \circ p is a plot of (N/K)/G.
Fix a parametrisation,
\begin{gathered} p \colon \ U \to N/G.\end{gathered}
Suppose that p is a plot of N/G. Let u \in U. Then there exist an open neighbourhood W of u in U and a plot q \colon W \to N such that p|_W = \pi_G \circ q. The composition \pi_K \circ q is a plot of N/K, and
\begin{gathered} \pi_{G/K} \circ \pi_K \circ q = e \circ \pi_G \circ q = e \circ p|_W.\end{gathered}
Because u \in U was arbitrary, this shows that e \circ p is a plot of (N/K)/G.
Conversely, suppose that e \circ p is a plot of (N/K)/G. Let u \in U. By applying the definition of the quotient diffeology at \pi_{G/K} and then at \pi_K, we obtain an open neighbourhood W of u in U and a plot r \colon W \to N such that
\begin{gathered} e \circ p|_W = \pi_{G/K} \circ \pi_K \circ r .\end{gathered}
By (?) and by the choice of r,
\begin{gathered}e \circ \pi_G \circ r = \pi_{G/K} \circ \pi_K \circ r = e \circ p|_W.\end{gathered}
Because e is one-to-one, this implies that \pi_G \circ r = p|_W. Because u \in U was arbitrary, this shows that p is a plot of N/G. This completes the proof that e is a diffeomorphism.
Because the diagram (?) commutes, \pi_K^* takes \operatorname{Image} \pi_{G/K}^* into \operatorname{Image} \pi_G^*. Because e is a diffeomorphism, we can consider its inverse. From the commuting diagram
\begin{gathered} \xymatrix{
N \ar[rr]^{\pi_K} \ar[d]_{\pi_G} && N/K \ar[d]^{\pi_{G/K}} \\
N/G && (N/K) / G \ar[ll]_{e^{-1}}
} \end{gathered}
we see that \pi_K^* takes \operatorname{Image} \pi_{G/K}^* onto \operatorname{Image} \pi_G^*. Because \pi_K^* is one-to-one (by Lemma 3.1), we have a bijection \pi_K^* \colon \operatorname{Image} \pi_{G/K}^* \to \operatorname{Image} \pi_G^*.
Now suppose that K acts on N properly and with a constant orbit-type, so that N/K is a manifold and \pi_K is a fibre bundle. Then we know that \pi_K^* is a bijection from the differential forms on N/K to the K-basic differential forms on N.
Because \pi_K is G-equivariant, \pi_K^* takes G-invariant forms on N/K to G-invariant forms on N and G-horizontal forms on N/K to G-horizontal forms on N. So we have an injection \pi_K^* \colon \Omega^*_{\rm basic}(N/K) \to \Omega^*_{\rm basic}(N).
Let \alpha be a G-basic form on N. In particular \alpha is K-basic, so there exists a form \beta on N/K such that \alpha = \pi_K^* \beta. Because \pi_K^* is one-to-one and \alpha is G-invariant, \beta is G-invariant. Because \pi_K is G-equivariant and \alpha is G-horizontal, \beta is G-horizontal. This completes the proof that the map \pi_K^* \colon \Omega^*_{\rm basic}(N/K) \to \Omega^*_{\rm basic}(N) is a bijection.