let n1, n2 be non zero Nat; :: thesis: ( ((0. X),x) to_power n1 = 0. X & ( for m being 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 Nat st ((0. X),x) to_power m = 0. X & m <> 0 holds
n2 <= m ) implies n1 = n2 )
assume ( ((0. X),x) to_power n1 = 0. X & ( for m being 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 Nat st ((0. X),x) to_power m = 0. X & m <> 0 holds
n2 <= m ) ) ; :: thesis: n1 = n2
then ( n1 <= n2 & n2 <= n1 ) ;
hence n1 = n2 by XXREAL_0:1; :: thesis: verum