theorem th1006a: :: DBLSEQ_2:41

for Rseq being Function of [:NAT,NAT:],REAL st Rseq is nonnegative-yielding & Partial_Sums Rseq is P-convergent holds
( Partial_Sums Rseq is convergent_in_cod1 & Partial_Sums Rseq is convergent_in_cod2 )