let Y be RealBanachSpace; :: thesis: for a, b, c, d, e being Real
for f being continuous PartFunc of REAL, the carrier of Y st [.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).|
let a, b, c, d, e be Real; :: thesis: for f being continuous PartFunc of REAL, the carrier of Y st [.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).|
let f be continuous PartFunc of REAL, the carrier of Y; :: thesis: ( [.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 ) implies ||.(integral (f,c,d)).|| <= e * |.(d - c).| )
set A = ['(min (c,d)),(max (c,d))'];
assume that
A1: ( [.a,b.] c= dom f & c in [.a,b.] & d in [.a,b.] ) and
A2: for x being Real st x in [.(min (c,d)),(max (c,d)).] holds
||.(f /. x).|| <= e ; :: thesis: ||.(integral (f,c,d)).|| <= e * |.(d - c).|
X0: ( a <= c & c <= b ) by A1, XXREAL_1:1;
then X3: a <= b by XXREAL_0:2;
X1: [.a,b.] = ['a,b'] by X0, XXREAL_0:2, INTEGRA5:def 3;
rng ||.f.|| c= REAL ;
then A3: ||.f.|| is Function of (dom ||.f.||),REAL by FUNCT_2:2;
( min (c,d) <= c & c <= max (c,d) ) by XXREAL_0:17, XXREAL_0:25;
then X2: ['(min (c,d)),(max (c,d))'] = [.(min (c,d)),(max (c,d)).] by XXREAL_0:2, INTEGRA5:def 3;
dom ||.f.|| = dom f by NORMSP_0:def 2;
then A4: ['(min (c,d)),(max (c,d))'] c= dom ||.f.|| by A1, X0, XXREAL_0:2, X1, INTEGR19:3;
then reconsider g = ||.f.|| | ['(min (c,d)),(max (c,d))'] as Function of ['(min (c,d)),(max (c,d))'],REAL by A3, FUNCT_2:32;
A5: vol ['(min (c,d)),(max (c,d))'] = |.(d - c).| by INTEGRA6:6;
A6: ||.f.|| is_integrable_on ['(min (c,d)),(max (c,d))'] by A1, X3, X1, INTEGR21:22;
consider h being Function of ['(min (c,d)),(max (c,d))'],REAL such that
A7: rng h = {e} and
A8: h | ['(min (c,d)),(max (c,d))'] is bounded by INTEGRA4:5;

A9: now :: thesis: for x being Real st x in ['(min (c,d)),(max (c,d))'] holds
g . x <= h . x

let x be Real; :: thesis: ( x in ['(min (c,d)),(max (c,d))'] implies g . x <= h . x )
assume A10: x in ['(min (c,d)),(max (c,d))'] ; :: thesis: g . x <= h . x
then g . x = ||.f.|| . x by FUNCT_1:49;
then A11: g . x = ||.(f /. x).|| by A10, A4, NORMSP_0:def 3;
h . x in {e} by A7, A10, FUNCT_2:4;
then h . x = e by TARSKI:def 1;
hence g . x <= h . x by A11, A2, A10, X2; :: thesis: verum

end;

A12: ||.(integral (f,c,d)).|| <= integral (||.f.||,(min (c,d)),(max (c,d))) by A1, X1, X3, INTEGR21:22;
( min (c,d) <= c & c <= max (c,d) ) by XXREAL_0:17, XXREAL_0:25;
then A13: integral (||.f.||,(min (c,d)),(max (c,d))) = integral (||.f.||,['(min (c,d)),(max (c,d))']) by INTEGRA5:def 4, XXREAL_0:2;
A14: g | ['(min (c,d)),(max (c,d))'] is bounded by A1, X1, X3, INTEGR21:22;
( h is integrable & integral h = e * (vol ['(min (c,d)),(max (c,d))']) ) by A7, INTEGRA4:4;
then integral (||.f.||,(min (c,d)),(max (c,d))) <= e * |.(d - c).| by A13, A8, A9, A6, A14, A5, INTEGRA2:34;
hence ||.(integral (f,c,d)).|| <= e * |.(d - c).| by A12, XXREAL_0:2; :: thesis: verum