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 ;
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 ;
hence integral ((r (#) (Re f)),A) = r * (integral ((Re f),A)) by ; :: thesis: integral ((r (#) (Im f)),A) = r * (integral ((Im f),A))
thus integral ((r (#) (Im f)),A) = r * (integral ((Im f),A)) by ; :: 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 ; :: 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 ;
A10: ( A c= dom (Re f) & A c= dom (Im f) ) by ;
( 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 ;
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 ;
hence integral ((r (#) f),A) = r * (integral (f,A)) ; :: thesis: verum