theorem th80a: :: DBLSEQ_2:29

for Rseq being Function of [:NAT,NAT:],REAL st Rseq is nonnegative-yielding holds
Partial_Sums Rseq is non-decreasing