let a, b, c, d, e be real number ; :: thesis: for f being PartFunc of REAL,REAL st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] & ( for x being real number st x in ['(min (c,d)),(max (c,d))'] holds
abs (f . x) <= e ) holds
abs (integral (f,c,d)) <= e * (abs (d - c))
let f be PartFunc of REAL,REAL; :: thesis: ( a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] & ( for x being real number st x in ['(min (c,d)),(max (c,d))'] holds
abs (f . x) <= e ) implies abs (integral (f,c,d)) <= e * (abs (d - c)) )
set A = ['(min (c,d)),(max (c,d))'];
assume that
A1: ( a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] ) and
A2: for x being real number st x in ['(min (c,d)),(max (c,d))'] holds
abs (f . x) <= e ; :: thesis: abs (integral (f,c,d)) <= e * (abs (d - c))
rng (abs f) c= REAL ;
then A3: abs f is Function of (dom (abs f)),REAL by FUNCT_2:2;
['(min (c,d)),(max (c,d))'] c= dom (abs f) by A1, Th21;
then reconsider g = (abs 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))'] = abs (d - c) by Th6;
abs f is_integrable_on ['(min (c,d)),(max (c,d))'] by A1, Th21;
then A5: g is integrable by INTEGRA5:def 1;
reconsider e = e as Real by XREAL_0:def 1;
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

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 = (abs f) . x by FUNCT_1:49;
then A10: g . x = abs (f . x) by VALUED_1:18;
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;

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