theorem SN: :: NEWTON04:21

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