let A be 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

A51: ( 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, BND01A;
then A52: ( (Re f2) | A is bounded & (Im f2) | A is bounded ) by Lm6;
( Re (f1 | A) is bounded & Im (f1 | A) is bounded ) by A3, BND01A;
then A53: ( (Re f1) | A is bounded & (Im f1) | A is bounded ) by Lm6;
A54: ( 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, Def16;
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 A51, A52, A53, 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 A51, A52, A53, A54, 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 ) by Def16; :: 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:28;
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 A6: ( 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:28;
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:19;
hence integral (f1 + f2),A = (integral f1,A) + (integral f2,A) by COMPLEX1:def 5; :: 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 A6, COMPLEX1:48;
hence integral (f1 - f2),A = (integral f1,A) - (integral f2,A) by COMPLEX1:def 5; :: thesis: verum