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 A2, FUNCT_2:32;

A7: {E} c= rng g

hence f is_integrable_on ['a,b'] by Th404; :: thesis: integral (f,a,b) = (b - a) * E

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: verum

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 A2, FUNCT_2:32;

A7: {E} c= rng g

proof

rng g c= {E}
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 A2, PARTFUN1:def 6;

then g . a = E by FUNCT_1:49;

hence x in rng g by A5, A6, FUNCT_1:3; :: thesis: verum

end;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 A2, PARTFUN1:def 6;

then g . a = E by FUNCT_1:49;

hence x in rng g by A5, A6, FUNCT_1:3; :: thesis: verum

proof

then A10:
rng g = {E}
by A7, XBOOLE_0:def 10;
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 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: verum

end;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 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: verum

hence f is_integrable_on ['a,b'] by Th404; :: thesis: integral (f,a,b) = (b - a) * E

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: verum