reconsider M = F₁() as Element of NAT by ORDINAL1:def 12;
defpred S₁[ Nat] means P₁[F₁() + $1];

A3: now

let m be Element of NAT ; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume S₁[m] ; :: thesis: S₁[m + 1]
then P₁[(M + 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;
A6: for m being Element of NAT holds S₁[m] from NAT_1:sch 1(A5, A3);
m in NAT by ORDINAL1:def 12;
hence P₁[i] by A6, A4; :: thesis: verum