:: deftheorem defines middle_sum INTEGR18:def 2 :
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 D being Division of A
for F being middle_volume of f,D holds middle_sum (f,F) = Sum F;