:: deftheorem Def1 defines middle_volume INTEGR22:def 5 :
for A being non empty closed_interval Subset of REAL
for rho being Function of A,REAL
for u being PartFunc of REAL,REAL st rho is bounded_variation & dom u = A holds
for t being Division of A
for b₅ being FinSequence of REAL holds
( b₅ is middle_volume of rho,u,t iff ( len b₅ = len t & ( for k being Nat st k in dom t holds
ex r being Real st
( r in rng (u | (divset (t,k))) & b₅ . k = r * (vol ((divset (t,k)),rho)) ) ) ) );