let r be Real; :: 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
( r (#) f is_integrable_on A & integral (r (#) f),A = r * (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
( 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, Def16;
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, BND01A;
then A51: ( (Re f) | A is bounded & (Im f) | A is bounded ) by Lm6;
A52: ( 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, A51, 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, A51, A52, INTEGRA6:9; :: thesis: verum

end;

A6: ( 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:28;
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 Lm6;
then A71: ( (Re f) | A is bounded & (Im f) | A is bounded ) by A3, BND01A;
A72: ( 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, Def16;
then ( r (#) (Re f) is_integrable_on A & r (#) (Im f) is_integrable_on A ) by A71, A72, 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 by Def16; :: 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 A6, LM001;
hence integral (r (#) f),A = r * (integral f,A) by COMPLEX1:def 5; :: thesis: verum