:: 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₆ being Element of REAL n holds
( b₆ = 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₆ . i = Sum Fi ) );