let f be PartFunc of REAL ,REAL ; :: thesis: for A being 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 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 and
A2: A c= Z and
A3: f `| Z is_integrable_on A and
A4: (f `| Z) | A is bounded ; :: thesis: integral (r (#) (f `| Z)),A = (r * (f . (upper_bound A))) - (r * (f . (lower_bound A)))
Z c= dom f by A1, FDIFF_1:def 7;
then Y: A c= dom f by A2, XBOOLE_1:1;
f | Z is continuous by A1, FDIFF_1:33;
then f | A is continuous by A2, FCONT_1:17;
then f is_integrable_on A by Y, INTEGRA5:11;
then A5: ( f || A is integrable & (f `| Z) || A is integrable ) by A3, INTEGRA5:def 2;
A c= dom (f `| Z) by A1, A2, FDIFF_1:def 8;
then A6: (f `| Z) || A is Function of A,REAL by FUNCT_2:131, INTEGRA5:6;
A7: ((f `| Z) || A) | A is bounded by A4, INTEGRA5:9;
integral (r (#) (f `| Z)),A = integral (r (#) ((f `| Z) || A)) by RFUNCT_1:65
.= r * (integral (f `| Z),A) by A5, A6, A7, INTEGRA2:31
.= r * ((f . (upper_bound A)) - (f . (lower_bound A))) by A1, A2, A3, A4, INTEGRA5:13 ;
hence integral (r (#) (f `| Z)),A = (r * (f . (upper_bound A))) - (r * (f . (lower_bound A))) ; :: thesis: verum