theorem :: INTEGR21:25

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