let G be commutative Group; :: thesis: for A, B being Subset of G holds (A * B) " = (A " ) * (B " )
let A, B be Subset of G; :: thesis: (A * B) " = (A " ) * (B " )
thus (A * B) " c= (A " ) * (B " ) :: according to XBOOLE_0:def 10 :: thesis: (A " ) * (B " ) c= (A * B) "

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (A * B) " or x in (A " ) * (B " ) )
assume x in (A * B) " ; :: thesis: x in (A " ) * (B " )
then consider g being Element of G such that
A1: ( x = g " & g in A * B ) ;
consider g1, g2 being Element of G such that
A2: ( g = g1 * g2 & g1 in A & g2 in B ) by A1;
( x = (g1 " ) * (g2 " ) & g1 " in A " & g2 " in B " ) by A1, A2, GROUP_1:94;
hence x in (A " ) * (B " ) ; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (A " ) * (B " ) or x in (A * B) " )
assume x in (A " ) * (B " ) ; :: thesis: x in (A * B) "
then consider g1, g2 being Element of G such that
A3: ( x = g1 * g2 & g1 in A " & g2 in B " ) ;
consider a being Element of G such that
A4: ( g1 = a " & a in A ) by A3;
consider b being Element of G such that
A5: ( g2 = b " & b in B ) by A3;
( x = (a * b) " & a * b in A * B ) by A3, A4, A5, GROUP_1:94;
hence x in (A * B) " ; :: thesis: verum