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 INTEGRA5:5
.= (integral ((f `| Z),A)) + (integral ((g `| Z),A)) by A8, A10, A9, A11, INTEGRA1:57
.= ((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