per cases ( x = 0 or x <> 0 ) ;
suppose x = 0 ; :: thesis: x " is real
hence x " is real by XCMPLX_0:def 7; :: thesis: verum
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;
end;