now :: thesis: for n being Nat holds (Nseq ^\ k) . n < (Nseq ^\ k) . (n + 1)

let n be Nat; :: thesis: (Nseq ^\ k) . n < (Nseq ^\ k) . (n + 1)
Nseq . (n + k) < Nseq . ((n + k) + 1) by Lm7;
then (Nseq ^\ k) . n < Nseq . ((n + 1) + k) by NAT_1:def 3;
hence (Nseq ^\ k) . n < (Nseq ^\ k) . (n + 1) by NAT_1:def 3; :: thesis: verum

end;

hence for b₁ being ext-real-valued Function st b₁ = Nseq ^\ k holds
( b₁ is increasing & b₁ is natural-valued ) by Lm7; :: thesis: verum