theorem Th53: :: INTEGR24:53

for f being PartFunc of REAL,REAL
for a, b, r being Real st a < b & ].a,b.] c= dom f & f is_left_improper_integrable_on a,b holds
( r (#) f is_left_improper_integrable_on a,b & left_improper_integral ((r (#) f),a,b) = r * (left_improper_integral (f,a,b)) )