consider x1, x2, y1, y2 being Element of REAL such that
A10: x = [*x1,x2*] and
A11: y = [*y1,y2*] and
A12: x + y = [*(+ x1,y1),(+ x2,y2)*] by XCMPLX_0:def 4;
( x2 = 0 & y2 = 0 ) by A10, A11, Lm1;
then + x2,y2 = 0 by ARYTM_0:13;
then x + y = + x1,y1 by A12, ARYTM_0:def 7;
hence x + y is real by Def1; :: thesis: verum