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;

verum