let A, B be complex-membered set ; :: thesis: A ** (-- B) = -- (A ** B)
let a be complex number ; :: according to MEMBERED:def 13 :: thesis: ( ( not a in A ** (-- B) or a in -- (A ** B) ) & ( not a in -- (A ** B) or a in A ** (-- B) ) )

hereby :: thesis: ( not a in -- (A ** B) or a in A ** (-- B) )

assume a in A ** (-- B) ; :: thesis: a in -- (A ** B)
then consider c, c1 being Element of COMPLEX such that
A1: a = c * c1 and
A2: c in A and
A3: c1 in -- B ;
A4: a = - (c * (- c1)) by A1;
- c1 in B by A3, Th18;
then c * (- c1) in A ** B by A2;
hence a in -- (A ** B) by A4; :: thesis: verum

end;

assume a in -- (A ** B) ; :: thesis: a in A ** (-- B)
then - a in A ** B by Th18;
then consider c, c1 being Element of COMPLEX such that
A5: - a = c * c1 and
A6: c in A and
A7: c1 in B ;
A8: a = c * (- c1) by A5;
- c1 in -- B by A7;
hence a in A ** (-- B) by A6, A8; :: thesis: verum