let f, g be PartFunc of REAL ,REAL ; :: thesis:
let x0 be Real; :: thesis:
assume x0 in (dom f) /\ (dom g) ; :: thesis:
then X: ( x0 in dom f & x0 in dom g ) by XBOOLE_0:def 4;
given r being Real such that A1: ( r > 0 & [.(x0 - r),x0.] c= dom f & [.(x0 - r),x0.] c= dom g & f is_differentiable_on ].(x0 - r),x0.[ & g is_differentiable_on ].(x0 - r),x0.[ & ].(x0 - r),x0.[ c= dom (f / g) & [.(x0 - r),x0.] c= dom ((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[)) & f . x0 = 0 & g . x0 = 0 & f is_continuous_in x0 & g is_continuous_in x0 & (f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[) is_left_convergent_in x0 ) ; :: thesis:
].(x0 - r),x0.[ c= [.(x0 - r),x0.] by XXREAL_1:25;
then LL: ( ].(x0 - r),x0.[ c= dom f & ].(x0 - r),x0.[ c= dom g ) by A1, XBOOLE_1:1;
A2: 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 A3: ( x0 - r < x & x < x0 ) ; :: thesis:
then x in { g1 where g1 is Real : ( x0 - r < g1 & g1 < x0 ) } ;
then A4: x in ].(x0 - r),x0.[ by RCOMP_1:def 2;
A7: ].x,x0.[ c= ].(x0 - r),x0.[

proof

let y be set ; :: 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
A8: ( g2 = y & x < g2 & g2 < x0 ) ;
x0 - r < g2 by A3, A8, XXREAL_0:2;
then y in { g3 where g3 is Real : ( x0 - r < g3 & g3 < x0 ) } by A8;
hence y in ].(x0 - r),x0.[ by RCOMP_1:def 2; :: thesis:

end;

then A9: f is_differentiable_on ].x,x0.[ by A1, FDIFF_1:34;
[.x,x0.] c= [.(x0 - r),x0.]

proof

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume Z: y in [.x,x0.] ; :: thesis:
then reconsider y = y as real number ;
( x <= y & y <= x0 ) by Z, XXREAL_1:1;
then ( x0 - r <= y & y <= x0 ) by A3, XXREAL_0:2;
hence y in [.(x0 - r),x0.] by XXREAL_1:1; :: thesis:

end;

then XX: ( [.x,x0.] c= dom f & [.x,x0.] c= dom g ) by A1, XBOOLE_1:1;
HA: ( dom ((f . x) (#) g) = dom g & dom ((g . x) (#) f) = dom f ) by VALUED_1:def 5;
then D85: dom (((f . x) (#) g) - ((g . x) (#) f)) = (dom f) /\ (dom g) by VALUED_1:12;
then B85: [.x,x0.] c= dom (((f . x) (#) g) - ((g . x) (#) f)) by XX, XBOOLE_1:19;
A10: g is_differentiable_on ].x,x0.[ by A1, A7, FDIFF_1:34;
f is_differentiable_in x by A1, A4, FDIFF_1:16;
then A11: f is_continuous_in x by FDIFF_1:32;
g is_differentiable_in x by A1, A4, FDIFF_1:16;
then A12: g is_continuous_in x by FDIFF_1:32;
A13: ( f | [.x,x0.] is continuous & g | [.x,x0.] is continuous )

proof

A14: [.x,x0.] c= dom f

proof

Y: ].(x0 - r),x0.[ c= dom f by LL;
then A15: ].x,x0.[ c= dom f by A7, XBOOLE_1:1;
A16: x0 in dom f by X;
x in dom f by A4, Y;
then {x,x0} c= dom f by A16, ZFMISC_1:38;
then ].x,x0.[ \/ {x,x0} c= dom f by A15, XBOOLE_1:8;
hence [.x,x0.] c= dom f by A3, XXREAL_1:128; :: thesis:

end;

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 A17: ( rng s c= [.x,x0.] & s is convergent & lim s in [.x,x0.] ) ; :: thesis:
set z = lim s;
A18: rng s c= dom f by A14, A17, XBOOLE_1:1;
A19: lim s in ].x,x0.[ \/ {x,x0} by A3, A17, XXREAL_1:128;

now

per cases by A19, XBOOLE_0:def 3;

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

then f is_differentiable_in lim s by A1, A7, FDIFF_1:16;
then f is_continuous_in lim s by FDIFF_1:32;
hence ( f /* s is convergent & f . (lim s) = lim (f /* s) ) by A17, A18, FCONT_1:def 1; :: thesis:

end;

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

now

per cases by A20, TARSKI:def 2;

suppose lim s = x0 ; :: thesis:

hence ( f /* s is convergent & f . (lim s) = lim (f /* s) ) by A1, A17, A18, FCONT_1:def 1; :: thesis:

end;

suppose lim s = x ; :: thesis:

hence ( f /* s is convergent & f . (lim s) = lim (f /* s) ) by A11, A17, A18, 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;

hence f | [.x,x0.] is continuous by A14, FCONT_1:14; :: thesis:
A21: [.x,x0.] c= dom g

proof

Y: ].(x0 - r),x0.[ c= dom g by LL;
then A22: ].x,x0.[ c= dom g by A7, XBOOLE_1:1;
A23: x0 in dom g by X;
x in dom g by A4, Y;
then {x,x0} c= dom g by A23, ZFMISC_1:38;
then ].x,x0.[ \/ {x,x0} c= dom g by A22, XBOOLE_1:8;
hence [.x,x0.] c= dom g by A3, XXREAL_1:128; :: thesis:

end;

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 A24: ( rng s c= [.x,x0.] & s is convergent & lim s in [.x,x0.] ) ; :: thesis:
set z = lim s;
A25: rng s c= dom g by A21, A24, XBOOLE_1:1;
A26: lim s in ].x,x0.[ \/ {x,x0} by A3, A24, XXREAL_1:128;

now

per cases by A26, XBOOLE_0:def 3;

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

then g is_differentiable_in lim s by A1, A7, FDIFF_1:16;
then g is_continuous_in lim s by FDIFF_1:32;
hence ( g /* s is convergent & g . (lim s) = lim (g /* s) ) by A24, A25, FCONT_1:def 1; :: thesis:

end;

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

now

per cases by A27, TARSKI:def 2;

suppose lim s = x0 ; :: thesis:

hence ( g /* s is convergent & g . (lim s) = lim (g /* s) ) by A1, A24, A25, FCONT_1:def 1; :: thesis:

end;

suppose lim s = x ; :: thesis:

hence ( g /* s is convergent & g . (lim s) = lim (g /* s) ) by A12, A24, A25, 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;

hence g | [.x,x0.] is continuous by A21, FCONT_1:14; :: thesis:

end;

then A28: ((g . x) (#) f) | [.x,x0.] is continuous by XX, FCONT_1:21;
((f . x) (#) g) | [.x,x0.] is continuous by A13, XX, FCONT_1:21;
then A29: (((f . x) (#) g) - ((g . x) (#) f)) | [.x,x0.] is continuous by A28, D85, B85, HA, FCONT_1:19;
A30: dom ((g . x) (#) f) = dom f by VALUED_1:def 5;
A31: dom ((f . x) (#) g) = dom g by VALUED_1:def 5;
A32: ].(x0 - r),x0.[ c= dom ((g . x) (#) f) by A30, LL;
A33: ].(x0 - r),x0.[ c= dom ((f . x) (#) g) by A31, LL;
A34: ].x,x0.[ c= dom ((g . x) (#) f) by A7, A32, XBOOLE_1:1;
then A35: (g . x) (#) f is_differentiable_on ].x,x0.[ by A9, FDIFF_1:28;
A36: ].x,x0.[ c= dom ((f . x) (#) g) by A7, A33, XBOOLE_1:1;
then ].x,x0.[ c= (dom ((f . x) (#) g)) /\ (dom ((g . x) (#) f)) by A34, XBOOLE_1:19;
then A37: ].x,x0.[ c= dom (((f . x) (#) g) - ((g . x) (#) f)) by VALUED_1:12;
A38: (f . x) (#) g is_differentiable_on ].x,x0.[ by A10, A36, FDIFF_1:28;
then A39: ((f . x) (#) g) - ((g . x) (#) f) is_differentiable_on ].x,x0.[ by A35, A37, FDIFF_1:27;
set f1 = ((f . x) (#) g) - ((g . x) (#) f);
A40: [.x,x0.] c= dom (((f . x) (#) g) - ((g . x) (#) f)) by B85;
A41: ( x0 in [.x,x0.] & x in [.x,x0.] ) by A3, XXREAL_1:1;
then ( x0 in dom (((f . x) (#) g) - ((g . x) (#) f)) & x in dom (((f . x) (#) g) - ((g . x) (#) f)) ) by A40;
then ( x0 in (dom ((f . x) (#) g)) /\ (dom ((g . x) (#) f)) & x in (dom ((f . x) (#) g)) /\ (dom ((g . x) (#) f)) ) by VALUED_1:12;
then A42: ( x0 in dom ((f . x) (#) g) & x0 in dom ((g . x) (#) f) & x in dom ((f . x) (#) g) & x in dom ((g . x) (#) f) ) by XBOOLE_0:def 4;
A43: (((f . x) (#) g) - ((g . x) (#) f)) . x0 = (((f . x) (#) g) . x0) - (((g . x) (#) f) . x0) by A40, A41, VALUED_1:13
.= ((f . x) * (g . x0)) - (((g . x) (#) f) . x0) by A42, VALUED_1:def 5
.= 0 - ((g . x) * 0 ) by A1, A42, VALUED_1:def 5
.= 0 ;
(((f . x) (#) g) - ((g . x) (#) f)) . x = (((f . x) (#) g) . x) - (((g . x) (#) f) . x) by A40, A41, VALUED_1:13
.= ((f . x) * (g . x)) - (((g . x) (#) f) . x) by A42, VALUED_1:def 5
.= ((g . x) * (f . x)) - ((g . x) * (f . x)) by A42, VALUED_1:def 5
.= 0 ;
then consider t being Real such that
A44: ( t in ].x,x0.[ & diff (((f . x) (#) g) - ((g . x) (#) f)),t = 0 ) by A3, A29, A39, A43, A40, ROLLE:1;
take t ; :: thesis:
A45: (f . x) (#) g is_differentiable_in t by A38, A44, FDIFF_1:16;
(g . x) (#) f is_differentiable_in t by A35, A44, FDIFF_1:16;
then A46: 0 = (diff ((f . x) (#) g),t) - (diff ((g . x) (#) f),t) by A44, A45, FDIFF_1:22;
A47: g is_differentiable_in t by A1, A7, A44, FDIFF_1:16;
f is_differentiable_in t by A1, A7, A44, FDIFF_1:16;
then 0 = (diff ((f . x) (#) g),t) - ((g . x) * (diff f,t)) by A46, FDIFF_1:23;
then A48: 0 = ((f . x) * (diff g,t)) - ((g . x) * (diff f,t)) by A47, FDIFF_1:23;

now

let y be set ; :: thesis:
assume y in [.x,x0.] \ {x0} ; :: thesis:
then A49: ( y in [.x,x0.] & not y in {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
A50: ( g4 = y & x <= g4 & g4 <= x0 ) ;
A51: x0 - r < g4 by A3, A50, XXREAL_0:2;
x0 <> g4 by A49, A50, TARSKI:def 1;
then g4 < x0 by A50, XXREAL_0:1;
then y in { g5 where g5 is Real : ( x0 - r < g5 & g5 < x0 ) } by A50, A51;
hence y in ].(x0 - r),x0.[ by RCOMP_1:def 2; :: thesis:

end;

then [.x,x0.] \ {x0} c= ].(x0 - r),x0.[ by TARSKI:def 3;
then A52: [.x,x0.] \ {x0} c= dom (f / g) by A1, XBOOLE_1:1;
then A53: [.x,x0.] \ {x0} c= (dom f) /\ ((dom g) \ (g " {0 })) by RFUNCT_1:def 4;
(dom f) /\ ((dom g) \ (g " {0 })) c= (dom g) \ (g " {0 }) by XBOOLE_1:17;
then A54: [.x,x0.] \ {x0} c= (dom g) \ (g " {0 }) by A53, XBOOLE_1:1;
not x in {x0} by A3, TARSKI:def 1;
then A55: x in [.x,x0.] \ {x0} by A41, XBOOLE_0:def 5;
then A56: ( x in dom g & not x in g " {0 } ) by A54, XBOOLE_0:def 5;

A57: now

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

end;

A58: x0 - r <= x0 by A1, XREAL_1:46;
A59: ].(x0 - r),x0.[ c= [.(x0 - r),x0.] by XXREAL_1:25;
x0 in { g6 where g6 is Real : ( x0 - r <= g6 & g6 <= x0 ) } by A58;
then x0 in [.(x0 - r),x0.] by RCOMP_1:def 1;
then [.x,x0.] c= [.(x0 - r),x0.] by A4, A59, XXREAL_2:def 12;
then A60: [.x,x0.] c= dom ((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[)) by A1, XBOOLE_1:1;
then A61: [.x,x0.] c= (dom (f `| ].(x0 - r),x0.[)) /\ ((dom (g `| ].(x0 - r),x0.[)) \ ((g `| ].(x0 - r),x0.[) " {0 })) by RFUNCT_1:def 4;
(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;
then A62: [.x,x0.] c= (dom (g `| ].(x0 - r),x0.[)) \ ((g `| ].(x0 - r),x0.[) " {0 }) by A61, XBOOLE_1:1;
].x,x0.[ c= [.x,x0.] by XXREAL_1:25;
then A63: t in [.x,x0.] by A44;
then A64: ( t in dom (g `| ].(x0 - r),x0.[) & not t in (g `| ].(x0 - r),x0.[) " {0 } ) by A62, XBOOLE_0:def 5;

now

assume diff g,t = 0 ; :: thesis:
then (g `| ].(x0 - r),x0.[) . t = 0 by A1, A7, A44, FDIFF_1:def 8;
then (g `| ].(x0 - r),x0.[) . t in {0 } by TARSKI:def 1;
hence contradiction by A64, FUNCT_1:def 13; :: thesis:

end;

then (f . x) / (g . x) = (diff f,t) / (diff g,t) by A48, A57, XCMPLX_1:95;
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 A52, A55, RFUNCT_1:def 4;
then (f / g) . x = ((f `| ].(x0 - r),x0.[) . t) * ((diff g,t) " ) by A1, A7, A44, FDIFF_1:def 8;
then (f / g) . x = ((f `| ].(x0 - r),x0.[) . t) * (((g `| ].(x0 - r),x0.[) . t) " ) by A1, A7, A44, FDIFF_1:def 8;
hence ( t in ].x,x0.[ & (f / g) . x = ((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[)) . t ) by A44, A60, A63, RFUNCT_1:def 4; :: thesis:

end;

A65: for r1 being Real st r1 < x0 holds
ex t being Real st
( r1 < t & t < x0 & t in dom (f / g) ) by A1, LIMFUNC2:3;
A66: 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

let a be Real_Sequence; :: thesis:
assume A67: ( a is convergent & lim a = x0 & rng a c= (dom (f / g)) /\ (left_open_halfline x0) ) ; :: thesis:
then consider k being Element of NAT such that
A68: for n being Element of NAT st k <= n holds
( x0 - r < a . n & a . n < x0 + r ) by A1, LIMFUNC3:7;
set a1 = a ^\ k;

A69: now

let n be Element of NAT ; :: thesis:
A70: (a ^\ k) . n = a . (n + k) by NAT_1:def 3;
a . (n + k) in rng a by VALUED_0:28;
then a . (n + k) in left_open_halfline x0 by A67, 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:
k <= n + k by NAT_1:12;
hence x0 - r < (a ^\ k) . n by A68, A70; :: thesis:

end;

defpred S₁[ Element of NAT , real number ] means ( $2 in ].((a ^\ k) . $1),x0.[ & (((f / g) /* a) ^\ k) . $1 = ((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[)) . $2 );
A71: for n being Element of NAT ex c being Real st S₁[n,c]

proof

let n be Element of NAT ; :: thesis:
( x0 - r < (a ^\ k) . n & (a ^\ k) . n < x0 ) by A69;
then consider c being Real such that
A72: ( c in ].((a ^\ k) . n),x0.[ & (f / g) . ((a ^\ k) . n) = ((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[)) . c ) by A2;
take c ; :: thesis:
A73: (dom (f / g)) /\ (left_open_halfline x0) c= dom (f / g) by XBOOLE_1:17;
then A74: rng a c= dom (f / g) by A67, XBOOLE_1:1;
rng (a ^\ k) c= rng a by VALUED_0:21;
then ((f / g) /* (a ^\ k)) . n = ((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[)) . c by A72, A74, FUNCT_2:185, XBOOLE_1:1;
hence S₁[n,c] by A67, A72, A73, VALUED_0:27, XBOOLE_1:1; :: thesis:

end;

consider b being Real_Sequence such that
A75: for n being Element of NAT holds S₁[n,b . n] from FUNCT_2:sch 3(A71);
reconsider d = NAT --> x0 as Real_Sequence ;
A77: lim d = d . 0 by SEQ_4:41
.= x0 by FUNCOP_1:13 ;
A78: ( a ^\ k is convergent & lim (a ^\ k) = x0 ) by A67, SEQ_4:33;

A79: now

let n be Element of NAT ; :: thesis:
b . n in ].((a ^\ k) . n),x0.[ by A75;
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 <= d . n ) by FUNCOP_1:13; :: thesis:

end;

then A80: b is convergent by A77, A78, SEQ_2:33;
A81: lim b = x0 by A77, A78, A79, SEQ_2:34;
A82: rng b c= (dom ((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[))) /\ (left_open_halfline x0)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in rng b ; :: thesis:
then consider n being Element of NAT such that
A83: x = b . n by FUNCT_2:190;
A84: ( x0 - r < (a ^\ k) . n & (a ^\ k) . n < x0 ) by A69;
A85: x in ].((a ^\ k) . n),x0.[ by A75, A83;
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 A86: x in left_open_halfline x0 by XXREAL_1:229;
A87: ].((a ^\ k) . n),x0.[ c= [.((a ^\ k) . n),x0.] by XXREAL_1:25;
x0 - r <= x0 by A1, XREAL_1:46;
then x0 in { g3 where g3 is Real : ( x0 - r <= g3 & g3 <= x0 ) } ;
then A88: x0 in [.(x0 - r),x0.] by RCOMP_1:def 1;
(a ^\ k) . n in { g4 where g4 is Real : ( x0 - r <= g4 & g4 <= x0 ) } by A84;
then (a ^\ k) . n in [.(x0 - r),x0.] by RCOMP_1:def 1;
then [.((a ^\ k) . n),x0.] c= [.(x0 - r),x0.] by A88, XXREAL_2:def 12;
then ].((a ^\ k) . n),x0.[ c= [.(x0 - r),x0.] by A87, XBOOLE_1:1;
then ].((a ^\ k) . n),x0.[ c= dom ((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[)) by A1, XBOOLE_1:1;
hence x in (dom ((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[))) /\ (left_open_halfline x0) by A85, A86, XBOOLE_0:def 4; :: thesis:

end;

A89: (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;
lim_left ((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[)),x0 = lim_left ((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[)),x0 ;
then A90: ( ((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[)) /* b is convergent & lim (((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[)) /* b) = lim_left ((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[)),x0 ) by A1, A80, A81, A82, LIMFUNC2:def 7;

A91: now

take m = 0 ; :: thesis:
let n be Element of NAT ; :: thesis:
assume m <= n ; :: thesis:
(((f / g) /* a) ^\ k) . n = ((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[)) . (b . n) by A75;
hence (((f / g) /* a) ^\ k) . n = (((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[)) /* b) . n by A82, A89, FUNCT_2:185, XBOOLE_1:1; :: thesis:

end;

then A92: ((f / g) /* a) ^\ k is convergent by A90, SEQ_4:31;
lim (((f / g) /* a) ^\ k) = lim_left ((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[)),x0 by A90, A91, SEQ_4:32;
hence ( (f / g) /* a is convergent & lim ((f / g) /* a) = lim_left ((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[)),x0 ) by A92, SEQ_4:35, SEQ_4:36; :: thesis:

end;

hence f / g is_left_convergent_in x0 by A65, Th3; :: thesis:
take r ; :: thesis:
thus r > 0 by A1; :: thesis:
thus lim_left (f / g),x0 = lim_left ((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[)),x0 by A65, A66, Th3; :: thesis: