let a, b, e be Real; 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; ( 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
; ( 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
then A10:
h = g
by FUNCT_2:12;
h is integrable
by A4, INTEGRA4:4;
hence
f is_integrable_on ['a,b']
by A10; ( f | ['a,b'] is bounded & integral (f,a,b) = e * (b - a) )
thus
f | ['a,b'] is bounded
by A5, A10; 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; verum