let A, B, C, D be complex-membered set ; :: thesis: ( A c= B & C c= D implies A ++ C c= B ++ D )
assume A1: ( A c= B & C c= D ) ; :: thesis: A ++ C c= B ++ D
let a be Complex; :: according to MEMBERED:def 7 :: thesis: ( not a in A ++ C or a in B ++ D )
assume a in A ++ C ; :: thesis: a in B ++ D
then ex c, c1 being Complex st
( a = c + c1 & c in A & c1 in C ) ;
hence a in B ++ D by A1; :: thesis: verum