let f1, f2 be PartFunc of REAL , REAL ; :: thesis: ( f1 is convergent_in-infty & f2 is_right_convergent_in lim_in-infty f1 & ( for r being Real ex g being Real st
( g < r & g in dom (f2 * f1) ) ) & ex r being Real st
for g being Real st g in (dom f1) /\ (left_open_halfline r) holds
lim_in-infty f1 < f1 . g implies ( f2 * f1 is convergent_in-infty & lim_in-infty (f2 * f1) = lim_right f2,(lim_in-infty f1) ) )
assume A1: ( f1 is convergent_in-infty & f2 is_right_convergent_in lim_in-infty f1 & ( for r being Real ex g being Real st
( g < r & g in dom (f2 * f1) ) ) ) ; :: thesis: ( for r being Real ex g being Real st
( g in (dom f1) /\ (left_open_halfline r) & not lim_in-infty f1 < f1 . g ) or ( f2 * f1 is convergent_in-infty & lim_in-infty (f2 * f1) = lim_right f2,(lim_in-infty f1) ) )
given r being Real such that A2: for g being Real st g in (dom f1) /\ (left_open_halfline r) holds
lim_in-infty f1 < f1 . g ; :: thesis: ( f2 * f1 is convergent_in-infty & lim_in-infty (f2 * f1) = lim_right f2,(lim_in-infty f1) )

A3: now

let s be Real_Sequence; :: thesis: ( s is divergent_to-infty & rng s c= dom (f2 * f1) implies ( (f2 * f1) /* s is convergent & lim ((f2 * f1) /* s) = lim_right f2,(lim_in-infty f1) ) )
assume A4: ( s is divergent_to-infty & rng s c= dom (f2 * f1) ) ; :: thesis: ( (f2 * f1) /* s is convergent & lim ((f2 * f1) /* s) = lim_right f2,(lim_in-infty f1) )
then consider k being Element of NAT such that
A5: for n being Element of NAT st k <= n holds
s . n < r by LIMFUNC1:def 5;
set q = s ^\ k;
A6: s ^\ k is divergent_to-infty by A4, LIMFUNC1:54;
A7: ( rng s c= dom f1 & rng (f1 /* s) c= dom f2 ) by A4, Lm2;
A8: rng (s ^\ k) c= rng s by VALUED_0:21;
then rng (s ^\ k) c= dom f1 by A7, XBOOLE_1:1;
then A9: ( f1 /* (s ^\ k) is convergent & lim (f1 /* (s ^\ k)) = lim_in-infty f1 ) by A1, A6, LIMFUNC1:def 13;
set L = lim_right f2,(lim_in-infty f1);
A10: lim_right f2,(lim_in-infty f1) = lim_right f2,(lim_in-infty f1) ;
rng (f1 /* (s ^\ k)) c= (dom f2) /\ (right_open_halfline (lim_in-infty f1))

proof

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

end;

then A15: ( f2 /* (f1 /* (s ^\ k)) is convergent & lim (f2 /* (f1 /* (s ^\ k))) = lim_right f2,(lim_in-infty f1) ) by A1, A9, A10, LIMFUNC2:def 8;
A16: f2 /* (f1 /* (s ^\ k)) = f2 /* ((f1 /* s) ^\ k) by A7, VALUED_0:27
.= (f2 /* (f1 /* s)) ^\ k by A7, VALUED_0:27
.= ((f2 * f1) /* s) ^\ k by A4, VALUED_0:31 ;
hence (f2 * f1) /* s is convergent by A15, SEQ_4:35; :: thesis: lim ((f2 * f1) /* s) = lim_right f2,(lim_in-infty f1)
thus lim ((f2 * f1) /* s) = lim_right f2,(lim_in-infty f1) by A15, A16, SEQ_4:36; :: thesis: verum

end;

hence f2 * f1 is convergent_in-infty by A1, LIMFUNC1:def 9; :: thesis: lim_in-infty (f2 * f1) = lim_right f2,(lim_in-infty f1)
hence lim_in-infty (f2 * f1) = lim_right f2,(lim_in-infty f1) by A3, LIMFUNC1:def 13; :: thesis: verum