let seq1, seq2 be Real_Sequence; :: thesis: ( seq1 is divergent_to-infty & ex r being Real st
( 0 < r & ( for n being Element of NAT holds seq2 . n >= r ) ) implies seq1 (#) seq2 is divergent_to-infty )
assume that
A1: seq1 is divergent_to-infty and
A2: ex r being Real st
( 0 < r & ( for n being Element of NAT holds seq2 . n >= r ) ) ; :: thesis: seq1 (#) seq2 is divergent_to-infty
(- 1) (#) seq1 is divergent_to+infty by A1, Th41;
then A3: ((- 1) (#) seq1) (#) seq2 is divergent_to+infty by A2, Th49;
(- 1) (#) (((- 1) (#) seq1) (#) seq2) = (- 1) (#) ((- 1) (#) (seq1 (#) seq2)) by SEQ_1:26
.= ((- 1) * (- 1)) (#) (seq1 (#) seq2) by SEQ_1:31
.= seq1 (#) seq2 by SEQ_1:35 ;
hence seq1 (#) seq2 is divergent_to-infty by A3, Th40; :: thesis: verum