let A be non empty closed_interval Subset of REAL; :: thesis: for f1, f2 being PartFunc of REAL,COMPLEX st f1 is_integrable_on A & f2 is_integrable_on A & A c= dom f1 & A c= dom f2 & f1 | A is bounded & f2 | A is bounded holds
( f1 + f2 is_integrable_on A & f1 - f2 is_integrable_on A & integral ((f1 + f2),A) = (integral (f1,A)) + (integral (f2,A)) & integral ((f1 - f2),A) = (integral (f1,A)) - (integral (f2,A)) )
let f1, f2 be PartFunc of REAL,COMPLEX; :: thesis: ( f1 is_integrable_on A & f2 is_integrable_on A & A c= dom f1 & A c= dom f2 & f1 | A is bounded & f2 | A is bounded implies ( f1 + f2 is_integrable_on A & f1 - f2 is_integrable_on A & integral ((f1 + f2),A) = (integral (f1,A)) + (integral (f2,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 ) and
A3: f1 | A is bounded and
A4: f2 | A is bounded ; :: thesis: ( f1 + f2 is_integrable_on A & f1 - f2 is_integrable_on A & integral ((f1 + f2),A) = (integral (f1,A)) + (integral (f2,A)) & integral ((f1 - f2),A) = (integral (f1,A)) - (integral (f2,A)) )
A5: ( (Re f1) + (Re f2) is_integrable_on A & (Im f1) + (Im f2) is_integrable_on A & integral (((Re f1) + (Re f2)),A) = (integral ((Re f1),A)) + (integral ((Re f2),A)) & integral (((Im f1) + (Im f2)),A) = (integral ((Im f1),A)) + (integral ((Im f2),A)) & (Re f1) - (Re f2) is_integrable_on A & (Im f1) - (Im f2) is_integrable_on A & integral (((Re f1) - (Re f2)),A) = (integral ((Re f1),A)) - (integral ((Re f2),A)) & integral (((Im f1) - (Im f2)),A) = (integral ((Im f1),A)) - (integral ((Im f2),A)) )

proof

A6: ( A c= dom (Re f1) & A c= dom (Re f2) & A c= dom (Im f1) & A c= dom (Im f2) ) by A2, COMSEQ_3:def 3, COMSEQ_3:def 4;
( Re (f2 | A) is bounded & Im (f2 | A) is bounded ) by A4, Th11;
then A7: ( (Re f2) | A is bounded & (Im f2) | A is bounded ) by Lm4;
( Re (f1 | A) is bounded & Im (f1 | A) is bounded ) by A3, Th11;
then A8: ( (Re f1) | A is bounded & (Im f1) | A is bounded ) by Lm4;
A9: ( Re f1 is_integrable_on A & Im f1 is_integrable_on A & Re f2 is_integrable_on A & Im f2 is_integrable_on A ) by A1;
hence ( (Re f1) + (Re f2) is_integrable_on A & (Im f1) + (Im f2) is_integrable_on A & integral (((Re f1) + (Re f2)),A) = (integral ((Re f1),A)) + (integral ((Re f2),A)) & integral (((Im f1) + (Im f2)),A) = (integral ((Im f1),A)) + (integral ((Im f2),A)) ) by A6, A7, A8, INTEGRA6:11; :: thesis: ( (Re f1) - (Re f2) is_integrable_on A & (Im f1) - (Im f2) is_integrable_on A & integral (((Re f1) - (Re f2)),A) = (integral ((Re f1),A)) - (integral ((Re f2),A)) & integral (((Im f1) - (Im f2)),A) = (integral ((Im f1),A)) - (integral ((Im f2),A)) )
thus ( (Re f1) - (Re f2) is_integrable_on A & (Im f1) - (Im f2) is_integrable_on A & integral (((Re f1) - (Re f2)),A) = (integral ((Re f1),A)) - (integral ((Re f2),A)) & integral (((Im f1) - (Im f2)),A) = (integral ((Im f1),A)) - (integral ((Im f2),A)) ) by A6, A7, A8, A9, INTEGRA6:11; :: thesis: verum

end;

then ( Re (f1 + f2) is_integrable_on A & Im (f1 + f2) is_integrable_on A & Re (f1 - f2) is_integrable_on A & Im (f1 - f2) is_integrable_on A ) by MESFUN6C:5, MESFUN6C:6;
hence ( f1 + f2 is_integrable_on A & f1 - f2 is_integrable_on A ) ; :: thesis: ( integral ((f1 + f2),A) = (integral (f1,A)) + (integral (f2,A)) & integral ((f1 - f2),A) = (integral (f1,A)) - (integral (f2,A)) )
( (Re (integral (f1,A))) + (Re (integral (f2,A))) = (integral ((Re f1),A)) + (integral ((Re f2),A)) & (Im (integral (f1,A))) + (Im (integral (f2,A))) = (integral ((Im f1),A)) + (integral ((Im f2),A)) & (Re (integral (f1,A))) - (Re (integral (f2,A))) = (integral ((Re f1),A)) - (integral ((Re f2),A)) & (Im (integral (f1,A))) - (Im (integral (f2,A))) = (integral ((Im f1),A)) - (integral ((Im f2),A)) )

proof

( Re (integral (f1,A)) = integral ((Re f1),A) & Im (integral (f1,A)) = integral ((Im f1),A) & Re (integral (f2,A)) = integral ((Re f2),A) & Im (integral (f2,A)) = integral ((Im f2),A) ) by COMPLEX1:12;
hence ( (Re (integral (f1,A))) + (Re (integral (f2,A))) = (integral ((Re f1),A)) + (integral ((Re f2),A)) & (Im (integral (f1,A))) + (Im (integral (f2,A))) = (integral ((Im f1),A)) + (integral ((Im f2),A)) & (Re (integral (f1,A))) - (Re (integral (f2,A))) = (integral ((Re f1),A)) - (integral ((Re f2),A)) & (Im (integral (f1,A))) - (Im (integral (f2,A))) = (integral ((Im f1),A)) - (integral ((Im f2),A)) ) ; :: thesis: verum

end;

then ( (Re (integral (f1,A))) + (Re (integral (f2,A))) = integral ((Re (f1 + f2)),A) & (Im (integral (f1,A))) + (Im (integral (f2,A))) = integral ((Im (f1 + f2)),A) & (Re (integral (f1,A))) - (Re (integral (f2,A))) = integral ((Re (f1 - f2)),A) & (Im (integral (f1,A))) - (Im (integral (f2,A))) = integral ((Im (f1 - f2)),A) ) by A5, MESFUN6C:5, MESFUN6C:6;
then A10: ( Re (integral ((f1 + f2),A)) = (Re (integral (f1,A))) + (Re (integral (f2,A))) & Im (integral ((f1 + f2),A)) = (Im (integral (f1,A))) + (Im (integral (f2,A))) & Re (integral ((f1 - f2),A)) = (Re (integral (f1,A))) - (Re (integral (f2,A))) & Im (integral ((f1 - f2),A)) = (Im (integral (f1,A))) - (Im (integral (f2,A))) ) by COMPLEX1:12;
then ( Re (integral ((f1 + f2),A)) = Re ((integral (f1,A)) + (integral (f2,A))) & Im (integral ((f1 + f2),A)) = Im ((integral (f1,A)) + (integral (f2,A))) ) by COMPLEX1:8;
hence integral ((f1 + f2),A) = (integral (f1,A)) + (integral (f2,A)) ; :: thesis: integral ((f1 - f2),A) = (integral (f1,A)) - (integral (f2,A))
( Re (integral ((f1 - f2),A)) = Re ((integral (f1,A)) - (integral (f2,A))) & Im (integral ((f1 - f2),A)) = Im ((integral (f1,A)) - (integral (f2,A))) ) by A10, COMPLEX1:19;
hence integral ((f1 - f2),A) = (integral (f1,A)) - (integral (f2,A)) ; :: thesis: verum