let a, b, c, d, e be Real; :: thesis:
let n be non zero Element of NAT ; :: thesis:
let f be PartFunc of REAL,(REAL n); :: thesis:
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:
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;

end;