let G be finite Group; :: thesis: for a being Element of G holds card { ((a -con_map ) " {x}) where x is Element of con_class a : verum } = card (con_class a)
let a be Element of G; :: thesis: card { ((a -con_map ) " {x}) where x is Element of con_class a : verum } = card (con_class 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;
deffunc H₁( set ) -> Element of bool the carrier of G = (a -con_map ) " {$1};
A1: for x being set st x in con_class a holds
H₁(x) in X ;
consider F being Function of (con_class a),X such that
A2: for x being set st x in con_class a holds
F . x = H₁(x) from FUNCT_2:sch 2(A1);
consider y being Element of con_class a;
for c being set st c in X holds
ex x being set st
( x in con_class a & c = F . x )

proof

let c be set ; :: thesis: ( c in X implies ex x being set st
( x in con_class a & c = F . x ) )
assume A3: c in X ; :: thesis: ex x being set st
( x in con_class a & c = F . x )
reconsider c = c as Subset of G by A3;
consider y being Element of con_class a such that
A4: c = (a -con_map ) " {y} by A3;
F . y = c by A2, A4;
hence ex x being set st
( x in con_class a & c = F . x ) ; :: thesis: verum

end;

then A5: rng F = X by FUNCT_2:16;
A6: dom F = con_class a by FUNCT_2:def 1;
for x1, x2 being set st x1 in dom F & x2 in dom F & F . x1 = F . x2 holds
x1 = x2

proof

let x1, x2 be set ; :: thesis: ( x1 in dom F & x2 in dom F & F . x1 = F . x2 implies x1 = x2 )
assume that
A7: x1 in dom F and
A8: x2 in dom F and
A9: F . x1 = F . x2 ; :: thesis: x1 = x2
reconsider y1 = x1 as Element of con_class a by A7;
reconsider y2 = x2 as Element of con_class a by A8;
A10: ( (a -con_map ) " {y1} = F . y1 & (a -con_map ) " {y2} = F . y2 ) by A2;

now

assume y1 <> y2 ; :: thesis: contradiction
then (a -con_map ) " {y1} misses (a -con_map ) " {y2} by Th10;
then A11: ((a -con_map ) " {y1}) /\ ((a -con_map ) " {y2}) = {} by XBOOLE_0:def 7;
consider d being Element of G such that
A12: ( d = y1 & a,d are_conjugated ) by GROUP_3:95;
consider g being Element of G such that
A13: d = a |^ g by A12, GROUP_3:def 7;
(a -con_map ) . g = y1 by A12, A13, Def2;
then A14: (a -con_map ) . g in {y1} by TARSKI:def 1;
dom (a -con_map ) = the carrier of G by FUNCT_2:def 1;
hence contradiction by A9, A10, A11, A14, FUNCT_1:def 13; :: thesis: verum

end;

hence x1 = x2 ; :: thesis: verum

end;

then F is one-to-one by FUNCT_1:def 8;
then con_class a,F .: (con_class a) are_equipotent by A6, CARD_1:60;
then con_class a, rng F are_equipotent by A6, RELAT_1:146;
hence card { ((a -con_map ) " {x}) where x is Element of con_class a : verum } = card (con_class a) by A5, CARD_1:21; :: thesis: verum