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

proof

let x be object ; :: thesis: ( x in con_class A implies ex y being object st S₁[x,y] )
assume x in con_class A ; :: thesis: ex y being object 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, Th88;
reconsider y = (Normalizer A) * g as set ;
take y ; :: thesis: S₁[x,y]
take g ; :: thesis: ( x = A |^ g & y = (Normalizer A) * g )
thus ( x = A |^ g & y = (Normalizer 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 object 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 = (Normalizer 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 = (Normalizer A) * b ; :: thesis: y1 = y2
A = (A |^ b) |^ (a ") by A8, A10, Th54
.= A |^ (b * (a ")) by Th47 ;
then b * (a ") in Normalizer A by Th129;
hence y1 = y2 by A9, A11, GROUP_2:120; :: thesis: verum

end;

A12: rng f = Right_Cosets (Normalizer A)

proof

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

proof

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

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Right_Cosets (Normalizer A) or x in rng f )
assume x in Right_Cosets (Normalizer A) ; :: thesis: x in rng f
then consider a being Element of G such that
A14: x = (Normalizer A) * a by GROUP_2:def 16;
set y = A |^ a;
A,A |^ a are_conjugated by Th88;
then A15: A |^ a in con_class A ;
then ex b being Element of G st
( A |^ a = A |^ b & f . (A |^ a) = (Normalizer A) * b ) by A6;
then x = f . (A |^ a) by A7, A14, A15;
hence x in rng f by A5, A15, FUNCT_1:def 3; :: thesis: verum

end;

f is one-to-one

proof

let x, y be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x in dom f or not y in dom 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 = (Normalizer A) * b by A5, A6, A17;
consider a being Element of G such that
A21: x = A |^ a and
A22: f . x = (Normalizer A) * a by A5, A6, A16;
b * (a ") in Normalizer A by A18, A22, A20, GROUP_2:120;
then ex h being Element of G st
( b * (a ") = h & A |^ h = A ) by Th129;
then A = (A |^ b) |^ (a ") by Th47;
hence x = y by A21, A19, Th54; :: thesis: verum

end;

then con_class A, Right_Cosets (Normalizer A) are_equipotent by A5, A12, WELLORD2:def 4;
hence card (con_class A) = card (Right_Cosets (Normalizer A)) by CARD_1:5
.= Index (Normalizer A) by GROUP_2:145 ;
:: thesis: verum