let f1, f2 be PartFunc of REAL,REAL; :: thesis: ( f1 is convergent_in+infty & f2 is_left_divergent_to-infty_in lim_in+infty f1 & ( for r being Real ex g being Real st
( r < g & g in dom (f2 * f1) ) ) & ex r being Real st
for g being Real st g in (dom f1) /\ (right_open_halfline r) holds
f1 . g < lim_in+infty f1 implies f2 * f1 is divergent_in+infty_to-infty )
assume that
A1: f1 is convergent_in+infty and
A2: f2 is_left_divergent_to-infty_in lim_in+infty f1 and
A3: for r being Real ex g being Real st
( r < g & g in dom (f2 * f1) ) ; :: thesis: ( for r being Real ex g being Real st
( g in (dom f1) /\ (right_open_halfline r) & not f1 . g < lim_in+infty f1 ) or f2 * f1 is divergent_in+infty_to-infty )
given r being Real such that A4: for g being Real st g in (dom f1) /\ (right_open_halfline r) holds
f1 . g < lim_in+infty f1 ; :: thesis: f2 * f1 is divergent_in+infty_to-infty

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
A5: s is divergent_to+infty and
A6: rng s c= dom (f2 * f1) ; :: thesis: (f2 * f1) /* s is divergent_to-infty
consider k being Nat such that
A7: for n being Nat st k <= n holds
r < s . n by A5;
A8: rng (f1 /* s) c= dom f2 by A6, Lm2;
set q = s ^\ k;
A9: s ^\ k is divergent_to+infty by A5, LIMFUNC1:26;
A10: rng s c= dom f1 by A6, Lm2;
A11: rng (s ^\ k) c= rng s by VALUED_0:21;
A12: rng (f1 /* (s ^\ k)) c= (dom f2) /\ (left_open_halfline (lim_in+infty f1))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (f1 /* (s ^\ k)) or x in (dom f2) /\ (left_open_halfline (lim_in+infty f1)) )
assume x in rng (f1 /* (s ^\ k)) ; :: thesis: x in (dom f2) /\ (left_open_halfline (lim_in+infty f1))
then consider n being Element of NAT such that
A13: (f1 /* (s ^\ k)) . n = x by FUNCT_2:113;
A14: x = f1 . ((s ^\ k) . n) by A10, A11, A13, FUNCT_2:108, XBOOLE_1:1
.= f1 . (s . (n + k)) by NAT_1:def 3 ;
r < s . (n + k) by A7, NAT_1:12;
then s . (n + k) in { r2 where r2 is Real : r < r2 } ;
then A15: s . (n + k) in right_open_halfline r by XXREAL_1:230;
s . (n + k) in rng s by VALUED_0:28;
then s . (n + k) in (dom f1) /\ (right_open_halfline r) by A10, A15, XBOOLE_0:def 4;
then f1 . (s . (n + k)) < lim_in+infty f1 by A4;
then x in { g1 where g1 is Real : g1 < lim_in+infty f1 } by A14;
then A16: x in left_open_halfline (lim_in+infty f1) by XXREAL_1:229;
A17: n + k in NAT by ORDINAL1:def 12;
(f1 /* s) . (n + k) in rng (f1 /* s) by VALUED_0:28;
then (f1 /* s) . (n + k) in dom f2 by A8;
then x in dom f2 by A10, A14, FUNCT_2:108, A17;
hence x in (dom f2) /\ (left_open_halfline (lim_in+infty f1)) by A16, XBOOLE_0:def 4; :: thesis: verum

end;

rng (s ^\ k) c= dom f1 by A10, A11;
then ( f1 /* (s ^\ k) is convergent & lim (f1 /* (s ^\ k)) = lim_in+infty f1 ) by A1, A9, LIMFUNC1:def 12;
then A18: f2 /* (f1 /* (s ^\ k)) is divergent_to-infty by A2, A12, LIMFUNC2:def 3;
f2 /* (f1 /* (s ^\ k)) = f2 /* ((f1 /* s) ^\ k) by A10, VALUED_0:27
.= (f2 /* (f1 /* s)) ^\ k by A8, VALUED_0:27
.= ((f2 * f1) /* s) ^\ k by A6, VALUED_0:31 ;
hence (f2 * f1) /* s is divergent_to-infty by A18, LIMFUNC1:7; :: thesis: verum

end;

hence f2 * f1 is divergent_in+infty_to-infty by A3; :: thesis: verum