consider x1, x2, y1, y2 being Element of REAL such that
A8: ( x = [*x1,x2*] & y = [*y1,y2*] ) and
A9: x + y = [*(+ (x1,y1)),(+ (x2,y2))*] by XCMPLX_0:def 4;
( x2 = 0 & y2 = 0 ) by A8, Lm1;
then + (x2,y2) = 0 by ARYTM_0:11;
hence x + y is real by A9, ARYTM_0:def 5; :: thesis: verum