theorem :: DBLSEQ_3:69

for f being nonnegative Function of [:NAT,NAT:],ExtREAL
for n, m being Nat st ( for i being Nat st i <= n holds
f . (i,m) is Real ) holds
(Partial_Sums_in_cod1 f) . (n,m) < +infty