let G be Group; :: thesis: for a being Element of G holds { ((a -con_map ) " {x}) where x is Element of con_class a : verum } is a_partition of the carrier of G
let a be Element of G; :: thesis: { ((a -con_map ) " {x}) where x is Element of con_class a : verum } is a_partition of the carrier of G
reconsider X = { ((a -con_map ) " {x}) where x is Element of con_class a : verum } as set ;
A1: union X = the carrier of G

proof

A2: for y being set st y in union X holds
y in the carrier of G

proof

let x be set ; :: thesis: ( x in union X implies x in the carrier of G )
assume A3: x in union X ; :: thesis: x in the carrier of G
consider Y being set such that
A4: x in Y and
A5: Y in X by A3, TARSKI:def 4;
consider z being Element of con_class a such that
A6: (a -con_map ) " {z} = Y by A5;
thus x in the carrier of G by A4, A6; :: thesis: verum

end;

for y being set st y in the carrier of G holds
y in union X

proof

let x be set ; :: thesis: ( x in the carrier of G implies x in union X )
assume A7: x in the carrier of G ; :: thesis: x in union X
reconsider y = x as Element of G by A7;
consider z being Element of G such that
A8: z in con_class a and
A9: z = a |^ y by GROUP_3:97;
(a -con_map ) . y = z by A9, Def2;
then A10: (a -con_map ) . y in {z} by TARSKI:def 1;
dom (a -con_map ) = the carrier of G by FUNCT_2:def 1;
then A11: y in (a -con_map ) " {z} by A10, FUNCT_1:def 13;
(a -con_map ) " {z} in X by A8;
hence x in union X by A11, TARSKI:def 4; :: thesis: verum

end;

hence union X = the carrier of G by A2, TARSKI:2; :: thesis: verum

end;

A12: for A being Subset of G st A in X holds
( A <> {} & ( for B being Subset of G holds
( not B in X or A = B or A misses B ) ) )

proof

let A be Subset of G; :: thesis: ( A in X implies ( A <> {} & ( for B being Subset of G holds
( not B in X or A = B or A misses B ) ) ) )
assume A13: A in X ; :: thesis: ( A <> {} & ( for B being Subset of G holds
( not B in X or A = B or A misses B ) ) )
consider x being Element of con_class a such that
A14: A = (a -con_map ) " {x} by A13;
a,x are_conjugated by GROUP_3:96;
then consider g being Element of G such that
A15: x = a |^ g by GROUP_3:88;
(a -con_map ) . g = x by A15, Def2;
then A16: (a -con_map ) . g in {x} by TARSKI:def 1;
A17: dom (a -con_map ) = the carrier of G by FUNCT_2:def 1;
for B being Subset of G holds
( not B in X or A = B or A misses B )

proof

let B be Subset of G; :: thesis: ( not B in X or A = B or A misses B )
assume A18: B in X ; :: thesis: ( A = B or A misses B )
consider y being Element of con_class a such that
A19: B = (a -con_map ) " {y} by A18;
thus ( A = B or A misses B ) by A14, A19, Th10; :: thesis: verum

end;

hence ( A <> {} & ( for B being Subset of G holds
( not B in X or A = B or A misses B ) ) ) by A14, A16, A17, FUNCT_1:def 13; :: thesis: verum

end;

X c= bool (union X) by ZFMISC_1:100;
hence { ((a -con_map ) " {x}) where x is Element of con_class a : verum } is a_partition of the carrier of G by A1, A12, EQREL_1:def 6; :: thesis: verum