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, Th34;
hence ( seq1 /" seq2 is convergent & lim (seq1 /" seq2) = 0 ) by A1, SEQ_2:25, SEQ_2:26; :: thesis: verum