theorem Th61: :: INTEGR24:61

for f being PartFunc of REAL,REAL
for a, b, r being Real st ].a,b.[ c= dom f & f is_improper_integrable_on a,b holds
( r (#) f is_improper_integrable_on a,b & improper_integral ((r (#) f),a,b) = r * (improper_integral (f,a,b)) )