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 H1( object ) -> Element of bool the carrier of G = (a -con_map) " {$1};
A1: for x being object st x in con_class a holds
H1(x) in X ;
consider F being Function of (con_class a),X such that
A2: for x being object st x in con_class a holds
F . x = H1(x) from FUNCT_2:sch 2(A1);
 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 = (a -con_map) " {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 <> y2
assume y1 <> y2 ; :: thesis: contradiction
then (a -con_map) " {y1} misses (a -con_map) " {y2} by Th10;
then ((a -con_map) " {y1}) /\ ((a -con_map) " {y2}) = {} by XBOOLE_0:def 7;
hence contradiction by A9, A10, A11; :: thesis: verum
end;
hence x1 = x2 ; :: thesis: verum
end;
then F is one-to-one ;
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