theorem th01a: :: DBLSEQ_2:22

for Rseq being Function of [:NAT,NAT:],REAL holds
( Partial_Sums Rseq is convergent_in_cod1 iff Partial_Sums_in_cod1 Rseq is convergent_in_cod1 )