theorem :: DBLSEQ_3:90

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