orbit-stabilizer theorem

Suppose that $G$ is a group acting (http://planetmath.org/GroupAction) on a set $X$ .For each $x\\in X$ , let $G x$ be the orbit of $x$ ,let $G_{x}$ be the stabilizer of $x$ ,and let ${\\cal L}_{x}$ be the set of left cosets of $G_{x}$ .Then for each $x\\in X$ the function $f\\colon Gx\\to{\\cal L}_{x}$ defined by $gx\\mapsto gG_{x}$ is a bijection.In particular,

|Gx|=[G:G_{x}]

and

|Gx|\\cdot|G_{x}|=|G|

for all $x\\in X$ .

Proof:
If $y\\in Gx$ is such that $y=g_{1}x=g_{2}x$ for some $g_{1},g_{2}\\in G$ ,then we have $g_{2}^{-1}g_{1}x=g_{2}^{-1}g_{2}x=1x=x$ , and so $g_{2}^{-1}g_{1}\\in G_{x}$ ,and therefore $g_{1}G_{x}=g_{2}G_{x}$ .This shows that $f$ is well-defined.

It is clear that $f$ is surjective.If $gG_{x}=g^{\\prime}G_{x}$ , then $g=g^{\\prime}h$ for some $h\\in G_{x}$ ,and so $gx=(g^{\\prime}h)x=g^{\\prime}(hx)=g^{\\prime}x$ .Thus $f$ is also injective.