for n being Nat
for f being nonnegative-yielding FinSequence of REAL holds Sum f >= f . n