theorem Th44: :: LIMFUNC2:44

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