let r be Real; :: thesis: for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL,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 A be non empty closed_interval Subset of REAL; :: thesis: for f being PartFunc of REAL,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: ( 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 that
A1: A c= dom f and
A2: ( f is_integrable_on A & f | A is bounded ) ; :: thesis: ( r (#) f is_integrable_on A & integral ((r (#) f),A) = r * (integral (f,A)) )
A3: ( f || A is integrable & (f || A) | A is bounded ) by A2;
rng f c= REAL ;
then f is Function of (dom f),REAL by FUNCT_2:2;
then A4: f | A is Function of A,REAL by A1, FUNCT_2:32;
r (#) (f || A) = (r (#) f) | A by RFUNCT_1:49;
then (r (#) f) || A is integrable by A3, A4, INTEGRA2:31;
hence r (#) f is_integrable_on A ; :: thesis: integral ((r (#) f),A) = r * (integral (f,A))
integral ((r (#) f),A) = integral (r (#) (f || A)) by RFUNCT_1:49;
hence integral ((r (#) f),A) = r * (integral (f,A)) by A3, A4, INTEGRA2:31; :: thesis: verum