let A be closed-interval Subset of REAL ; :: thesis: for f being PartFunc of REAL ,REAL
for r being Real st A c= dom f & f is_integrable_on A & f | A is bounded holds
( r (#) f is_integrable_on A & integral (r (#) f),A = r * (integral f,A) )
let f be PartFunc of REAL ,REAL ; :: thesis: for r being Real st A c= dom f & f is_integrable_on A & f | A is bounded holds
( r (#) f is_integrable_on A & integral (r (#) f),A = r * (integral f,A) )
let r be Real; :: thesis: ( A c= dom f & f is_integrable_on A & f | A is bounded implies ( r (#) f is_integrable_on A & integral (r (#) f),A = r * (integral f,A) ) )
assume A1: ( A c= dom f & f is_integrable_on A & f | A is bounded ) ; :: thesis: ( r (#) f is_integrable_on A & integral (r (#) f),A = r * (integral f,A) )
then A2: ( f || A is integrable & (f || A) | A is bounded ) by INTEGRA5:9, INTEGRA5:def 2;
rng f c= REAL ;
then f is Function of (dom f),REAL by FUNCT_2:4;
then A3: f | A is Function of A,REAL by A1, FUNCT_2:38;
r (#) (f || A) = (r (#) f) | A by RFUNCT_1:65;
then (r (#) f) || A is integrable by A2, A3, INTEGRA2:31;
hence r (#) f is_integrable_on A by INTEGRA5:def 2; :: thesis: integral (r (#) f),A = r * (integral f,A)
integral (r (#) f),A = integral (r (#) (f || A)) by RFUNCT_1:65;
hence integral (r (#) f),A = r * (integral f,A) by A2, A3, INTEGRA2:31; :: thesis: verum