let n be Element of NAT ; :: thesis: for a, b, c, d, e being Real
for f being PartFunc of 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 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,() 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,(); :: 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 ;
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 ;
then A6: x in ['a,b'] by A4;
then f /. x = f . x by
.= f1 /. x by ;
hence |.(f1 /. x).| <= e by ; :: 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 ; :: thesis: verum