theorem Th32: :: LIMFUNC3:32

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