let x0 be Real; :: thesis: for f1, f2 being PartFunc of REAL ,REAL st f1 is_convergent_in x0 & f2 is_left_convergent_in lim f1,x0 & ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom (f2 * f1) & g2 < r2 & x0 < g2 & g2 in dom (f2 * f1) ) ) & ex g being Real st
( 0 < g & ( for r being Real st r in (dom f1) /\ (].(x0 - g),x0.[ \/ ].x0,(x0 + g).[) holds
f1 . r < lim f1,x0 ) ) holds
( f2 * f1 is_convergent_in x0 & lim (f2 * f1),x0 = lim_left f2,(lim f1,x0) )
let f1, f2 be PartFunc of REAL ,REAL ; :: thesis: ( f1 is_convergent_in x0 & f2 is_left_convergent_in lim f1,x0 & ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom (f2 * f1) & g2 < r2 & x0 < g2 & g2 in dom (f2 * f1) ) ) & ex g being Real st
( 0 < g & ( for r being Real st r in (dom f1) /\ (].(x0 - g),x0.[ \/ ].x0,(x0 + g).[) holds
f1 . r < lim f1,x0 ) ) implies ( f2 * f1 is_convergent_in x0 & lim (f2 * f1),x0 = lim_left f2,(lim f1,x0) ) )
assume A1: ( f1 is_convergent_in x0 & f2 is_left_convergent_in lim f1,x0 & ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom (f2 * f1) & g2 < r2 & x0 < g2 & g2 in dom (f2 * f1) ) ) ) ; :: thesis: ( for g being Real holds
( not 0 < g or ex r being Real st
( r in (dom f1) /\ (].(x0 - g),x0.[ \/ ].x0,(x0 + g).[) & not f1 . r < lim f1,x0 ) ) or ( f2 * f1 is_convergent_in x0 & lim (f2 * f1),x0 = lim_left f2,(lim f1,x0) ) )
given g being Real such that A2: ( 0 < g & ( for r being Real st r in (dom f1) /\ (].(x0 - g),x0.[ \/ ].x0,(x0 + g).[) holds
f1 . r < lim f1,x0 ) ) ; :: thesis: ( f2 * f1 is_convergent_in x0 & lim (f2 * f1),x0 = lim_left f2,(lim f1,x0) )

A3: now

let s be Real_Sequence; :: thesis: ( s is convergent & lim s = x0 & rng s c= (dom (f2 * f1)) \ {x0} implies ( (f2 * f1) /* s is convergent & lim ((f2 * f1) /* s) = lim_left f2,(lim f1,x0) ) )
assume A4: ( s is convergent & lim s = x0 & rng s c= (dom (f2 * f1)) \ {x0} ) ; :: thesis: ( (f2 * f1) /* s is convergent & lim ((f2 * f1) /* s) = lim_left f2,(lim f1,x0) )
then A5: ( rng s c= dom (f2 * f1) & rng s c= dom f1 & rng s c= (dom f1) \ {x0} & rng (f1 /* s) c= dom f2 ) by Th2;
then A6: ( f1 /* s is convergent & lim (f1 /* s) = lim f1,x0 ) by A1, A4, LIMFUNC3:def 4;
consider k being Element of NAT such that
A7: for n being Element of NAT st k <= n holds
( x0 - g < s . n & s . n < x0 + g ) by A2, A4, LIMFUNC3:7;
set q = (f1 /* s) ^\ k;
A8: ( (f1 /* s) ^\ k is convergent & lim ((f1 /* s) ^\ k) = lim f1,x0 ) by A6, SEQ_4:33;
A9: lim_left f2,(lim f1,x0) = lim_left f2,(lim f1,x0) ;

now

let x be set ; :: thesis: ( x in rng ((f1 /* s) ^\ k) implies x in (dom f2) /\ (left_open_halfline (lim f1,x0)) )
assume x in rng ((f1 /* s) ^\ k) ; :: thesis: x in (dom f2) /\ (left_open_halfline (lim f1,x0))
then consider n being Element of NAT such that
A10: ((f1 /* s) ^\ k) . n = x by FUNCT_2:190;
k <= n + k by NAT_1:12;
then ( x0 - g < s . (n + k) & s . (n + k) < x0 + g ) by A7;
then s . (n + k) in { g1 where g1 is Real : ( x0 - g < g1 & g1 < x0 + g ) } ;
then A11: s . (n + k) in ].(x0 - g),(x0 + g).[ by RCOMP_1:def 2;
A12: s . (n + k) in rng s by VALUED_0:28;
then ( s . (n + k) in dom f1 & not s . (n + k) in {x0} ) by A5, XBOOLE_0:def 5;
then s . (n + k) in ].(x0 - g),(x0 + g).[ \ {x0} by A11, XBOOLE_0:def 5;
then s . (n + k) in ].(x0 - g),x0.[ \/ ].x0,(x0 + g).[ by A2, LIMFUNC3:4;
then s . (n + k) in (dom f1) /\ (].(x0 - g),x0.[ \/ ].x0,(x0 + g).[) by A5, A12, XBOOLE_0:def 4;
then f1 . (s . (n + k)) < lim f1,x0 by A2;
then f1 . (s . (n + k)) in { g2 where g2 is Real : g2 < lim f1,x0 } ;
then A13: f1 . (s . (n + k)) in left_open_halfline (lim f1,x0) by XXREAL_1:229;
A14: f1 . (s . (n + k)) in dom f2 by A5, A12, FUNCT_1:21;
f1 . (s . (n + k)) = (f1 /* s) . (n + k) by A5, FUNCT_2:185
.= x by A10, NAT_1:def 3 ;
hence x in (dom f2) /\ (left_open_halfline (lim f1,x0)) by A13, A14, XBOOLE_0:def 4; :: thesis: verum

end;

then rng ((f1 /* s) ^\ k) c= (dom f2) /\ (left_open_halfline (lim f1,x0)) by TARSKI:def 3;
then A15: ( f2 /* ((f1 /* s) ^\ k) is convergent & lim (f2 /* ((f1 /* s) ^\ k)) = lim_left f2,(lim f1,x0) ) by A1, A8, A9, LIMFUNC2:def 7;
A16: f2 /* ((f1 /* s) ^\ k) = (f2 /* (f1 /* s)) ^\ k by A5, VALUED_0:27
.= ((f2 * f1) /* s) ^\ k by A5, VALUED_0:31 ;
hence (f2 * f1) /* s is convergent by A15, SEQ_4:35; :: thesis: lim ((f2 * f1) /* s) = lim_left f2,(lim f1,x0)
thus lim ((f2 * f1) /* s) = lim_left f2,(lim f1,x0) by A15, A16, SEQ_4:36; :: thesis: verum

end;

hence f2 * f1 is_convergent_in x0 by A1, LIMFUNC3:def 1; :: thesis: lim (f2 * f1),x0 = lim_left f2,(lim f1,x0)
hence lim (f2 * f1),x0 = lim_left f2,(lim f1,x0) by A3, LIMFUNC3:def 4; :: thesis: verum