theorem :: LIMFUNC1:55

for f1, f2 being PartFunc of REAL,REAL st f1 is divergent_in+infty_to+infty & ( for r being Real ex g being Real st
( r < g & g in dom (f1 (#) f2) ) ) & ex r, r1 being Real st
( 0 < r & ( for g being Real st g in (dom f2) /\ (right_open_halfline r1) holds
r <= f2 . g ) ) holds
f1 (#) f2 is divergent_in+infty_to+infty