let G be finite Group; :: thesis:
let a be Element of G; :: thesis:
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 ) )

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

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 ) ) )

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

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:

end;