theorem :: LIMFUNC2:48

for x0 being Real
for f being PartFunc of REAL,REAL st f is_left_convergent_in x0 holds
( abs f is_left_convergent_in x0 & lim_left ((abs f),x0) = |.(lim_left (f,x0)).| )