let x0 be Real; :: thesis:
let f1, f2 be PartFunc of REAL ,REAL ; :: thesis:
assume A1: ( 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) ) ) ) ; :: thesis:
given r being Real such that A2: ( 0 < r & f2 | ].(x0 - r),x0.[ is bounded ) ; :: thesis:
consider g being real number such that
A3: for r1 being set st r1 in ].(x0 - r),x0.[ /\ (dom f2) holds
abs (f2 . r1) <= g by A2, RFUNCT_1:90;

A4: now

let s be Real_Sequence; :: thesis:
assume A5: ( s is convergent & lim s = x0 & rng s c= (dom (f1 (#) f2)) /\ (left_open_halfline x0) ) ; :: thesis:
then A6: ( rng s c= dom (f1 (#) f2) & rng s c= left_open_halfline x0 & dom (f1 (#) f2) = (dom f1) /\ (dom f2) & rng s c= dom f1 & rng s c= dom f2 & rng s c= (dom f1) /\ (left_open_halfline x0) & rng s c= (dom f2) /\ (left_open_halfline x0) ) by Lm2;
x0 - r < x0 by A2, Lm1;
then consider k being Element of NAT such that
A7: for n being Element of NAT st k <= n holds
x0 - r < s . n by A5, Th1;
A8: ( s ^\ k is convergent & lim (s ^\ k) = x0 ) by A5, SEQ_4:33;
set L = left_open_halfline x0;
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 & rng (s ^\ k) c= (dom f1) /\ (left_open_halfline x0) & rng (s ^\ k) c= left_open_halfline x0 & rng (s ^\ k) c= (dom f2) /\ (left_open_halfline x0) ) by A6, XBOOLE_1:1;
then A11: ( f1 /* (s ^\ k) is convergent & lim (f1 /* (s ^\ k)) = 0 ) by A1, A8, Def7;

now

set t = (abs g) + 1;
0 <= abs g by COMPLEX1:132;
hence 0 < (abs g) + 1 ; :: thesis:
let n be Element of NAT ; :: thesis:
A12: (s ^\ k) . n in rng (s ^\ k) by VALUED_0:28;
then A13: ( (s ^\ k) . n in dom f2 & (s ^\ k) . n in left_open_halfline x0 ) by A10;
x0 - r < s . (n + k) by A7, NAT_1:12;
then A14: x0 - r < (s ^\ k) . n by NAT_1:def 3;
(s ^\ k) . n in { g1 where g1 is Real : g1 < x0 } by A13, 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 A14;
then (s ^\ k) . n in ].(x0 - r),x0.[ by RCOMP_1:def 2;
then (s ^\ k) . n in ].(x0 - r),x0.[ /\ (dom f2) by A10, A12, XBOOLE_0:def 4;
then abs (f2 . ((s ^\ k) . n)) <= g by A3;
then A15: 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 A15, XXREAL_0:2; :: thesis:

end;

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

end;

hence f1 (#) f2 is_left_convergent_in x0 by A1, Def1; :: thesis:
hence lim_left (f1 (#) f2),x0 = 0 by A4, Def7; :: thesis: