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),(opp (* x2,y2))),(+ (* x1,y2),(* x2,y1))*] by XCMPLX_0:def 5;
x2 = 0 by A10, Lm1;
then A13: * x2,y1 = 0 by ARYTM_0:14;
A14: y2 = 0 by A11, Lm1;
then * (opp x2),y2 = 0 by ARYTM_0:14;
then A15: opp (* x2,y2) = 0 by ARYTM_0:17;
* x1,y2 = 0 by A14, ARYTM_0:14;
then + (* x1,y2),(* x2,y1) = 0 by A13, ARYTM_0:13;
then x * y = + (* x1,y1),0 by A12, A15, ARYTM_0:def 7
.= * x1,y1 by ARYTM_0:13 ;
hence x * y is real by Def1; :: thesis: verum