let x0 be Real; :: thesis:
let f1, f2 be PartFunc of REAL,REAL; :: thesis:
assume that
A1: f1 is_convergent_in x0 and
A2: lim (f1,x0) = 0 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 (f1 (#) f2) & g2 < r2 & x0 < g2 & g2 in dom (f1 (#) f2) ) ; :: thesis:
given r being Real such that A4: 0 < r and
A5: f2 | (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) is bounded ; :: thesis:
consider g being Real such that
A6: for r1 being object st r1 in (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) /\ (dom f2) holds
|.(f2 . r1).| <= g by A5, RFUNCT_1:73;

A7: now :: thesis:

let s be Real_Sequence; :: thesis:
assume that
A8: s is convergent and
A9: lim s = x0 and
A10: rng s c= (dom (f1 (#) f2)) \ {x0} ; :: thesis:
consider k being Element of NAT such that
A11: for n being Element of NAT st k <= n holds
( x0 - r < s . n & s . n < x0 + r ) by A4, A8, A9, Th7;
A12: rng (s ^\ k) c= rng s by VALUED_0:21;
rng s c= (dom f1) \ {x0} by A10, Lm2;
then A13: rng (s ^\ k) c= (dom f1) \ {x0} by A12;
A14: lim (s ^\ k) = x0 by A8, A9, SEQ_4:20;
then A15: f1 /* (s ^\ k) is convergent by A1, A8, A13;
A16: rng s c= dom f2 by A10, Lm2;
then A17: rng (s ^\ k) c= dom f2 by A12;

set t = |.g.| + 1;
0 <= |.g.| by COMPLEX1:46;
hence 0 < |.g.| + 1 ; :: thesis:
let n be Nat; :: thesis:
A18: n in NAT by ORDINAL1:def 12;
A19: k <= n + k by NAT_1:12;
then s . (n + k) < x0 + r by A11;
then A20: (s ^\ k) . n < x0 + r by NAT_1:def 3;
x0 - r < s . (n + k) by A11, A19;
then x0 - r < (s ^\ k) . n by NAT_1:def 3;
then (s ^\ k) . n in { g1 where g1 is Real : ( x0 - r < g1 & g1 < x0 + r ) } by A20;
then A21: (s ^\ k) . n in ].(x0 - r),(x0 + r).[ by RCOMP_1:def 2;
A22: (s ^\ k) . n in rng (s ^\ k) by VALUED_0:28;
then not (s ^\ k) . n in {x0} by A13, XBOOLE_0:def 5;
then (s ^\ k) . n in ].(x0 - r),(x0 + r).[ \ {x0} by A21, XBOOLE_0:def 5;
then (s ^\ k) . n in ].(x0 - r),x0.[ \/ ].x0,(x0 + r).[ by A4, Th4;
then (s ^\ k) . n in (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) /\ (dom f2) by A17, A22, XBOOLE_0:def 4;
then |.(f2 . ((s ^\ k) . n)).| <= g by A6;
then A23: |.((f2 /* (s ^\ k)) . n).| <= g by A16, A12, FUNCT_2:108, XBOOLE_1:1, A18;
g <= |.g.| by ABSVALUE:4;
then g < |.g.| + 1 by Lm1;
hence |.((f2 /* (s ^\ k)) . n).| < |.g.| + 1 by A23, XXREAL_0:2; :: thesis:

end;

then A24: f2 /* (s ^\ k) is bounded by SEQ_2:3;
A25: rng s c= dom (f1 (#) f2) by A10, Lm2;
dom (f1 (#) f2) = (dom f1) /\ (dom f2) by A10, Lm2;
then rng (s ^\ k) c= (dom f1) /\ (dom f2) by A25, A12;
then A26: (f1 /* (s ^\ k)) (#) (f2 /* (s ^\ k)) = (f1 (#) f2) /* (s ^\ k) by RFUNCT_2:8
.= ((f1 (#) f2) /* s) ^\ k by A25, VALUED_0:27 ;
A27: lim (f1 /* (s ^\ k)) = 0 by A1, A2, A8, A14, A13, Def4;
then A28: (f1 /* (s ^\ k)) (#) (f2 /* (s ^\ k)) is convergent by A15, A24, SEQ_2:25;
hence (f1 (#) f2) /* s is convergent by A26, SEQ_4:21; :: thesis:
lim ((f1 /* (s ^\ k)) (#) (f2 /* (s ^\ k))) = 0 by A15, A27, A24, SEQ_2:26;
hence lim ((f1 (#) f2) /* s) = 0 by A28, A26, SEQ_4:22; :: thesis:

end;

hence f1 (#) f2 is_convergent_in x0 by A3; :: thesis:
hence lim ((f1 (#) f2),x0) = 0 by A7, Def4; :: thesis: