let a, b be Real; 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; 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; 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; ( 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
; ( 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
rng g c= {E}
then A10:
rng g = {E}
by A7, XBOOLE_0:def 10;
hence
f is_integrable_on ['a,b']
by Th404; 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; verum