theorem :: DBLSEQ_3:51

for f1, f2 being without+infty Function of [:NAT,NAT:],ExtREAL holds Partial_Sums (f1 + f2) = (Partial_Sums f1) + (Partial_Sums f2)