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