[<< 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 }