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