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
A2: x = [*x1,x2*] and
A3: - x = [*y1,y2*] and
A4: 0 = [*(+ (x1,y1)),(+ (x2,y2))*] by Def4;
A5: + (x2,y2) = 0 by A4, ARYTM_0:24;
then A6: + (x1,y1) = 0 by A4, ARYTM_0:def 5;
y2 = 0 by A1, A3, ARYTM_0:24;
then A7: y1 = 0 by A1, A3, ARYTM_0:def 5;
x2 = 0 by A1, A3, A5, ARYTM_0:11, ARYTM_0:24;
then x = x1 by A2, ARYTM_0:def 5
.= 0 by A6, A7, ARYTM_0:11 ;
hence contradiction ; :: thesis: verum