ex x1, x2, y1, y2 being Element of REAL st
( z = [*x1,x2*] & z9 = [*y1,y2*] & z + z9 = [*(+ (x1,y1)),(+ (x2,y2))*] ) by Def3;
hence z + z9 in COMPLEX ; :: according to XCMPLX_0:def 2 :: thesis: verum