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

for k being Nat st k in dom F holds

0 <= F . k

let rho be Function of A,REAL; :: thesis: for t being Division of A

for F being var_volume of rho,t

for k being Nat st k in dom F holds

0 <= F . k

let t be Division of A; :: thesis: for F being var_volume of rho,t

for k being Nat st k in dom F holds

0 <= F . k

let F be var_volume of rho,t; :: thesis: for k being Nat st k in dom F holds

0 <= F . k

let k be Nat; :: thesis: ( k in dom F implies 0 <= F . k )

assume k in dom F ; :: thesis: 0 <= F . k

then k in Seg (len F) by FINSEQ_1:def 3;

then k in Seg (len t) by defvm;

then k in dom t by FINSEQ_1:def 3;

then F . k = |.(vol ((divset (t,k)),rho)).| by defvm;

hence 0 <= F . k by COMPLEX1:46; :: thesis: verum

for t being Division of A

for F being var_volume of rho,t

for k being Nat st k in dom F holds

0 <= F . k

let rho be Function of A,REAL; :: thesis: for t being Division of A

for F being var_volume of rho,t

for k being Nat st k in dom F holds

0 <= F . k

let t be Division of A; :: thesis: for F being var_volume of rho,t

for k being Nat st k in dom F holds

0 <= F . k

let F be var_volume of rho,t; :: thesis: for k being Nat st k in dom F holds

0 <= F . k

let k be Nat; :: thesis: ( k in dom F implies 0 <= F . k )

assume k in dom F ; :: thesis: 0 <= F . k

then k in Seg (len F) by FINSEQ_1:def 3;

then k in Seg (len t) by defvm;

then k in dom t by FINSEQ_1:def 3;

then F . k = |.(vol ((divset (t,k)),rho)).| by defvm;

hence 0 <= F . k by COMPLEX1:46; :: thesis: verum