for i being Nat st i in dom f holds
f . i >= 0 ;
hence not Sum f is negative by RVSUM_1:84; :: thesis: verum