theorem :: LIMFUNC1:61

for f being PartFunc of REAL,REAL st ( f is divergent_in-infty_to+infty or f is divergent_in-infty_to-infty ) holds
abs f is divergent_in-infty_to+infty