:: deftheorem Def5 defines middle_volume INTEGR15:def 5 :
for n being Element of NAT
for A being non empty closed_interval Subset of REAL
for f being Function of A,(REAL n)
for D being Division of A
for b₅ being FinSequence of REAL n 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 n st
( r in rng (f | (divset (D,i))) & b₅ . i = (vol (divset (D,i))) * r ) ) ) );