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