let Rseq1, Rseq2 be Function of [:NAT,NAT:],REAL; :: thesis: ( Rseq1 is nonnegative-yielding & ( for n, m being Nat holds Rseq1 . (n,m) <= Rseq2 . (n,m) ) & Partial_Sums Rseq2 is P-convergent implies Partial_Sums Rseq1 is P-convergent )
set RPS1 = Partial_Sums Rseq1;
set RPS2 = Partial_Sums Rseq2;
assume that
a2: ( Rseq1 is nonnegative-yielding & ( for n, m being Nat holds Rseq1 . (n,m) <= Rseq2 . (n,m) ) ) and
a1: Partial_Sums Rseq2 is P-convergent ; :: thesis: Partial_Sums Rseq1 is P-convergent
for n, m being Nat holds 0 <= Rseq2 . (n,m)

proof

let n, m be Nat; :: thesis: 0 <= Rseq2 . (n,m)
( 0 <= Rseq1 . (n,m) & Rseq1 . (n,m) <= Rseq2 . (n,m) ) by a2;
hence 0 <= Rseq2 . (n,m) ; :: thesis: verum

end;

then Rseq2 is nonnegative-yielding ;
then Partial_Sums Rseq2 is non-decreasing by th80a;
then Partial_Sums Rseq2 is bounded_above by a1;
then consider M being Real such that
a3: M is UpperBound of (Partial_Sums Rseq2) .: [:NAT,NAT:] by XXREAL_2:def 10;

now :: thesis: for a being ExtReal st a in (Partial_Sums Rseq1) .: [:NAT,NAT:] holds
a <= M

let a be ExtReal; :: thesis: ( a in (Partial_Sums Rseq1) .: [:NAT,NAT:] implies a <= M )
assume a in (Partial_Sums Rseq1) .: [:NAT,NAT:] ; :: thesis: a <= M
then consider x being Element of [:NAT,NAT:] such that
a5: ( x in [:NAT,NAT:] & a = (Partial_Sums Rseq1) . x ) by FUNCT_2:65;
consider n, m being object such that
a6: ( n in NAT & m in NAT & x = [n,m] ) by ZFMISC_1:def 2;
reconsider n = n, m = m as Element of NAT by a6;
a7: (Partial_Sums Rseq1) . (n,m) <= (Partial_Sums Rseq2) . (n,m) by a2, lm84;
(Partial_Sums Rseq2) . (n,m) <= M by a3, XXREAL_2:def 1, a6, FUNCT_2:35;
hence a <= M by a5, a6, a7, XXREAL_0:2; :: thesis: verum

end;

then M is UpperBound of (Partial_Sums Rseq1) .: [:NAT,NAT:] by XXREAL_2:def 1;
then a8: Partial_Sums Rseq1 is bounded_above by XXREAL_2:def 10;
Partial_Sums Rseq1 is non-decreasing by a2, th80a;
hence Partial_Sums Rseq1 is P-convergent by a8; :: thesis: verum