theorem :: DBLSEQ_3:82

for f being nonnegative Function of [:NAT,NAT:],ExtREAL st Partial_Sums f is convergent_in_cod2_to_finite holds
for m being Element of NAT holds (Partial_Sums (lim_in_cod2 (Partial_Sums_in_cod2 f))) . m = lim (ProjMap1 ((Partial_Sums_in_cod2 (Partial_Sums_in_cod1 f)),m))