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