let G be Group; :: thesis: for a being Element of G
for A being Subset of G holds (con_class a) * A = A * (con_class a)
let a be Element of G; :: thesis: for A being Subset of G holds (con_class a) * A = A * (con_class a)
let A be Subset of G; :: thesis: (con_class a) * A = A * (con_class a)
thus (con_class a) * A c= A * (con_class a) :: according to XBOOLE_0:def 10 :: thesis: A * (con_class a) c= (con_class a) * A

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (con_class a) * A or x in A * (con_class a) )
assume x in (con_class a) * A ; :: thesis: x in A * (con_class a)
then consider b, c being Element of G such that
A1: x = b * c and
A2: b in con_class a and
A3: c in A ;
reconsider h = x as Element of G by A1;
b,a are_conjugated by A2, Th96;
then consider g being Element of G such that
A4: b = a |^ g by Def7;
h |^ (c " ) = (c * ((a |^ g) * c)) * (c " ) by A1, A4
.= c * (((a |^ g) * c) * (c " )) by GROUP_1:def 4
.= c * (a |^ g) by Th1 ;
then A5: x = (c * (a |^ g)) |^ c by Th30
.= (c |^ c) * ((a |^ g) |^ c) by Th28
.= c * ((a |^ g) |^ c) by Th25
.= c * (a |^ (g * c)) by Th29 ;
a |^ (g * c) in con_class a by Th97;
hence x in A * (con_class a) by A3, A5; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A * (con_class a) or x in (con_class a) * A )
assume x in A * (con_class a) ; :: thesis: x in (con_class a) * A
then consider b, c being Element of G such that
A6: x = b * c and
A7: b in A and
A8: c in con_class a ;
reconsider h = x as Element of G by A6;
c,a are_conjugated by A8, Th96;
then consider g being Element of G such that
A9: c = a |^ g by Def7;
h |^ b = (a |^ g) * b by A6, A9, Th1;
then A10: x = ((a |^ g) * b) |^ (b " ) by Th30
.= ((a |^ g) |^ (b " )) * (b |^ (b " )) by Th28
.= (a |^ (g * (b " ))) * (b |^ (b " )) by Th29
.= (a |^ (g * (b " ))) * b by Th1 ;
a |^ (g * (b " )) in con_class a by Th97;
hence x in (con_class a) * A by A7, A10; :: thesis: verum