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 (dom |.f.|),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 A1, Th3;

then reconsider g = |.f.| | ['(min (c,d)),(max (c,d))'] as Function of ['(min (c,d)),(max (c,d))'],REAL by A3, FUNCT_2:32;

A5: vol ['(min (c,d)),(max (c,d))'] = |.(d - c).| by INTEGRA6:6;

|.f.| is_integrable_on ['(min (c,d)),(max (c,d))'] by A1, Th22;

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;

( min (c,d) <= c & c <= max (c,d) ) by XXREAL_0:17, XXREAL_0:25;

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 A1, Th22;

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 A7, INTEGRA4:4;

then integral (|.f.|,(min (c,d)),(max (c,d))) <= e * |.(d - c).| by A13, A8, A9, A6, A14, A5, INTEGRA2:34;

hence |.(integral (f,c,d)).| <= e * |.(d - c).| by A12, XXREAL_0:2; :: thesis: verum

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 (dom |.f.|),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 A1, Th3;

then reconsider g = |.f.| | ['(min (c,d)),(max (c,d))'] as Function of ['(min (c,d)),(max (c,d))'],REAL by A3, FUNCT_2:32;

A5: vol ['(min (c,d)),(max (c,d))'] = |.(d - c).| by INTEGRA6:6;

|.f.| is_integrable_on ['(min (c,d)),(max (c,d))'] by A1, Th22;

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

A12:
|.(integral (f,c,d)).| <= integral (|.f.|,(min (c,d)),(max (c,d)))
by A1, Th22;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 A10, A4, PARTFUN1:def 6;

then A11: g . x = |.(f /. x).| by A10, A4, NFCONT_4:def 2;

h . x in {e} by A7, A10, FUNCT_2:4;

then h . x = e by TARSKI:def 1;

hence g . x <= h . x by A11, A2, A10; :: thesis: verum

end;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 A10, A4, PARTFUN1:def 6;

then A11: g . x = |.(f /. x).| by A10, A4, NFCONT_4:def 2;

h . x in {e} by A7, A10, FUNCT_2:4;

then h . x = e by TARSKI:def 1;

hence g . x <= h . x by A11, A2, A10; :: thesis: verum

( min (c,d) <= c & c <= max (c,d) ) by XXREAL_0:17, XXREAL_0:25;

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 A1, Th22;

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 A7, INTEGRA4:4;

then integral (|.f.|,(min (c,d)),(max (c,d))) <= e * |.(d - c).| by A13, A8, A9, A6, A14, A5, INTEGRA2:34;

hence |.(integral (f,c,d)).| <= e * |.(d - c).| by A12, XXREAL_0:2; :: thesis: verum