let n be non zero Element of NAT ; :: thesis: for a, b, c, d, e being Real
for f being PartFunc of REAL,(REAL-NS n) st a <= b & c <= d & 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 ['c,d'] holds
||.(f /. x).|| <= e ) holds
( ||.(integral (f,c,d)).|| <= e * (d - c) & ||.(integral (f,d,c)).|| <= e * (d - c) )
let a, b, c, d, e be Real; :: thesis: for f being PartFunc of REAL,(REAL-NS n) st a <= b & c <= d & 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 ['c,d'] holds
||.(f /. x).|| <= e ) holds
( ||.(integral (f,c,d)).|| <= e * (d - c) & ||.(integral (f,d,c)).|| <= e * (d - c) )
let f be PartFunc of REAL,(REAL-NS n); :: thesis: ( a <= b & c <= d & 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 ['c,d'] holds
||.(f /. x).|| <= e ) implies ( ||.(integral (f,c,d)).|| <= e * (d - c) & ||.(integral (f,d,c)).|| <= e * (d - c) ) )
assume A1: ( a <= b & c <= d & 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 ['c,d'] holds
||.(f /. x).|| <= e ) ) ; :: thesis: ( ||.(integral (f,c,d)).|| <= e * (d - c) & ||.(integral (f,d,c)).|| <= e * (d - c) )
A2: ['a,b'] = [.a,b.] by A1, INTEGRA5:def 3;
then A3: ex g being Real st
( c = g & a <= g & g <= b ) by A1;
A4: ex g being Real st
( d = g & a <= g & g <= b ) by A2, A1;
reconsider f1 = f as PartFunc of REAL,(REAL n) by REAL_NS1:def 4;
A5: f1 | ['a,b'] is bounded by A1, INTEGR19:34;
A6: f1 is_integrable_on ['a,b'] by A5, A1, INTEGR19:43;
A7: |.f1.| is_integrable_on ['a,b'] by A1, NFCONT_4:9;

now :: thesis: for x being Real st x in ['c,d'] holds
|.(f1 /. x).| <= e

let x be Real; :: thesis: ( x in ['c,d'] implies |.(f1 /. x).| <= e )
assume A8: x in ['c,d'] ; :: thesis: |.(f1 /. x).| <= e
then A9: ||.(f /. x).|| <= e by A1;
A10: ['c,d'] c= dom f by A1, INTEGR19:2, A3, A4;
then f /. x = f . x by A8, PARTFUN1:def 6
.= f1 /. x by A8, A10, PARTFUN1:def 6 ;
hence |.(f1 /. x).| <= e by A9, REAL_NS1:1; :: thesis: verum

end;

then ( |.(integral (f1,c,d)).| <= e * (d - c) & |.(integral (f1,d,c)).| <= e * (d - c) ) by A1, A5, A6, A7, INTEGR19:24;
hence ( ||.(integral (f,c,d)).|| <= e * (d - c) & ||.(integral (f,d,c)).|| <= e * (d - c) ) by REAL_NS1:1, A1, INTEGR19:48; :: thesis: verum