theorem :: DBLSEQ_2:15

for Rseq being Function of [:NAT,NAT:],REAL st Partial_Sums Rseq is P-convergent holds
( Rseq is P-convergent & P-lim Rseq = 0 )