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);
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:10;
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 by A2;
A11: (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 A12: ((a -con_map) " {y1}) /\ ((a -con_map) " {y2}) = {} by XBOOLE_0:def 7;
consider d being Element of G such that
A13: d = y1 and
A14: a,d are_conjugated by GROUP_3:80;
consider g being Element of G such that
A15: d = a |^ g by A14, GROUP_3:def 7;
(a -con_map) . g = y1 by A13, A15, Def2;
then A16: (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, A12, A16, FUNCT_1:def 7; :: thesis: verum

end;

hence x1 = x2 ; :: thesis: verum

end;

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