assume not A ++ B is empty ; :: thesis: contradiction
then the Element of A ++ B in A ++ B ;
then ex c1, c2 being Element of COMPLEX st
( the Element of A ++ B = c1 + c2 & c1 in A & c2 in B ) ;
hence contradiction ; :: thesis: verum