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;

reconsider zz = 0 as Element of REAL by NUMBERS:19;

x2 = 0 by A10, Lm1;

then A13: * (x2,y1) = 0 by ARYTM_0:12;

A14: y2 = 0 by A11, Lm1;

then * ((opp x2),y2) = 0 by ARYTM_0:12;

then A15: opp (* (x2,y2)) = 0 by ARYTM_0:15;

* (x1,y2) = 0 by A14, ARYTM_0:12;

then + ((* (x1,y2)),(* (x2,y1))) = 0 by A13, ARYTM_0:11;

then x * y = + ((* (x1,y1)),zz) by A12, A15, ARYTM_0:def 5

.= * (x1,y1) by ARYTM_0:11 ;

hence x * y is real ; :: thesis: verum

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;

reconsider zz = 0 as Element of REAL by NUMBERS:19;

x2 = 0 by A10, Lm1;

then A13: * (x2,y1) = 0 by ARYTM_0:12;

A14: y2 = 0 by A11, Lm1;

then * ((opp x2),y2) = 0 by ARYTM_0:12;

then A15: opp (* (x2,y2)) = 0 by ARYTM_0:15;

* (x1,y2) = 0 by A14, ARYTM_0:12;

then + ((* (x1,y2)),(* (x2,y1))) = 0 by A13, ARYTM_0:11;

then x * y = + ((* (x1,y1)),zz) by A12, A15, ARYTM_0:def 5

.= * (x1,y1) by ARYTM_0:11 ;

hence x * y is real ; :: thesis: verum