:: deftheorem Def4 defines middle_sum INTEGR22:def 7 :
for A being non empty closed_interval Subset of REAL
for rho being Function of A,REAL
for u being PartFunc of REAL,REAL
for T being DivSequence of A
for S being middle_volume_Sequence of rho,u,T
for b₆ being Real_Sequence holds
( b₆ = middle_sum S iff for i being Nat holds b₆ . i = Sum (S . i) );