let f1, f2 be PartFunc of REAL,REAL; :: thesis:
assume that
A1: f1 is divergent_in-infty_to+infty and
A2: for r being Real ex g being Real st
( g < r & g in dom (f1 (#) f2) ) ; :: thesis:
given r2, r1 being Real such that A3: 0 < r2 and
A4: for g being Real st g in (dom f2) /\ (left_open_halfline r1) holds
r2 <= f2 . g ; :: thesis:

let seq be Real_Sequence; :: thesis:
assume that
A5: seq is divergent_to-infty and
A6: rng seq c= dom (f1 (#) f2) ; :: thesis:
consider k being Nat such that
A7: for n being Nat st k <= n holds
seq . n < r1 by A5;
A8: rng (seq ^\ k) c= rng seq by VALUED_0:21;
A9: rng seq c= dom f2 by A6, Lm3;
then A10: rng (seq ^\ k) c= dom f2 by A8;

A11: now :: thesis:

thus 0 < r2 by A3; :: thesis:
let n be Nat; :: thesis:
A12: n in NAT by ORDINAL1:def 12;
seq . (n + k) < r1 by A7, NAT_1:12;
then (seq ^\ k) . n < r1 by NAT_1:def 3;
then (seq ^\ k) . n in { g2 where g2 is Real : g2 < r1 } ;
then ( (seq ^\ k) . n in rng (seq ^\ k) & (seq ^\ k) . n in left_open_halfline r1 ) by VALUED_0:28, XXREAL_1:229;
then (seq ^\ k) . n in (dom f2) /\ (left_open_halfline r1) by A10, XBOOLE_0:def 4;
then r2 <= f2 . ((seq ^\ k) . n) by A4;
hence r2 <= (f2 /* (seq ^\ k)) . n by A9, A8, FUNCT_2:108, XBOOLE_1:1, A12; :: thesis:

end;

dom (f1 (#) f2) = (dom f1) /\ (dom f2) by A6, Lm3;
then rng (seq ^\ k) c= (dom f1) /\ (dom f2) by A6, A8;
then A13: (f1 /* (seq ^\ k)) (#) (f2 /* (seq ^\ k)) = (f1 (#) f2) /* (seq ^\ k) by RFUNCT_2:8
.= ((f1 (#) f2) /* seq) ^\ k by A6, VALUED_0:27 ;
rng seq c= dom f1 by A6, Lm3;
then A14: rng (seq ^\ k) c= dom f1 by A8;
seq ^\ k is divergent_to-infty by A5, Th27;
then f1 /* (seq ^\ k) is divergent_to+infty by A1, A14;
then (f1 /* (seq ^\ k)) (#) (f2 /* (seq ^\ k)) is divergent_to+infty by A11, Th22;
hence (f1 (#) f2) /* seq is divergent_to+infty by A13, Th7; :: thesis:

end;

hence f1 (#) f2 is divergent_in-infty_to+infty by A2; :: thesis: