:: deftheorem defvm defines var_volume INTEGR22:def 2 :
for A being non empty closed_interval Subset of REAL
for rho being real-valued Function
for t being Division of A
for b₄ being FinSequence of REAL holds
( b₄ is var_volume of rho,t iff ( len b₄ = len t & ( for k being Nat st k in dom t holds
b₄ . k = |.(vol ((divset (t,k)),rho)).| ) ) );