theorem lm80: :: DBLSEQ_2:28

for Rseq being Function of [:NAT,NAT:],REAL st Rseq is nonnegative-yielding holds
( Partial_Sums_in_cod2 Rseq is nonnegative-yielding & Partial_Sums_in_cod1 Rseq is nonnegative-yielding )