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

A2: now :: thesis: for n, m being Element of NAT holds f1 . (n,m) <= sup (rng f2)

let n, m be Element of NAT ; :: thesis: f1 . (n,m) <= sup (rng f2)
dom f2 = [:NAT,NAT:] by FUNCT_2:def 1;
then [n,m] in dom f2 by ZFMISC_1:87;
then A3: f2 . (n,m) in rng f2 by FUNCT_1:def 3;
A4: f1 . (n,m) <= f2 . (n,m) by A1;
sup (rng f2) is UpperBound of rng f2 by XXREAL_2:def 3;
then f2 . (n,m) <= sup (rng f2) by A3, XXREAL_2:def 1;
hence f1 . (n,m) <= sup (rng f2) by A4, XXREAL_0:2; :: thesis: verum

end;

now :: thesis: for x being ExtReal st x in rng f1 holds
x <= sup (rng f2)

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

end;

then sup (rng f2) is UpperBound of rng f1 by XXREAL_2:def 1;
hence sup (rng f1) <= sup (rng f2) by XXREAL_2:def 3; :: thesis: verum