let seq be Real_Sequence; :: thesis: ( seq is non-zero & seq is convergent & lim seq = 0 & seq is non-decreasing implies seq " is divergent_to-infty )
assume that
A1: seq is non-zero and
A2: ( seq is convergent & lim seq = 0 ) and
A3: seq is non-decreasing ; :: thesis: seq " is divergent_to-infty
for n being Nat st 0 <= n holds
seq . n < 0 by A1, A2, A3, Th2;
hence seq " is divergent_to-infty by A2, Th36; :: thesis: verum