let z be set ; :: thesis: ( z in [:{0 },NAT :] \ {[0 ,0 ]} implies ex k being Element of NAT st z = - k )
A1: [:{0 },NAT :] c= [:{0 },REAL+ :] by ARYTM_2:2, ZFMISC_1:118;
assume A2: z in [:{0 },NAT :] \ {[0 ,0 ]} ; :: thesis: ex k being Element of 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 set such that
x in {0 } and
A4: y in NAT and
A5: z = [x,y] by A2, ZFMISC_1:103;
reconsider y = y as Element of NAT by A4;
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 2, ARYTM_2:2;
x9 = y9 by A5, A6, A7, ZFMISC_1:33;
then A9: y9 - x9 = 0 by ARYTM_1:18;
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:26;
then A14: + x2,y2 = 0 by A11, ARYTM_0:13, ARYTM_0:26;
y2 = 0 by A11, ARYTM_0:26;
then A15: y = y1 by A11, ARYTM_0:def 7;
z9 = x1 by A10, A13, ARYTM_0:def 7;
then z9 + y = 0 by A12, A15, A8, A9, A14, ARYTM_0:def 7;
hence z = - y ; :: thesis: verum