Proof: We define f : G / G x → X {\displaystyle f:G/G_{x}\to X} as follows: g G x {\displaystyle gG_{x}} shall be mapped to g x {\displaystyle gx} . First, we show that this map is well-defined. Indeed, suppose that we take h ∈ G x {\displaystyle h\in G_{x}} . Then g h G x {\displaystyle ghG_{x}} is mapped to g h x = x {\displaystyle ghx=x} . Then we note that the map is surjective by transitivity. Finally, it is also injective, because whenever g x = h x {\displaystyle gx=hx} , we have h − 1 g x = x {\displaystyle h^{-1}gx=x} by applying h − 1 {\displaystyle h^{-1}} to both sides and using a property of a group action, and thus h − 1 g ∈ G x {\displaystyle h^{-1}g\in G_{x}} , that is to say g G x = h G x {\displaystyle gG_{x}=hG_{x}} . That f ( g h G x ) = g ( h x ) {\displaystyle f(ghG_{x})=g(hx)} follows immediately from the definition, so that we do have an isomorphism of representations. ◻ {\displaystyle \Box } We are now in a position to derive some standard formulae for permutation representations. Proof: G {\displaystyle G} acts transitively on G x {\displaystyle Gx} . The above G {\displaystyle G} -isomorphism between G x {\displaystyle Gx} and G / G x {\displaystyle G/G_{x}} is bijective as an isomorphism in the category of sets. But the notation [ G : G x ] {\displaystyle [G:G_{x}]} stood for | G / G x | {\displaystyle |G/G_{x}|} . ◻ {\displaystyle \Box } Proof: G {\displaystyle G} acts transitively on each orbits, and the orbits partition X {\displaystyle X} . Hence, by the orbit-stabilizer theorem, | X | = ∑ j = 1 n | G x j | = ∑ j = 1 n [ G : G x j ] {\displaystyle |X|=\sum _{j=1}^{n}|Gx_{j}|=\sum _{j=1}^{n}[G:G_{x_{j}}]} . ◻ {\displaystyle \Box }