let G be finite Group; :: thesis: for a being Element of G holds card { (() " {x}) where x is Element of con_class a : verum } = card ()
let a be Element of G; :: thesis: card { (() " {x}) where x is Element of con_class a : verum } = card ()
reconsider X = { (() " {x}) where x is Element of con_class a : verum } as a_partition of the carrier of G by Th11;
deffunc H1( object ) -> Element of bool the carrier of G = () " {\$1};
A1: for x being object st x in con_class a holds
H1(x) in X ;
consider F being Function of (),X such that
A2: for x being object st x in con_class a holds
F . x = H1(x) from for c being object st c in X holds
ex x being object st
( x in con_class a & c = F . x )
proof
let c be object ; :: thesis: ( c in X implies ex x being object st
( x in con_class a & c = F . x ) )

assume A3: c in X ; :: thesis: ex x being object 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 = () " {y} by A3;
F . y = c by A2, A4;
hence ex x being object 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 object st x1 in dom F & x2 in dom F & F . x1 = F . x2 holds
x1 = x2
proof
let x1, x2 be object ; :: 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 :: thesis: not y1 <> y2end;
hence x1 = x2 ; :: thesis: verum
end;
then F is one-to-one ;
then con_class a,F .: () are_equipotent by ;
then con_class a, rng F are_equipotent by ;
hence card { (() " {x}) where x is Element of con_class a : verum } = card () by ; :: thesis: verum