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 & b in con_class a & c in A ) ;
b,a are_conjugated by A1, Th96;
then consider g being Element of G such that
A2: b = a |^ g by Def7;
reconsider h = x as Element of G by A1;
h |^ (c " ) = (c * ((a |^ g) * c)) * (c " ) by A1, A2
.= c * (((a |^ g) * c) * (c " )) by GROUP_1:def 4
.= c * (a |^ g) by Th1 ;
then A3: 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 A1, A3; :: 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
A4: ( x = b * c & b in A & c in con_class a ) ;
c,a are_conjugated by A4, Th96;
then consider g being Element of G such that
A5: c = a |^ g by Def7;
reconsider h = x as Element of G by A4;
h |^ b = (a |^ g) * b by A4, A5, Th1;
then A6: 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 Th26 ;
a |^ (g * (b " )) in con_class a by Th97;
hence x in (con_class a) * A by A4, A6; :: thesis: verum