theorem lm74: :: DBLSEQ_2:16

for Rseq1, Rseq2 being Function of [:NAT,NAT:],REAL holds Partial_Sums (Rseq1 + Rseq2) = (Partial_Sums Rseq1) + (Partial_Sums Rseq2)