let seq1, seq2 be Real_Sequence; :: thesis: ( seq1 is divergent_to+infty & ex r being Real st
( r > 0 & ( 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
( r > 0 & ( for n being Element of NAT holds seq2 . n >= r ) ) ) ; :: thesis: seq1 (#) seq2 is divergent_to+infty
then consider M being Real such that
A2: ( M > 0 & ( for n being Element of NAT holds seq2 . n >= M ) ) ;
let r be Real; :: according to LIMFUNC1:def 4 :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
r < (seq1 (#) seq2) . m
consider n being Element of NAT such that
A3: for m being Element of NAT st n <= m holds
(abs r) / M < seq1 . m by A1, Def4;
take n ; :: thesis: for m being Element of NAT st n <= m holds
r < (seq1 (#) seq2) . m
let m be Element of NAT ; :: thesis: ( n <= m implies r < (seq1 (#) seq2) . m )
assume n <= m ; :: thesis: r < (seq1 (#) seq2) . m
then A4: (abs r) / M < seq1 . m by A3;
0 <= abs r by COMPLEX1:132;
then ((abs r) / M) * M < (seq1 . m) * (seq2 . m) by A2, A4, XREAL_1:99;
then A5: abs r < (seq1 . m) * (seq2 . m) by A2, XCMPLX_1:88;
r <= abs r by ABSVALUE:11;
then r < (seq1 . m) * (seq2 . m) by A5, XXREAL_0:2;
hence r < (seq1 (#) seq2) . m by SEQ_1:12; :: thesis: verum