:: deftheorem Def8 defines middle_sum INTEGR15:def 8 :

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 T being DivSequence of A

for S being middle_volume_Sequence of f,T

for b_{6} being sequence of (REAL-NS n) holds

( b_{6} = middle_sum (f,S) iff for i being Element of NAT holds b_{6} . i = middle_sum (f,(S . i)) );

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 T being DivSequence of A

for S being middle_volume_Sequence of f,T

for b

( b