let j be Nat; :: thesis: for f being real-valued nonnegative-yielding FinSequence holds Sum f >= Sum (f | j)
let f be real-valued nonnegative-yielding FinSequence; :: thesis: Sum f >= Sum (f | j)
A1: (f | j) ^ (f /^ j) = f by RFINSEQ:8;
(Sum (f | j)) + (Sum (f /^ j)) >= (Sum (f | j)) + 0 by XREAL_1:6;
hence Sum f >= Sum (f | j) by A1, RVSUM_1:75; :: thesis: verum