let G be Group; :: thesis: for a being Element of G holds card (con_class a) = Index (Normalizer {a})
let a be Element of G; :: thesis: card (con_class a) = Index (Normalizer {a})
deffunc H1( object ) -> set = {$1};
consider f being Function such that
A1: dom f = con_class a and
A2: for x being object st x in con_class a holds
f . x = H1(x) from FUNCT_1:sch 3();
 A3: rng f = con_class {a}
proof
thus rng f c= con_class {a} :: according to XBOOLE_0:def 10 :: thesis: con_class {a} c= rng f
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in con_class {a} )
assume x in rng f ; :: thesis: x in con_class {a}
then consider y being object such that
A4: y in dom f and
A5: f . y = x by FUNCT_1:def 3;
reconsider y = y as Element of G by A1, A4;
f . y = {y} by A1, A2, A4;
then x in { {d} where d is Element of G : d in con_class a } by A1, A4, A5;
hence x in con_class {a} by Th100; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in con_class {a} or x in rng f )
assume x in con_class {a} ; :: thesis: x in rng f
then x in { {b} where b is Element of G : b in con_class a } by Th100;
then consider b being Element of G such that
A6: x = {b} and
A7: b in con_class a ;
f . b = {b} by A2, A7;
hence x in rng f by A1, A6, A7, 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
A8: ( x in dom f & y in dom f ) and
A9: f . x = f . y ; :: thesis: x = y
( f . x = {x} & f . y = {y} ) by A1, A2, A8;
hence x = y by A9, ZFMISC_1:3; :: thesis: verum
end;
then con_class a, con_class {a} are_equipotent by A1, A3, WELLORD2:def 4;
hence card (con_class a) = card (con_class {a}) by CARD_1:5
.= Index (Normalizer {a}) by Th130 ;
:: thesis: verum