for f being PartFunc of REAL,REAL st f is divergent_in+infty_to-infty holds
( not f is convergent_in+infty & not f is divergent_in+infty_to+infty )