let A, B be complex-membered set ; :: thesis: A ** (-- B) = -- (A ** B)
let a be Complex; :: 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 Complex such that
A1: a = c * c1 and
A2: c in A and
A3: c1 in -- B ;
- c1 in B by A3, Th12;
then A4: c * (- c1) in A ** B by A2;
a = - (c * (- c1)) by A1;
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 Th12;
then consider c, c1 being Complex such that
A5: - a = c * c1 and
A6: c in A and
A7: c1 in B ;
( a = c * (- c1) & - c1 in -- B ) by A5, A7;
hence a in A ** (-- B) by A6; :: thesis: verum