theorem Th54: :: INTEGR24:54

for f being PartFunc of REAL,REAL
for a, b, r being Real st a < b & [.a,b.[ c= dom f & f is_right_improper_integrable_on a,b holds
( r (#) f is_right_improper_integrable_on a,b & right_improper_integral ((r (#) f),a,b) = r * (right_improper_integral (f,a,b)) )