theorem :: DBLSEQ_2:42

for Rseq being Function of [:NAT,NAT:],REAL st Rseq is nonnegative-yielding & Partial_Sums Rseq is P-convergent holds
( lim_in_cod1 (Partial_Sums_in_cod1 Rseq) is summable & lim_in_cod2 (Partial_Sums_in_cod2 Rseq) is summable )