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 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
A2: x = B and
A3: A,B are_conjugated ;
consider g being Element of G such that
A4: B = A |^ g by A3, 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 A2, A4; :: thesis: verum

end;

consider f being Function such that
A5: dom f = con_class A and
A6: for x being set st x in con_class A holds
S₁[x,f . x] from CLASSES1:sch 1(A1);
A7: 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 A8: x = A |^ a and
A9: y1 = (Normalizator A) * a ; :: thesis: ( not S₁[x,y2] or y1 = y2 )
given b being Element of G such that A10: x = A |^ b and
A11: y2 = (Normalizator A) * b ; :: thesis: y1 = y2
A = (A |^ b) |^ (a " ) by A8, A10, Th63
.= A |^ (b * (a " )) by Th56 ;
then b * (a " ) in Normalizator A by Th154;
hence y1 = y2 by A9, A11, GROUP_2:143; :: thesis: verum

end;

A12: 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
A13: ( 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 A5, A6, A13;
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
A14: x = (Normalizator A) * a by GROUP_2:def 16;
set y = A |^ a;
A,A |^ a are_conjugated by Th104;
then A15: 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 A6;
then x = f . (A |^ a) by A7, A14, A15;
hence x in rng f by A5, A15, 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 proj1 f or not b₁ in proj1 f or not f . x = f . b₁ or x = b₁ )
let y be set ; :: thesis: ( not x in proj1 f or not y in proj1 f or not f . x = f . y or x = y )
assume that
A16: x in dom f and
A17: y in dom f and
A18: f . x = f . y ; :: thesis: x = y
consider b being Element of G such that
A19: y = A |^ b and
A20: f . y = (Normalizator A) * b by A5, A6, A17;
consider a being Element of G such that
A21: x = A |^ a and
A22: f . x = (Normalizator A) * a by A5, A6, A16;
b * (a " ) in Normalizator A by A18, A22, A20, 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 A21, A19, Th63; :: thesis: verum

end;

then con_class A, Right_Cosets (Normalizator A) are_equipotent by A5, A12, 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