let f1, f2 be PartFunc of REAL,REAL; :: thesis: ( f1 is convergent_in-infty & f2 is_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
f1 . g <> lim_in-infty f1 implies ( f2 * f1 is convergent_in-infty & lim_in-infty (f2 * f1) = lim (f2,(lim_in-infty f1)) ) )
assume that
A1: f1 is convergent_in-infty and
A2: f2 is_convergent_in lim_in-infty f1 and
A3: 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 f1 . g <> lim_in-infty f1 ) or ( f2 * f1 is convergent_in-infty & lim_in-infty (f2 * f1) = lim (f2,(lim_in-infty f1)) ) )
given r being Real such that A4: for g being Real st g in (dom f1) /\ (left_open_halfline r) holds
f1 . g <> lim_in-infty f1 ; :: thesis: ( f2 * f1 is convergent_in-infty & lim_in-infty (f2 * f1) = lim (f2,(lim_in-infty f1)) )

A5: now :: thesis: for s being Real_Sequence st s is divergent_to-infty & rng s c= dom (f2 * f1) holds
( (f2 * f1) /* s is convergent & lim ((f2 * f1) /* s) = lim (f2,(lim_in-infty f1)) )

set L = lim (f2,(lim_in-infty f1));
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 (f2,(lim_in-infty f1)) ) )
assume that
A6: s is divergent_to-infty and
A7: rng s c= dom (f2 * f1) ; :: thesis: ( (f2 * f1) /* s is convergent & lim ((f2 * f1) /* s) = lim (f2,(lim_in-infty f1)) )
consider k being Nat such that
A8: for n being Nat st k <= n holds
s . n < r by A6;
set q = s ^\ k;
A9: s ^\ k is divergent_to-infty by A6, LIMFUNC1:27;
A10: rng s c= dom f1 by A7, Lm2;
A11: rng (s ^\ k) c= rng s by VALUED_0:21;
then rng (s ^\ k) c= dom f1 by A10;
then A12: ( f1 /* (s ^\ k) is convergent & lim (f1 /* (s ^\ k)) = lim_in-infty f1 ) by A1, A9, LIMFUNC1:def 13;
A13: rng (f1 /* s) c= dom f2 by A7, Lm2;
A14: rng (f1 /* (s ^\ k)) c= (dom f2) \ {(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) \ {(lim_in-infty f1)} )
assume x in rng (f1 /* (s ^\ k)) ; :: thesis: x in (dom f2) \ {(lim_in-infty f1)}
then consider n being Element of NAT such that
A15: (f1 /* (s ^\ k)) . n = x by FUNCT_2:113;
A16: x = f1 . ((s ^\ k) . n) by A10, A11, A15, FUNCT_2:108, XBOOLE_1:1
.= f1 . (s . (n + k)) by NAT_1:def 3 ;
s . (n + k) < r by A8, NAT_1:12;
then s . (n + k) in { r2 where r2 is Real : r2 < r } ;
then A17: 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 A10, A17, XBOOLE_0:def 4;
then f1 . (s . (n + k)) <> lim_in-infty f1 by A4;
then A18: not f1 . (s . (n + k)) in {(lim_in-infty f1)} by TARSKI:def 1;
A19: 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 A13;
then x in dom f2 by A10, A16, FUNCT_2:108, A19;
hence x in (dom f2) \ {(lim_in-infty f1)} by A16, A18, XBOOLE_0:def 5; :: thesis: verum

end;

A20: f2 /* (f1 /* (s ^\ k)) = f2 /* ((f1 /* s) ^\ k) by A10, VALUED_0:27
.= (f2 /* (f1 /* s)) ^\ k by A13, VALUED_0:27
.= ((f2 * f1) /* s) ^\ k by A7, VALUED_0:31 ;
lim (f2,(lim_in-infty f1)) = lim (f2,(lim_in-infty f1)) ;
then A21: f2 /* (f1 /* (s ^\ k)) is convergent by A2, A12, A14, LIMFUNC3:def 4;
hence (f2 * f1) /* s is convergent by A20, SEQ_4:21; :: thesis: lim ((f2 * f1) /* s) = lim (f2,(lim_in-infty f1))
lim (f2 /* (f1 /* (s ^\ k))) = lim (f2,(lim_in-infty f1)) by A2, A12, A14, LIMFUNC3:def 4;
hence lim ((f2 * f1) /* s) = lim (f2,(lim_in-infty f1)) by A21, A20, SEQ_4:22; :: thesis: verum

end;

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