theorem Th104: :: DBLSEQ_3:104

for f1 being without-infty Function of [:NAT,NAT:],ExtREAL
for f2 being Function of [:NAT,NAT:],ExtREAL
for c being Real st 0 <= c & ( for n, m being Nat holds f2 . (n,m) = c * (f1 . (n,m)) ) holds
( sup (rng f2) = c * (sup (rng f1)) & f2 is without-infty )