let A be non empty closed_interval Subset of REAL; :: thesis: for f, g being PartFunc of REAL,REAL st A c= dom f & A c= dom g & f is_integrable_on A & f | A is bounded & g is_integrable_on A & g | A is bounded holds
( f + g is_integrable_on A & f - g is_integrable_on A & integral ((f + g),A) = (integral (f,A)) + (integral (g,A)) & integral ((f - g),A) = (integral (f,A)) - (integral (g,A)) )
let f, g be PartFunc of REAL,REAL; :: thesis: ( A c= dom f & A c= dom g & f is_integrable_on A & f | A is bounded & g is_integrable_on A & g | A is bounded implies ( f + g is_integrable_on A & f - g is_integrable_on A & integral ((f + g),A) = (integral (f,A)) + (integral (g,A)) & integral ((f - g),A) = (integral (f,A)) - (integral (g,A)) ) )
assume that
A1: ( A c= dom f & A c= dom g ) and
A2: f is_integrable_on A and
A3: f | A is bounded and
A4: g is_integrable_on A and
A5: g | A is bounded ; :: thesis: ( f + g is_integrable_on A & f - g is_integrable_on A & integral ((f + g),A) = (integral (f,A)) + (integral (g,A)) & integral ((f - g),A) = (integral (f,A)) - (integral (g,A)) )
A6: ( (f || A) | A is bounded & (g || A) | A is bounded ) by A3, A5;
A7: ( f || A is Function of A,REAL & g || A is Function of A,REAL ) by A1, Lm1;
A8: ( (f || A) + (g || A) = (f + g) || A & (f || A) - (g || A) = (f - g) || A ) by RFUNCT_1:44, RFUNCT_1:47;
A9: ( f || A is integrable & g || A is integrable ) by A2, A4;
then ( (f || A) + (g || A) is integrable & (f || A) - (g || A) is integrable ) by A6, A7, INTEGRA1:57, INTEGRA2:33;
hence ( f + g is_integrable_on A & f - g is_integrable_on A ) by A8; :: thesis: ( integral ((f + g),A) = (integral (f,A)) + (integral (g,A)) & integral ((f - g),A) = (integral (f,A)) - (integral (g,A)) )
thus ( integral ((f + g),A) = (integral (f,A)) + (integral (g,A)) & integral ((f - g),A) = (integral (f,A)) - (integral (g,A)) ) by A9, A6, A7, A8, INTEGRA1:57, INTEGRA2:33; :: thesis: verum