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

set t = (abs g) + 1;
0 <= abs g by COMPLEX1:46;
hence 0 < (abs g) + 1 ; :: thesis:
let n be Element of NAT ; :: thesis:
x0 - r < s . (n + k) by A11, NAT_1:12;
then A21: x0 - r < (s ^\ k) . n by NAT_1:def 3;
A22: (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 A21;
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, A22, XBOOLE_0:def 4;
then abs (f2 . ((s ^\ k) . n)) <= g by A6;
then A23: abs ((f2 /* (s ^\ k)) . n) <= g by A19, A12, FUNCT_2:108, XBOOLE_1:1;
g <= abs g by ABSVALUE:4;
then g < (abs g) + 1 by Lm1;
hence abs ((f2 /* (s ^\ k)) . n) < (abs g) + 1 by A23, XXREAL_0:2; :: thesis:

end;

end;