let seq1, seq2 be Real_Sequence; :: thesis: ( seq1 is divergent_to-infty & seq2 is divergent_to-infty implies seq1 (#) seq2 is divergent_to+infty )
assume ( seq1 is divergent_to-infty & seq2 is divergent_to-infty ) ; :: thesis: seq1 (#) seq2 is divergent_to+infty
then A1: ( (- jj) (#) seq1 is divergent_to+infty & (- jj) (#) seq2 is divergent_to+infty ) by Th14;
((- 1) (#) seq1) (#) ((- 1) (#) seq2) = (- 1) (#) (seq1 (#) ((- 1) (#) seq2)) by SEQ_1:18
.= (- 1) (#) ((- 1) (#) (seq1 (#) seq2)) by SEQ_1:19
.= ((- 1) * (- 1)) (#) (seq1 (#) seq2) by SEQ_1:23
.= seq1 (#) seq2 by SEQ_1:27 ;
hence seq1 (#) seq2 is divergent_to+infty by A1, Th10; :: thesis: verum