theorem th03a: :: DBLSEQ_2:26

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