theorem :: DBLSEQ_2:43

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