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

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