theorem :: NEWTON04:13

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