theorem Th53: :: LIMFUNC2:53

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