let r be Real; :: 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
( r (#) f is_integrable_on A & integral ((r (#) f),A) = r * (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
( r (#) f is_integrable_on A & integral ((r (#) f),A) = r * (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 ( r (#) f is_integrable_on A & integral ((r (#) f),A) = r * (integral (f,A)) ) )
assume that
A1: A c= dom f and
A2: f is_integrable_on A and
A3: f | A is bounded ; :: thesis: ( r (#) f is_integrable_on A & integral ((r (#) f),A) = r * (integral (f,A)) )
A4: ( Re f is_integrable_on A & Im f is_integrable_on A ) by A2;
A5: ( integral ((r (#) (Re f)),A) = r * (integral ((Re f),A)) & integral ((r (#) (Im f)),A) = r * (integral ((Im f),A)) )

proof

( Re (f | A) is bounded & Im (f | A) is bounded ) by A3, Th11;
then A6: ( (Re f) | A is bounded & (Im f) | A is bounded ) by Lm4;
A7: ( A c= dom (Re f) & A c= dom (Im f) ) by A1, COMSEQ_3:def 3, COMSEQ_3:def 4;
hence integral ((r (#) (Re f)),A) = r * (integral ((Re f),A)) by A4, A6, INTEGRA6:9; :: thesis: integral ((r (#) (Im f)),A) = r * (integral ((Im f),A))
thus integral ((r (#) (Im f)),A) = r * (integral ((Im f),A)) by A4, A6, A7, INTEGRA6:9; :: thesis: verum

end;

A8: ( Re (integral ((r (#) f),A)) = r * (Re (integral (f,A))) & Im (integral ((r (#) f),A)) = r * (Im (integral (f,A))) )

proof

( Re (integral ((r (#) f),A)) = integral ((Re (r (#) f)),A) & r * (Re (integral (f,A))) = r * (integral ((Re f),A)) & Im (integral ((r (#) f),A)) = integral ((Im (r (#) f)),A) & r * (Im (integral (f,A))) = r * (integral ((Im f),A)) ) by COMPLEX1:12;
hence ( Re (integral ((r (#) f),A)) = r * (Re (integral (f,A))) & Im (integral ((r (#) f),A)) = r * (Im (integral (f,A))) ) by A5, MESFUN6C:2; :: thesis: verum

end;

( Re (r (#) f) is_integrable_on A & Im (r (#) f) is_integrable_on A )

proof

( (Re f) | A = Re (f | A) & (Im f) | A = Im (f | A) ) by Lm4;
then A9: ( (Re f) | A is bounded & (Im f) | A is bounded ) by A3, Th11;
A10: ( A c= dom (Re f) & A c= dom (Im f) ) by A1, COMSEQ_3:def 3, COMSEQ_3:def 4;
( Re f is_integrable_on A & Im f is_integrable_on A ) by A2;
then ( r (#) (Re f) is_integrable_on A & r (#) (Im f) is_integrable_on A ) by A9, A10, INTEGRA6:9;
hence ( Re (r (#) f) is_integrable_on A & Im (r (#) f) is_integrable_on A ) by MESFUN6C:2; :: thesis: verum

end;

hence r (#) f is_integrable_on A ; :: thesis: integral ((r (#) f),A) = r * (integral (f,A))
( Re (integral ((r (#) f),A)) = Re (r * (integral (f,A))) & Im (integral ((r (#) f),A)) = Im (r * (integral (f,A))) ) by A8, Th1;
hence integral ((r (#) f),A) = r * (integral (f,A)) ; :: thesis: verum