theorem :: DBLSEQ_2:4

for Rseq being Function of [:NAT,NAT:],REAL st Rseq is non-decreasing & Rseq is P-convergent holds
for n, m being Nat holds Rseq . (n,m) <= P-lim Rseq