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 A1: ( a <= b & ['a,b'] c= dom f & ( 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) )
reconsider e1 = e as Real by XREAL_0:def 1;
A2: integral f,a,b = integral f,['a,b'] by A1, INTEGRA5:def 5;
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 A1, FUNCT_2:38;
consider h being Function of ['a,b'],REAL such that
A3: ( rng h = {e1} & h | ['a,b'] is bounded ) by INTEGRA4:5;
A4: 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 A5: x0 in ['a,b'] ; :: thesis: g . x0 = h . x0
then reconsider x = x0 as real number ;
A6: h . x in {e1} by A3, A5, FUNCT_2:6;
g . x0 = f . x by A5, FUNCT_1:72;
then g . x0 = e by A1, A5;
hence g . x0 = h . x0 by A6, TARSKI:def 1; :: thesis: verum

end;

then A7: h = g by FUNCT_2:18;
h is integrable by A3, INTEGRA4:4;
hence f is_integrable_on ['a,b'] by A7, 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
A8: for c being set st c in ['a,b'] /\ (dom g) holds
abs (g . c) <= r by A3, A7, RFUNCT_1:90;

now

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

end;

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

end;

integral h = e1 * (vol ['a,b']) by A3, INTEGRA4:4;
then integral h = e * (b - a) by A1, Th5;
hence integral f,a,b = e * (b - a) by A2, A4, FUNCT_2:18; :: thesis: verum