theorem th02b: :: DBLSEQ_2:25

for Rseq being Function of [:NAT,NAT:],REAL st Partial_Sums Rseq is convergent_in_cod2 holds
for k being Nat holds (lim_in_cod2 (Partial_Sums Rseq)) . (k + 1) = ((lim_in_cod2 (Partial_Sums Rseq)) . k) + ((lim_in_cod2 (Partial_Sums_in_cod2 Rseq)) . (k + 1))