let i, j be Nat; :: thesis: for f being real-valued nonnegative-yielding FinSequence st i >= j holds
Sum (f | i) >= Sum (f | j)
let f be real-valued nonnegative-yielding FinSequence; :: 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