assume A1: - x = 0 ; :: according to XCMPLX_0:def 3 :: thesis: contradiction
A2: x + (- x) = 0 by Def6;
consider x1, x2, y1, y2 being Element of REAL such that
A3: x = [*x1,x2*] and
A4: - x = [*y1,y2*] and
A5: 0 = [*(+ x1,y1),(+ x2,y2)*] by A2, Def4;
A6: + x2,y2 = 0 by A5, ARYTM_0:26;
A7: + x1,y1 = 0 by A5, A6, ARYTM_0:def 7;
A8: y2 = 0 by A1, A4, ARYTM_0:26;
A9: y1 = 0 by A1, A4, A8, ARYTM_0:def 7;
A10: x2 = 0 by A1, A4, A6, ARYTM_0:13, ARYTM_0:26;
A11: x = x1 by A3, A10, ARYTM_0:def 7
.= 0 by A7, A9, ARYTM_0:13 ;
thus contradiction by A11; :: thesis: verum