theorem :: DBLSEQ_3:99

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