defpred S1[ Nat] means F1($1) = 0 ;
defpred S2[ Nat] means ex n being Nat st $1 = F1(n);
A2: for k being Nat st k <> 0 & S2[k] holds
ex m being Nat st
( m < k & S2[m] )
proof
let k be Nat; :: thesis: ( k <> 0 & S2[k] implies ex m being Nat st
( m < k & S2[m] ) )
assume that
A3: k <> 0 and
A4: S2[k] ; :: thesis: ex m being Nat st
( m < k & S2[m] )
consider n being Nat such that
A5: k = F1(n) by A4;
take IT = F1((n + 1)); :: thesis: ( IT < k & S2[IT] )
thus ( IT < k & S2[IT] ) by A1, A3, A5; :: thesis: verum
end;
F1(0) is Nat ;
then A6: ex k being Nat st S2[k] ;
S2[ 0 ] from NAT_1:sch 7(A6, A2);
 then A7: ex k being Nat st S1[k] ;
consider k being Nat such that
A8: ( S1[k] & ( for n being Nat st S1[n] holds
k <= n ) ) from NAT_1:sch 5(A7);
 take k ; :: thesis: ( F1(k) = 0 & ( for n being Nat st F1(n) = 0 holds
k <= n ) )
thus ( F1(k) = 0 & ( for n being Nat st F1(n) = 0 holds
k <= n ) ) by A8; :: thesis: verum