let seq1, seq2 be Real_Sequence; :: thesis: ( seq1 is divergent_to-infty & ex r being Real st
( 0 < r & ( for n being 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 Nat holds seq2 . n >= r ) ) ; :: thesis: seq1 (#) seq2 is divergent_to-infty
(- jj) (#) seq1 is divergent_to+infty by A1, Th14;
then A3: ((- jj) (#) seq1) (#) seq2 is divergent_to+infty by A2, Th22;
(- 1) (#) (((- 1) (#) seq1) (#) seq2) = (- 1) (#) ((- 1) (#) (seq1 (#) seq2)) by SEQ_1:18
.= ((- 1) * (- 1)) (#) (seq1 (#) seq2) by SEQ_1:23
.= seq1 (#) seq2 by SEQ_1:27 ;
hence seq1 (#) seq2 is divergent_to-infty by A3, Th13; :: thesis: verum