defpred S₁[ Nat] means F₁($1) = 0 ;
defpred S₂[ Nat] means ex n being Nat st $1 = F₁(n);
A2: for k being Nat st k <> 0 & S₂[k] holds
ex m being Nat st
( m < k & S₂[m] )

proof

let k be Nat; :: thesis: ( k <> 0 & S₂[k] implies ex m being Nat st
( m < k & S₂[m] ) )
assume that
A3: k <> 0 and
A4: S₂[k] ; :: thesis: ex m being Nat st
( m < k & S₂[m] )
consider n being Nat such that
A5: k = F₁(n) by A4;
take F₁((n + 1)) ; :: thesis: ( F₁((n + 1)) < k & S₂[F₁((n + 1))] )
thus ( F₁((n + 1)) < k & S₂[F₁((n + 1))] ) by A1, A3, A5; :: thesis: verum

end;

F₁(0 ) is Nat ;
then A6: ex k being Nat st S₂[k] ;
S₂[ 0 ] from NAT_1:sch 7(A6, A2);
then A7: ex k being Nat st S₁[k] ;
consider k being Nat such that
A8: ( S₁[k] & ( for n being Nat st S₁[n] holds
k <= n ) ) from NAT_1:sch 5(A7);
take k ; :: thesis: ( F₁(k) = 0 & ( for n being Nat st F₁(n) = 0 holds
k <= n ) )
thus ( F₁(k) = 0 & ( for n being Nat st F₁(n) = 0 holds
k <= n ) ) by A8; :: thesis: verum