:: deftheorem Def1 defines middle_volume INTEGR16:def 1 :
for A being non empty closed_interval Subset of REAL
for f being Function of A,COMPLEX
for D being Division of A
for b₄ being FinSequence of COMPLEX 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 Element of COMPLEX st
( c in rng (f | (divset (D,i))) & b₄ . i = c * (vol (divset (D,i))) ) ) ) );