let f, g be PartFunc of REAL,REAL; :: thesis:
let x0 be Real; :: thesis:
assume A1: x0 in (dom f) /\ (dom g) ; :: thesis:
given r being Real such that A2: r > 0 and
A3: [.(x0 - r),x0.] c= dom f and
A4: [.(x0 - r),x0.] c= dom g and
A5: f is_differentiable_on ].(x0 - r),x0.[ and
A6: g is_differentiable_on ].(x0 - r),x0.[ and
A7: ].(x0 - r),x0.[ c= dom (f / g) and
A8: [.(x0 - r),x0.] c= dom ((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[)) and
A9: ( f . x0 = 0 & g . x0 = 0 ) and
A10: f is_continuous_in x0 and
A11: g is_continuous_in x0 and
A12: (f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[) is_left_convergent_in x0 ; :: thesis:
A13: ].(x0 - r),x0.[ c= [.(x0 - r),x0.] by XXREAL_1:25;
then A14: ].(x0 - r),x0.[ c= dom g by A4;
A15: ].(x0 - r),x0.[ c= dom f by A3, A13;
A16: for x being Real st x0 - r < x & x < x0 holds
ex c being Real st
( c in ].x,x0.[ & (f / g) . x = ((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[)) . c )

proof

let x be Real; :: thesis:
assume that
A17: x0 - r < x and
A18: x < x0 ; :: thesis:
x in { g1 where g1 is Real : ( x0 - r < g1 & g1 < x0 ) } by A17, A18;
then A19: x in ].(x0 - r),x0.[ by RCOMP_1:def 2;
( ].(x0 - r),x0.[ c= dom f & x0 in dom f ) by A1, A3, A13, XBOOLE_0:def 4;
then A20: {x,x0} c= dom f by A19, ZFMISC_1:32;
A21: ].x,x0.[ c= ].(x0 - r),x0.[

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in ].x,x0.[ ; :: thesis:
then y in { g2 where g2 is Real : ( x < g2 & g2 < x0 ) } by RCOMP_1:def 2;
then consider g2 being Real such that
A22: g2 = y and
A23: x < g2 and
A24: g2 < x0 ;
x0 - r < g2 by A17, A23, XXREAL_0:2;
then y in { g3 where g3 is Real : ( x0 - r < g3 & g3 < x0 ) } by A22, A24;
hence y in ].(x0 - r),x0.[ by RCOMP_1:def 2; :: thesis:

end;

then ].x,x0.[ c= dom f by A15;
then ].x,x0.[ \/ {x,x0} c= dom f by A20, XBOOLE_1:8;
then A25: [.x,x0.] c= dom f by A18, XXREAL_1:128;
].(x0 - r),x0.[ c= dom ((f . x) (#) g) by A14, VALUED_1:def 5;
then A26: ].x,x0.[ c= dom ((f . x) (#) g) by A21;
].(x0 - r),x0.[ c= dom ((g . x) (#) f) by A15, VALUED_1:def 5;
then A27: ].x,x0.[ c= dom ((g . x) (#) f) by A21;
then ].x,x0.[ c= (dom ((f . x) (#) g)) /\ (dom ((g . x) (#) f)) by A26, XBOOLE_1:19;
then A28: ].x,x0.[ c= dom (((f . x) (#) g) - ((g . x) (#) f)) by VALUED_1:12;
f is_differentiable_on ].x,x0.[ by A5, A21, FDIFF_1:26;
then A29: (g . x) (#) f is_differentiable_on ].x,x0.[ by A27, FDIFF_1:20;
( ].(x0 - r),x0.[ c= dom g & x0 in dom g ) by A1, A4, A13, XBOOLE_0:def 4;
then A30: {x,x0} c= dom g by A19, ZFMISC_1:32;
set f1 = ((f . x) (#) g) - ((g . x) (#) f);
A31: ( dom ((f . x) (#) g) = dom g & dom ((g . x) (#) f) = dom f ) by VALUED_1:def 5;
then A32: dom (((f . x) (#) g) - ((g . x) (#) f)) = (dom f) /\ (dom g) by VALUED_1:12;
A33: [.x,x0.] c= [.(x0 - r),x0.]

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume A34: y in [.x,x0.] ; :: thesis:
then reconsider y = y as Real ;
x <= y by A34, XXREAL_1:1;
then A35: x0 - r <= y by A17, XXREAL_0:2;
y <= x0 by A34, XXREAL_1:1;
hence y in [.(x0 - r),x0.] by A35, XXREAL_1:1; :: thesis:

end;

then A36: ( [.x,x0.] c= dom f & [.x,x0.] c= dom g ) by A3, A4;
then A37: [.x,x0.] c= dom (((f . x) (#) g) - ((g . x) (#) f)) by A32, XBOOLE_1:19;
A38: x in [.x,x0.] by A18, XXREAL_1:1;
then x in dom (((f . x) (#) g) - ((g . x) (#) f)) by A37;
then A39: x in (dom ((f . x) (#) g)) /\ (dom ((g . x) (#) f)) by VALUED_1:12;
then A40: x in dom ((f . x) (#) g) by XBOOLE_0:def 4;
A41: x0 in [.x,x0.] by A18, XXREAL_1:1;
then x0 in dom (((f . x) (#) g) - ((g . x) (#) f)) by A37;
then A42: x0 in (dom ((f . x) (#) g)) /\ (dom ((g . x) (#) f)) by VALUED_1:12;
then A43: x0 in dom ((f . x) (#) g) by XBOOLE_0:def 4;
A44: x in dom ((g . x) (#) f) by A39, XBOOLE_0:def 4;
A45: (((f . x) (#) g) - ((g . x) (#) f)) . x = (((f . x) (#) g) . x) - (((g . x) (#) f) . x) by A37, A38, VALUED_1:13
.= ((f . x) * (g . x)) - (((g . x) (#) f) . x) by A40, VALUED_1:def 5
.= ((g . x) * (f . x)) - ((g . x) * (f . x)) by A44, VALUED_1:def 5
.= 0 ;
A46: x0 in dom ((g . x) (#) f) by A42, XBOOLE_0:def 4;
not x in {x0} by A18, TARSKI:def 1;
then A47: x in [.x,x0.] \ {x0} by A38, XBOOLE_0:def 5;
].x,x0.[ c= dom g by A14, A21;
then ].x,x0.[ \/ {x,x0} c= dom g by A30, XBOOLE_1:8;
then A48: [.x,x0.] c= dom g by A18, XXREAL_1:128;
g is_differentiable_in x by A6, A19, FDIFF_1:9;
then A49: g is_continuous_in x by FDIFF_1:24;
for s being Real_Sequence st rng s c= [.x,x0.] & s is convergent & lim s in [.x,x0.] holds
( g /* s is convergent & g . (lim s) = lim (g /* s) )

proof

let s be Real_Sequence; :: thesis:
assume that
A50: rng s c= [.x,x0.] and
A51: s is convergent and
A52: lim s in [.x,x0.] ; :: thesis:
set z = lim s;
A53: rng s c= dom g by A48, A50;
A54: lim s in ].x,x0.[ \/ {x,x0} by A18, A52, XXREAL_1:128;

now :: thesis:

per cases by A54, XBOOLE_0:def 3;

suppose lim s in ].x,x0.[ ; :: thesis:

then g is_differentiable_in lim s by A6, A21, FDIFF_1:9;
then g is_continuous_in lim s by FDIFF_1:24;
hence ( g /* s is convergent & g . (lim s) = lim (g /* s) ) by A51, A53, FCONT_1:def 1; :: thesis:

end;

suppose A55: lim s in {x,x0} ; :: thesis:

now :: thesis:

per cases by A55, TARSKI:def 2;

suppose lim s = x0 ; :: thesis:

hence ( g /* s is convergent & g . (lim s) = lim (g /* s) ) by A11, A51, A53, FCONT_1:def 1; :: thesis:

end;

suppose lim s = x ; :: thesis:

hence ( g /* s is convergent & g . (lim s) = lim (g /* s) ) by A49, A51, A53, FCONT_1:def 1; :: thesis:

end;

hence ( g /* s is convergent & g . (lim s) = lim (g /* s) ) ; :: thesis:

end;

hence ( g /* s is convergent & g . (lim s) = lim (g /* s) ) ; :: thesis:

end;

then g | [.x,x0.] is continuous by A48, FCONT_1:13;
then A56: ((f . x) (#) g) | [.x,x0.] is continuous by A4, A33, FCONT_1:20, XBOOLE_1:1;
A57: [.x,x0.] c= dom (((f . x) (#) g) - ((g . x) (#) f)) by A36, A32, XBOOLE_1:19;
f is_differentiable_in x by A5, A19, FDIFF_1:9;
then A58: f is_continuous_in x by FDIFF_1:24;
for s being Real_Sequence st rng s c= [.x,x0.] & s is convergent & lim s in [.x,x0.] holds
( f /* s is convergent & f . (lim s) = lim (f /* s) )

proof

let s be Real_Sequence; :: thesis:
assume that
A59: rng s c= [.x,x0.] and
A60: s is convergent and
A61: lim s in [.x,x0.] ; :: thesis:
set z = lim s;
A62: rng s c= dom f by A25, A59;
A63: lim s in ].x,x0.[ \/ {x,x0} by A18, A61, XXREAL_1:128;

now :: thesis:

per cases by A63, XBOOLE_0:def 3;

suppose lim s in ].x,x0.[ ; :: thesis:

then f is_differentiable_in lim s by A5, A21, FDIFF_1:9;
then f is_continuous_in lim s by FDIFF_1:24;
hence ( f /* s is convergent & f . (lim s) = lim (f /* s) ) by A60, A62, FCONT_1:def 1; :: thesis:

end;

suppose A64: lim s in {x,x0} ; :: thesis:

now :: thesis:

per cases by A64, TARSKI:def 2;

suppose lim s = x0 ; :: thesis:

hence ( f /* s is convergent & f . (lim s) = lim (f /* s) ) by A10, A60, A62, FCONT_1:def 1; :: thesis:

end;

suppose lim s = x ; :: thesis:

hence ( f /* s is convergent & f . (lim s) = lim (f /* s) ) by A58, A60, A62, FCONT_1:def 1; :: thesis:

end;

hence ( f /* s is convergent & f . (lim s) = lim (f /* s) ) ; :: thesis:

end;

hence ( f /* s is convergent & f . (lim s) = lim (f /* s) ) ; :: thesis:

end;

then f | [.x,x0.] is continuous by A25, FCONT_1:13;
then ((g . x) (#) f) | [.x,x0.] is continuous by A3, A33, FCONT_1:20, XBOOLE_1:1;
then A65: (((f . x) (#) g) - ((g . x) (#) f)) | [.x,x0.] is continuous by A31, A32, A57, A56, FCONT_1:18;
g is_differentiable_on ].x,x0.[ by A6, A21, FDIFF_1:26;
then A66: (f . x) (#) g is_differentiable_on ].x,x0.[ by A26, FDIFF_1:20;
(((f . x) (#) g) - ((g . x) (#) f)) . x0 = (((f . x) (#) g) . x0) - (((g . x) (#) f) . x0) by A37, A41, VALUED_1:13
.= ((f . x) * (g . x0)) - (((g . x) (#) f) . x0) by A43, VALUED_1:def 5
.= 0 - ((g . x) * 0) by A9, A46, VALUED_1:def 5
.= 0 ;
then consider t being Real such that
A67: t in ].x,x0.[ and
A68: diff ((((f . x) (#) g) - ((g . x) (#) f)),t) = 0 by A18, A65, A29, A28, A66, A37, A45, FDIFF_1:19, ROLLE:1;
A69: (g . x) (#) f is_differentiable_in t by A29, A67, FDIFF_1:9;
A70: f is_differentiable_in t by A5, A21, A67, FDIFF_1:9;
(f . x) (#) g is_differentiable_in t by A66, A67, FDIFF_1:9;
then 0 = (diff (((f . x) (#) g),t)) - (diff (((g . x) (#) f),t)) by A68, A69, FDIFF_1:14;
then A71: 0 = (diff (((f . x) (#) g),t)) - ((g . x) * (diff (f,t))) by A70, FDIFF_1:15;
A72: (dom (f `| ].(x0 - r),x0.[)) /\ ((dom (g `| ].(x0 - r),x0.[)) \ ((g `| ].(x0 - r),x0.[) " {0})) c= (dom (g `| ].(x0 - r),x0.[)) \ ((g `| ].(x0 - r),x0.[) " {0}) by XBOOLE_1:17;
A73: (dom f) /\ ((dom g) \ (g " {0})) c= (dom g) \ (g " {0}) by XBOOLE_1:17;

now :: thesis:

let y be object ; :: thesis:
assume A74: y in [.x,x0.] \ {x0} ; :: thesis:
then y in [.x,x0.] by XBOOLE_0:def 5;
then y in { g4 where g4 is Real : ( x <= g4 & g4 <= x0 ) } by RCOMP_1:def 1;
then consider g4 being Real such that
A75: g4 = y and
A76: x <= g4 and
A77: g4 <= x0 ;
not y in {x0} by A74, XBOOLE_0:def 5;
then x0 <> g4 by A75, TARSKI:def 1;
then A78: g4 < x0 by A77, XXREAL_0:1;
x0 - r < g4 by A17, A76, XXREAL_0:2;
then y in { g5 where g5 is Real : ( x0 - r < g5 & g5 < x0 ) } by A75, A78;
hence y in ].(x0 - r),x0.[ by RCOMP_1:def 2; :: thesis:

end;

then [.x,x0.] \ {x0} c= ].(x0 - r),x0.[ ;
then A79: [.x,x0.] \ {x0} c= dom (f / g) by A7;
then [.x,x0.] \ {x0} c= (dom f) /\ ((dom g) \ (g " {0})) by RFUNCT_1:def 1;
then [.x,x0.] \ {x0} c= (dom g) \ (g " {0}) by A73;
then A80: ( x in dom g & not x in g " {0} ) by A47, XBOOLE_0:def 5;

A81: now :: thesis:

assume g . x = 0 ; :: thesis:
then g . x in {0} by TARSKI:def 1;
hence contradiction by A80, FUNCT_1:def 7; :: thesis:

end;

take t ; :: thesis:
].x,x0.[ c= [.x,x0.] by XXREAL_1:25;
then A82: t in [.x,x0.] by A67;
x0 - r <= x0 by A2, XREAL_1:44;
then x0 in { g6 where g6 is Real : ( x0 - r <= g6 & g6 <= x0 ) } ;
then ( ].(x0 - r),x0.[ c= [.(x0 - r),x0.] & x0 in [.(x0 - r),x0.] ) by RCOMP_1:def 1, XXREAL_1:25;
then [.x,x0.] c= [.(x0 - r),x0.] by A19, XXREAL_2:def 12;
then A83: [.x,x0.] c= dom ((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[)) by A8;
then [.x,x0.] c= (dom (f `| ].(x0 - r),x0.[)) /\ ((dom (g `| ].(x0 - r),x0.[)) \ ((g `| ].(x0 - r),x0.[) " {0})) by RFUNCT_1:def 1;
then [.x,x0.] c= (dom (g `| ].(x0 - r),x0.[)) \ ((g `| ].(x0 - r),x0.[) " {0}) by A72;
then A84: ( t in dom (g `| ].(x0 - r),x0.[) & not t in (g `| ].(x0 - r),x0.[) " {0} ) by A82, XBOOLE_0:def 5;

A85: now :: thesis:

assume diff (g,t) = 0 ; :: thesis:
then (g `| ].(x0 - r),x0.[) . t = 0 by A6, A21, A67, FDIFF_1:def 7;
then (g `| ].(x0 - r),x0.[) . t in {0} by TARSKI:def 1;
hence contradiction by A84, FUNCT_1:def 7; :: thesis:

end;

g is_differentiable_in t by A6, A21, A67, FDIFF_1:9;
then 0 = ((f . x) * (diff (g,t))) - ((g . x) * (diff (f,t))) by A71, FDIFF_1:15;
then (f . x) / (g . x) = (diff (f,t)) / (diff (g,t)) by A81, A85, XCMPLX_1:94;
then (f . x) * ((g . x) ") = (diff (f,t)) / (diff (g,t)) by XCMPLX_0:def 9;
then (f . x) * ((g . x) ") = (diff (f,t)) * ((diff (g,t)) ") by XCMPLX_0:def 9;
then (f / g) . x = (diff (f,t)) * ((diff (g,t)) ") by A79, A47, RFUNCT_1:def 1;
then (f / g) . x = ((f `| ].(x0 - r),x0.[) . t) * ((diff (g,t)) ") by A5, A21, A67, FDIFF_1:def 7;
then (f / g) . x = ((f `| ].(x0 - r),x0.[) . t) * (((g `| ].(x0 - r),x0.[) . t) ") by A6, A21, A67, FDIFF_1:def 7;
hence ( t in ].x,x0.[ & (f / g) . x = ((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[)) . t ) by A67, A83, A82, RFUNCT_1:def 1; :: thesis:

end;

A86: for a being Real_Sequence st a is convergent & lim a = x0 & rng a c= (dom (f / g)) /\ (left_open_halfline x0) holds
( (f / g) /* a is convergent & lim ((f / g) /* a) = lim_left (((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[)),x0) )

proof

reconsider xx0 = x0 as Element of REAL by XREAL_0:def 1;
set d = seq_const x0;
let a be Real_Sequence; :: thesis:
assume that
A87: a is convergent and
A88: lim a = x0 and
A89: rng a c= (dom (f / g)) /\ (left_open_halfline x0) ; :: thesis:
consider k being Element of NAT such that
A90: for n being Element of NAT st k <= n holds
( x0 - r < a . n & a . n < x0 + r ) by A2, A87, A88, LIMFUNC3:7;
set a1 = a ^\ k;
defpred S₁[ Element of NAT , Real] means ( $2 in ].((a ^\ k) . $1),x0.[ & (((f / g) /* a) ^\ k) . $1 = ((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[)) . $2 );

A91: now :: thesis:

let n be Element of NAT ; :: thesis:
a . (n + k) in rng a by VALUED_0:28;
then a . (n + k) in left_open_halfline x0 by A89, XBOOLE_0:def 4;
then a . (n + k) in { g1 where g1 is Real : g1 < x0 } by XXREAL_1:229;
then ex g1 being Real st
( a . (n + k) = g1 & g1 < x0 ) ;
hence (a ^\ k) . n < x0 by NAT_1:def 3; :: thesis:
( (a ^\ k) . n = a . (n + k) & k <= n + k ) by NAT_1:12, NAT_1:def 3;
hence x0 - r < (a ^\ k) . n by A90; :: thesis:

end;

A92: for n being Element of NAT ex c being Element of REAL st S₁[n,c]

proof

let n be Element of NAT ; :: thesis:
A93: rng (a ^\ k) c= rng a by VALUED_0:21;
( x0 - r < (a ^\ k) . n & (a ^\ k) . n < x0 ) by A91;
then consider c being Real such that
A94: c in ].((a ^\ k) . n),x0.[ and
A95: (f / g) . ((a ^\ k) . n) = ((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[)) . c by A16;
take c ; :: thesis:
A96: (dom (f / g)) /\ (left_open_halfline x0) c= dom (f / g) by XBOOLE_1:17;
then rng a c= dom (f / g) by A89;
then ((f / g) /* (a ^\ k)) . n = ((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[)) . c by A95, A93, FUNCT_2:108, XBOOLE_1:1;
hence ( c is set & c is Element of REAL & S₁[n,c] ) by A89, A94, A96, VALUED_0:27, XBOOLE_1:1; :: thesis:

end;

consider b being Real_Sequence such that
A97: for n being Element of NAT holds S₁[n,b . n] from FUNCT_2:sch 3(A92);
A98: rng b c= (dom ((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[))) /\ (left_open_halfline x0)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in rng b ; :: thesis:
then consider n being Element of NAT such that
A99: x = b . n by FUNCT_2:113;
x0 - r <= x0 by A2, XREAL_1:44;
then x0 in { g3 where g3 is Real : ( x0 - r <= g3 & g3 <= x0 ) } ;
then A100: x0 in [.(x0 - r),x0.] by RCOMP_1:def 1;
( x0 - r < (a ^\ k) . n & (a ^\ k) . n < x0 ) by A91;
then (a ^\ k) . n in { g4 where g4 is Real : ( x0 - r <= g4 & g4 <= x0 ) } ;
then (a ^\ k) . n in [.(x0 - r),x0.] by RCOMP_1:def 1;
then ( ].((a ^\ k) . n),x0.[ c= [.((a ^\ k) . n),x0.] & [.((a ^\ k) . n),x0.] c= [.(x0 - r),x0.] ) by A100, XXREAL_1:25, XXREAL_2:def 12;
then ].((a ^\ k) . n),x0.[ c= [.(x0 - r),x0.] ;
then A101: ].((a ^\ k) . n),x0.[ c= dom ((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[)) by A8;
A102: x in ].((a ^\ k) . n),x0.[ by A97, A99;
then x in { g1 where g1 is Real : ( (a ^\ k) . n < g1 & g1 < x0 ) } by RCOMP_1:def 2;
then ex g1 being Real st
( g1 = x & (a ^\ k) . n < g1 & g1 < x0 ) ;
then x in { g2 where g2 is Real : g2 < x0 } ;
then x in left_open_halfline x0 by XXREAL_1:229;
hence x in (dom ((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[))) /\ (left_open_halfline x0) by A102, A101, XBOOLE_0:def 4; :: thesis:

end;

A103: now :: thesis:

let n be Nat; :: thesis:
A104: n in NAT by ORDINAL1:def 12;
b . n in ].((a ^\ k) . n),x0.[ by A97, A104;
then b . n in { g1 where g1 is Real : ( (a ^\ k) . n < g1 & g1 < x0 ) } by RCOMP_1:def 2;
then ex g1 being Real st
( g1 = b . n & (a ^\ k) . n < g1 & g1 < x0 ) ;
hence ( (a ^\ k) . n <= b . n & b . n <= (seq_const x0) . n ) by SEQ_1:57; :: thesis:

end;

A105: lim (seq_const x0) = (seq_const x0) . 0 by SEQ_4:26
.= x0 by SEQ_1:57 ;
lim (a ^\ k) = x0 by A87, A88, SEQ_4:20;
then A106: ( b is convergent & lim b = x0 ) by A87, A105, A103, SEQ_2:19, SEQ_2:20;
A107: (dom ((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[))) /\ (left_open_halfline x0) c= dom ((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[)) by XBOOLE_1:17;

A108: now :: thesis:

reconsider m = 0 as Nat ;
take m = m; :: thesis:
let n be Nat; :: thesis:
assume m <= n ; :: thesis:
A109: n in NAT by ORDINAL1:def 12;
(((f / g) /* a) ^\ k) . n = ((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[)) . (b . n) by A97, A109;
hence (((f / g) /* a) ^\ k) . n = (((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[)) /* b) . n by A98, A107, FUNCT_2:108, XBOOLE_1:1, A109; :: thesis:

end;

lim_left (((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[)),x0) = lim_left (((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[)),x0) ;
then A110: ((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[)) /* b is convergent by A12, A106, A98, LIMFUNC2:def 7;
then A111: ((f / g) /* a) ^\ k is convergent by A108, SEQ_4:18;
lim (((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[)) /* b) = lim_left (((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[)),x0) by A12, A106, A98, LIMFUNC2:def 7;
then lim (((f / g) /* a) ^\ k) = lim_left (((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[)),x0) by A110, A108, SEQ_4:19;
hence ( (f / g) /* a is convergent & lim ((f / g) /* a) = lim_left (((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[)),x0) ) by A111, SEQ_4:21, SEQ_4:22; :: thesis:

end;

A112: for r1 being Real st r1 < x0 holds
ex t being Real st
( r1 < t & t < x0 & t in dom (f / g) ) by A2, A7, LIMFUNC2:3;
hence f / g is_left_convergent_in x0 by A86, Th3; :: thesis:
take r ; :: thesis:
thus r > 0 by A2; :: thesis:
thus lim_left ((f / g),x0) = lim_left (((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[)),x0) by A112, A86, Th3; :: thesis: