for Y being RealNormSpace
for A being non empty closed_interval Subset of REAL
for f being Function of A, the carrier of Y
for E being Point of Y st rng f = {E} holds
( f is integrable & integral f = (vol A) * E )