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;

( 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

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

A12:
||.(integral (f,c,d)).|| <= integral (||.f.||,(min (c,d)),(max (c,d)))
by A1, X1, X3, INTEGR21:22;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;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

( 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