:: deftheorem defines tagged_sum COUSIN2:def 9 :
for I being non empty closed_interval Subset of REAL
for f being PartFunc of I,REAL
for TD being tagged_division of I holds tagged_sum (f,TD) = Sum (tagged_volume (f,TD));