let i be Nat; :: thesis: ( F₁() <= i implies P₁[i] )
assume A3: F₁() <= i ; :: thesis: P₁[i]
defpred S₁[ Nat] means P₁[F₁() + $1];
A4: S₁[ 0 ] by A1;
reconsider M = F₁() as Element of NAT by ORDINAL1:def 13;

A5: 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;

A6: for m being Element of NAT holds S₁[m] from NAT_1:sch 1(A4, A5);
consider m being Nat such that
A7: i = F₁() + m by A3, Th10;
m in NAT by ORDINAL1:def 13;
hence P₁[i] by A6, A7; :: thesis: verum