defpred S₁[ Nat] means P₁[F₁() + $1];

A3: now :: thesis: for m being Nat st S₁[m] holds
S₁[m + 1]

let m be Nat; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume S₁[m] ; :: thesis: S₁[m + 1]
then P₁[(F₁() + m) + 1] by A2, Th11;
hence S₁[m + 1] ; :: thesis: verum

end;

let i be Nat; :: thesis: ( F₁() <= i implies P₁[i] )
assume F₁() <= i ; :: thesis: P₁[i]
then consider m being Nat such that
A4: i = F₁() + m by Th10;
A5: S₁[ 0 ] by A1;
for m being Nat holds S₁[m] from NAT_1:sch 2(A5, A3);
hence P₁[i] by A4; :: thesis: verum