let x0 be Real; :: thesis:
let f1, f2 be PartFunc of REAL,REAL; :: thesis:
assume that
A1: f1 is_convergent_in x0 and
A2: f2 is_convergent_in lim (f1,x0) and
A3: 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:
given g being Real such that A4: 0 < g and
A5: for r being Real st r in (dom f1) /\ (].(x0 - g),x0.[ \/ ].x0,(x0 + g).[) holds
f1 . r <> lim (f1,x0) ; :: thesis:

let s be Real_Sequence; :: thesis:
assume that
A7: ( s is convergent & lim s = x0 ) and
A8: rng s c= (dom (f2 * f1)) \ {x0} ; :: thesis:
consider k being Element of NAT such that
A9: for n being Element of NAT st k <= n holds
( x0 - g < s . n & s . n < x0 + g ) by A4, A7, LIMFUNC3:7;
set q = (f1 /* s) ^\ k;
A10: rng s c= dom (f2 * f1) by A8, Th2;
A11: rng s c= dom f1 by A8, Th2;

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

end;

then A17: rng ((f1 /* s) ^\ k) c= (dom f2) \ {(lim (f1,x0))} ;
rng (f1 /* s) c= dom f2 by A8, Th2;
then A18: f2 /* ((f1 /* s) ^\ k) = (f2 /* (f1 /* s)) ^\ k by VALUED_0:27
.= ((f2 * f1) /* s) ^\ k by A10, VALUED_0:31 ;
A19: rng s c= (dom f1) \ {x0} by A8, Th2;
then A20: f1 /* s is convergent by A1, A2, A7, LIMFUNC3:def 4;
lim (f1 /* s) = lim (f1,x0) by A1, A7, A19, LIMFUNC3:def 4;
then A21: lim ((f1 /* s) ^\ k) = lim (f1,x0) by A20, SEQ_4:20;
lim (f2,(lim (f1,x0))) = lim (f2,(lim (f1,x0))) ;
then A22: f2 /* ((f1 /* s) ^\ k) is convergent by A2, A20, A21, A17, LIMFUNC3:def 4;
hence (f2 * f1) /* s is convergent by A18, SEQ_4:21; :: thesis:
lim (f2 /* ((f1 /* s) ^\ k)) = lim (f2,(lim (f1,x0))) by A2, A20, A21, A17, LIMFUNC3:def 4;
hence lim ((f2 * f1) /* s) = lim (f2,(lim (f1,x0))) by A22, A18, SEQ_4:22; :: thesis:

end;