let seq be Real_Sequence; :: thesis: ( seq is non-zero & seq is convergent & lim seq = 0 & seq is non-increasing implies seq " is divergent_to+infty )
assume A1: ( seq is non-zero & seq is convergent & lim seq = 0 & seq is non-increasing ) ; :: thesis: seq " is divergent_to+infty
then for n being Element of NAT st 0 <= n holds
0 < seq . n by Th28;
hence seq " is divergent_to+infty by A1, Th62; :: thesis: verum