let n1, n2 be non empty Element of NAT ; :: thesis: ( (0. X),x to_power n1 = 0. X & ( for m being Element of NAT st (0. X),x to_power m = 0. X & m <> 0 holds
n1 <= m ) & (0. X),x to_power n2 = 0. X & ( for m being Element of NAT st (0. X),x to_power m = 0. X & m <> 0 holds
n2 <= m ) implies n1 = n2 )
assume that
A6: ( (0. X),x to_power n1 = 0. X & ( for m being Element of NAT st (0. X),x to_power m = 0. X & m <> 0 holds
n1 <= m ) ) and
A7: ( (0. X),x to_power n2 = 0. X & ( for m being Element of NAT st (0. X),x to_power m = 0. X & m <> 0 holds
n2 <= m ) ) ; :: thesis: n1 = n2
( n1 <= n2 & n2 <= n1 ) by A6, A7;
hence n1 = n2 by XXREAL_0:1; :: thesis: verum