let i0 be Integer; :: thesis: ( F₁() <= i0 implies P₁[i0] )
assume A3: F₁() <= i0 ; :: thesis: P₁[i0]
defpred S₁[ natural number ] means for i2 being Integer st $1 = i2 - F₁() holds
P₁[i2];
A4: S₁[ 0 ] by A1;
A5: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
reconsider i8 = k as Integer ;
assume A6: S₁[k] ; :: thesis: S₁[k + 1]
let i2 be Integer; :: thesis: ( k + 1 = i2 - F₁() implies P₁[i2] )
assume A7: k + 1 = i2 - F₁() ; :: thesis: P₁[i2]
then A8: k = (i2 - 1) - F₁() ;
F₁() <= i2 - 1

proof

i2 - 1 = i8 + F₁() by A7;
hence F₁() <= i2 - 1 by Th19; :: thesis: verum

end;

then P₁[(i2 - 1) + 1] by A2, A6, A8;
hence P₁[i2] ; :: thesis: verum

end;

A9: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A4, A5);
reconsider l = i0 - F₁() as Element of NAT by A3, Th18;
l = i0 - F₁() ;
hence P₁[i0] by A9; :: thesis: verum