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:13, ARYTM_0:14;
then ( x1 = 0 or y2 = 0 ) by ARYTM_0:23;
then x " = y1 by A4, A5, A6, Lm1, ARYTM_0:def 7;
hence x " is real by Def1; :: thesis: verum

end;

end;