:: deftheorem Def4 defines middle_sum INTEGR18:def 4 :
for X being RealNormSpace
for A being non empty closed_interval Subset of REAL
for f being Function of A, the carrier of X
for T being DivSequence of A
for S being middle_volume_Sequence of f,T
for b₆ being sequence of X holds
( b₆ = middle_sum (f,S) iff for i being Nat holds b₆ . i = middle_sum (f,(S . i)) );