let A be 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, INTEGRA5:9;
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:60, RFUNCT_1:63;
A9: ( f || A is integrable & g || A is integrable ) by A2, A4, INTEGRA5:def 2;
then ( (f || A) + (g || A) is integrable & (f || A) - (g || A) is integrable ) by A6, A7, INTEGRA1:59, INTEGRA2:33;
hence ( f + g is_integrable_on A & f - g is_integrable_on A ) by A8, INTEGRA5:def 2; :: 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:59, INTEGRA2:33; :: thesis: verum