theorem :: LIMFUNC1:57

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
( g < r & g in dom (f1 (#) f2) ) ) & ex r, r1 being Real st
( 0 < r & ( for g being Real st g in (dom f2) /\ (left_open_halfline r1) holds
r <= f2 . g ) ) holds
f1 (#) f2 is divergent_in-infty_to+infty