theorem :: DBLSEQ_3:98

for f being Function of [:NAT,NAT:],ExtREAL
for n, m being Nat holds f . (n,m) <= sup (rng f)