theorem :: LIMFUNC1:115

for f being PartFunc of REAL,REAL st f is convergent_in-infty & lim_in-infty f = 0 & ex r being Real st
for g being Real st g in (dom f) /\ (left_open_halfline r) holds
f . g < 0 holds
f ^ is divergent_in-infty_to-infty