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 ; :: 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 ; :: 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 ;
A8: ( A c= dom (Re f) & A c= dom (Im f) ) by ;
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 ;
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 ;
( dom (Re f) = dom f & dom (Im f) = dom f ) by ;
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 ;
then A14: Re (c (#) f) is_integrable_on A by ;
Im (c (#) f) is_integrable_on A by ;
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
.= ((Re c) * (integral ((Re f),A))) - (integral (((Im c) (#) (Im f)),A)) by
.= Re (c * (integral (f,A))) by ;
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
.= ((Re c) * (integral ((Im f),A))) + (integral (((Im c) (#) (Re f)),A)) by
.= Im (c * (integral (f,A))) by ;
hence integral ((c (#) f),A) = c * (integral (f,A)) by A15; :: thesis: verum