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

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