for f being nonnegative Function of [:NAT,NAT:],ExtREAL
for m being Element of NAT st not ProjMap1 ((Partial_Sums_in_cod2 f),m) is convergent_to_+infty holds
for n being Nat holds f . (m,n) is Real