theorem :: DBLSEQ_2:17

for Rseq1, Rseq2 being Function of [:NAT,NAT:],REAL st Partial_Sums Rseq1 is P-convergent & Partial_Sums Rseq2 is P-convergent holds
Partial_Sums (Rseq1 + Rseq2) is P-convergent