theorem th01b: :: DBLSEQ_2:23
for Rseq being Function of [:NAT,NAT:],REAL holds
( Partial_Sums Rseq is convergent_in_cod2 iff Partial_Sums_in_cod2 Rseq is convergent_in_cod2 )