assume A1: - x = 0 ; :: according to XCMPLX_0:def 3 :: thesis: contradiction
x + (- x) = 0 by Def6;
then 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 Def4;
A6: + (x2,y2) = 0 by A5, ARYTM_0:26;
then A7: + (x1,y1) = 0 by A5, ARYTM_0:def 7;
y2 = 0 by A1, A4, ARYTM_0:26;
then A9: y1 = 0 by A1, A4, ARYTM_0:def 7;
x2 = 0 by A1, A4, A6, ARYTM_0:13, ARYTM_0:26;
then x = x1 by A3, ARYTM_0:def 7
.= 0 by A7, A9, ARYTM_0:13 ;
hence contradiction ; :: thesis: verum