defpred S₁[ Nat] means for n being Nat st n >= F₁() & n < $1 holds
P₁[n];
A2: S₁[F₁()] ;
A3: 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 A4: 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 A5: ( n >= F₁() & n < k + 1 ) ; :: thesis: P₁[n]
then n <= k by Th13;
then ( n < k or n = k ) by XXREAL_0:1;
hence P₁[n] by A1, A4, A5; :: thesis: verum

end;

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