Let be a subgroup of . Then for any two left cosets of in , there is a bijective function between the two cosets.
Let be two cosets. Define the function by .
This has the correct codomain: if (so , say), then so .
The function is injective: if then (pre-multiplying both sides by ) we obtain .
The function is surjective: given , we want to find such that . Let to obtain , as required.