Proof of Burnside's lemma by double counting

Proof

We count the set $F = \set{(g, x) \in G \times X : g \cdot x = x}$ in two ways. Both $G$ and $X$ are finite, and $X/G$ denotes the set of orbits.

1. For fixed $g$, the pairs $(g, x)$ in $F$ correspond to the points $x \in X^g$, the points fixed by $g$. Summing over $g$ gives $\abs{F} = \sum_{g \in G} \abs{X^g}$.
2. For fixed $x$, the pairs $(g, x)$ in $F$ correspond to the elements $g$ of the stabiliser $G_x$. Summing over $x$ gives $\abs{F} = \sum_{x \in X} \abs{G_x}$.
3. By the orbit size formula, $\abs{G_x} = \abs{G} / \abs{G \cdot x}$ for each $x$. So $\abs{F} = \abs{G} \sum_{x \in X} \frac{1}{\abs{G \cdot x}}$.
4. The orbits partition $X$. So we can split the sum in step 3 into one sum for each orbit $O \in X/G$.
5. If $x \in O$, then $G \cdot x = O$, since each point lies in exactly one orbit and $x \in G \cdot x$. So the points of $O$ contribute $\sum_{x \in O} \frac{1}{\abs{O}} = 1$.
6. Hence $\sum_{x \in X} \frac{1}{\abs{G \cdot x}} = \abs{X/G}$, and $\abs{F} = \abs{G} \cdot \abs{X/G}$.
7. Comparing with step 1, $\sum_{g \in G} \abs{X^g} = \abs{G} \cdot \abs{X/G}$. Dividing by $\abs{G} \geq 1$ gives $\abs{X/G} = \frac{1}{\abs{G}} \sum_{g \in G} \abs{X^g}$.