let f be without-infty Function of [:NAT,NAT:],ExtREAL; :: thesis: ( sup (rng f) <> +infty iff ex K being Real st
( 0 < K & ( for n, m being Nat holds f . (n,m) <= K ) ) )
A1: -infty < f . (1,1) by MESFUNC5:def 5;
A2: dom f = [:NAT,NAT:] by FUNCT_2:def 1;
then [1,1] in dom f by ZFMISC_1:87;
then A3: f . (1,1) <= sup (rng f) by FUNCT_1:3, XXREAL_2:4;

A4: now :: thesis: ( sup (rng f) <> +infty implies ex K being object st
( 0 < K & ( for n, m being Nat holds f . (n,m) <= K ) ) )

assume sup (rng f) <> +infty ; :: thesis: ex K being object st
( 0 < K & ( for n, m being Nat holds f . (n,m) <= K ) )
then not sup (rng f) in {-infty,+infty} by A1, A3, TARSKI:def 2;
then sup (rng f) in REAL by XBOOLE_0:def 3, XXREAL_0:def 4;
then reconsider S = sup (rng f) as Real ;
take K = max (S,1); :: thesis: ( 0 < K & ( for n, m being Nat holds f . (n,m) <= K ) )
thus 0 < K by XXREAL_0:25; :: thesis: for n, m being Nat holds f . (n,m) <= K
let n, m be Nat; :: thesis: f . (n,m) <= K
( n in NAT & m in NAT ) by ORDINAL1:def 12;
then [n,m] in [:NAT,NAT:] by ZFMISC_1:87;
then A5: f . (n,m) <= sup (rng f) by A2, FUNCT_1:3, XXREAL_2:4;
S <= K by XXREAL_0:25;
hence f . (n,m) <= K by A5, XXREAL_0:2; :: thesis: verum

end;

now :: thesis: ( ex K being Real st
( 0 < K & ( for n, m being Nat holds f . (n,m) <= K ) ) implies sup (rng f) <> +infty )

given K being Real such that 0 < K and
A6: for n, m being Nat holds f . (n,m) <= K ; :: thesis: sup (rng f) <> +infty

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

let w be ExtReal; :: thesis: ( w in rng f implies w <= K )
assume w in rng f ; :: thesis: w <= K
then consider z being object such that
A7: ( z in dom f & w = f . z ) by FUNCT_1:def 3;
consider n, m being object such that
A8: ( n in NAT & m in NAT & z = [n,m] ) by A7, ZFMISC_1:def 2;
reconsider n = n, m = m as Element of NAT by A8;
w = f . (n,m) by A7, A8;
hence w <= K by A6; :: 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 XXREAL_0:9, XREAL_0:def 1; :: thesis: verum

end;

hence ( sup (rng f) <> +infty iff ex K being Real st
( 0 < K & ( for n, m being Nat holds f . (n,m) <= K ) ) ) by A4; :: thesis: verum