let G be Group; :: thesis: for H being strict Subgroup of G holds card (con_class H) = Index (Normalizator H)
let H be strict Subgroup of G; :: thesis: card (con_class H) = Index (Normalizator H)
defpred S₁[ set , set ] means ex H1 being strict Subgroup of G st
( $1 = H1 & $2 = carr H1 );
A1: for x being set st x in con_class H holds
ex y being set st S₁[x,y]

proof

let x be set ; :: thesis: ( x in con_class H implies ex y being set st S₁[x,y] )
assume x in con_class H ; :: thesis: ex y being set st S₁[x,y]
then reconsider H = x as strict Subgroup of G by Def1;
reconsider y = carr H as set ;
take y ; :: thesis: S₁[x,y]
take H ; :: thesis: ( x = H & y = carr H )
thus ( x = H & y = carr H ) ; :: thesis: verum

end;

consider f being Function such that
A2: dom f = con_class H and
A3: for x being set st x in con_class H holds
S₁[x,f . x] from CLASSES1:sch 1(A1);
A4: rng f = con_class (carr H)

proof

thus rng f c= con_class (carr H) :: according to XBOOLE_0:def 10 :: thesis: con_class (carr H) c= rng f

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in con_class (carr H) )
assume x in rng f ; :: thesis: x in con_class (carr H)
then consider y being set such that
A5: ( y in dom f & f . y = x ) by FUNCT_1:def 5;
consider H1 being strict Subgroup of G such that
A6: ( y = H1 & x = carr H1 ) by A2, A3, A5;
H1,H are_conjugated by A2, A5, A6, Th128;
then carr H1, carr H are_conjugated by Th134;
hence x in con_class (carr H) by A6; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in con_class (carr H) or x in rng f )
assume x in con_class (carr H) ; :: thesis: x in rng f
then consider B being Subset of G such that
A7: ( B = x & carr H,B are_conjugated ) ;
consider H1 being strict Subgroup of G such that
A8: the carrier of H1 = B by A7, Th109;
B = carr H1 by A8;
then H1,H are_conjugated by A7, Th134;
then A9: H1 in con_class H by Th128;
then ex H2 being strict Subgroup of G st
( H1 = H2 & f . H1 = carr H2 ) by A3;
hence x in rng f by A2, A7, A8, A9, 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
A10: x in dom f and
A11: y in dom f and
A12: f . x = f . y ; :: thesis: x = y
consider H1 being strict Subgroup of G such that
A13: ( x = H1 & f . x = carr H1 ) by A2, A3, A10;
consider H2 being strict Subgroup of G such that
A14: ( y = H2 & f . y = carr H2 ) by A2, A3, A11;
thus x = y by A12, A13, A14, GROUP_2:68; :: thesis: verum

end;

then con_class H, con_class (carr H) are_equipotent by A2, A4, WELLORD2:def 4;
hence card (con_class H) = card (con_class (carr H)) by CARD_1:21
.= Index (Normalizator H) by Th155 ;
:: thesis: verum