[proofplan] We double-count the set of pairs $(g, x) \in G \times X$ satisfying $g \cdot x = x$. Summing over group elements yields $\sum_{g \in G} |X^g|$; summing over set elements yields $\sum_{x \in X} |G_x|$, where $G_x$ is the stabiliser of $x$. The [Orbit-Stabiliser Theorem](/theorems/???) converts each stabiliser size into $|G| / |G \cdot x|$, so the sum over $x$ telescopes to $|G|$ times the number of orbits. Equating the two counts gives the result. [/proofplan] [step:Double-count the set of pairs $(g, x)$ with $g \cdot x = x$] Define the set \begin{align*} S = \{(g, x) \in G \times X : g \cdot x = x\}. \end{align*} Since $G$ and $X$ are both finite, $S$ is a finite subset of $G \times X$. We compute $|S|$ in two ways. **Summing over $G$:** For each $g \in G$, the fibre $\{x \in X : (g, x) \in S\} = X^g$. Therefore \begin{align*} |S| = \sum_{g \in G} |X^g|. \end{align*} **Summing over $X$:** For each $x \in X$, define the stabiliser $G_x = \{g \in G : g \cdot x = x\}$. The fibre $\{g \in G : (g, x) \in S\} = G_x$. Therefore \begin{align*} |S| = \sum_{x \in X} |G_x|. \end{align*} Equating the two expressions: \begin{align*} \sum_{g \in G} |X^g| = \sum_{x \in X} |G_x|. \end{align*} [guided] The proof hinges on a single double-counting argument. Define the incidence set \begin{align*} S = \{(g, x) \in G \times X : g \cdot x = x\}. \end{align*} Since $G$ and $X$ are both finite, $S$ is a finite subset of $G \times X$ and we may compute its cardinality in two ways by choosing which coordinate to sum over first. **Summing over group elements first.** For a fixed $g \in G$, the elements $x \in X$ with $(g, x) \in S$ are exactly the fixed points of $g$, namely $X^g = \{x \in X : g \cdot x = x\}$. Ranging over all $g$: \begin{align*} |S| = \sum_{g \in G} |X^g|. \end{align*} **Summing over set elements first.** For a fixed $x \in X$, the elements $g \in G$ with $(g, x) \in S$ are exactly those that fix $x$, namely the stabiliser $G_x = \{g \in G : g \cdot x = x\}$. The stabiliser $G_x$ is a subgroup of $G$ (it contains $e$, is closed under composition and inverses). Ranging over all $x$: \begin{align*} |S| = \sum_{x \in X} |G_x|. \end{align*} Equating the two expressions for $|S|$: \begin{align*} \sum_{g \in G} |X^g| = \sum_{x \in X} |G_x|. \end{align*} The left-hand side is what appears in the formula we want to prove. The task is now to evaluate the right-hand side in terms of the number of orbits. [/guided] [/step] [step:Replace each stabiliser size using the Orbit-Stabiliser Theorem] By the [Orbit-Stabiliser Theorem](/theorems/???), for each $x \in X$ the stabiliser $G_x \le G$ satisfies \begin{align*} |G| = |G \cdot x| \cdot |G_x|, \end{align*} where $G \cdot x = \{g \cdot x : g \in G\}$ is the orbit of $x$. This holds because the map $gG_x \mapsto g \cdot x$ is a well-defined bijection from the set of left cosets $G / G_x$ to the orbit $G \cdot x$, so $|G \cdot x| = [G : G_x] = |G| / |G_x|$. Rearranging: \begin{align*} |G_x| = \frac{|G|}{|G \cdot x|}. \end{align*} Substituting into the identity from the previous step: \begin{align*} \sum_{g \in G} |X^g| = \sum_{x \in X} \frac{|G|}{|G \cdot x|}. \end{align*} [guided] We need to convert stabiliser sizes into orbit sizes. The key tool is the [Orbit-Stabiliser Theorem](/theorems/???), which states: if a finite group $G$ acts on a set $X$ and $x \in X$, then \begin{align*} |G| = |G \cdot x| \cdot |G_x|. \end{align*} Why does this hold? Consider the map $\pi: G \to G \cdot x$ defined by $\pi(g) = g \cdot x$. This map is surjective by definition of the orbit. Two elements $g, h \in G$ satisfy $\pi(g) = \pi(h)$ iff $g \cdot x = h \cdot x$ iff $h^{-1}g \cdot x = x$ iff $h^{-1}g \in G_x$ iff $g \in hG_x$. So the fibres of $\pi$ are exactly the left cosets of $G_x$ in $G$, and the number of such cosets is $[G : G_x] = |G| / |G_x|$ by [Lagrange's Theorem](/theorems/???). Hence $|G \cdot x| = |G| / |G_x|$, or equivalently $|G_x| = |G| / |G \cdot x|$. Substituting into the double-counting identity: \begin{align*} \sum_{g \in G} |X^g| = \sum_{x \in X} |G_x| = \sum_{x \in X} \frac{|G|}{|G \cdot x|}. \end{align*} The right-hand side is a sum over all elements $x \in X$, with each element contributing $|G| / |G \cdot x|$. This is not yet the number of orbits, but we are about to see that grouping by orbit collapses the sum. [/guided] [/step] [step:Group the sum by orbits to obtain $|G|$ times the number of orbits] Let $\mathcal{O}_1, \mathcal{O}_2, \dots, \mathcal{O}_k$ denote the distinct orbits of the action $G \curvearrowright X$, so that $X = \mathcal{O}_1 \sqcup \mathcal{O}_2 \sqcup \cdots \sqcup \mathcal{O}_k$ is a disjoint partition and $k = |X / G|$. For every $x$ in a given orbit $\mathcal{O}_j$, we have $G \cdot x = \mathcal{O}_j$, so $|G \cdot x| = |\mathcal{O}_j|$. Therefore \begin{align*} \sum_{x \in X} \frac{|G|}{|G \cdot x|} = \sum_{j=1}^{k} \sum_{x \in \mathcal{O}_j} \frac{|G|}{|\mathcal{O}_j|} = \sum_{j=1}^{k} |\mathcal{O}_j| \cdot \frac{|G|}{|\mathcal{O}_j|} = \sum_{j=1}^{k} |G| = k \cdot |G|. \end{align*} Combining with the double-counting identity: \begin{align*} \sum_{g \in G} |X^g| = k \cdot |G| = |X / G| \cdot |G|. \end{align*} Dividing both sides by $|G| > 0$: \begin{align*} |X / G| = \frac{1}{|G|} \sum_{g \in G} |X^g|. \end{align*} [guided] The orbits of $G \curvearrowright X$ partition $X$ into disjoint subsets. Let $\mathcal{O}_1, \mathcal{O}_2, \dots, \mathcal{O}_k$ be the distinct orbits, where $k = |X / G|$ is the number of orbits we wish to compute. Then $X = \mathcal{O}_1 \sqcup \mathcal{O}_2 \sqcup \cdots \sqcup \mathcal{O}_k$. The key observation is that if $x \in \mathcal{O}_j$, then $G \cdot x = \mathcal{O}_j$ (every element of an orbit generates the same orbit), so $|G \cdot x| = |\mathcal{O}_j|$. We split the sum accordingly: \begin{align*} \sum_{x \in X} \frac{|G|}{|G \cdot x|} = \sum_{j=1}^{k} \sum_{x \in \mathcal{O}_j} \frac{|G|}{|\mathcal{O}_j|}. \end{align*} In the inner sum, $|G| / |\mathcal{O}_j|$ is constant with respect to $x$, so the inner sum equals $|\mathcal{O}_j| \cdot |G| / |\mathcal{O}_j| = |G|$. Each orbit contributes exactly $|G|$ to the total, regardless of the orbit's size. This is the cancellation that makes the formula work: large orbits have many terms but each is small, while small orbits have few terms but each is large, and in both cases the contribution is $|G|$. Summing over all $k$ orbits: \begin{align*} \sum_{x \in X} \frac{|G|}{|G \cdot x|} = k \cdot |G| = |X / G| \cdot |G|. \end{align*} Returning to the double-counting identity $\sum_{g \in G} |X^g| = \sum_{x \in X} |G_x| = |X / G| \cdot |G|$ and dividing both sides by $|G|$ (which is strictly positive since $G$ is a finite group containing at least the identity): \begin{align*} |X / G| = \frac{1}{|G|} \sum_{g \in G} |X^g|. \end{align*} This is exactly the formula stated in the theorem, completing the proof. [/guided] [/step]