for n being Element of NAT
for a, b being Real
for f being PartFunc of REAL,(REAL n)
for E being Element of REAL n st a <= b & ['a,b'] c= dom f & ( for x being Real st x in ['a,b'] holds
f . x = E ) holds
( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & integral (f,a,b) = (b - a) * E )