:: 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₆ being sequence of (REAL-NS n) holds
( b₆ = middle_sum (f,S) iff for i being Element of NAT holds b₆ . i = middle_sum (f,(S . i)) );