theorem Th81: :: LIMFUNC1:81

for f being PartFunc of REAL,REAL st f is convergent_in+infty holds
( - f is convergent_in+infty & lim_in+infty (- f) = - (lim_in+infty f) )