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
( g < r & g in dom (f2 * f1) ) ) implies f2 * f1 is divergent_in-infty_to+infty )

assume that
A1: f1 is divergent_in-infty_to-infty and
A2: f2 is divergent_in-infty_to+infty and
A3: for r being Real ex g being Real st
( g < r & g in dom (f2 * f1) ) ; :: thesis:
now :: thesis: for s being Real_Sequence st s is divergent_to-infty & rng s c= dom (f2 * f1) holds
(f2 * f1) /* s is divergent_to+infty
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 that
A4: s is divergent_to-infty and
A5: rng s c= dom (f2 * f1) ; :: thesis: (f2 * f1) /* s is divergent_to+infty
rng s c= dom f1 by ;
then A6: f1 /* s is divergent_to-infty by A1, A4;
rng (f1 /* s) c= dom f2 by ;
then f2 /* (f1 /* s) is divergent_to+infty by A2, A6;
hence (f2 * f1) /* s is divergent_to+infty by ; :: thesis: verum
end;
hence f2 * f1 is divergent_in-infty_to+infty by A3; :: thesis: verum