for i being Nat st i in dom (- f) holds
(- f) . i >= 0

proof

let i be Nat; :: thesis: ( i in dom (- f) implies (- f) . i >= 0 )
assume A1: i in dom (- f) ; :: thesis: (- f) . i >= 0
( i in dom f & (- f) . i = - (f . i) ) by A1, VALUED_1:8;
hence (- f) . i >= 0 ; :: thesis: verum

end;

then Sum (- f) >= Sum ((len f) |-> 0) by RVSUM_1:84;
then (- (Sum f)) + (Sum f) >= 0 + (Sum f) by RVSUM_1:88;
hence not Sum f is positive ; :: thesis: verum