theorem :: DBLSEQ_3:105

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 n1, m1, n2, m2 being Nat st n1 <= n2 & m1 <= m2 holds
f1 . (n1,m1) <= f1 . (n2,m2) ) & ( for n, m being Nat holds f2 . (n,m) = c * (f1 . (n,m)) ) holds
( ( for n1, m1, n2, m2 being Nat st n1 <= n2 & m1 <= m2 holds
f2 . (n1,m1) <= f2 . (n2,m2) ) & f2 is without-infty & f2 is P-convergent & P-lim f2 = sup (rng f2) & P-lim f2 = c * (P-lim f1) )