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