assume A12: x " = 0 ; :: according to XCMPLX_0:def 3 :: thesis: contradiction
x * (x ") = 1 by Def7;
then consider x1, x2, y1, y2 being Element of REAL such that
x = [*x1,x2*] and
A14: x " = [*y1,y2*] and
A15: 1 = [*(+ ((* (x1,y1)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*] by Def5;
y2 = 0 by A12, A14, ARYTM_0:26;
then A17: y1 = 0 by A12, A14, ARYTM_0:def 7;
+ ((* (x1,y2)),(* (x2,y1))) = 0 by A15, ARYTM_0:26;
then 1 = + ((* (x1,y1)),(opp (* (x2,y2)))) by A15, ARYTM_0:def 7
.= + ((* (x1,y1)),(* ((opp x2),y2))) by ARYTM_0:17
.= * ((opp x2),y2) by A17, ARYTM_0:13, ARYTM_0:14 ;
hence contradiction by A12, A14, ARYTM_0:14, ARYTM_0:26; :: thesis: verum