let n be Element of NAT ; :: thesis: for a, b, c, d, e being Real
for f being PartFunc of REAL,(REAL-NS n) 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 st x in ['(min (c,d)),(max (c,d))'] holds
||.(f /. x).|| <= e ) holds
||.(integral (f,c,d)).|| <= (n * e) * |.(d - c).|
let a, b, c, d, e be Real; :: thesis: for f being PartFunc of REAL,(REAL-NS n) 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 st x in ['(min (c,d)),(max (c,d))'] holds
||.(f /. x).|| <= e ) holds
||.(integral (f,c,d)).|| <= (n * e) * |.(d - c).|
let f be PartFunc of REAL,(REAL-NS n); :: 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 st x in ['(min (c,d)),(max (c,d))'] holds
||.(f /. x).|| <= e ) implies ||.(integral (f,c,d)).|| <= (n * e) * |.(d - c).| )
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 st x in ['(min (c,d)),(max (c,d))'] holds
||.(f /. x).|| <= e ) ) ; :: thesis: ||.(integral (f,c,d)).|| <= (n * e) * |.(d - c).|
reconsider f1 = f as PartFunc of REAL,(REAL n) by REAL_NS1:def 4;
A2: f1 | ['a,b'] is bounded by A1, Th34;
A3: f1 is_integrable_on ['a,b'] by Th43, A2, A1;
for x being Real st x in ['(min (c,d)),(max (c,d))'] holds
|.(f1 /. x).| <= e

proof

let x be Real; :: thesis: ( x in ['(min (c,d)),(max (c,d))'] implies |.(f1 /. x).| <= e )
assume A4: x in ['(min (c,d)),(max (c,d))'] ; :: thesis: |.(f1 /. x).| <= e
then A5: ||.(f /. x).|| <= e by A1;
['(min (c,d)),(max (c,d))'] c= ['a,b'] by A1, Lm2;
then A6: x in ['a,b'] by A4;
then f /. x = f . x by A1, PARTFUN1:def 6
.= f1 /. x by A6, A1, PARTFUN1:def 6 ;
hence |.(f1 /. x).| <= e by A5, REAL_NS1:1; :: thesis: verum

end;

then |.(integral (f1,c,d)).| <= (n * e) * |.(d - c).| by A1, A2, A3, Th32;
hence ||.(integral (f,c,d)).|| <= (n * e) * |.(d - c).| by Th48, A1, REAL_NS1:1; :: thesis: verum