theorem Th38: :: LIMFUNC1:38

for seq being Real_Sequence st seq is non-zero & seq is convergent & lim seq = 0 & seq is non-increasing holds
seq " is divergent_to+infty