theorem thADD: :: DBLSEQ_2:8

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