let a, b, c, d, e be Real; :: thesis:
let Y be RealBanachSpace; :: thesis:
let f be continuous PartFunc of REAL, the carrier of Y; :: thesis:
set A = ['(min (c,d)),(max (c,d))'];
assume that
A1: ( a <= b & ['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;
B1: ['(min (c,d)),(max (c,d))'] c= ['a,b'] by A1, Lm2;
B2: dom ||.f.|| = dom f by NORMSP_0:def 2;
then ['(min (c,d)),(max (c,d))'] c= dom ||.f.|| by A1, B1;
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;
A4: vol ['(min (c,d)),(max (c,d))'] = |.(d - c).| by INTEGRA6:6;
A5: ( ||.f.|| is_integrable_on ['(min (c,d)),(max (c,d))'] & g | ['(min (c,d)),(max (c,d))'] is bounded & ||.(integral (f,c,d)).|| <= integral (||.f.||,(min (c,d)),(max (c,d))) ) by A1, Th1922;
consider h being Function of ['(min (c,d)),(max (c,d))'],REAL such that
A6: rng h = {e} and
A7: h | ['(min (c,d)),(max (c,d))'] is bounded by INTEGRA4:5;

end;