:: deftheorem Def6 defines middle_sum INTEGR15:def 6 :

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 F being middle_volume of f,D

for b_{6} being Element of REAL n holds

( b_{6} = middle_sum (f,F) iff for i being Element of NAT st i in Seg n holds

ex Fi being FinSequence of REAL st

( Fi = (proj (i,n)) * F & b_{6} . i = Sum Fi ) );

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 F being middle_volume of f,D

for b

( b

ex Fi being FinSequence of REAL st

( Fi = (proj (i,n)) * F & b