let G be Group; :: thesis: for a being Element of G holds { (() " {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: { (() " {x}) where x is Element of con_class a : verum } is a_partition of the carrier of G
reconsider X = { (() " {x}) where x is Element of con_class a : verum } as set ;
A1: for y being object st y in union X holds
y in the carrier of G
proof
let x be object ; :: thesis: ( x in union X implies x in the carrier of G )
assume x in union X ; :: thesis: x in the carrier of G
then consider Y being set such that
A2: x in Y and
A3: Y in X by TARSKI:def 4;
ex z being Element of con_class a st () " {z} = Y by A3;
hence x in the carrier of G by A2; :: thesis: verum
end;
for y being object st y in the carrier of G holds
y in union X
proof
let x be object ; :: thesis: ( x in the carrier of G implies x in union X )
assume x in the carrier of G ; :: thesis: x in union X
then reconsider y = x as Element of G ;
consider z being Element of G such that
A4: z in con_class a and
A5: z = a |^ y by GROUP_3:82;
(a -con_map) . y = z by ;
then A6: (a -con_map) . y in {z} by TARSKI:def 1;
dom () = the carrier of G by FUNCT_2:def 1;
then A7: y in () " {z} by ;
(a -con_map) " {z} in X by A4;
hence x in union X by ; :: thesis: verum
end;
then A8: union X = the carrier of G by ;
A9: 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 A in X ; :: thesis: ( A <> {} & ( for B being Subset of G holds
( not B in X or A = B or A misses B ) ) )

then consider x being Element of con_class a such that
A10: A = () " {x} ;
a,x are_conjugated by GROUP_3:81;
then consider g being Element of G such that
A11: x = a |^ g by GROUP_3:74;
(a -con_map) . g = x by ;
then A12: (a -con_map) . g in {x} by TARSKI:def 1;
A13: dom () = 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 B in X ; :: thesis: ( A = B or A misses B )
then ex y being Element of con_class a st B = () " {y} ;
hence ( A = B or A misses B ) by ; :: thesis: verum
end;
hence ( A <> {} & ( for B being Subset of G holds
( not B in X or A = B or A misses B ) ) ) by ; :: thesis: verum
end;
X c= bool () by ZFMISC_1:82;
hence { ((a -con_map) " {x}) where x is Element of con_class a : verum } is a_partition of the carrier of G by ; :: thesis: verum