let a, b, e be Real; :: thesis: for f being PartFunc of REAL,REAL st a <= b & ['a,b'] c= dom f & ( for x being Real 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 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 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:2;
then reconsider g = f || ['a,b'] as Function of ['a,b'],REAL by A2, FUNCT_2:32;
reconsider e1 = e as Real ;
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 object st x in ['a,b'] holds
g . x = h . x

proof

let x0 be object ; :: 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 ;
g . x0 = f . x by A8, FUNCT_1:49;
then A9: g . x0 = e by A3, A8;
h . x in {e1} by A4, A8, FUNCT_2:4;
hence g . x0 = h . x0 by A9, TARSKI:def 1; :: thesis: verum

end;

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