let a, b be Real; :: thesis:
let Y be RealBanachSpace; :: thesis:
let f be PartFunc of REAL, the carrier of Y; :: thesis:
let E be Point of Y; :: thesis:
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:
reconsider A = ['a,b'] as non empty closed_interval Subset of REAL ;
f is Function of (dom f),(rng f) by FUNCT_2:1;
then f is Function of (dom f), the carrier of Y by FUNCT_2:2;
then reconsider g = f | A as Function of A, the carrier of Y by A2, FUNCT_2:32;
A7: {E} c= rng g

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in {E} ; :: thesis:
then A5: x = E by TARSKI:def 1;
consider a being Element of A such that
A6: a in dom g by SUBSET_1:4;
f /. a = E by A3;
then f . a = E by A2, PARTFUN1:def 6;
then g . a = E by FUNCT_1:49;
hence x in rng g by A5, A6, FUNCT_1:3; :: thesis:

end;

rng g c= {E}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in rng g ; :: thesis:
then consider a being Element of A such that
a in dom g and
A9: g . a = x by PARTFUN1:3;
f . a = x by A9, FUNCT_1:49;
then f /. a = x by A2, PARTFUN1:def 6;
then x = E by A3;
hence x in {E} by TARSKI:def 1; :: thesis:

end;

then A10: rng g = {E} by A7, XBOOLE_0:def 10;
hence f is_integrable_on ['a,b'] by Th404; :: thesis:
integral g = (vol A) * E by A10, Th404;
then integral (f,A) = (vol A) * E by A2, INTEGR18:def 8;
then integral (f,A) = (b - a) * E by A1, INTEGRA6:5;
hence integral (f,a,b) = (b - a) * E by A1, INTEGR18:def 9; :: thesis: