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 A1: ( 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 ) ; :: 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) )
then A2: ( f || A is integrable & g || A is integrable & (f || A) | A is bounded & (g || A) | A is bounded ) by INTEGRA5:9, INTEGRA5:def 2;
A3: ( f || A is Function of A,REAL & g || A is Function of A,REAL ) by A1, Lm1;
then A4: ( (f || A) + (g || A) is integrable & (f || A) - (g || A) is integrable ) by A2, INTEGRA1:59, INTEGRA2:33;
A5: ( (f || A) + (g || A) = (f + g) || A & (f || A) - (g || A) = (f - g) || A ) by RFUNCT_1:60, RFUNCT_1:63;
hence ( f + g is_integrable_on A & f - g is_integrable_on A ) by A4, 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 A2, A3, A5, INTEGRA1:59, INTEGRA2:33; :: thesis: verum