theorem Th101: :: DBLSEQ_3:101

for f being without-infty Function of [:NAT,NAT:],ExtREAL holds
( sup (rng f) <> +infty iff ex K being Real st
( 0 < K & ( for n, m being Nat holds f . (n,m) <= K ) ) )