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

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

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

then
|.(integral (f1,c,d)).| <= (n * e) * |.(d - c).|
by A1, A2, A3, Th32;
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;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

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