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