let f be Function of [:NAT,NAT:],ExtREAL; :: thesis: for K being R_eal st K <> +infty & ( for n, m being Nat holds f . (n,m) <= K ) holds
sup (rng f) < +infty
let K be R_eal; :: thesis: ( K <> +infty & ( for n, m being Nat holds f . (n,m) <= K ) implies sup (rng f) < +infty )
assume A1: ( K <> +infty & ( for n, m being Nat holds f . (n,m) <= K ) ) ; :: thesis: sup (rng f) < +infty

now :: thesis: for x being ExtReal st x in rng f holds
x <= K

let x be ExtReal; :: thesis: ( x in rng f implies x <= K )
assume x in rng f ; :: thesis: x <= K
then consider z being object such that
A2: ( z in dom f & x = f . z ) by FUNCT_1:def 3;
consider n, m being object such that
A3: ( n in NAT & m in NAT & z = [n,m] ) by A2, ZFMISC_1:def 2;
reconsider n = n, m = m as Element of NAT by A3;
x = f . (n,m) by A2, A3;
hence x <= K by A1; :: thesis: verum

end;

then K is UpperBound of rng f by XXREAL_2:def 1;
then sup (rng f) <= K by XXREAL_2:def 3;
hence sup (rng f) < +infty by A1, XXREAL_0:2, XXREAL_0:4; :: thesis: verum