let f, g be PartFunc of REAL,REAL; :: thesis: for A being non empty 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 non empty 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)))
A8: ( (f `| Z) || A is integrable & (g `| Z) || A is integrable ) by A4, A6;
A c= dom (g `| Z) by A2, A3, FDIFF_1:def 7;
then A9: (g `| Z) || A is Function of A,REAL by FUNCT_2:68, INTEGRA5:6;
A c= dom (f `| Z) by A1, A3, FDIFF_1:def 7;
then A10: (f `| Z) || A is Function of A,REAL by FUNCT_2:68, INTEGRA5:6;
A11: ( ((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:47
.= (integral ((f `| Z),A)) - (integral ((g `| Z) || A)) by A8, A10, A9, A11, 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