theorem :: DBLSEQ_3:103

for f being Function of [:NAT,NAT:],ExtREAL
for f1, f2 being without-infty Function of [:NAT,NAT:],ExtREAL st ( for n1, m1, n2, m2 being Nat st n1 <= n2 & m1 <= m2 holds
f1 . (n1,m1) <= f1 . (n2,m2) ) & ( for n1, m1, n2, m2 being Nat st n1 <= n2 & m1 <= m2 holds
f2 . (n1,m1) <= f2 . (n2,m2) ) & ( for n, m being Nat holds (f1 . (n,m)) + (f2 . (n,m)) = f . (n,m) ) holds
( f is P-convergent & P-lim f = sup (rng f) & P-lim f = (P-lim f1) + (P-lim f2) & sup (rng f) = (sup (rng f1)) + (sup (rng f2)) )