:: deftheorem defines ++ MEMBER_1:def 6 :
for A, B being complex-membered set holds A ++ B = { (c1 + c2) where c1, c2 is Complex : ( c1 in A & c2 in B ) } ;