defpred S₁[ Nat] means ex w being Element of NAT st
( w = $1 & (0. X),x to_power w = 0. X & w <> 0 );
ex k being non empty Element of NAT st (0. X),x to_power k = 0. X by A1, Def6;
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 empty Element of NAT by A3;
take k ; :: thesis: ( (0. X),x to_power k = 0. X & ( for m being Element of 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 Element of NAT st (0. X),x to_power m = 0. X & m <> 0 holds
k <= m ) ) by A3, A4; :: thesis: verum