theorem Th45: :: DBLSEQ_3:45

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