theorem
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).|