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 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'] & ( 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))
then A2: ( ['(min c,d),(max c,d)'] c= dom (abs f) & abs f is_integrable_on ['(min c,d),(max c,d)'] & (abs f) | ['(min c,d),(max c,d)'] is bounded & abs (integral f,c,d) <= integral (abs f),(min c,d),(max c,d) ) by 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 A3: integral (abs f),(min c,d),(max c,d) = integral (abs f),['(min c,d),(max c,d)'] by INTEGRA5:def 5;
reconsider e = e as Real by XREAL_0:def 1;
rng (abs f) c= REAL ;
then abs f is Function of (dom (abs f)),REAL by FUNCT_2:4;
then reconsider g = (abs f) || ['(min c,d),(max c,d)'] as Function of ['(min c,d),(max c,d)'],REAL by A2, FUNCT_2:38;
consider h being Function of ['(min c,d),(max c,d)'],REAL such that
A4: ( rng h = {e} & h | ['(min c,d),(max c,d)'] is bounded ) by INTEGRA4:5;

A5: now

let x be Real; :: thesis: ( x in ['(min c,d),(max c,d)'] implies g . x <= h . x )
assume A6: x in ['(min c,d),(max c,d)'] ; :: thesis: g . x <= h . x
then h . x in {e} by A4, FUNCT_2:6;
then A7: h . x = e by TARSKI:def 1;
g . x = (abs f) . x by A6, FUNCT_1:72;
then g . x = abs (f . x) by VALUED_1:18;
hence g . x <= h . x by A1, A6, A7; :: thesis: verum

end;

A8: ( g is integrable & g | ['(min c,d),(max c,d)'] is bounded ) by A2, INTEGRA5:9, INTEGRA5:def 2;
A9: ( h is integrable & integral h = e * (vol ['(min c,d),(max c,d)']) ) by A4, INTEGRA4:4;
vol ['(min c,d),(max c,d)'] = abs (d - c) by Th6;
then integral (abs f),(min c,d),(max c,d) <= e * (abs (d - c)) by A3, A4, A5, A8, A9, INTEGRA2:34;
hence abs (integral f,c,d) <= e * (abs (d - c)) by A2, XXREAL_0:2; :: thesis: verum