let a, b, r be Real; :: thesis: for f being PartFunc of REAL,REAL st a <= b & ['a,b'] c= dom f & ( for t being Real st t in ['a,b'] holds
f . t = r ) holds
( f | ['a,b'] is continuous & f | ['a,b'] is bounded & f is_integrable_on ['a,b'] & integral (f,a,b) = r * (b - a) )
let f be PartFunc of REAL,REAL; :: thesis: ( a <= b & ['a,b'] c= dom f & ( for t being Real st t in ['a,b'] holds
f . t = r ) implies ( f | ['a,b'] is continuous & f | ['a,b'] is bounded & f is_integrable_on ['a,b'] & integral (f,a,b) = r * (b - a) ) )
assume A1: ( a <= b & ['a,b'] c= dom f & ( for t being Real st t in ['a,b'] holds
f . t = r ) ) ; :: thesis: ( f | ['a,b'] is continuous & f | ['a,b'] is bounded & f is_integrable_on ['a,b'] & integral (f,a,b) = r * (b - a) )
A2: dom (f | ['a,b']) = ['a,b'] by A1, RELAT_1:62;
for y being object holds
( y in rng (f | ['a,b']) iff y in {r} )

proof

let y be object ; :: thesis: ( y in rng (f | ['a,b']) iff y in {r} )

hereby :: thesis: ( y in {r} implies y in rng (f | ['a,b']) )

assume y in rng (f | ['a,b']) ; :: thesis: y in {r}
then consider x being object such that
A3: ( x in dom (f | ['a,b']) & y = (f | ['a,b']) . x ) by FUNCT_1:def 3;
reconsider x = x as Real by A2, A3;
y = f . x by A2, A3, FUNCT_1:49
.= r by A1, A2, A3 ;
hence y in {r} by TARSKI:def 1; :: thesis: verum

end;

assume y in {r} ; :: thesis: y in rng (f | ['a,b'])
then A4: y = r by TARSKI:def 1;
A5: ['a,b'] = [.a,b.] by A1, INTEGRA5:def 3;
then y = f . a by A1, A4, XXREAL_1:1
.= (f | ['a,b']) . a by A1, A5, FUNCT_1:49, XXREAL_1:1 ;
hence y in rng (f | ['a,b']) by A1, A2, A5, FUNCT_1:3, XXREAL_1:1; :: thesis: verum

end;

then A7: rng (f | ['a,b']) = {r} by TARSKI:2;
rng (f | ['a,b']) c= REAL ;
then reconsider g = f || ['a,b'] as Function of ['a,b'],REAL by A2, FUNCT_2:2;
integral g = r * (vol ['a,b']) by A7, INTEGRA4:4
.= r * (b - a) by A1, Th5 ;
then integral (f,['a,b']) = r * (b - a) ;
hence ( f | ['a,b'] is continuous & f | ['a,b'] is bounded & f is_integrable_on ['a,b'] & integral (f,a,b) = r * (b - a) ) by A1, A7, FCONT_1:39, INTEGRA5:10, INTEGRA5:11, INTEGRA5:def 4; :: thesis: verum