[<< wikibooks] Group Theory/Cardinality identities for finite representations
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 }