theorem Th22: :: LIMFUNC1:22

for seq1, seq2 being Real_Sequence st seq1 is divergent_to+infty & ex r being Real st
( r > 0 & ( for n being Nat holds seq2 . n >= r ) ) holds
seq1 (#) seq2 is divergent_to+infty