let i, j be Nat; :: thesis: for f being nonnegative-yielding FinSequence of REAL st i >= j holds
Sum (f | i) >= Sum (f | j)
let f be nonnegative-yielding FinSequence of REAL ; :: thesis: ( i >= j implies Sum (f | i) >= Sum (f | j) )
assume i >= j ; :: thesis: Sum (f | i) >= Sum (f | j)
then Sum ((f | i) | j) = Sum (f | j) by FINSEQ_1:82;
hence Sum (f | i) >= Sum (f | j) by SF; :: thesis: verum