per cases
( x = 0 or x <> 0 )
;

end;

suppose A4:
x <> 0
; :: thesis: x " is real

then
x * (x ") = 1
by XCMPLX_0:def 7;

then consider x1, x2, y1, y2 being Element of REAL such that

A5: x = [*x1,x2*] and

A6: x " = [*y1,y2*] and

A7: 1 = [*(+ ((* (x1,y1)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*] by XCMPLX_0:def 5;

( + ((* (x1,y2)),(* (x2,y1))) = 0 & x2 = 0 ) by A5, A7, Lm1;

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

then ( x1 = 0 or y2 = 0 ) by ARYTM_0:21;

hence x " is real by A4, A5, A6, Lm1, ARYTM_0:def 5; :: thesis: verum

end;then consider x1, x2, y1, y2 being Element of REAL such that

A5: x = [*x1,x2*] and

A6: x " = [*y1,y2*] and

A7: 1 = [*(+ ((* (x1,y1)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*] by XCMPLX_0:def 5;

( + ((* (x1,y2)),(* (x2,y1))) = 0 & x2 = 0 ) by A5, A7, Lm1;

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

then ( x1 = 0 or y2 = 0 ) by ARYTM_0:21;

hence x " is real by A4, A5, A6, Lm1, ARYTM_0:def 5; :: thesis: verum