let a, b, e be real number ; :: thesis: for f being PartFunc of REAL,REAL st a <= b & ['a,b'] c= dom f & ( for x being real number st x in ['a,b'] holds
f . x = e ) holds
( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & integral (f,a,b) = e * (b - a) )
let f be PartFunc of REAL,REAL; :: thesis: ( a <= b & ['a,b'] c= dom f & ( for x being real number st x in ['a,b'] holds
f . x = e ) implies ( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & integral (f,a,b) = e * (b - a) ) )
assume that
A1: a <= b and
A2: ['a,b'] c= dom f and
A3: for x being real number st x in ['a,b'] holds
f . x = e ; :: thesis: ( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & integral (f,a,b) = e * (b - a) )
rng f c= REAL ;
then f is Function of (dom f),REAL by FUNCT_2:4;
then reconsider g = f || ['a,b'] as Function of ['a,b'],REAL by A2, FUNCT_2:38;
reconsider e1 = e as Real by XREAL_0:def 1;
consider h being Function of ['a,b'],REAL such that
A4: rng h = {e1} and
A5: h | ['a,b'] is bounded by INTEGRA4:5;
integral h = e1 * (vol ['a,b']) by A4, INTEGRA4:4;
then A6: integral h = e * (b - a) by A1, Th5;
A7: for x being set st x in ['a,b'] holds
g . x = h . x

proof

let x0 be set ; :: thesis: ( x0 in ['a,b'] implies g . x0 = h . x0 )
assume A8: x0 in ['a,b'] ; :: thesis: g . x0 = h . x0
then reconsider x = x0 as real number ;
g . x0 = f . x by A8, FUNCT_1:72;
then A9: g . x0 = e by A3, A8;
h . x in {e1} by A4, A8, FUNCT_2:6;
hence g . x0 = h . x0 by A9, TARSKI:def 1; :: thesis: verum

end;

then A10: h = g by FUNCT_2:18;
h is integrable by A4, INTEGRA4:4;
hence f is_integrable_on ['a,b'] by A10, INTEGRA5:def 2; :: thesis: ( f | ['a,b'] is bounded & integral (f,a,b) = e * (b - a) )
thus f | ['a,b'] is bounded :: thesis: integral (f,a,b) = e * (b - a)

proof

consider r being real number such that
A11: for c being set st c in ['a,b'] /\ (dom g) holds
abs (g . c) <= r by A5, A10, RFUNCT_1:90;

now

let c be set ; :: thesis: ( c in ['a,b'] /\ (dom f) implies abs (f . c) <= r )
['a,b'] /\ (dom g) = ['a,b'] /\ ((dom f) /\ ['a,b']) by RELAT_1:90;
then A12: ['a,b'] /\ (dom g) = (['a,b'] /\ ['a,b']) /\ (dom f) by XBOOLE_1:16;
assume c in ['a,b'] /\ (dom f) ; :: thesis: abs (f . c) <= r
then ( abs (g . c) <= r & c in dom g ) by A11, A12, XBOOLE_0:def 4;
hence abs (f . c) <= r by FUNCT_1:70; :: thesis: verum

end;

hence f | ['a,b'] is bounded by RFUNCT_1:90; :: thesis: verum

end;

integral (f,a,b) = integral (f,['a,b']) by A1, INTEGRA5:def 5;
hence integral (f,a,b) = e * (b - a) by A7, A6, FUNCT_2:18; :: thesis: verum