theorem Th83: :: DBLSEQ_3:83

for f being nonnegative Function of [:NAT,NAT:],ExtREAL
for seq being ExtREAL_sequence st ( for m being Element of NAT holds seq . m = lim_inf (ProjMap2 (f,m)) ) holds
Sum seq <= lim_inf (lim_in_cod2 (Partial_Sums_in_cod2 f))