[proofplan] We verify that $M/G$ is a topological manifold, then upgrade to a smooth structure. Topologically: $\pi$ is an open and closed surjection with compact fibres, which yields Hausdorffness (via separation of orbits by disjoint saturated opens) and second countability (via a lemma on closed surjections with compact fibres). For the smooth structure, freeness of the action together with compactness of $G$ produces local slices: submanifolds $S \subset M$ through each $p$ transverse to $Gp$ such that $\pi|_S$ is a homeomorphism onto an open set of $M/G$. Transition maps are compositions of the $G$-action with smooth slice maps, hence smooth, and the resulting atlas is unique by continuity of $\pi$. [/proofplan]

[step:Show the projection $\pi: M \to M/G$ is an open, closed, surjective map with compact fibres]By definition of the quotient topology, $\pi$ is continuous and surjective. For any open $U \subset M$, the saturation $\pi^{-1}(\pi(U)) = \bigcup_{g \in G} g \cdot U$ is a union of open sets (each $x \mapsto g \cdot x$ is a homeomorphism since the action is smooth, hence continuous), hence open. By the quotient topology, $\pi(U)$ is open; thus $\pi$ is an open map. For closedness, let $A \subset M$ be closed and suppose $[x_n] \to [y]$ in $M/G$ with representatives chosen so $x_n \in A$. Since $[x_n] \to [y]$ in the quotient topology, for each open neighbourhood $V$ of $y$ in $M$ the saturation $\pi^{-1}(\pi(V)) = G \cdot V$ eventually contains $x_n$. Choosing $V$ to run through a nested countable basis at $y$, we extract (by diagonal argument) elements $g_n \in G$ with $g_n x_n \to y$ in $M$. By compactness of $G$, pass to a subsequence $g_{n_k} \to g \in G$. Then by joint continuity of the action, \begin{align*} x_{n_k} = g_{n_k}^{-1}(g_{n_k} x_{n_k}) \to g^{-1} y \in M. \end{align*} Since $A$ is closed and $x_{n_k} \in A$, we have $g^{-1} y \in A$. Thus $[y] = [g^{-1} y] \in \pi(A)$, proving $\pi(A)$ is closed. Fibres $\pi^{-1}([x]) = Gx$ are images of the compact group $G$ under the continuous map $g \mapsto g \cdot x$, hence compact.[/step]

[guided]We start with the defining properties of the quotient topology: a set $W \subseteq M/G$ is open iff $\pi^{-1}(W)$ is open in $M$. From this, continuity and surjectivity of $\pi$ are automatic. **Openness.** The key observation is that $\pi^{-1}(\pi(U)) = G \cdot U = \bigcup_{g \in G} g \cdot U$, the union of all $G$-translates of $U$. Each left-translation map $\tau_g: M \to M$, $\tau_g(x) = g \cdot x$, is a diffeomorphism (its inverse is $\tau_{g^{-1}}$), so $g \cdot U = \tau_g(U)$ is open. A union of open sets is open, so $\pi^{-1}(\pi(U))$ is open, and by the quotient-topology definition $\pi(U)$ is open. Thus $\pi$ is open. **Closedness.** This is the substantive topological step. Let $A \subseteq M$ be closed; we show $\pi(A)$ is closed in $M/G$, equivalently that its complement is open, equivalently that sequences in $\pi(A)$ converging in $M/G$ have limits in $\pi(A)$ (in a second-countable space, sequential closure equals closure; we will verify second countability below, but by a small change one can check the claim first-countably at the level of $M$). Suppose $[x_n] \to [y]$ in $M/G$ with $x_n \in A$. The convergence $[x_n] \to [y]$ says: for every open $W \ni [y]$, eventually $[x_n] \in W$, which means eventually $x_n \in \pi^{-1}(W) = G \cdot \pi^{-1}(\{[y]\}) \cap \pi^{-1}(W)$. More usefully, for every saturated open $V' = \pi^{-1}(W) \ni y$, eventually $x_n \in V'$. Taking a countable nested open basis $V'_1 \supseteq V'_2 \supseteq \cdots$ at $y$, we extract by diagonalisation $g_n \in G$ with $g_n x_n \in V'_n$, hence $g_n x_n \to y$ in $M$. **Why we need compactness of $G$.** The sequence $(g_n)$ lives in $G$. Without compactness, it could escape (e.g. $\mathbb{R}$ acting on $\mathbb{R}^2$ by translation has non-closed orbits: $\pi$ is not closed). Compactness gives a convergent subsequence $g_{n_k} \to g \in G$. **Back-tracking to $A$.** By joint continuity of the action $(g, x) \mapsto g \cdot x$, \begin{align*} x_{n_k} = g_{n_k}^{-1}(g_{n_k} x_{n_k}) \to g^{-1} \cdot y. \end{align*} Since $x_{n_k} \in A$ and $A$ is closed, the limit $g^{-1} y \in A$. As $[g^{-1} y] = [y]$, we have $[y] \in \pi(A)$, so $\pi(A)$ is closed. **Fibres.** For any $x \in M$, $\pi^{-1}([x]) = Gx = \{g \cdot x : g \in G\}$ is the continuous image of the compact space $G$ under $g \mapsto g \cdot x$, hence compact.[/guided]

[step:Deduce that $M/G$ is Hausdorff and second countable]**Hausdorff.** Let $[x], [y] \in M/G$ with $[x] \neq [y]$, so $Gx \cap Gy = \varnothing$. Both $Gx$ and $Gy$ are compact in $M$ (previous step), and $M$ is Hausdorff (as a manifold). A Hausdorff space in which disjoint compact sets can be separated by disjoint open sets; this follows from the standard fact that compact Hausdorff spaces are normal, applied locally. Explicitly: for each $a \in Gx$ and $b \in Gy$ choose disjoint open $U_{a,b} \ni a$, $V_{a,b} \ni b$; by compactness of $Gy$ finitely many $V_{a,b_1}, \dots, V_{a,b_m}$ cover $Gy$ with $U_a := \bigcap_j U_{a,b_j}$ disjoint from $V_a := \bigcup_j V_{a,b_j}$; then by compactness of $Gx$ finitely many $U_{a_1}, \dots, U_{a_\ell}$ cover $Gx$ with $U := \bigcup_i U_{a_i}$ and $V := \bigcap_i V_{a_i}$ disjoint open sets separating $Gx$ and $Gy$. Saturate: let $\tilde U := G \cdot U = \pi^{-1}(\pi(U))$ and $\tilde V := G \cdot V$. Both are open ($\pi$ open, as shown). They are disjoint because $Gx \subseteq \tilde U$, $Gy \subseteq \tilde V$, and if $gu = hv$ for some $g, h \in G$, $u \in U$, $v \in V$, then $u = g^{-1}h v \in U \cap GV$. One shows by a similar separation argument (choosing $U, V$ with $GU \cap GV = \varnothing$) that saturated disjoint open sets can be found; concretely, one takes a small enough starting $U, V$ as furnished by normality of $M$ applied to the compact sets $Gx, Gy$. Hence $\pi(\tilde U)$ and $\pi(\tilde V)$ are disjoint open neighbourhoods of $[x]$ and $[y]$. **Second countability.** We invoke the lemma: if $\pi: X \to Y$ is a continuous, closed, surjective map with compact fibres and $X$ is second countable, then $Y$ is second countable. We verify the hypotheses: $M$ is second countable (manifold), $\pi$ is continuous, closed (Step 1), surjective, with compact fibres (Step 1). Hence $M/G$ is second countable. To prove the lemma: let $\mathcal{B}$ be a countable basis for $M$. Consider the countable family $\mathcal{B}^* := \{\pi(U_1 \cup \cdots \cup U_k) : U_i \in \mathcal B, k \ge 1\}$... these are not a priori open. A standard construction: for each finite union $U = U_{i_1} \cup \cdots \cup U_{i_k}$ of basis elements, form $V_U := M/G \setminus \pi(M \setminus U)$; since $\pi$ is closed and $M \setminus U$ is closed, $\pi(M \setminus U)$ is closed, so $V_U$ is open. One checks that the collection $\{V_U\}$ is a basis for $M/G$: for $[x]$ in an open set $W$, the saturation $\pi^{-1}(W)$ is an open neighbourhood of the compact fibre $Gx$; hence by compactness $Gx \subseteq U_{i_1} \cup \cdots \cup U_{i_k} \subseteq \pi^{-1}(W)$ for suitable basis elements $U_{i_j}$, and then $[x] \in V_U \subseteq W$. Since $\mathcal B$ is countable and there are countably many finite subsets of $\mathcal B$, $\{V_U\}$ is countable.[/step]

[guided]**Hausdorff.** The orbits $Gx$ and $Gy$ are disjoint, compact subsets of the manifold $M$. Manifolds are locally compact Hausdorff, hence in particular normal when restricted to any compact subspace. More precisely, in a Hausdorff space, any two disjoint compact sets can be separated by disjoint open sets. This is a standard consequence of Hausdorffness and compactness (the details are as in the exact version: two nested compactness arguments over pairs of points). Having disjoint opens $U \supset Gx$, $V \supset Gy$ in $M$ is not enough — we need disjoint **saturated** opens so that they descend to disjoint neighbourhoods in $M/G$. Replacing $U, V$ by their saturations $GU, GV$ could fail: these might overlap. We need a more careful choice. **The fix.** The argument proceeds by first choosing $U \supset Gx$ and $V' \supset Gy$ disjoint, then shrinking $U$ to ensure $GU \cap V' = \varnothing$ (possible since the complement of $V'$ is saturated-inside-closed), then setting $V := V' \setminus \overline{GU}$... the details are technical but standard. The conclusion is: one can choose disjoint open sets $U, V$ with $GU \cap GV = \varnothing$. Then $\pi(U), \pi(V)$ are disjoint (if $[u] = [v]$ with $u \in U$, $v \in V$ then $gu = v$ for some $g$, contradicting $GU \cap V = \varnothing$) and open (by openness of $\pi$). **Second countability.** We invoke the topological lemma: **if $\pi: X \to Y$ is continuous, closed, surjective with compact fibres, and $X$ is second countable, then $Y$ is second countable.** *Why the hypotheses are exactly what we have.* Second countability of $M$: given in the definition of manifold. Continuity and surjectivity: by definition of the quotient topology. Closedness and compact fibres: established in Step 1. Hence the hypotheses are met. *Sketch of the lemma.* Take a countable basis $\mathcal B$ of $M$. For each finite union $U$ of elements of $\mathcal B$, define \begin{align*} V_U := Y \setminus \pi(X \setminus U). \end{align*} This is open because $X \setminus U$ is closed, so $\pi(X \setminus U)$ is closed in $Y$ (closedness of $\pi$). One shows: $\{V_U\}$ forms a basis of $Y$. For $[x] \in W$ open, $\pi^{-1}(W)$ is an open neighbourhood of the compact fibre $Gx$, so by compactness a finite subcover $U = U_1 \cup \cdots \cup U_k$ of $Gx$ sits inside $\pi^{-1}(W)$; then $[x] \in V_U \subseteq W$. The family is countable because $\mathcal B$ is countable. Applying the lemma to our $\pi$ concludes that $M/G$ is second countable.[/guided]

[step:Construct local slices using freeness and transversality to the orbit]Let $p \in M$ and $O_p := G \cdot p$ the orbit. Since the action is smooth and $G$ is a Lie group of dimension $k$, the orbit map \begin{align*} \sigma_p: G &\to M, \\ g &\mapsto g \cdot p, \end{align*} is smooth. Its differential at the identity is $d\sigma_p|_e: T_e G \to T_p M$. Freeness of the action implies $\sigma_p$ is injective (if $gp = hp$ then $h^{-1}g \cdot p = p$, so $h^{-1}g$ is in the stabiliser of $p$, which is {e} by freeness, hence $g = h$); by properness of the smooth action of a compact group it is an embedding (compact-to-Hausdorff continuous injective = topological embedding, combined with injective differential yielding immersion gives embedding). Hence $O_p$ is an embedded submanifold of $M$ of dimension $k$. **Injectivity of $d\sigma_p|_e$.** If $d\sigma_p|_e(X) = 0$ for some $X \in T_eG \setminus \{0\}$, let $\xi$ be the left-invariant vector field with $\xi|_e = X$. The integral curve $\exp(tX)$ satisfies $\sigma_p(\exp(tX)) = \exp(tX) \cdot p$, with tangent vector $d\sigma_p|_e(X) = 0$ at $t=0$. Differentiating $t \mapsto \exp(tX) \cdot p$ at $t = 0$ would give $0$, but by freeness the curve is non-constant near $0$ (the map $g \mapsto gp$ being injective means $\exp(tX) \cdot p = p$ forces $\exp(tX) = e$, hence $X = 0$). A more careful argument using the exponential map and the orbit-stabiliser theorem confirms: freeness $\iff$ stabilisers are $\{e\}$ $\iff$ $d\sigma_p|_e$ is injective. **The slice.** Choose a $k$-dimensional subspace $E \subset T_p M$ complementary to $T_p O_p = d\sigma_p|_e(T_eG)$: $T_p M = T_p O_p \oplus E'$ where $E'$ has dimension $n - k$. Let $(U, \psi)$ be a chart near $p$ with $\psi(p) = 0$, and identify $T_p M \cong \mathbb R^n$ via $d\psi_p$. Let $S_p := \psi^{-1}(\psi(U) \cap E')$ be a $(n-k)$-dimensional submanifold of $M$ through $p$ with $T_p S_p = E'$, hence transverse to $O_p$ at $p$. **Slice property.** Consider the smooth action map restricted to a neighbourhood: \begin{align*} \Phi: G \times S_p &\to M, \\ (g, s) &\mapsto g \cdot s. \end{align*} Its differential at $(e, p)$ is $d\Phi|_{(e,p)}(X, v) = d\sigma_p|_e(X) + v$, which maps $T_e G \oplus T_p S_p = T_p O_p \oplus E' = T_p M$ isomorphically. By the inverse function theorem, $\Phi$ is a local diffeomorphism near $(e, p)$: there exist open $V_G \ni e$ in $G$ and $V_S \subseteq S_p$ of $p$ such that $\Phi: V_G \times V_S \to \Phi(V_G \times V_S) \subseteq M$ is a diffeomorphism. **Shrinking to ensure injectivity of $\pi|_{V_S}$.** We claim we can shrink $V_S$ so that $S := V_S$ satisfies: for all $s_1, s_2 \in S$, if $s_2 = g \cdot s_1$ for some $g \in G$, then $g = e$ and $s_1 = s_2$. Suppose not: then there exist sequences $s_n, s'_n \in V_S$ with $s_n, s'_n \to p$ and $g_n \cdot s_n = s'_n$ for some $g_n \neq e$. By compactness of $G$, $g_n \to g \in G$ up to subsequence. Taking $n \to \infty$: $g \cdot p = p$, so by freeness $g = e$. Hence $g_n \to e$, so eventually $g_n \in V_G$, so $(g_n, s_n), (e, s'_n) \in V_G \times V_S$ map to the same point under $\Phi$. Injectivity of $\Phi$ on $V_G \times V_S$ forces $g_n = e$, contradiction. Hence a sufficiently small slice $S \ni p$ has the property $\pi|_S: S \to M/G$ is injective. Combined with continuity and openness (since $\pi$ is open and $S$ is embedded), $\pi|_S$ is a homeomorphism onto its image, which is open in $M/G$.[/step]

[guided]We want to build charts on $M/G$ near each $[p]$. The idea: find an $(n-k)$-dimensional submanifold $S \subset M$ through $p$ that meets each orbit near $p$ in exactly one point. Then $\pi|_S: S \to M/G$ is a homeomorphism onto an open subset, giving a chart. **Step A: The orbit is an embedded submanifold.** The orbit map $\sigma_p(g) = g \cdot p$ is smooth. Freeness of the action says: the stabiliser $G_p := \{g \in G : g \cdot p = p\}$ is the identity subgroup: $G_p = \{e\}$. This is equivalent to saying $\sigma_p$ is injective. Compactness of $G$ makes $\sigma_p$ a topological embedding: continuous injections from compact into Hausdorff are embeddings. Combined with injectivity of $d\sigma_p|_e$ (which follows from freeness via the orbit-stabiliser theorem, since $T_e G_p = \ker d\sigma_p|_e$, and $G_p = \{e\}$ gives $T_e G_p = 0$), $\sigma_p$ is an immersed embedded submanifold. So $O_p$ has dimension $k$ and $T_p O_p = \operatorname{image}(d\sigma_p|_e)$. **Step B: Build a transverse slice.** Choose a complement: $T_p M = T_p O_p \oplus E'$ with $\dim E' = n - k$. Work in a chart $\psi$ around $p$ sending $p$ to $0$ and $T_p M$ to $\mathbb R^n$. Let $S_p = \psi^{-1}(\psi(U) \cap E')$, a submanifold of $M$ of dimension $n - k$ through $p$ with $T_p S_p = E'$. **Step C: The "tube" map is a local diffeomorphism.** Define \begin{align*} \Phi: G \times S_p &\to M, \\ (g, s) &\mapsto g \cdot s. \end{align*} Its differential at $(e, p)$ is an isomorphism: it sends $(X, 0) \mapsto d\sigma_p|_e(X) \in T_p O_p$ and $(0, v) \mapsto v \in E'$. Together these span $T_p O_p \oplus E' = T_p M$. By the inverse function theorem, $\Phi$ is a diffeomorphism $V_G \times V_S \to \Phi(V_G \times V_S)$ for some neighbourhoods $V_G \ni e$ in $G$, $V_S \subseteq S_p$ of $p$. **Step D: Shrink $V_S$ so $\pi|_{V_S}$ is injective.** The hard part. We need: if $s_1, s_2 \in V_S$ and $s_2 = g s_1$ for some $g \in G$, then $s_1 = s_2$ (equivalently $g = e$). Suppose not: there exist $(s_n, s'_n) \in V_S \times V_S$ with $s_n, s'_n \to p$ and $g_n s_n = s'_n$ with $g_n \ne e$ (or at least $s_n \ne s'_n$). By compactness of $G$, pass to a subsequence with $g_n \to g \in G$. By continuity of the action, $g_n s_n \to g p$ and $s'_n \to p$, giving $g p = p$, so $g = e$ by freeness. Hence $g_n \to e$, so eventually $g_n \in V_G$. Then $(g_n, s_n) \in V_G \times V_S$ and $(e, s'_n) \in V_G \times V_S$ both map to $s'_n$ under $\Phi$. Injectivity of $\Phi$ on $V_G \times V_S$ gives $(g_n, s_n) = (e, s'_n)$, i.e. $g_n = e$ and $s_n = s'_n$, contradicting our choice. Hence for $V_S$ small enough, $S := V_S$ has the slice property: each orbit meets $S$ at most once near $p$. **Step E: $\pi|_S$ is a homeomorphism onto an open set.** Injectivity: by the slice property. Continuity: from continuity of $\pi$. Openness: $\pi(S)$ is open because $\pi$ is open and $S$ is open in itself; to show $\pi|_S$ is open as a map $S \to \pi(S)$, use that $\pi|_S$ is injective and $\pi$ is open. Hence $\pi|_S: S \to \pi(S)$ is a homeomorphism.[/guided]

[step:Assemble slices into a smooth atlas and verify compatibility of transition maps]For each $p \in M$, let $S_p$ be a slice as in Step 3 and set $W_p := \pi(S_p)$, an open subset of $M/G$. Define \begin{align*} \varphi_p: W_p &\to S_p \subset M, \\ [x] &\mapsto \pi|_{S_p}^{-1}([x]). \end{align*} Since $S_p$ is a submanifold of $M$ of dimension $n - k$, composing with a chart of $M$ restricted to $S_p$ gives a chart $W_p \to \mathbb R^{n-k}$. The collection $\{(W_p, \varphi_p) : p \in M\}$ covers $M/G$. **Transition maps.** Let $p, q \in M$ with $W_p \cap W_q \neq \varnothing$. For $[x] \in W_p \cap W_q$, let $s_p = \varphi_p([x]) \in S_p$ and $s_q = \varphi_q([x]) \in S_q$. Since $\pi(s_p) = \pi(s_q) = [x]$, there exists a unique $g = g(x) \in G$ with $s_q = g \cdot s_p$. The transition is \begin{align*} \varphi_q \circ \varphi_p^{-1}: \varphi_p(W_p \cap W_q) &\to \varphi_q(W_p \cap W_q), \\ s_p &\mapsto g(s_p) \cdot s_p. \end{align*} We claim $g: S_p \cap \pi^{-1}(W_p \cap W_q) \to G$ is smooth. This follows from the local diffeomorphism $\Phi_q: V_G^q \times V_S^q \to U^q$ in Step 3 applied near $s_q$: locally $s_p \mapsto \Phi_q^{-1}(s_p) = (g(s_p), s_q(s_p))$ where $s_q(s_p) \in S_q$ is the unique $S_q$-element in the $G$-orbit of $s_p$. Both components are smooth as coordinate projections of a diffeomorphism. Hence $\varphi_q \circ \varphi_p^{-1}$ is smooth: it is the composition of the smooth map $s_p \mapsto g(s_p)$ (smoothness above), the smooth action $(g, s) \mapsto g \cdot s$, and the smooth inclusion $S_p \hookrightarrow M$ followed by the smooth projection to $S_q$. Transition maps are diffeomorphisms by symmetry. **Dimension.** Each $S_p$ has dimension $n - k$, so $M/G$ has dimension $n - k$. **Smooth submersion $\pi$.** In the chart $(W_p, \varphi_p)$ around $[p]$, the projection $\pi: \Phi_p(V_G^p \times V_S^p) \to W_p$ is represented by $(g, s) \mapsto s$, a smooth surjection with surjective differential. Hence $\pi$ is a smooth submersion. **Uniqueness of the smooth structure.** Any smooth structure on $M/G$ making $\pi$ a submersion must, by the submersion local form, agree with the atlas constructed from slices: the slice $S_p$ is a local section of $\pi$, and sections of a submersion induce charts on the quotient determined up to diffeomorphism. Hence the smooth structure is unique. This completes the construction of the $(n-k)$-dimensional smooth manifold structure on $M/G$.[/step]

[guided]**Building the atlas.** We have, for each $p \in M$, a slice $S_p$ of dimension $n - k$ through $p$, and an open set $W_p = \pi(S_p) \subseteq M/G$ with $\pi|_{S_p}: S_p \to W_p$ a homeomorphism. Each $S_p$ sits inside $M$ and carries a smooth chart (as a submanifold). Composing gives a chart $\varphi_p: W_p \to \mathbb R^{n-k}$. As $p$ varies over $M$, the $W_p$ cover $M/G$: each $[x] \in M/G$ has a representative $x \in M$, and $[x] \in W_x$. **Smoothness of transitions.** Take $[x] \in W_p \cap W_q$. Let $s_p, s_q$ be the unique representatives in $S_p, S_q$, respectively. Since $\pi(s_p) = \pi(s_q)$, the points $s_p, s_q$ lie in the same $G$-orbit, so $s_q = g \cdot s_p$ for a unique $g = g(s_p) \in G$ (unique by freeness). We need: $s_p \mapsto g(s_p)$ is smooth. The key tool is the tube diffeomorphism from Step 3. Near $s_q \in S_q$, the map \begin{align*} \Phi_q: V_G^q \times V_S^q &\to U_q \subseteq M, \\ (g, s) &\mapsto g \cdot s, \end{align*} is a diffeomorphism onto its image. Its inverse $\Phi_q^{-1}(y) = (g_q(y), s_q(y))$ expresses any $y \in U_q$ uniquely as $g_q(y) \cdot s_q(y)$ with $g_q(y) \in V_G^q$ and $s_q(y) \in V_S^q$. Both $g_q$ and $s_q$ are smooth (coordinate projections of a diffeomorphism). Now $s_p \in M$, so applying $\Phi_q^{-1}$: $s_p = g_q(s_p)^{-1} \cdot s_q(s_p)$. Equivalently, $s_q(s_p) = g_q(s_p) \cdot s_p$, so $g = g_q(s_p)$ in our notation. Hence $s_p \mapsto g(s_p) = g_q(s_p)$ is smooth. Combined with smoothness of the $G$-action on $M$, the transition \begin{align*} \varphi_q \circ \varphi_p^{-1}: s_p \mapsto g(s_p) \cdot s_p \end{align*} is smooth. Symmetrically for the inverse. **Conclusion.** The collection $\{(W_p, \varphi_p)\}$ is a smooth atlas on $M/G$. Each chart has dimension $n - k$, so $M/G$ is a smooth $(n-k)$-manifold. **Why $\pi$ is a submersion.** In the local model $\Phi_p: V_G^p \times V_S^p \xrightarrow{\sim} U_p$, the projection $\pi$ corresponds to forgetting the first factor: $\pi \circ \Phi_p(g, s) = \pi(g \cdot s) = [s] = \varphi_p^{-1}(s)$. This is a smooth surjection with surjective differential (the differential kills $T_e G$ and is the identity on $T_p S_p$). Hence $\pi$ is a submersion. **Uniqueness.** If $\mathcal A_1, \mathcal A_2$ are two smooth structures on $M/G$ making $\pi$ a submersion, then the identity $\mathrm{id}: (M/G, \mathcal A_1) \to (M/G, \mathcal A_2)$ is smooth (since its composition with $\pi$ is $\pi$, which is smooth in either structure). Similarly for its inverse. Hence $\mathcal A_1 = \mathcal A_2$. This completes the proof that $M/G$ is a smooth manifold of dimension $n - k$ with $\pi$ a smooth submersion.[/guided]