theorem :: INTEGR21:28

for a, b, c, d being Real
for Y being RealBanachSpace
for E being Point of Y
for f being PartFunc of REAL, the carrier of Y st a <= b & c in ['a,b'] & d in ['a,b'] & ['a,b'] c= dom f & ( for x being Real st x in ['a,b'] holds
f /. x = E ) holds
integral (f,c,d) = (d - c) * E