theorem Lm5: :: FUZZY_6:4

for A being non empty closed_interval Subset of REAL
for e being Real
for f being PartFunc of REAL,REAL st A c= dom f & ( for x being Real st x in A holds
f . x = e ) holds
( f is_integrable_on A & f | A is bounded & integral (f,(lower_bound A),(upper_bound A)) = e * ((upper_bound A) - (lower_bound A)) )