theorem Th36: :: COUSIN2:40

for I being non empty closed_interval Subset of REAL
for f being Function of I,REAL st f is constant holds
( f is HK-integrable & ex r being Real st
( f = r (#) (chi (I,I)) & HK-integral f = r * (vol I) ) )