let G be addGroup; :: 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 object ; :: 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 a, b being Element of G such that
A1: x = a * b and
A2: a in - A and
A3: b in B ;
consider c being Element of G such that
A4: ( a = - c & c in A ) by A2;
( x = - (c * b) & c * b in A * B ) by A1, A3, A4, Th26;
hence x in - (A * B) ; :: thesis: verum

end;

let x be object ; :: 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 a being Element of G such that
A5: x = - a and
A6: a in A * B ;
consider b, c being Element of G such that
A7: a = b * c and
A8: b in A and
A9: c in B by A6;
A10: - b in - A by A8;
x = (- b) * c by A5, A7, Th26;
hence x in (- A) * B by A9, A10; :: thesis: verum