theorem SF: :: NEWTON04:19

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