let A be non empty closed_interval Subset of REAL; :: thesis: for rho being Function of A,REAL
for t being Division of A
for F being var_volume of rho,t holds 0 <= Sum F
let rho be Function of A,REAL; :: thesis: for t being Division of A
for F being var_volume of rho,t holds 0 <= Sum F
let t be Division of A; :: thesis: for F being var_volume of rho,t holds 0 <= Sum F
let F be var_volume of rho,t; :: thesis: 0 <= Sum F
for k being Nat st k in dom F holds
0 <= F . k by LM1;
hence 0 <= Sum F by RVSUM_1:84; :: thesis: verum