theorem Th61: :: MESFUNC5:61

for J, K, L being ExtREAL_sequence st ( for n, m being Nat st n <= m holds
J . n <= J . m ) & ( for n, m being Nat st n <= m holds
K . n <= K . m ) & J is () & K is () & ( for n being Nat holds (J . n) + (K . n) = L . n ) holds
( L is convergent & lim L = sup (rng L) & lim L = (lim J) + (lim K) & sup (rng L) = (sup (rng K)) + (sup (rng J)) )