let G be finite Group; :: thesis: for a being Element of G holds card G = (card ()) * (card ())
let a be Element of G; :: thesis: card G = (card ()) * (card ())
reconsider X = { (() " {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 () & ( 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 () & ( 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 () & ( for B being set st B in X & A <> B holds
A misses B ) )

reconsider A = A as Subset of G by A2;
ex x being Element of con_class a st A = () " {x} by A2;
hence ( A is finite & card A = card () & ( for B being set st B in X & A <> B holds
A misses B ) ) by ; :: thesis: verum
end;
reconsider k = card () 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 A3: 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 A3;
A4: card Y = card () by A1, A3;
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
A5: Z in X and
A6: Y <> Z ; :: thesis: ( Y,Z are_equipotent & Y misses Z )
A7: card Y = card () by A1, A3;
card Z = card () by A1, A5;
hence ( Y,Z are_equipotent & Y misses Z ) by A1, A3, A5, A6, A7, CARD_1:5; :: 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 A4; :: thesis: verum
end;
then consider C being finite set such that
A8: C = union X and
A9: card C = (card X) * k by GROUP_2:156;
card G = card C by
.= (card ()) * (card ()) by ;
hence card G = (card ()) * (card ()) ; :: thesis: verum