let X be RealNormSpace; :: thesis: for r being Real
for A being closed-interval Subset of REAL
for f being PartFunc of REAL ,the carrier of X st A c= dom f & f is_integrable_on A holds
( r (#) f is_integrable_on A & integral (r (#) f),A = r * (integral f,A) )
let r be Real; :: thesis: for A being closed-interval Subset of REAL
for f being PartFunc of REAL ,the carrier of X st A c= dom f & f is_integrable_on A holds
( r (#) f is_integrable_on A & integral (r (#) f),A = r * (integral f,A) )
let A be closed-interval Subset of REAL ; :: thesis: for f being PartFunc of REAL ,the carrier of X st A c= dom f & f is_integrable_on A holds
( r (#) f is_integrable_on A & integral (r (#) f),A = r * (integral f,A) )
let f be PartFunc of REAL ,the carrier of X; :: thesis: ( A c= dom f & f is_integrable_on A implies ( r (#) f is_integrable_on A & integral (r (#) f),A = r * (integral f,A) ) )
assume AS: ( A c= dom f & f is_integrable_on A ) ; :: thesis: ( r (#) f is_integrable_on A & integral (r (#) f),A = r * (integral f,A) )
P0: A c= dom (r (#) f) by VFUNCT_1:def 4, AS;
consider g being Function of A,the carrier of X such that
P1: ( g = f | A & g is integrable ) by AS, Def16;
P2: (r (#) f) | A = r (#) (f | A) by VFUNCT_1:37
.= r (#) g by P1, Th03C ;
r (#) g is total by VFUNCT_1:40;
then reconsider gg = r (#) g as Function of A,the carrier of X ;
( gg is integrable & integral gg = r * (integral g) ) by P1, LMth03;
hence r (#) f is_integrable_on A by P2, Th01; :: thesis: integral (r (#) f),A = r * (integral f,A)
thus integral (r (#) f),A = integral gg by P2, P0, Def17
.= r * (integral g) by P1, LMth03
.= r * (integral f,A) by P1, AS, Def17 ; :: thesis: verum