let f be PartFunc of REAL,REAL; :: thesis: for A being non empty closed_interval Subset of REAL
for r being Real
for Z being open Subset of REAL st f is_differentiable_on Z & A c= Z & f `| Z is_integrable_on A & (f `| Z) | A is bounded holds
integral ((r (#) (f `| Z)),A) = (r * (f . (upper_bound A))) - (r * (f . (lower_bound A)))
let A be non empty closed_interval Subset of REAL; :: thesis: for r being Real
for Z being open Subset of REAL st f is_differentiable_on Z & A c= Z & f `| Z is_integrable_on A & (f `| Z) | A is bounded holds
integral ((r (#) (f `| Z)),A) = (r * (f . (upper_bound A))) - (r * (f . (lower_bound A)))
let r be Real; :: thesis: for Z being open Subset of REAL st f is_differentiable_on Z & A c= Z & f `| Z is_integrable_on A & (f `| Z) | A is bounded holds
integral ((r (#) (f `| Z)),A) = (r * (f . (upper_bound A))) - (r * (f . (lower_bound A)))
let Z be open Subset of REAL; :: thesis: ( f is_differentiable_on Z & A c= Z & f `| Z is_integrable_on A & (f `| Z) | A is bounded implies integral ((r (#) (f `| Z)),A) = (r * (f . (upper_bound A))) - (r * (f . (lower_bound A))) )
assume that
A1: ( f is_differentiable_on Z & A c= Z ) and
A2: ( f `| Z is_integrable_on A & (f `| Z) | A is bounded ) ; :: thesis: integral ((r (#) (f `| Z)),A) = (r * (f . (upper_bound A))) - (r * (f . (lower_bound A)))
A3: ( (f `| Z) || A is integrable & ((f `| Z) || A) | A is bounded ) by A2, INTEGRA5:9;
A c= dom (f `| Z) by A1, FDIFF_1:def 7;
then A4: (f `| Z) || A is Function of A,REAL by FUNCT_2:68, INTEGRA5:6;
integral ((r (#) (f `| Z)),A) = integral (r (#) ((f `| Z) || A)) by RFUNCT_1:49
.= r * (integral ((f `| Z),A)) by A4, A3, INTEGRA2:31
.= r * ((f . (upper_bound A)) - (f . (lower_bound A))) by A1, A2, INTEGRA5:13 ;
hence integral ((r (#) (f `| Z)),A) = (r * (f . (upper_bound A))) - (r * (f . (lower_bound A))) ; :: thesis: verum