defpred S₁[ Nat] means ex w being Nat st
( w = $1 & ((0. X),x) to_power w = 0. X & w <> 0 );
ex k being non zero Nat st ((0. X),x) to_power k = 0. X by A1;
then A2: ex n being Nat st S₁[n] ;
consider k being Nat such that
A3: S₁[k] and
A4: for n being Nat st S₁[n] holds
k <= n from NAT_1:sch 5(A2);
reconsider k = k as non zero Nat by A3;
take k ; :: thesis: ( ((0. X),x) to_power k = 0. X & ( for m being Nat st ((0. X),x) to_power m = 0. X & m <> 0 holds
k <= m ) )
thus ( ((0. X),x) to_power k = 0. X & ( for m being Nat st ((0. X),x) to_power m = 0. X & m <> 0 holds
k <= m ) ) by A3, A4; :: thesis: verum