:: deftheorem Def1 defines middle_volume INTEGR15:def 1 :
for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL
for D being Division of A
for b₄ being FinSequence of REAL holds
( b₄ is middle_volume of f,D iff ( len b₄ = len D & ( for i being Nat st i in dom D holds
ex r being Element of REAL st
( r in rng (f | (divset (D,i))) & b₄ . i = r * (vol (divset (D,i))) ) ) ) );