let c be complex number ; :: thesis: for A being 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 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

X1: Re (integral (f,A)) = integral ((Re f),A) by COMPLEX1:28;
X2: Im (integral (f,A)) = integral ((Im f),A) by COMPLEX1:28;
hence Re (c * (integral (f,A))) = ((Re c) * (integral ((Re f),A))) - ((Im c) * (integral ((Im f),A))) by COMPLEX1:24, X1; :: 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 COMPLEX1:24, X1, X2; :: thesis: verum

end;

( (Re f) | A = Re (f | A) & (Im f) | A = Im (f | A) ) by Lm6;
then A5: ( (Re f) | A is bounded & (Im f) | A is bounded ) by A3, BND01A;
A6: ( A c= dom (Re f) & A c= dom (Im f) ) by A1, COMSEQ_3:def 3, COMSEQ_3:def 4;
X0: ( Re f is_integrable_on A & Im f is_integrable_on A ) by A2, Def16;
then X1: ( (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 A5, A6, INTEGRA6:9;
X2: ( Re (c (#) f) = ((Re c) (#) (Re f)) - ((Im c) (#) (Im f)) & Im (c (#) f) = ((Re c) (#) (Im f)) + ((Im c) (#) (Re f)) ) by Th16C;
X3: ( ((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 A5, RFUNCT_1:97;
( dom (Re f) = dom f & dom (Im f) = dom f ) by COMSEQ_3:def 3, COMSEQ_3:def 4;
then X4: ( 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 Z1: Re (c (#) f) is_integrable_on A by INTEGRA6:11, X1, X2, X3;
Im (c (#) f) is_integrable_on A by INTEGRA6:11, X1, X2, X3, X4;
hence c (#) f is_integrable_on A by Z1, Def16; :: thesis: integral ((c (#) f),A) = c * (integral (f,A))
Z3: Re (integral ((c (#) f),A)) = integral ((Re (c (#) f)),A) by COMPLEX1:28
.= (integral (((Re c) (#) (Re f)),A)) - (integral (((Im c) (#) (Im f)),A)) by INTEGRA6:11, X1, X2, X3, X4
.= ((Re c) * (integral ((Re f),A))) - (integral (((Im c) (#) (Im f)),A)) by X0, A5, A6, INTEGRA6:9
.= Re (c * (integral (f,A))) by A4, X0, A5, A6, INTEGRA6:9 ;
Im (integral ((c (#) f),A)) = integral ((Im (c (#) f)),A) by COMPLEX1:28
.= (integral (((Re c) (#) (Im f)),A)) + (integral (((Im c) (#) (Re f)),A)) by INTEGRA6:11, X1, X2, X3, X4
.= ((Re c) * (integral ((Im f),A))) + (integral (((Im c) (#) (Re f)),A)) by X0, A5, A6, INTEGRA6:9
.= Im (c * (integral (f,A))) by A4, X0, A5, A6, INTEGRA6:9 ;
hence integral ((c (#) f),A) = c * (integral (f,A)) by Z3, COMPLEX1:def 5; :: thesis: verum