let x0 be Real; :: thesis: for f1, f2 being PartFunc of REAL,REAL st f1 is_right_convergent_in x0 & f2 is_left_convergent_in lim_right (f1,x0) & ( for r being Real st x0 < r holds
ex g being Real st
( g < r & x0 < g & g in dom (f2 * f1) ) ) & ex g being Real st
( 0 < g & ( for r being Real st r in (dom f1) /\ ].x0,(x0 + g).[ holds
f1 . r < lim_right (f1,x0) ) ) holds
( f2 * f1 is_right_convergent_in x0 & lim_right ((f2 * f1),x0) = lim_left (f2,(lim_right (f1,x0))) )
let f1, f2 be PartFunc of REAL,REAL; :: thesis: ( f1 is_right_convergent_in x0 & f2 is_left_convergent_in lim_right (f1,x0) & ( for r being Real st x0 < r holds
ex g being Real st
( g < r & x0 < g & g in dom (f2 * f1) ) ) & ex g being Real st
( 0 < g & ( for r being Real st r in (dom f1) /\ ].x0,(x0 + g).[ holds
f1 . r < lim_right (f1,x0) ) ) implies ( f2 * f1 is_right_convergent_in x0 & lim_right ((f2 * f1),x0) = lim_left (f2,(lim_right (f1,x0))) ) )
assume that
A1: f1 is_right_convergent_in x0 and
A2: f2 is_left_convergent_in lim_right (f1,x0) and
A3: for r being Real st x0 < r holds
ex g being Real st
( g < r & x0 < g & g in dom (f2 * f1) ) ; :: thesis: ( for g being Real holds
( not 0 < g or ex r being Real st
( r in (dom f1) /\ ].x0,(x0 + g).[ & not f1 . r < lim_right (f1,x0) ) ) or ( f2 * f1 is_right_convergent_in x0 & lim_right ((f2 * f1),x0) = lim_left (f2,(lim_right (f1,x0))) ) )
given g being Real such that A4: 0 < g and
A5: for r being Real st r in (dom f1) /\ ].x0,(x0 + g).[ holds
f1 . r < lim_right (f1,x0) ; :: thesis: ( f2 * f1 is_right_convergent_in x0 & lim_right ((f2 * f1),x0) = lim_left (f2,(lim_right (f1,x0))) )

A6: now :: thesis: for s being Real_Sequence st s is convergent & lim s = x0 & rng s c= (dom (f2 * f1)) /\ (right_open_halfline x0) holds
( (f2 * f1) /* s is convergent & lim ((f2 * f1) /* s) = lim_left (f2,(lim_right (f1,x0))) )

let s be Real_Sequence; :: thesis: ( s is convergent & lim s = x0 & rng s c= (dom (f2 * f1)) /\ (right_open_halfline x0) implies ( (f2 * f1) /* s is convergent & lim ((f2 * f1) /* s) = lim_left (f2,(lim_right (f1,x0))) ) )
assume that
A7: ( s is convergent & lim s = x0 ) and
A8: rng s c= (dom (f2 * f1)) /\ (right_open_halfline x0) ; :: thesis: ( (f2 * f1) /* s is convergent & lim ((f2 * f1) /* s) = lim_left (f2,(lim_right (f1,x0))) )
consider k being Nat such that
A9: for n being Nat st k <= n holds
s . n < x0 + g by A4, A7, Lm1, LIMFUNC2:2;
A10: rng s c= dom f1 by A8, Th1;
set q = (f1 /* s) ^\ k;
A11: rng s c= dom (f2 * f1) by A8, Th1;
A12: rng s c= right_open_halfline x0 by A8, Th1;

now :: thesis: for x being object st x in rng ((f1 /* s) ^\ k) holds
x in (dom f2) /\ (left_open_halfline (lim_right (f1,x0)))

let x be object ; :: thesis: ( x in rng ((f1 /* s) ^\ k) implies x in (dom f2) /\ (left_open_halfline (lim_right (f1,x0))) )
assume x in rng ((f1 /* s) ^\ k) ; :: thesis: x in (dom f2) /\ (left_open_halfline (lim_right (f1,x0)))
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: s . (n + k) < x0 + g by A9, NAT_1:12;
A17: s . (n + k) in rng s by VALUED_0:28;
then s . (n + k) in right_open_halfline x0 by A12;
then s . (n + k) in { g1 where g1 is Real : x0 < g1 } by XXREAL_1:230;
then ex g1 being Real st
( g1 = s . (n + k) & x0 < g1 ) ;
then s . (n + k) in { g2 where g2 is Real : ( x0 < g2 & g2 < x0 + g ) } by A16;
then s . (n + k) in ].x0,(x0 + g).[ by RCOMP_1:def 2;
then s . (n + k) in (dom f1) /\ ].x0,(x0 + g).[ by A10, A17, XBOOLE_0:def 4;
then f1 . (s . (n + k)) < lim_right (f1,x0) by A5;
then f1 . (s . (n + k)) in { r1 where r1 is Real : r1 < lim_right (f1,x0) } ;
then A18: f1 . (s . (n + k)) in left_open_halfline (lim_right (f1,x0)) by XXREAL_1:229;
f1 . (s . (n + k)) in dom f2 by A11, A17, FUNCT_1:11;
hence x in (dom f2) /\ (left_open_halfline (lim_right (f1,x0))) by A18, A15, XBOOLE_0:def 4; :: thesis: verum

end;

then A19: rng ((f1 /* s) ^\ k) c= (dom f2) /\ (left_open_halfline (lim_right (f1,x0))) ;
rng (f1 /* s) c= dom f2 by A8, Th1;
then A20: f2 /* ((f1 /* s) ^\ k) = (f2 /* (f1 /* s)) ^\ k by VALUED_0:27
.= ((f2 * f1) /* s) ^\ k by A11, VALUED_0:31 ;
A21: rng s c= (dom f1) /\ (right_open_halfline x0) by A8, Th1;
then A22: f1 /* s is convergent by A1, A2, A7, LIMFUNC2:def 8;
lim (f1 /* s) = lim_right (f1,x0) by A1, A7, A21, LIMFUNC2:def 8;
then A23: lim ((f1 /* s) ^\ k) = lim_right (f1,x0) by A22, SEQ_4:20;
lim_left (f2,(lim_right (f1,x0))) = lim_left (f2,(lim_right (f1,x0))) ;
then A24: f2 /* ((f1 /* s) ^\ k) is convergent by A2, A22, A23, A19, LIMFUNC2:def 7;
hence (f2 * f1) /* s is convergent by A20, SEQ_4:21; :: thesis: lim ((f2 * f1) /* s) = lim_left (f2,(lim_right (f1,x0)))
lim (f2 /* ((f1 /* s) ^\ k)) = lim_left (f2,(lim_right (f1,x0))) by A2, A22, A23, A19, LIMFUNC2:def 7;
hence lim ((f2 * f1) /* s) = lim_left (f2,(lim_right (f1,x0))) by A24, A20, SEQ_4:22; :: thesis: verum

end;

hence f2 * f1 is_right_convergent_in x0 by A3, LIMFUNC2:def 4; :: thesis: lim_right ((f2 * f1),x0) = lim_left (f2,(lim_right (f1,x0)))
hence lim_right ((f2 * f1),x0) = lim_left (f2,(lim_right (f1,x0))) by A6, LIMFUNC2:def 8; :: thesis: verum