defpred S₁[ Nat] means for i2 being Integer st $1 = i2 - F₁() holds
P₁[i2];
A3: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
reconsider i8 = k as Integer ;
assume A4: S₁[k] ; :: thesis: S₁[k + 1]
let i2 be Integer; :: thesis: ( k + 1 = i2 - F₁() implies P₁[i2] )
assume A5: k + 1 = i2 - F₁() ; :: thesis: P₁[i2]
then i2 - 1 = i8 + F₁() ;
then A6: F₁() <= i2 - 1 by Th6;
k = (i2 - 1) - F₁() by A5;
then P₁[(i2 - 1) + 1] by A2, A4, A6;
hence P₁[i2] ; :: thesis: verum

end;

let i0 be Integer; :: thesis: ( F₁() <= i0 implies P₁[i0] )
assume F₁() <= i0 ; :: thesis: P₁[i0]
then reconsider l = i0 - F₁() as Element of NAT by Th5;
A7: l = i0 - F₁() ;
A8: S₁[ 0 ] by A1;
for k being Nat holds S₁[k] from NAT_1:sch 2(A8, A3);
hence P₁[i0] by A7; :: thesis: verum