theorem Th64: :: DBLSEQ_3:64

for f being nonnegative Function of [:NAT,NAT:],ExtREAL
for n being Element of NAT holds ProjMap2 ((Partial_Sums_in_cod1 f),n) is non-decreasing