let seq1, seq2 be Real_Sequence; :: thesis: ( seq1 is divergent_to+infty & seq2 is convergent & 0 < lim seq2 implies seq1 (#) seq2 is divergent_to+infty )
assume A1: ( seq1 is divergent_to+infty & seq2 is convergent & 0 < lim seq2 ) ; :: thesis: seq1 (#) seq2 is divergent_to+infty
then consider n1 being Element of NAT such that
A2: for m being Element of NAT st n1 <= m holds
(lim seq2) / 2 < seq2 . m by Th30;

now

thus 0 < (lim seq2) / 2 by A1, XREAL_1:217; :: thesis: for n being Element of NAT holds (lim seq2) / 2 <= (seq2 ^\ n1) . n
let n be Element of NAT ; :: thesis: (lim seq2) / 2 <= (seq2 ^\ n1) . n
(lim seq2) / 2 < seq2 . (n + n1) by A2, NAT_1:12;
hence (lim seq2) / 2 <= (seq2 ^\ n1) . n by NAT_1:def 3; :: thesis: verum

end;

then (seq1 ^\ n1) (#) (seq2 ^\ n1) is divergent_to+infty by Th49, A1, Th53;
then (seq1 (#) seq2) ^\ n1 is divergent_to+infty by SEQM_3:42;
hence seq1 (#) seq2 is divergent_to+infty by Th34; :: thesis: verum