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

A4: 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 A5: ( s is divergent_to-infty & rng s c= dom (f1 (#) f2) ) ; :: thesis: ( (f1 (#) f2) /* s is convergent & lim ((f1 (#) f2) /* s) = 0 )
then A6: ( dom (f1 (#) f2) = (dom f1) /\ (dom f2) & rng s c= dom f1 & rng s c= dom f2 ) by Lm3;
consider k being Element of NAT such that
A7: for n being Element of NAT st k <= n holds
s . n < r by A5, Def5;
A8: s ^\ k is divergent_to-infty by A5, Th54;
A9: rng (s ^\ k) c= rng s by VALUED_0:21;
then A10: ( rng (s ^\ k) c= (dom f1) /\ (dom f2) & rng (s ^\ k) c= dom f1 & rng (s ^\ k) c= dom f2 ) by A5, A6, XBOOLE_1:1;
then A11: ( f1 /* (s ^\ k) is convergent & lim (f1 /* (s ^\ k)) = 0 ) by A1, A8, Def13;

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
A12: (s ^\ k) . n in rng (s ^\ k) by VALUED_0:28;
s . (n + k) < r by A7, 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 left_open_halfline r by XXREAL_1:229;
then (s ^\ k) . n in (left_open_halfline r) /\ (dom f2) by A10, A12, XBOOLE_0:def 4;
then abs (f2 . ((s ^\ k) . n)) <= g by A3;
then A13: abs ((f2 /* (s ^\ k)) . n) <= g by A6, 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 A13, XXREAL_0:2; :: thesis: verum

end;

then A14: f2 /* (s ^\ k) is bounded by SEQ_2:15;
then A15: (f1 /* (s ^\ k)) (#) (f2 /* (s ^\ k)) is convergent by A11, SEQ_2:39;
A16: lim ((f1 /* (s ^\ k)) (#) (f2 /* (s ^\ k))) = 0 by A11, A14, SEQ_2:40;
A17: (f1 /* (s ^\ k)) (#) (f2 /* (s ^\ k)) = (f1 (#) f2) /* (s ^\ k) by A10, RFUNCT_2:23
.= ((f1 (#) f2) /* s) ^\ k by A5, VALUED_0:27 ;
hence (f1 (#) f2) /* s is convergent by A15, SEQ_4:35; :: thesis: lim ((f1 (#) f2) /* s) = 0
thus lim ((f1 (#) f2) /* s) = 0 by A15, A16, A17, SEQ_4:36; :: thesis: verum

end;

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