theorem :: LIMFUNC1:94

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