let G be finite Group; :: thesis: for a being Element of G holds card G = (card (con_class a)) * (card (Centralizer a))
let a be Element of G; :: thesis: card G = (card (con_class a)) * (card (Centralizer a))
reconsider X = { ((a -con_map ) " {x}) where x is Element of con_class a : verum } as a_partition of the carrier of G by Th11;
A1: for A being set st A in X holds
( A is finite & card A = card (Centralizer a) & ( for B being set st B in X & A <> B holds
A misses B ) )

proof

let A be set ; :: thesis: ( A in X implies ( A is finite & card A = card (Centralizer a) & ( for B being set st B in X & A <> B holds
A misses B ) ) )
assume A2: A in X ; :: thesis: ( A is finite & card A = card (Centralizer a) & ( for B being set st B in X & A <> B holds
A misses B ) )
reconsider A = A as Subset of G by A2;
consider x being Element of con_class a such that
A3: A = (a -con_map ) " {x} by A2;
thus ( A is finite & card A = card (Centralizer a) & ( for B being set st B in X & A <> B holds
A misses B ) ) by A2, A3, Th9, EQREL_1:def 6; :: thesis: verum

end;

reconsider k = card (Centralizer a) as Element of NAT ;
for Y being set st Y in X holds
ex B being finite set st
( B = Y & card B = k & ( for Z being set st Z in X & Y <> Z holds
( Y,Z are_equipotent & Y misses Z ) ) )

proof

let Y be set ; :: thesis: ( Y in X implies ex B being finite set st
( B = Y & card B = k & ( for Z being set st Z in X & Y <> Z holds
( Y,Z are_equipotent & Y misses Z ) ) ) )
assume A4: Y in X ; :: thesis: ex B being finite set st
( B = Y & card B = k & ( for Z being set st Z in X & Y <> Z holds
( Y,Z are_equipotent & Y misses Z ) ) )
reconsider Y = Y as finite set by A4;
A5: card Y = card (Centralizer a) by A1, A4;
for Z being set st Z in X & Y <> Z holds
( Y,Z are_equipotent & Y misses Z )

proof

let Z be set ; :: thesis: ( Z in X & Y <> Z implies ( Y,Z are_equipotent & Y misses Z ) )
assume that
A6: Z in X and
A7: Y <> Z ; :: thesis: ( Y,Z are_equipotent & Y misses Z )
A8: card Y = card (Centralizer a) by A1, A4;
card Z = card (Centralizer a) by A1, A6;
hence ( Y,Z are_equipotent & Y misses Z ) by A1, A4, A6, A7, A8, CARD_1:21; :: thesis: verum

end;

hence ex B being finite set st
( B = Y & card B = k & ( for Z being set st Z in X & Y <> Z holds
( Y,Z are_equipotent & Y misses Z ) ) ) by A5; :: thesis: verum

end;

then consider C being finite set such that
A9: C = union X and
A10: card C = (card X) * k by GROUP_2:186;
card G = card C by A9, EQREL_1:def 6
.= (card (con_class a)) * (card (Centralizer a)) by A10, Th12 ;
hence card G = (card (con_class a)) * (card (Centralizer a)) ; :: thesis: verum