assume A12: x " = 0 ; :: according to XCMPLX_0:def 3 :: thesis: contradiction
A13: x * (x " ) = 1 by Def7;
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 A13, Def5;
A16: y2 = 0 by A12, A14, ARYTM_0:26;
A17: y1 = 0 by A12, A14, A16, ARYTM_0:def 7;
A18: + (* x1,y2),(* x2,y1) = 0 by A15, ARYTM_0:26;
A19: 1 = + (* x1,y1),(opp (* x2,y2)) by A15, A18, ARYTM_0:def 7
.= + (* x1,y1),(* (opp x2),y2) by ARYTM_0:17
.= * (opp x2),y2 by A17, ARYTM_0:13, ARYTM_0:14 ;
thus contradiction by A12, A14, A19, ARYTM_0:14, ARYTM_0:26; :: thesis: verum