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