let a, b, c, d, e be Real; :: thesis: 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).|

let Y be RealBanachSpace; :: thesis: 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).|

let f be continuous PartFunc of REAL, the carrier of Y; :: thesis: ( 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 ) implies ||.(integral (f,c,d)).|| <= e * |.(d - c).| )

set A = ['(min (c,d)),(max (c,d))'];

assume that

A1: ( a <= b & ['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).|

rng ||.f.|| c= REAL ;

then A3: ||.f.|| is Function of (dom ||.f.||),REAL by FUNCT_2:2;

B1: ['(min (c,d)),(max (c,d))'] c= ['a,b'] by A1, Lm2;

B2: dom ||.f.|| = dom f by NORMSP_0:def 2;

then ['(min (c,d)),(max (c,d))'] c= dom ||.f.|| by A1, B1;

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;

A4: vol ['(min (c,d)),(max (c,d))'] = |.(d - c).| by INTEGRA6:6;

A5: ( ||.f.|| is_integrable_on ['(min (c,d)),(max (c,d))'] & g | ['(min (c,d)),(max (c,d))'] is bounded & ||.(integral (f,c,d)).|| <= integral (||.f.||,(min (c,d)),(max (c,d))) ) by A1, Th1922;

consider h being Function of ['(min (c,d)),(max (c,d))'],REAL such that

A6: rng h = {e} and

A7: h | ['(min (c,d)),(max (c,d))'] is bounded by INTEGRA4:5;

then A12: integral (||.f.||,(min (c,d)),(max (c,d))) = integral (||.f.||,['(min (c,d)),(max (c,d))']) by INTEGRA5:def 4, XXREAL_0:2;

( h is integrable & integral h = e * (vol ['(min (c,d)),(max (c,d))']) ) by A6, INTEGRA4:4;

then integral (||.f.||,(min (c,d)),(max (c,d))) <= e * |.(d - c).| by A12, A7, A8, A5, A4, INTEGRA2:34;

hence ||.(integral (f,c,d)).|| <= e * |.(d - c).| by A5, XXREAL_0:2; :: thesis: verum

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

let Y be RealBanachSpace; :: thesis: 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).|

let f be continuous PartFunc of REAL, the carrier of Y; :: thesis: ( 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 ) implies ||.(integral (f,c,d)).|| <= e * |.(d - c).| )

set A = ['(min (c,d)),(max (c,d))'];

assume that

A1: ( a <= b & ['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).|

rng ||.f.|| c= REAL ;

then A3: ||.f.|| is Function of (dom ||.f.||),REAL by FUNCT_2:2;

B1: ['(min (c,d)),(max (c,d))'] c= ['a,b'] by A1, Lm2;

B2: dom ||.f.|| = dom f by NORMSP_0:def 2;

then ['(min (c,d)),(max (c,d))'] c= dom ||.f.|| by A1, B1;

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;

A4: vol ['(min (c,d)),(max (c,d))'] = |.(d - c).| by INTEGRA6:6;

A5: ( ||.f.|| is_integrable_on ['(min (c,d)),(max (c,d))'] & g | ['(min (c,d)),(max (c,d))'] is bounded & ||.(integral (f,c,d)).|| <= integral (||.f.||,(min (c,d)),(max (c,d))) ) by A1, Th1922;

consider h being Function of ['(min (c,d)),(max (c,d))'],REAL such that

A6: rng h = {e} and

A7: h | ['(min (c,d)),(max (c,d))'] is bounded by INTEGRA4:5;

A8: now :: thesis: for x being Real st x in ['(min (c,d)),(max (c,d))'] holds

g . x <= h . x

( min (c,d) <= c & c <= max (c,d) )
by XXREAL_0:17, XXREAL_0:25;g . x <= h . x

let x be Real; :: thesis: ( x in ['(min (c,d)),(max (c,d))'] implies g . x <= h . x )

assume A9: x in ['(min (c,d)),(max (c,d))'] ; :: thesis: g . x <= h . x

then g . x = ||.f.|| . x by FUNCT_1:49;

then A10: g . x = ||.(f /. x).|| by A9, B2, A1, B1, NORMSP_0:def 2;

h . x in {e} by A6, A9, FUNCT_2:4;

then h . x = e by TARSKI:def 1;

hence g . x <= h . x by A2, A9, A10; :: thesis: verum

end;assume A9: x in ['(min (c,d)),(max (c,d))'] ; :: thesis: g . x <= h . x

then g . x = ||.f.|| . x by FUNCT_1:49;

then A10: g . x = ||.(f /. x).|| by A9, B2, A1, B1, NORMSP_0:def 2;

h . x in {e} by A6, A9, FUNCT_2:4;

then h . x = e by TARSKI:def 1;

hence g . x <= h . x by A2, A9, A10; :: thesis: verum

then A12: integral (||.f.||,(min (c,d)),(max (c,d))) = integral (||.f.||,['(min (c,d)),(max (c,d))']) by INTEGRA5:def 4, XXREAL_0:2;

( h is integrable & integral h = e * (vol ['(min (c,d)),(max (c,d))']) ) by A6, INTEGRA4:4;

then integral (||.f.||,(min (c,d)),(max (c,d))) <= e * |.(d - c).| by A12, A7, A8, A5, A4, INTEGRA2:34;

hence ||.(integral (f,c,d)).|| <= e * |.(d - c).| by A5, XXREAL_0:2; :: thesis: verum