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 that
A1: seq1 is divergent_to+infty and
A2: seq2 is convergent and
A3: 0 < lim seq2 ; :: thesis: seq1 (#) seq2 is divergent_to+infty
consider n1 being Element of NAT such that
A4: for m being Element of NAT st n1 <= m holds
(lim seq2) / 2 < seq2 . m by A2, A3, Th30;

now

thus 0 < (lim seq2) / 2 by A3, 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 A4, 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 A1, Th49, Th53;
then (seq1 (#) seq2) ^\ n1 is divergent_to+infty by SEQM_3:42;
hence seq1 (#) seq2 is divergent_to+infty by Th34; :: thesis: verum