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

A7: now :: thesis: for s being Real_Sequence st s is convergent & lim s = x0 & rng s c= (dom (f1 (#) f2)) /\ (left_open_halfline x0) holds
( (f1 (#) f2) /* s is convergent & lim ((f1 (#) f2) /* s) = 0 )

set L = left_open_halfline x0;
let s be Real_Sequence; :: thesis: ( s is convergent & lim s = x0 & rng s c= (dom (f1 (#) f2)) /\ (left_open_halfline x0) implies ( (f1 (#) f2) /* s is convergent & lim ((f1 (#) f2) /* s) = 0 ) )
assume that
A8: s is convergent and
A9: lim s = x0 and
A10: rng s c= (dom (f1 (#) f2)) /\ (left_open_halfline x0) ; :: thesis: ( (f1 (#) f2) /* s is convergent & lim ((f1 (#) f2) /* s) = 0 )
x0 - r < x0 by A4, Lm1;
then consider k being Nat such that
A11: for n being Nat st k <= n holds
x0 - r < s . n by A8, A9, Th1;
A12: rng (s ^\ k) c= rng s by VALUED_0:21;
A13: rng s c= dom (f1 (#) f2) by A10, Lm2;
dom (f1 (#) f2) = (dom f1) /\ (dom f2) by A10, Lm2;
then rng (s ^\ k) c= (dom f1) /\ (dom f2) by A13, A12, XBOOLE_1:1;
then A14: (f1 /* (s ^\ k)) (#) (f2 /* (s ^\ k)) = (f1 (#) f2) /* (s ^\ k) by RFUNCT_2:8
.= ((f1 (#) f2) /* s) ^\ k by A13, VALUED_0:27 ;
rng s c= (dom f1) /\ (left_open_halfline x0) by A10, Lm2;
then A15: rng (s ^\ k) c= (dom f1) /\ (left_open_halfline x0) by A12, XBOOLE_1:1;
A16: lim (s ^\ k) = x0 by A8, A9, SEQ_4:20;
then A17: f1 /* (s ^\ k) is convergent by A1, A8, A15;
rng s c= left_open_halfline x0 by A10, Lm2;
then A18: rng (s ^\ k) c= left_open_halfline x0 by A12, XBOOLE_1:1;
A19: rng s c= dom f2 by A10, Lm2;
then A20: rng (s ^\ k) c= dom f2 by A12, XBOOLE_1:1;

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
A21: n in NAT by ORDINAL1:def 12;
x0 - r < s . (n + k) by A11, NAT_1:12;
then A22: x0 - r < (s ^\ k) . n by NAT_1:def 3;
A23: (s ^\ k) . n in rng (s ^\ k) by VALUED_0:28;
then (s ^\ k) . n in left_open_halfline x0 by A18;
then (s ^\ k) . n in { g1 where g1 is Real : g1 < x0 } by XXREAL_1:229;
then ex g1 being Real st
( g1 = (s ^\ k) . n & g1 < x0 ) ;
then (s ^\ k) . n in { g2 where g2 is Real : ( x0 - r < g2 & g2 < x0 ) } by A22;
then (s ^\ k) . n in ].(x0 - r),x0.[ by RCOMP_1:def 2;
then (s ^\ k) . n in ].(x0 - r),x0.[ /\ (dom f2) by A20, A23, XBOOLE_0:def 4;
then |.(f2 . ((s ^\ k) . n)).| <= g by A6;
then A24: |.((f2 /* (s ^\ k)) . n).| <= g by A19, A12, FUNCT_2:108, XBOOLE_1:1, A21;
g <= |.g.| by ABSVALUE:4;
then g < |.g.| + 1 by Lm1;
hence |.((f2 /* (s ^\ k)) . n).| < |.g.| + 1 by A24, XXREAL_0:2; :: thesis: verum

end;

then A25: f2 /* (s ^\ k) is bounded by SEQ_2:3;
A26: lim (f1 /* (s ^\ k)) = 0 by A1, A2, A8, A16, A15, Def7;
then A27: (f1 /* (s ^\ k)) (#) (f2 /* (s ^\ k)) is convergent by A17, A25, SEQ_2:25;
hence (f1 (#) f2) /* s is convergent by A14, SEQ_4:21; :: thesis: lim ((f1 (#) f2) /* s) = 0
lim ((f1 /* (s ^\ k)) (#) (f2 /* (s ^\ k))) = 0 by A17, A26, A25, SEQ_2:26;
hence lim ((f1 (#) f2) /* s) = 0 by A27, A14, SEQ_4:22; :: thesis: verum

end;

hence f1 (#) f2 is_left_convergent_in x0 by A3; :: thesis: lim_left ((f1 (#) f2),x0) = 0
hence lim_left ((f1 (#) f2),x0) = 0 by A7, Def7; :: thesis: verum