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 )
A1: ( a in COMPLEX & b in COMPLEX ) by XCMPLX_0:def 2;
A -- B = { (c1 - c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) } by Th65;
hence ( a in A & b in B implies a - b in A -- B ) by A1; :: thesis: verum