let A be non empty closed_interval Subset of REAL; 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; ( 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
; ( 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;
( (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;
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 )
; ( 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)) )
;
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))
; 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))
; verum