let f, g be PartFunc of REAL ,REAL ; :: thesis: for A being closed-interval Subset of REAL
for Z being open Subset of REAL st f is_differentiable_on Z & g is_differentiable_on Z & A c= Z & f `| Z is_integrable_on A & (f `| Z) | A is bounded & g `| Z is_integrable_on A & (g `| Z) | A is bounded holds
integral ((f `| Z) - (g `| Z)),A = ((f . (upper_bound A)) - (f . (lower_bound A))) - ((g . (upper_bound A)) - (g . (lower_bound A)))
let A be closed-interval Subset of REAL ; :: thesis: for Z being open Subset of REAL st f is_differentiable_on Z & g is_differentiable_on Z & A c= Z & f `| Z is_integrable_on A & (f `| Z) | A is bounded & g `| Z is_integrable_on A & (g `| Z) | A is bounded holds
integral ((f `| Z) - (g `| Z)),A = ((f . (upper_bound A)) - (f . (lower_bound A))) - ((g . (upper_bound A)) - (g . (lower_bound A)))
let Z be open Subset of REAL ; :: thesis: ( f is_differentiable_on Z & g is_differentiable_on Z & A c= Z & f `| Z is_integrable_on A & (f `| Z) | A is bounded & g `| Z is_integrable_on A & (g `| Z) | A is bounded implies integral ((f `| Z) - (g `| Z)),A = ((f . (upper_bound A)) - (f . (lower_bound A))) - ((g . (upper_bound A)) - (g . (lower_bound A))) )
assume that
A1: f is_differentiable_on Z and
A2: g is_differentiable_on Z and
A3: A c= Z and
A4: f `| Z is_integrable_on A and
A5: (f `| Z) | A is bounded and
A6: g `| Z is_integrable_on A and
A7: (g `| Z) | A is bounded ; :: thesis: integral ((f `| Z) - (g `| Z)),A = ((f . (upper_bound A)) - (f . (lower_bound A))) - ((g . (upper_bound A)) - (g . (lower_bound A)))
( Z c= dom f & Z c= dom g ) by A1, A2, FDIFF_1:def 7;
then Y: ( A c= dom f & A c= dom g ) by A3, XBOOLE_1:1;
( f | Z is continuous & g | Z is continuous ) by A1, A2, FDIFF_1:33;
then ( f | A is continuous & g | A is continuous ) by A3, FCONT_1:17;
then ( f is_integrable_on A & g is_integrable_on A ) by Y, INTEGRA5:11;
then A8: ( f || A is integrable & g || A is integrable & (f `| Z) || A is integrable & (g `| Z) || A is integrable ) by A4, A6, INTEGRA5:def 2;
( A c= dom (f `| Z) & A c= dom (g `| Z) ) by A1, A2, A3, FDIFF_1:def 8;
then A9: ( (f `| Z) || A is Function of A,REAL & (g `| Z) || A is Function of A,REAL ) by FUNCT_2:131, INTEGRA5:6;
A10: ( ((f `| Z) || A) | A is bounded & ((g `| Z) || A) | A is bounded ) by A5, A7, INTEGRA5:9;
integral ((f `| Z) - (g `| Z)),A = integral (((f `| Z) || A) - ((g `| Z) || A)) by RFUNCT_1:63
.= (integral (f `| Z),A) - (integral ((g `| Z) || A)) by A8, A9, A10, INTEGRA2:33
.= ((f . (upper_bound A)) - (f . (lower_bound A))) - (integral (g `| Z),A) by A1, A3, A4, A5, INTEGRA5:13
.= ((f . (upper_bound A)) - (f . (lower_bound A))) - ((g . (upper_bound A)) - (g . (lower_bound A))) by A2, A3, A6, A7, INTEGRA5:13 ;
hence integral ((f `| Z) - (g `| Z)),A = ((f . (upper_bound A)) - (f . (lower_bound A))) - ((g . (upper_bound A)) - (g . (lower_bound A))) ; :: thesis: verum