defpred S₁[ Nat] means ex n being Nat st $1 = F₁(n);
F₁(0 ) is Nat ;
then A3: ex k being Nat st S₁[k] ;
A4: 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 A5: ( k <> 0 & S₁[k] ) ; :: thesis: ex m being Nat st
( m < k & S₁[m] )
then consider n being Nat such that
A6: k = F₁(n) ;
take F₁((n + 1)) ; :: thesis: ( F₁((n + 1)) < k & S₁[F₁((n + 1))] )
thus ( F₁((n + 1)) < k & S₁[F₁((n + 1))] ) by A2, A5, A6; :: thesis: verum

end;

defpred S₂[ Nat] means F₁($1) = 0 ;
S₁[ 0 ] from NAT_1:sch 7(A3, A4);
then A7: ex k being Nat st S₂[k] ;
consider k being Nat such that
A8: S₂[k] and
A9: 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, A9; :: thesis: verum