let Rseq be Function of [:NAT,NAT:],REAL; :: thesis: ( Rseq is nonnegative-yielding implies ( Partial_Sums Rseq is P-convergent iff ( Partial_Sums Rseq is bounded_below & Partial_Sums Rseq is bounded_above ) ) )
assume Rseq is nonnegative-yielding ; :: thesis: ( Partial_Sums Rseq is P-convergent iff ( Partial_Sums Rseq is bounded_below & Partial_Sums Rseq is bounded_above ) )
then a2: Partial_Sums Rseq is non-decreasing by th80a;
hence ( Partial_Sums Rseq is P-convergent implies ( Partial_Sums Rseq is bounded_below & Partial_Sums Rseq is bounded_above ) ) ; :: thesis: ( Partial_Sums Rseq is bounded_below & Partial_Sums Rseq is bounded_above implies Partial_Sums Rseq is P-convergent )
assume ( Partial_Sums Rseq is bounded_below & Partial_Sums Rseq is bounded_above ) ; :: thesis: Partial_Sums Rseq is P-convergent
hence Partial_Sums Rseq is P-convergent by a2; :: thesis: verum