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

hereby :: thesis: verum

let n, m be Nat; :: thesis: f . (n,m) <= sup (rng f)
A0: ( n in NAT & m in NAT ) by ORDINAL1:def 12;
dom f = [:NAT,NAT:] by FUNCT_2:def 1;
then [n,m] in dom f by A0, ZFMISC_1:87;
then A1: f . (n,m) in rng f by FUNCT_1:def 3;
sup (rng f) is UpperBound of rng f by XXREAL_2:def 3;
hence f . (n,m) <= sup (rng f) by A1, XXREAL_2:def 1; :: thesis: verum

end;