theorem :: LIMFUNC1:40

for seq being Real_Sequence st seq is non-zero & seq is convergent & lim seq = 0 & seq is decreasing holds
seq " is divergent_to+infty by Th38;