**Proof plan.** Construct an explicit bijection between the orbit $G \cdot x$ and the coset space $G/G_x$, then invoke [Lagrange's Theorem](/theorems/841) for the finite case. **Step 1: Define the map.** Define \begin{align*} \psi : G/G_x &\to G \cdot x \\ gG_x &\mapsto g \cdot x. \end{align*} **Step 2: Well-definedness.** [claim: Well-Defined Map] $\psi$ is well-defined. [/claim] [proof] If $gG_x = g'G_x$ then $g^{-1}g' \in G_x$, so $(g^{-1}g') \cdot x = x$, giving $g' \cdot x = g \cdot x$. Hence $\psi(gG_x) = \psi(g'G_x)$. [/proof] **Step 3: $\psi$ is a bijection.** [claim: Bijection] $\psi$ is a bijection between $G/G_x$ and $G \cdot x$. [/claim] [proof] Surjectivity: every element $g \cdot x \in G \cdot x$ equals $\psi(gG_x)$. Injectivity: if $\psi(gG_x) = \psi(g'G_x)$ then $g \cdot x = g' \cdot x$, so $(g^{-1}g') \cdot x = x$, meaning $g^{-1}g' \in G_x$, hence $gG_x = g'G_x$. [/proof] **Step 4: Counting.** Since $|G/G_x| = |G : G_x|$, the bijection gives $|G \cdot x| = |G : G_x|$. When $G$ is finite, [Lagrange's Theorem](/theorems/841) yields $|G| = |G_x| \cdot |G : G_x|$, so \begin{align*} |G| = |G_x| \cdot |G \cdot x|. \qquad \square \end{align*}