theorem :: DBLSEQ_2:33

for Rseq1, Rseq2 being Function of [:NAT,NAT:],REAL st Rseq1 is nonnegative-yielding & ( for n, m being Nat holds Rseq1 . (n,m) <= Rseq2 . (n,m) ) & Partial_Sums Rseq2 is P-convergent holds
Partial_Sums Rseq1 is P-convergent