:: deftheorem Def3 defines + XCMPLX_0:def 3 :
for x, y being Complex
for b₃ being number holds
( b₃ = x + y iff ex x1, x2, y1, y2 being Element of REAL st
( x = [*x1,x2*] & y = [*y1,y2*] & b₃ = [*(+ (x1,y1)),(+ (x2,y2))*] ) );