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 object ; :: 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, Th81;
then consider g being Element of G such that
A4: b = a |^ g ;
h |^ (c ") = (c * ((a |^ g) * c)) * (c ") by A1, A4
.= c * (((a |^ g) * c) * (c ")) by GROUP_1:def 3
.= c * (a |^ g) by Th1 ;
then A5: x = (c * (a |^ g)) |^ c by Th25
.= (c |^ c) * ((a |^ g) |^ c) by Th23
.= c * ((a |^ g) |^ c) by Th20
.= c * (a |^ (g * c)) by Th24 ;
a |^ (g * c) in con_class a by Th82;
hence x in A * (con_class a) by A3, A5; :: thesis: verum

end;

let x be object ; :: 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, Th81;
then consider g being Element of G such that
A9: c = a |^ g ;
h |^ b = (a |^ g) * b by A6, A9, Th1;
then A10: x = ((a |^ g) * b) |^ (b ") by Th25
.= ((a |^ g) |^ (b ")) * (b |^ (b ")) by Th23
.= (a |^ (g * (b "))) * (b |^ (b ")) by Th24
.= (a |^ (g * (b "))) * b by Th1 ;
a |^ (g * (b ")) in con_class a by Th82;
hence x in (con_class a) * A by A7, A10; :: thesis: verum