let a, b, c, d, e be Real; :: thesis: for n being non zero Element of NAT
for f being PartFunc of REAL,(REAL n) st a <= b & f is_integrable_on ['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 st x in ['(min (c,d)),(max (c,d))'] holds
|.(f /. x).| <= e ) holds
|.(integral (f,c,d)).| <= e * |.(d - c).|

let n be non zero Element of NAT ; :: thesis: for f being PartFunc of REAL,(REAL n) st a <= b & f is_integrable_on ['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 st x in ['(min (c,d)),(max (c,d))'] holds
|.(f /. x).| <= e ) holds
|.(integral (f,c,d)).| <= e * |.(d - c).|

let f be PartFunc of REAL,(REAL n); :: thesis: ( a <= b & f is_integrable_on ['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 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 & f is_integrable_on ['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 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 (),REAL by FUNCT_2:2;
dom |.f.| = dom f by NFCONT_4:def 2;
then A4: ['(min (c,d)),(max (c,d))'] c= dom |.f.| by ;
then reconsider g = |.f.| | ['(min (c,d)),(max (c,d))'] as Function of ['(min (c,d)),(max (c,d))'],REAL by ;
A5: vol ['(min (c,d)),(max (c,d))'] = |.(d - c).| by INTEGRA6:6;
|.f.| is_integrable_on ['(min (c,d)),(max (c,d))'] by ;
then A6: g is integrable ;
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 g . x = |.f.| /. x by ;
then A11: g . x = |.(f /. x).| by ;
h . x in {e} by ;
then h . x = e by TARSKI:def 1;
hence g . x <= h . x by A11, A2, A10; :: thesis: verum
end;
A12: |.(integral (f,c,d)).| <= integral (|.f.|,(min (c,d)),(max (c,d))) by ;
( min (c,d) <= c & c <= max (c,d) ) by ;
then min (c,d) <= max (c,d) by XXREAL_0:2;
then A13: integral (|.f.|,(min (c,d)),(max (c,d))) = integral (|.f.|,['(min (c,d)),(max (c,d))']) by INTEGRA5:def 4;
|.f.| | ['(min (c,d)),(max (c,d))'] is bounded by ;
then A14: g | ['(min (c,d)),(max (c,d))'] is bounded ;
( h is integrable & integral h = e * (vol ['(min (c,d)),(max (c,d))']) ) by ;
then integral (|.f.|,(min (c,d)),(max (c,d))) <= e * |.(d - c).| by ;
hence |.(integral (f,c,d)).| <= e * |.(d - c).| by ; :: thesis: verum