Let $G$ be a finite group, acting on a set $X$. Let $x\in X$. Writing ${Stab}_G\left(x\right)$ for the stabiliser of $x$, and ${Orb}_G\left(x\right)$ for the orbit of $x$, we have $$|G|=|{Stab}_G\left(x\right)|\times |{Orb}_G\left(x\right)|$$ where $|\cdot |$ refers to the size of a set.

This statement generalises to infinite groups, where the same proof goes through to show that there is a bijection between the left cosets of the group ${Stab}_G\left(x\right)$ and the orbit ${Orb}_G\left(x\right)$.

Proof

Recall that the stabiliser is a subgroup of the parent group.

Firstly, it is enough to show that there is a bijection between the left cosets of the stabiliser, and the orbit. Indeed, then $$|{Orb}_G\left(x\right)||{Stab}_G\left(x\right)|=|\left\{\text{left cosets of}{Stab}_G\right(x\left)\right\}||{Stab}_G\left(x\right)|$$ but the right-hand side is simply $|G|$ because an element of $G$ is specified exactly by specifying an element of the stabiliser and a coset. (This follows because the cosets partition the group.)

Finding the bijection

Define $\theta :{Orb}_G\left(x\right)\to \left\{\text{left cosets of}{Stab}_G\right(x\left)\right\}$, by $$g\left(x\right)\mapsto g{Stab}_G\left(x\right)$$

This map is well-defined: note that any element of ${Orb}_G\left(x\right)$ is given by $g\left(x\right)$ for some $g\in G$, so we need to show that if $g\left(x\right)=h\left(x\right)$, then $g{Stab}_G\left(x\right)=h{Stab}_G\left(x\right)$. This follows: $h^{-1}g\left(x\right)=x$ so $h^{-1}g\in {Stab}_G\left(x\right)$.

The map is injective: if $g{Stab}_G\left(x\right)=h{Stab}_G\left(x\right)$ then we need $g\left(x\right)=h\left(x\right)$. But this is true: $h^{-1}g\in {Stab}_G\left(x\right)$ and so $h^{-1}g\left(x\right)=x$, from which $g\left(x\right)=h\left(x\right)$.

The map is surjective: let $g{Stab}_G\left(x\right)$ be a left coset. Then $g\left(x\right)\in {Orb}_G\left(x\right)$ by definition of the orbit, so $g\left(x\right)$ gets taken to $g{Stab}_G\left(x\right)$ as required.

Hence $\theta$ is a well-defined bijection.