:: deftheorem Def4 defines middle_sum INTEGR15:def 4 :
for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL
for T being DivSequence of A
for S being middle_volume_Sequence of f,T
for b₅ being Real_Sequence holds
( b₅ = middle_sum (f,S) iff for i being Element of NAT holds b₅ . i = middle_sum (f,(S . i)) );