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