let A, B be complex-membered set ; :: thesis: for a, b being complex number st a in A & b in B holds
a + b in A ++ B
let a, b be complex number ; :: thesis: ( a in A & b in B implies a + b in A ++ B )
( a in COMPLEX & b in COMPLEX ) by XCMPLX_0:def 2;
hence ( a in A & b in B implies a + b in A ++ B ) ; :: thesis: verum