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: now

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

end;

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