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) )