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 number such that
A4: for r1 being set st r1 in (left_open_halfline r) /\ (dom f2) holds
abs (f2 . r1) <= g by A3, RFUNCT_1:90;

A5: now

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 Element of NAT such that
A8: for n being Element of NAT st k <= n holds
s . n < r by A6, Def5;
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, XBOOLE_1:1;

now

set t = (abs g) + 1;
0 <= abs g by COMPLEX1:132;
hence 0 < (abs g) + 1 ; :: thesis: for n being Element of NAT holds abs ((f2 /* (s ^\ k)) . n) < (abs g) + 1
let n be Element of NAT ; :: thesis: abs ((f2 /* (s ^\ k)) . n) < (abs g) + 1
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 abs (f2 . ((s ^\ k) . n)) <= g by A4;
then A12: abs ((f2 /* (s ^\ k)) . n) <= g by A10, A9, FUNCT_2:185, XBOOLE_1:1;
g <= abs g by ABSVALUE:11;
then g < (abs g) + 1 by Lm1;
hence abs ((f2 /* (s ^\ k)) . n) < (abs g) + 1 by A12, XXREAL_0:2; :: thesis: verum

end;

then A13: f2 /* (s ^\ k) is bounded by SEQ_2:15;
dom (f1 (#) f2) = (dom f1) /\ (dom f2) by A7, Lm3;
then rng (s ^\ k) c= (dom f1) /\ (dom f2) by A7, A9, XBOOLE_1:1;
then A14: (f1 /* (s ^\ k)) (#) (f2 /* (s ^\ k)) = (f1 (#) f2) /* (s ^\ k) by RFUNCT_2:23
.= ((f1 (#) f2) /* s) ^\ k by A7, VALUED_0:27 ;
rng s c= dom f1 by A7, Lm3;
then A15: rng (s ^\ k) c= dom f1 by A9, XBOOLE_1:1;
s ^\ k is divergent_to-infty by A6, Th54;
then A16: ( f1 /* (s ^\ k) is convergent & lim (f1 /* (s ^\ k)) = 0 ) by A1, A15, Def13;
then A17: (f1 /* (s ^\ k)) (#) (f2 /* (s ^\ k)) is convergent by A13, SEQ_2:39;
hence (f1 (#) f2) /* s is convergent by A14, SEQ_4:35; :: thesis: lim ((f1 (#) f2) /* s) = 0
lim ((f1 /* (s ^\ k)) (#) (f2 /* (s ^\ k))) = 0 by A16, A13, SEQ_2:40;
hence lim ((f1 (#) f2) /* s) = 0 by A17, A14, SEQ_4:36; :: thesis: verum

end;

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