defpred S₁[ Nat] means for n being Nat st n >= F₁() & n < $1 holds
P₁[n];
A2: for k being Nat st k >= F₁() & S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( k >= F₁() & S₁[k] implies S₁[k + 1] )
assume k >= F₁() ; :: thesis: ( not S₁[k] or S₁[k + 1] )
assume A3: for n being Nat st n >= F₁() & n < k holds
P₁[n] ; :: thesis: S₁[k + 1]
let n be Nat; :: thesis: ( n >= F₁() & n < k + 1 implies P₁[n] )
assume that
A4: n >= F₁() and
A5: n < k + 1 ; :: thesis: P₁[n]
n <= k by A5, Th13;
then ( n < k or n = k ) by XXREAL_0:1;
hence P₁[n] by A1, A3, A4; :: thesis: verum

end;

let k be Nat; :: thesis: ( k >= F₁() implies P₁[k] )
assume A6: k >= F₁() ; :: thesis: P₁[k]
A7: S₁[F₁()] ;
for k being Nat st k >= F₁() holds
S₁[k] from NAT_1:sch 8(A7, A2);
then for n being Nat st n >= F₁() & n < k holds
P₁[n] by A6;
hence P₁[k] by A1, A6; :: thesis: verum