theorem th1005: :: DBLSEQ_2:39

for Rseq being Function of [:NAT,NAT:],REAL st Rseq is nonnegative-yielding holds
for k being Element of NAT holds
( ProjMap2 ((Partial_Sums_in_cod1 Rseq),k) is non-decreasing & ProjMap1 ((Partial_Sums_in_cod2 Rseq),k) is non-decreasing & ProjMap2 ((Partial_Sums_in_cod1 Rseq),k) is nonnegative & ProjMap1 ((Partial_Sums_in_cod2 Rseq),k) is nonnegative & ProjMap2 ((Partial_Sums_in_cod2 Rseq),k) is nonnegative & ProjMap1 ((Partial_Sums_in_cod1 Rseq),k) is nonnegative )