theorem :: INTEGR16:20

for r being Real
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)) )