let Nseq be increasing sequence of NAT ; :: thesis: for n being Element of NAT holds n <= Nseq . n
defpred S₁[ Element of NAT ] means $1 <= Nseq . $1;
A1: S₁[ 0 ] by NAT_1:2;

A2: now

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: S₁[k] ; :: thesis: S₁[k + 1]
Nseq . k < Nseq . (k + 1) by Lm6A;
then k < Nseq . (k + 1) by A3, XXREAL_0:2;
hence S₁[k + 1] by NAT_1:13; :: thesis: verum

end;

thus for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A1, A2); :: thesis: verum