theorem :: DBLSEQ_3:49

for f being Function of [:NAT,NAT:],ExtREAL st ( not f is without-infty or not f is without+infty ) holds
Partial_Sums f = Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f) by Lm8, Lm9;