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: f2 is_convergent_in lim_left (f1,x0) and
A3: for r being Real st r < x0 holds
ex g being Real st
( r < g & g < x0 & g in dom (f2 * f1) ) ; :: thesis:
given g being Real such that A4: 0 < g and
A5: for r being Real st r in (dom f1) /\ ].(x0 - g),x0.[ holds
f1 . r <> lim_left (f1,x0) ; :: thesis:

let x be object ; :: thesis:
assume x in rng ((f1 /* s) ^\ k) ; :: thesis:
then consider n being Element of NAT such that
A13: ((f1 /* s) ^\ k) . n = x by FUNCT_2:113;
A14: n + k in NAT by ORDINAL1:def 12;
A15: f1 . (s . (n + k)) = (f1 /* s) . (n + k) by A10, FUNCT_2:108, A14
.= x by A13, NAT_1:def 3 ;
A16: x0 - g < s . (n + k) by A9, NAT_1:12;
A17: s . (n + k) in rng s by VALUED_0:28;
then s . (n + k) in left_open_halfline x0 by A12;
then s . (n + k) in { g1 where g1 is Real : g1 < x0 } by XXREAL_1:229;
then ex g1 being Real st
( g1 = s . (n + k) & g1 < x0 ) ;
then s . (n + k) in { g2 where g2 is Real : ( x0 - g < g2 & g2 < x0 ) } by A16;
then s . (n + k) in ].(x0 - g),x0.[ by RCOMP_1:def 2;
then s . (n + k) in (dom f1) /\ ].(x0 - g),x0.[ by A10, A17, XBOOLE_0:def 4;
then f1 . (s . (n + k)) <> lim_left (f1,x0) by A5;
then A18: not f1 . (s . (n + k)) in {(lim_left (f1,x0))} by TARSKI:def 1;
f1 . (s . (n + k)) in dom f2 by A11, A17, FUNCT_1:11;
hence x in (dom f2) \ {(lim_left (f1,x0))} by A18, A15, XBOOLE_0:def 5; :: thesis:

end;

end;