theorem :: DBLSEQ_3:50

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