theorem :: DBLSEQ_3:97

for f1, f2 being Function of [:NAT,NAT:],ExtREAL st ( for n, m being Nat holds f1 . (n,m) <= f2 . (n,m) ) holds
sup (rng f1) <= sup (rng f2)