let z be object ; :: thesis: ( z in [:{0},NAT:] \ {[0,0]} implies ex k being Nat st z = - k )
A1: [:{0},NAT:] c= [:{0},REAL+:] by ARYTM_2:2, ZFMISC_1:95;
assume A2: z in [:{0},NAT:] \ {[0,0]} ; :: thesis: ex k being Nat st z = - k
then A3: not z in {[0,0]} by XBOOLE_0:def 5;
z in NAT \/ [:{0},NAT:] by A2, XBOOLE_0:def 3;
then z in INT by A3, NUMBERS:def 4, XBOOLE_0:def 5;
then reconsider z9 = z as Element of REAL by NUMBERS:15;
consider x, y being object such that
x in {0} and
A4: y in NAT and
A5: z = [x,y] by A2, ZFMISC_1:84;
reconsider y = y as Element of REAL by A4, NUMBERS:19;
z in [:{0},NAT:] by A2;
then consider x9, y9 being Element of REAL+ such that
A6: z9 = [0,x9] and
A7: y = y9 and
A8: + (z9,y) = y9 - x9 by A4, A1, ARYTM_0:def 1, ARYTM_2:2;
x9 = y9 by A5, A6, A7, XTUPLE_0:1;
then A9: y9 - x9 = 0 by ARYTM_1:18;
reconsider y = y as Element of NAT by A4;
take y ; :: thesis: z = - y
consider x1, x2, y1, y2 being Element of REAL such that
A10: z9 = [*x1,x2*] and
A11: y = [*y1,y2*] and
A12: z9 + y = [*(+ (x1,y1)),(+ (x2,y2))*] by XCMPLX_0:def 4;
A13: x2 = 0 by A10, ARYTM_0:24;
then A14: + (x2,y2) = 0 by A11, ARYTM_0:11, ARYTM_0:24;
y2 = 0 by A11, ARYTM_0:24;
then A15: y = y1 by A11, ARYTM_0:def 5;
z9 = x1 by A10, A13, ARYTM_0:def 5;
then z9 + y = 0 by A12, A15, A8, A9, A14, ARYTM_0:def 5;
hence z = - y ; :: thesis: verum