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 A1: ( seq1 is divergent_to-infty & ex r being Real st
( 0 < r & ( for n being Element of NAT holds seq2 . n >= r ) ) ) ; :: thesis: seq1 (#) seq2 is divergent_to-infty
then (- 1) (#) seq1 is divergent_to+infty by Th41;
then A2: ((- 1) (#) seq1) (#) seq2 is divergent_to+infty by A1, 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 A2, Th40; :: thesis: verum