let X be RealNormSpace; :: thesis: for A being non empty 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 non empty 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 A3: A c= dom (f1 + f2) by VFUNCT_1:def 1;
consider g1 being Function of A, the carrier of X such that
A4: ( g1 = f1 | A & g1 is integrable ) by A1;
consider g2 being Function of A, the carrier of X such that
A5: ( g2 = f2 | A & g2 is integrable ) by A1;
(f1 + f2) | A = (f1 | A) + (f2 | A) by VFUNCT_1:27;
then A6: (f1 + f2) | A = g1 + g2 by A4, A5, Th10;
g1 + g2 is total by VFUNCT_1:32;
then reconsider g = g1 + g2 as Function of A, the carrier of X ;
g is integrable by Th6, A4, A5;
hence f1 + f2 is_integrable_on A by A6; :: thesis: integral ((f1 + f2),A) = (integral (f1,A)) + (integral (f2,A))
thus integral ((f1 + f2),A) = integral g by Def8, A6, A3
.= (integral g1) + (integral g2) by Th6, A4, A5
.= (integral (f1,A)) + (integral g2) by A2, A4, Def8
.= (integral (f1,A)) + (integral (f2,A)) by A2, A5, Def8 ; :: thesis: verum