for f being Function of [:NAT,NAT:],ExtREAL
for i, j, k being Nat st ( for m being Element of NAT holds ProjMap2 (f,m) is non-decreasing ) & i <= j holds
(Partial_Sums_in_cod2 f) . (i,k) <= (Partial_Sums_in_cod2 f) . (j,k)