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_{1}( object ) -> Element of bool the carrier of G = (a -con_map) " {$1};

A1: for x being object st x in con_class a holds

H_{1}(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 = H_{1}(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 )

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

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

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

A1: for x being object st x in con_class a holds

H

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 = H

for c being object st c in X holds

ex x being object st

( x in con_class a & c = F . x )

proof

then A5:
rng F = X
by FUNCT_2:10;
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;( 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

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

then
F is one-to-one
;
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;

end;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

hence
x1 = x2
; :: thesis: verumassume
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;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

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