theorem th54b: :: DBLSEQ_1:12

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) )