theorem Th63: :: DBLSEQ_3:63

for f being nonnegative Function of [:NAT,NAT:],ExtREAL
for m being Element of NAT holds ProjMap1 ((Partial_Sums_in_cod2 f),m) is non-decreasing