theorem :: LIMFUNC2:47

for x0 being Real
for f being PartFunc of REAL,REAL st f is_left_convergent_in x0 & f " {0} = {} & lim_left (f,x0) <> 0 holds
( f ^ is_left_convergent_in x0 & lim_left ((f ^),x0) = (lim_left (f,x0)) " )