let seq1, seq2 be Real_Sequence; :: thesis: ( seq1 is bounded & ( seq2 is divergent_to+infty or seq2 is divergent_to-infty ) & seq2 is non-zero implies ( seq1 /" seq2 is convergent & lim (seq1 /" seq2) = 0 ) )
assume A1: ( seq1 is bounded & ( seq2 is divergent_to+infty or seq2 is divergent_to-infty ) & seq2 is non-zero ) ; :: thesis: ( seq1 /" seq2 is convergent & lim (seq1 /" seq2) = 0 )
then ( seq2 " is convergent & lim (seq2 " ) = 0 ) by Th61;
hence ( seq1 /" seq2 is convergent & lim (seq1 /" seq2) = 0 ) by A1, SEQ_2:39, SEQ_2:40; :: thesis: verum