consider x1, x2, y1, y2 being Element of REAL such that
A13: x = [*x1,x2*] and
A14: y = [*y1,y2*] and
A15: x * y = [*(+ (* x1,y1),(opp (* x2,y2))),(+ (* x1,y2),(* x2,y1))*] by XCMPLX_0:def 5;
A16: ( x2 = 0 & y2 = 0 ) by A13, A14, Lm1;
then ( * x2,y1 = 0 & * x1,y2 = 0 ) by ARYTM_0:14;
then A17: + (* x1,y2),(* x2,y1) = 0 by ARYTM_0:13;
* (opp x2),y2 = 0 by A16, ARYTM_0:14;
then opp (* x2,y2) = 0 by ARYTM_0:17;
then x * y = + (* x1,y1),0 by A15, A17, ARYTM_0:def 7
.= * x1,y1 by ARYTM_0:13 ;
hence x * y is real by Def1; :: thesis: verum