let j be Nat; :: thesis: for f being nonnegative-yielding FinSequence of REAL holds Sum f >= Sum (f | j)
let f be nonnegative-yielding FinSequence of REAL ; :: thesis: Sum f >= Sum (f | j)
A1: (f | j) ^ (f /^ j) = f by RFINSEQ:8;
for i being Nat st i in dom (f /^ j) holds
(f /^ j) . i >= 0 ;
then (Sum (f | j)) + (Sum (f /^ j)) >= (Sum (f | j)) + 0 by RVSUM_1:84, XREAL_1:6;
hence Sum f >= Sum (f | j) by A1, RVSUM_1:75; :: thesis: verum