theorem SN: :: NEWTON04:21

for n being Nat
for f being real-valued nonnegative-yielding FinSequence holds Sum f >= f . n