let c be Complex; :: thesis: for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL,COMPLEX st A c= dom f & f is_integrable_on A & f | A is bounded holds
( c (#) f is_integrable_on A & integral ((c (#) f),A) = c * (integral (f,A)) )
let A be non empty closed_interval Subset of REAL; :: thesis: for f being PartFunc of REAL,COMPLEX st A c= dom f & f is_integrable_on A & f | A is bounded holds
( c (#) f is_integrable_on A & integral ((c (#) f),A) = c * (integral (f,A)) )
let f be PartFunc of REAL,COMPLEX; :: thesis: ( A c= dom f & f is_integrable_on A & f | A is bounded implies ( c (#) f is_integrable_on A & integral ((c (#) f),A) = c * (integral (f,A)) ) )
assume that
A1: A c= dom f and
A2: f is_integrable_on A and
A3: f | A is bounded ; :: thesis: ( c (#) f is_integrable_on A & integral ((c (#) f),A) = c * (integral (f,A)) )
A4: ( Re (c * (integral (f,A))) = ((Re c) * (integral ((Re f),A))) - ((Im c) * (integral ((Im f),A))) & Im (c * (integral (f,A))) = ((Re c) * (integral ((Im f),A))) + ((Im c) * (integral ((Re f),A))) )

proof

A5: Re (integral (f,A)) = integral ((Re f),A) by COMPLEX1:12;
A6: Im (integral (f,A)) = integral ((Im f),A) by COMPLEX1:12;
hence Re (c * (integral (f,A))) = ((Re c) * (integral ((Re f),A))) - ((Im c) * (integral ((Im f),A))) by A5, COMPLEX1:9; :: thesis: Im (c * (integral (f,A))) = ((Re c) * (integral ((Im f),A))) + ((Im c) * (integral ((Re f),A)))
thus Im (c * (integral (f,A))) = ((Re c) * (integral ((Im f),A))) + ((Im c) * (integral ((Re f),A))) by A5, A6, COMPLEX1:9; :: thesis: verum

end;

( (Re f) | A = Re (f | A) & (Im f) | A = Im (f | A) ) by Lm4;
then A7: ( (Re f) | A is bounded & (Im f) | A is bounded ) by A3, Th11;
A8: ( A c= dom (Re f) & A c= dom (Im f) ) by A1, COMSEQ_3:def 3, COMSEQ_3:def 4;
A9: ( Re f is_integrable_on A & Im f is_integrable_on A ) by A2;
then A10: ( (Re c) (#) (Re f) is_integrable_on A & (Re c) (#) (Im f) is_integrable_on A & (Im c) (#) (Re f) is_integrable_on A & (Im c) (#) (Im f) is_integrable_on A ) by A7, A8, INTEGRA6:9;
A11: ( Re (c (#) f) = ((Re c) (#) (Re f)) - ((Im c) (#) (Im f)) & Im (c (#) f) = ((Re c) (#) (Im f)) + ((Im c) (#) (Re f)) ) by Th18;
A12: ( ((Re c) (#) (Re f)) | A is bounded & ((Re c) (#) (Im f)) | A is bounded & ((Im c) (#) (Re f)) | A is bounded & ((Im c) (#) (Im f)) | A is bounded ) by A7, RFUNCT_1:80;
( dom (Re f) = dom f & dom (Im f) = dom f ) by COMSEQ_3:def 3, COMSEQ_3:def 4;
then A13: ( A c= dom ((Re c) (#) (Re f)) & A c= dom ((Re c) (#) (Im f)) & A c= dom ((Im c) (#) (Re f)) & A c= dom ((Im c) (#) (Im f)) ) by A1, VALUED_1:def 5;
then A14: Re (c (#) f) is_integrable_on A by A10, A11, A12, INTEGRA6:11;
Im (c (#) f) is_integrable_on A by A10, A11, A12, A13, INTEGRA6:11;
hence c (#) f is_integrable_on A by A14; :: thesis: integral ((c (#) f),A) = c * (integral (f,A))
A15: Re (integral ((c (#) f),A)) = integral ((Re (c (#) f)),A) by COMPLEX1:12
.= (integral (((Re c) (#) (Re f)),A)) - (integral (((Im c) (#) (Im f)),A)) by A10, A11, A12, A13, INTEGRA6:11
.= ((Re c) * (integral ((Re f),A))) - (integral (((Im c) (#) (Im f)),A)) by A9, A7, A8, INTEGRA6:9
.= Re (c * (integral (f,A))) by A4, A9, A7, A8, INTEGRA6:9 ;
Im (integral ((c (#) f),A)) = integral ((Im (c (#) f)),A) by COMPLEX1:12
.= (integral (((Re c) (#) (Im f)),A)) + (integral (((Im c) (#) (Re f)),A)) by A10, A11, A12, A13, INTEGRA6:11
.= ((Re c) * (integral ((Im f),A))) + (integral (((Im c) (#) (Re f)),A)) by A9, A7, A8, INTEGRA6:9
.= Im (c * (integral (f,A))) by A4, A9, A7, A8, INTEGRA6:9 ;
hence integral ((c (#) f),A) = c * (integral (f,A)) by A15; :: thesis: verum