:: deftheorem defines middle_sum INTEGR15:def 2 :

for A being non empty closed_interval Subset of REAL

for f being Function of A,REAL

for D being Division of A

for F being middle_volume of f,D holds middle_sum (f,F) = Sum F;

for A being non empty closed_interval Subset of REAL

for f being Function of A,REAL

for D being Division of A

for F being middle_volume of f,D holds middle_sum (f,F) = Sum F;