theorem SF: :: NEWTON04:19

for j being Nat
for f being real-valued nonnegative-yielding FinSequence holds Sum f >= Sum (f | j)