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

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;
hence sup (rng f) <= K by XXREAL_2:def 3; :: thesis: verum