let f1, f2 be PartFunc of REAL,REAL; :: thesis: ( f1 is convergent_in-infty & lim_in-infty f1 = 0 & ( for r being Real ex g being Real st
( g < r & g in dom (f1 (#) f2) ) ) & ex r being Real st f2 | (left_open_halfline r) is bounded implies ( f1 (#) f2 is convergent_in-infty & lim_in-infty (f1 (#) f2) = 0 ) )
assume that
A1: ( f1 is convergent_in-infty & lim_in-infty f1 = 0 ) and
A2: for r being Real ex g being Real st
( g < r & g in dom (f1 (#) f2) ) ; :: thesis: ( for r being Real holds not f2 | (left_open_halfline r) is bounded or ( f1 (#) f2 is convergent_in-infty & lim_in-infty (f1 (#) f2) = 0 ) )
given r being Real such that A3: f2 | (left_open_halfline r) is bounded ; :: thesis: ( f1 (#) f2 is convergent_in-infty & lim_in-infty (f1 (#) f2) = 0 )
consider g being Real such that
A4: for r1 being object st r1 in (left_open_halfline r) /\ (dom f2) holds
|.(f2 . r1).| <= g by A3, RFUNCT_1:73;

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

let s be Real_Sequence; :: thesis: ( s is divergent_to-infty & rng s c= dom (f1 (#) f2) implies ( (f1 (#) f2) /* s is convergent & lim ((f1 (#) f2) /* s) = 0 ) )
assume that
A6: s is divergent_to-infty and
A7: rng s c= dom (f1 (#) f2) ; :: thesis: ( (f1 (#) f2) /* s is convergent & lim ((f1 (#) f2) /* s) = 0 )
consider k being Nat such that
A8: for n being Nat st k <= n holds
s . n < r by A6;
A9: rng (s ^\ k) c= rng s by VALUED_0:21;
A10: rng s c= dom f2 by A7, Lm3;
then A11: rng (s ^\ k) c= dom f2 by A9;

now :: thesis: ( 0 < |.g.| + 1 & ( for n being Nat holds |.((f2 /* (s ^\ k)) . n).| < |.g.| + 1 ) )

set t = |.g.| + 1;
0 <= |.g.| by COMPLEX1:46;
hence 0 < |.g.| + 1 ; :: thesis: for n being Nat holds |.((f2 /* (s ^\ k)) . n).| < |.g.| + 1
let n be Nat; :: thesis: |.((f2 /* (s ^\ k)) . n).| < |.g.| + 1
A12: n in NAT by ORDINAL1:def 12;
s . (n + k) < r by A8, NAT_1:12;
then (s ^\ k) . n < r by NAT_1:def 3;
then (s ^\ k) . n in { g1 where g1 is Real : g1 < r } ;
then ( (s ^\ k) . n in rng (s ^\ k) & (s ^\ k) . n in left_open_halfline r ) by VALUED_0:28, XXREAL_1:229;
then (s ^\ k) . n in (left_open_halfline r) /\ (dom f2) by A11, XBOOLE_0:def 4;
then |.(f2 . ((s ^\ k) . n)).| <= g by A4;
then A13: |.((f2 /* (s ^\ k)) . n).| <= g by A10, A9, FUNCT_2:108, XBOOLE_1:1, A12;
g <= |.g.| by ABSVALUE:4;
then g < |.g.| + 1 by Lm1;
hence |.((f2 /* (s ^\ k)) . n).| < |.g.| + 1 by A13, XXREAL_0:2; :: thesis: verum

end;

then A14: f2 /* (s ^\ k) is bounded by SEQ_2:3;
dom (f1 (#) f2) = (dom f1) /\ (dom f2) by A7, Lm3;
then rng (s ^\ k) c= (dom f1) /\ (dom f2) by A7, A9;
then A15: (f1 /* (s ^\ k)) (#) (f2 /* (s ^\ k)) = (f1 (#) f2) /* (s ^\ k) by RFUNCT_2:8
.= ((f1 (#) f2) /* s) ^\ k by A7, VALUED_0:27 ;
rng s c= dom f1 by A7, Lm3;
then A16: rng (s ^\ k) c= dom f1 by A9;
s ^\ k is divergent_to-infty by A6, Th27;
then A17: ( f1 /* (s ^\ k) is convergent & lim (f1 /* (s ^\ k)) = 0 ) by A1, A16, Def13;
then A18: (f1 /* (s ^\ k)) (#) (f2 /* (s ^\ k)) is convergent by A14, SEQ_2:25;
hence (f1 (#) f2) /* s is convergent by A15, SEQ_4:21; :: thesis: lim ((f1 (#) f2) /* s) = 0
lim ((f1 /* (s ^\ k)) (#) (f2 /* (s ^\ k))) = 0 by A17, A14, SEQ_2:26;
hence lim ((f1 (#) f2) /* s) = 0 by A18, A15, SEQ_4:22; :: thesis: verum

end;

hence f1 (#) f2 is convergent_in-infty by A2; :: thesis: lim_in-infty (f1 (#) f2) = 0
hence lim_in-infty (f1 (#) f2) = 0 by A5, Def13; :: thesis: verum