let G be Group; :: thesis: for A being Subset of G holds card (con_class A) = Index (Normalizator A)
let A be Subset of G; :: thesis: card (con_class A) = Index (Normalizator A)
defpred S₁[ set , set ] means ex a being Element of G st
( $1 = A |^ a & $2 = (Normalizator A) * a );
A1: for x, y1, y2 being set st x in con_class A & S₁[x,y1] & S₁[x,y2] holds
y1 = y2

proof

let x, y1, y2 be set ; :: thesis: ( x in con_class A & S₁[x,y1] & S₁[x,y2] implies y1 = y2 )
assume x in con_class A ; :: thesis: ( not S₁[x,y1] or not S₁[x,y2] or y1 = y2 )
given a being Element of G such that A2: x = A |^ a and
A3: y1 = (Normalizator A) * a ; :: thesis: ( not S₁[x,y2] or y1 = y2 )
given b being Element of G such that A4: x = A |^ b and
A5: y2 = (Normalizator A) * b ; :: thesis: y1 = y2
A = (A |^ b) |^ (a " ) by A2, A4, Th63
.= A |^ (b * (a " )) by Th56 ;
then b * (a " ) in Normalizator A by Th154;
hence y1 = y2 by A3, A5, GROUP_2:143; :: thesis: verum

end;

A6: for x being set st x in con_class A holds
ex y being set st S₁[x,y]

proof

let x be set ; :: thesis: ( x in con_class A implies ex y being set st S₁[x,y] )
assume x in con_class A ; :: thesis: ex y being set st S₁[x,y]
then consider B being Subset of G such that
A7: ( x = B & A,B are_conjugated ) ;
consider g being Element of G such that
A8: B = A |^ g by A7, Th104;
reconsider y = (Normalizator A) * g as set ;
take y ; :: thesis: S₁[x,y]
take g ; :: thesis: ( x = A |^ g & y = (Normalizator A) * g )
thus ( x = A |^ g & y = (Normalizator A) * g ) by A7, A8; :: thesis: verum

end;

consider f being Function such that
A9: dom f = con_class A and
A10: for x being set st x in con_class A holds
S₁[x,f . x] from CLASSES1:sch 1(A6);
A11: rng f = Right_Cosets (Normalizator A)

proof

thus rng f c= Right_Cosets (Normalizator A) :: according to XBOOLE_0:def 10 :: thesis: Right_Cosets (Normalizator A) c= rng f

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in Right_Cosets (Normalizator A) )
assume x in rng f ; :: thesis: x in Right_Cosets (Normalizator A)
then consider y being set such that
A12: ( y in dom f & f . y = x ) by FUNCT_1:def 5;
ex a being Element of G st
( y = A |^ a & x = (Normalizator A) * a ) by A9, A10, A12;
hence x in Right_Cosets (Normalizator A) by GROUP_2:def 16; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Right_Cosets (Normalizator A) or x in rng f )
assume x in Right_Cosets (Normalizator A) ; :: thesis: x in rng f
then consider a being Element of G such that
A13: x = (Normalizator A) * a by GROUP_2:def 16;
set y = A |^ a;
A,A |^ a are_conjugated by Th104;
then A14: A |^ a in con_class A ;
then ex b being Element of G st
( A |^ a = A |^ b & f . (A |^ a) = (Normalizator A) * b ) by A10;
then x = f . (A |^ a) by A1, A13, A14;
hence x in rng f by A9, A14, FUNCT_1:def 5; :: thesis: verum

end;

f is one-to-one

proof

let x be set ; :: according to FUNCT_1:def 8 :: thesis: for b₁ being set holds
( not x in dom f or not b₁ in dom f or not f . x = f . b₁ or x = b₁ )
let y be set ; :: thesis: ( not x in dom f or not y in dom f or not f . x = f . y or x = y )
assume that
A15: x in dom f and
A16: y in dom f and
A17: f . x = f . y ; :: thesis: x = y
consider a being Element of G such that
A18: ( x = A |^ a & f . x = (Normalizator A) * a ) by A9, A10, A15;
consider b being Element of G such that
A19: ( y = A |^ b & f . y = (Normalizator A) * b ) by A9, A10, A16;
b * (a " ) in Normalizator A by A17, A18, A19, GROUP_2:143;
then ex h being Element of G st
( b * (a " ) = h & A |^ h = A ) by Th154;
then A = (A |^ b) |^ (a " ) by Th56;
hence x = y by A18, A19, Th63; :: thesis: verum

end;

then con_class A, Right_Cosets (Normalizator A) are_equipotent by A9, A11, WELLORD2:def 4;
hence card (con_class A) = card (Right_Cosets (Normalizator A)) by CARD_1:21
.= Index (Normalizator A) by GROUP_2:175 ;
:: thesis: verum