for f being PartFunc of REAL,REAL
for a being Real st f is_+infty_improper_integrable_on a & improper_integral_+infty (f,a) = -infty holds
for Intf being PartFunc of REAL,REAL st dom Intf = right_closed_halfline a & ( for x being Real st x in dom Intf holds
Intf . x = integral (f,a,x) ) holds
Intf is divergent_in+infty_to-infty