let a, b be Real; :: thesis: for Y being RealBanachSpace
for f being PartFunc of REAL, the carrier of Y
for E being Point of Y 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'] & integral (f,a,b) = (b - a) * E )

let Y be RealBanachSpace; :: thesis: for f being PartFunc of REAL, the carrier of Y
for E being Point of Y 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'] & integral (f,a,b) = (b - a) * E )

let f be PartFunc of REAL, the carrier of Y; :: thesis: for E being Point of Y 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'] & integral (f,a,b) = (b - a) * E )

let E be Point of Y; :: 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'] & integral (f,a,b) = (b - a) * E ) )

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'] & integral (f,a,b) = (b - a) * E )
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 ;
A7: {E} c= rng g
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {E} or x in rng g )
assume x in {E} ; :: thesis: x in rng g
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 ;
then g . a = E by FUNCT_1:49;
hence x in rng g by ; :: thesis: verum
end;
rng g c= {E}
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng g or x in {E} )
assume x in rng g ; :: thesis: x in {E}
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 ;
then f /. a = x by ;
then x = E by A3;
hence x in {E} by TARSKI:def 1; :: thesis: verum
end;
then A10: rng g = {E} by ;
hence f is_integrable_on ['a,b'] by Th404; :: thesis: integral (f,a,b) = (b - a) * E
integral g = (vol A) * E by ;
then integral (f,A) = (vol A) * E by ;
then integral (f,A) = (b - a) * E by ;
hence integral (f,a,b) = (b - a) * E by ; :: thesis: verum