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 z be Complex; :: according to MEMBERED:def 7 :: thesis: ( not z in A -- C or z in B -- D )
A2: A -- C = { (c1 - c2) where c1, c2 is Complex : ( c1 in A & c2 in C ) } by Th65;
assume z in A -- C ; :: thesis: z in B -- D
then ex c, c1 being Complex st
( z = c - c1 & c in A & c1 in C ) by A2;
hence z in B -- D by A1, Th66; :: thesis: verum