let Rseq1, Rseq2 be Function of [:NAT,NAT:],REAL; :: thesis: ( Partial_Sums Rseq1 is P-convergent & Partial_Sums Rseq2 is P-convergent implies Partial_Sums (Rseq1 + Rseq2) is P-convergent )
assume ( Partial_Sums Rseq1 is P-convergent & Partial_Sums Rseq2 is P-convergent ) ; :: thesis: Partial_Sums (Rseq1 + Rseq2) is P-convergent
then (Partial_Sums Rseq1) + (Partial_Sums Rseq2) is P-convergent by DBLSEQ_1:11;
hence Partial_Sums (Rseq1 + Rseq2) is P-convergent by lm74; :: thesis: verum