let X be RealNormSpace; :: thesis: for A being closed-interval Subset of REAL
for f1, f2 being PartFunc of REAL ,the carrier of X st f1 is_integrable_on A & f2 is_integrable_on A & A c= dom f1 & A c= dom f2 holds
( f1 + f2 is_integrable_on A & integral (f1 + f2),A = (integral f1,A) + (integral f2,A) )
let A be closed-interval Subset of REAL ; :: thesis: for f1, f2 being PartFunc of REAL ,the carrier of X st f1 is_integrable_on A & f2 is_integrable_on A & A c= dom f1 & A c= dom f2 holds
( f1 + f2 is_integrable_on A & integral (f1 + f2),A = (integral f1,A) + (integral f2,A) )
let f1, f2 be PartFunc of REAL ,the carrier of X; :: thesis: ( f1 is_integrable_on A & f2 is_integrable_on A & A c= dom f1 & A c= dom f2 implies ( f1 + f2 is_integrable_on A & integral (f1 + f2),A = (integral f1,A) + (integral f2,A) ) )
assume that
A1: ( f1 is_integrable_on A & f2 is_integrable_on A ) and
A2: ( A c= dom f1 & A c= dom f2 ) ; :: thesis: ( f1 + f2 is_integrable_on A & integral (f1 + f2),A = (integral f1,A) + (integral f2,A) )
A c= (dom f1) /\ (dom f2) by A2, XBOOLE_1:19;
then P0: A c= dom (f1 + f2) by VFUNCT_1:def 1;
consider g1 being Function of A,the carrier of X such that
P11: ( g1 = f1 | A & g1 is integrable ) by A1, Def16;
consider g2 being Function of A,the carrier of X such that
P12: ( g2 = f2 | A & g2 is integrable ) by A1, Def16;
(f1 + f2) | A = (f1 | A) + (f2 | A) by VFUNCT_1:33;
then P1: (f1 + f2) | A = g1 + g2 by P11, P12, Th03A;
g1 + g2 is total by VFUNCT_1:38;
then reconsider g = g1 + g2 as Function of A,the carrier of X ;
g is integrable by LMth01, P11, P12;
hence f1 + f2 is_integrable_on A by P1, Th01; :: thesis: integral (f1 + f2),A = (integral f1,A) + (integral f2,A)
thus integral (f1 + f2),A = integral g by Def17, P1, P0
.= (integral g1) + (integral g2) by LMth01, P11, P12
.= (integral f1,A) + (integral g2) by A2, P11, Def17
.= (integral f1,A) + (integral f2,A) by A2, P12, Def17 ; :: thesis: verum