:: deftheorem Def1 defines middle_volume INTEGR18:def 1 :
for X being RealNormSpace
for A being non empty closed_interval Subset of REAL
for f being Function of A, the carrier of X
for D being Division of A
for b₅ being FinSequence of X holds
( b₅ is middle_volume of f,D iff ( len b₅ = len D & ( for i being Nat st i in dom D holds
ex c being Point of X st
( c in rng (f | (divset (D,i))) & b₅ . i = (vol (divset (D,i))) * c ) ) ) );