theorem Th43: :: LIMFUNC2:43

for r, x0 being Real
for f being PartFunc of REAL,REAL st f is_left_convergent_in x0 holds
( r (#) f is_left_convergent_in x0 & lim_left ((r (#) f),x0) = r * (lim_left (f,x0)) )