theorem :: DBLSEQ_1:11

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