let f1, f2 be PartFunc of REAL , REAL ; :: thesis: ( f1 is divergent_in+infty_to+infty & f2 is divergent_in+infty_to-infty & ( for r being Real ex g being Real st
( r < g & g in dom (f2 * f1) ) ) implies f2 * f1 is divergent_in+infty_to-infty )
assume A1: ( f1 is divergent_in+infty_to+infty & f2 is divergent_in+infty_to-infty & ( for r being Real ex g being Real st
( r < g & g in dom (f2 * f1) ) ) ) ; :: thesis: f2 * f1 is divergent_in+infty_to-infty

now

let s be Real_Sequence; :: thesis: ( s is divergent_to+infty & rng s c= dom (f2 * f1) implies (f2 * f1) /* s is divergent_to-infty )
assume A2: ( s is divergent_to+infty & rng s c= dom (f2 * f1) ) ; :: thesis: (f2 * f1) /* s is divergent_to-infty
then A3: ( rng s c= dom f1 & rng (f1 /* s) c= dom f2 ) by Lm2;
then f1 /* s is divergent_to+infty by A1, A2, LIMFUNC1:def 7;
then f2 /* (f1 /* s) is divergent_to-infty by A1, A3, LIMFUNC1:def 8;
hence (f2 * f1) /* s is divergent_to-infty by A2, VALUED_0:31; :: thesis: verum

end;

hence f2 * f1 is divergent_in+infty_to-infty by A1, LIMFUNC1:def 8; :: thesis: verum