:: 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_{5} being FinSequence of REAL n holds

( b_{5} is middle_volume of f,D iff ( len b_{5} = 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_{5} . i = (vol (divset (D,i))) * r ) ) ) );

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

( b

ex r being Element of REAL n st

( r in rng (f | (divset (D,i))) & b