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 V115() & ProjMap1 ((Partial_Sums_in_cod2 Rseq),k) is V115() & 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 )