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

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

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

then A10:
h = g
by FUNCT_2:12;
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;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

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