let f, g be PartFunc of REAL ,REAL ; :: thesis:
let x0 be Real; :: thesis:
given N being Neighbourhood of x0 such that A0: ( N c= dom f & N c= dom g ) and
A1: ( f is_differentiable_on N & g is_differentiable_on N & N \ {x0} c= dom (f / g) & N c= dom ((f `| N) / (g `| N)) & f . x0 = 0 & g . x0 = 0 & (f `| N) / (g `| N) is_divergent_to+infty_in x0 ) ; :: thesis:
consider r being real number such that
A2: ( 0 < r & N = ].(x0 - r),(x0 + r).[ ) by RCOMP_1:def 7;
A3: r is Real by XREAL_0:def 1;
A4: for x being Real st x0 < x & x < x0 + r holds
ex c being Real st
( c in ].x0,x.[ & (f / g) . x = ((f `| N) / (g `| N)) . c )

proof

let x be Real; :: thesis:
assume A5: ( x0 < x & x < x0 + r ) ; :: thesis:
A6: f | N is continuous by A1, FDIFF_1:33;
A7: g | N is continuous by A1, FDIFF_1:33;
B6: N c= dom f by A0;
A8: x0 - r < x0 by A2, XREAL_1:46;
x0 + 0 < x0 + r by A2, XREAL_1:10;
then x0 in { g1 where g1 is Real : ( x0 - r < g1 & g1 < x0 + r ) } by A8;
then A9: x0 in ].(x0 - r),(x0 + r).[ by RCOMP_1:def 2;
x0 - r < x by A5, A8, XXREAL_0:2;
then x in { g1 where g1 is Real : ( x0 - r < g1 & g1 < x0 + r ) } by A5;
then x in ].(x0 - r),(x0 + r).[ by RCOMP_1:def 2;
then A11: [.x0,x.] c= N by A2, A9, XXREAL_2:def 12;
then X1: [.x0,x.] c= dom f by A0, XBOOLE_1:1;
f | [.x0,x.] is continuous by A6, A11, FCONT_1:17;
then A12: ((g . x) (#) f) | [.x0,x.] is continuous by X1, FCONT_1:21;
X2: [.x0,x.] c= dom g by A11, A0, XBOOLE_1:1;
then X3: [.x0,x.] c= (dom f) /\ (dom g) by X1, XBOOLE_1:19;
HA: ( dom ((f . x) (#) g) = dom g & dom ((g . x) (#) f) = dom f ) by VALUED_1:def 5;
g | [.x0,x.] is continuous by A11, A7, FCONT_1:17;
then ((f . x) (#) g) | [.x0,x.] is continuous by X2, FCONT_1:21;
then A13: (((f . x) (#) g) - ((g . x) (#) f)) | [.x0,x.] is continuous by A12, X3, HA, FCONT_1:19;
A14: dom ((g . x) (#) f) = dom f by VALUED_1:def 5;
A15: dom ((f . x) (#) g) = dom g by VALUED_1:def 5;
A16: N c= dom ((g . x) (#) f) by B6, A14;
A17: N c= dom ((f . x) (#) g) by A15, A0;
A18: ].x0,x.[ c= [.x0,x.] by XXREAL_1:25;
then A19: ].x0,x.[ c= N by A11, XBOOLE_1:1;
A20: f is_differentiable_on ].x0,x.[ by A1, A11, A18, FDIFF_1:34, XBOOLE_1:1;
A21: ].x0,x.[ c= dom ((g . x) (#) f) by A16, A19, XBOOLE_1:1;
then A22: (g . x) (#) f is_differentiable_on ].x0,x.[ by A20, FDIFF_1:28;
A23: ].x0,x.[ c= dom ((f . x) (#) g) by A17, A19, XBOOLE_1:1;
then ].x0,x.[ c= (dom ((f . x) (#) g)) /\ (dom ((g . x) (#) f)) by A21, XBOOLE_1:19;
then A24: ].x0,x.[ c= dom (((f . x) (#) g) - ((g . x) (#) f)) by VALUED_1:12;
g is_differentiable_on ].x0,x.[ by A1, A11, A18, FDIFF_1:34, XBOOLE_1:1;
then A25: (f . x) (#) g is_differentiable_on ].x0,x.[ by A23, FDIFF_1:28;
then A26: ((f . x) (#) g) - ((g . x) (#) f) is_differentiable_on ].x0,x.[ by A22, A24, FDIFF_1:27;
set f1 = ((f . x) (#) g) - ((g . x) (#) f);
A27: [.x0,x.] c= dom (((f . x) (#) g) - ((g . x) (#) f)) by X3, HA, VALUED_1:12;
A28: ( x0 in [.x0,x.] & x in [.x0,x.] ) by A5, XXREAL_1:1;
then ( x0 in dom (((f . x) (#) g) - ((g . x) (#) f)) & x in dom (((f . x) (#) g) - ((g . x) (#) f)) ) by A27;
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 A29: ( 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;
A30: (((f . x) (#) g) - ((g . x) (#) f)) . x0 = (((f . x) (#) g) . x0) - (((g . x) (#) f) . x0) by A27, A28, VALUED_1:13
.= ((f . x) * (g . x0)) - (((g . x) (#) f) . x0) by A29, VALUED_1:def 5
.= 0 - ((g . x) * 0 ) by A1, A29, VALUED_1:def 5
.= 0 ;
(((f . x) (#) g) - ((g . x) (#) f)) . x = (((f . x) (#) g) . x) - (((g . x) (#) f) . x) by A27, A28, VALUED_1:13
.= ((f . x) * (g . x)) - (((g . x) (#) f) . x) by A29, VALUED_1:def 5
.= ((g . x) * (f . x)) - ((g . x) * (f . x)) by A29, VALUED_1:def 5
.= 0 ;
then consider t being Real such that
A31: ( t in ].x0,x.[ & diff (((f . x) (#) g) - ((g . x) (#) f)),t = 0 ) by A5, A13, A26, A30, A27, ROLLE:1;
take t ; :: thesis:
A32: (f . x) (#) g is_differentiable_in t by A25, A31, FDIFF_1:16;
(g . x) (#) f is_differentiable_in t by A22, A31, FDIFF_1:16;
then A33: 0 = (diff ((f . x) (#) g),t) - (diff ((g . x) (#) f),t) by A31, A32, FDIFF_1:22;
A34: g is_differentiable_in t by A1, A19, A31, FDIFF_1:16;
f is_differentiable_in t by A1, A19, A31, FDIFF_1:16;
then 0 = (diff ((f . x) (#) g),t) - ((g . x) * (diff f,t)) by A33, FDIFF_1:23;
then A35: 0 = ((f . x) * (diff g,t)) - ((g . x) * (diff f,t)) by A34, FDIFF_1:23;
[.x0,x.] \ {x0} c= N \ {x0} by A11, XBOOLE_1:33;
then A36: [.x0,x.] \ {x0} c= dom (f / g) by A1, XBOOLE_1:1;
then A37: [.x0,x.] \ {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 A38: [.x0,x.] \ {x0} c= (dom g) \ (g " {0 }) by A37, XBOOLE_1:1;
not x in {x0} by A5, TARSKI:def 1;
then A39: x in [.x0,x.] \ {x0} by A28, XBOOLE_0:def 5;
then A40: ( x in dom g & not x in g " {0 } ) by A38, XBOOLE_0:def 5;

A41: now

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

end;

A42: [.x0,x.] c= dom ((f `| N) / (g `| N)) by A1, A11, XBOOLE_1:1;
then A43: [.x0,x.] c= (dom (f `| N)) /\ ((dom (g `| N)) \ ((g `| N) " {0 })) by RFUNCT_1:def 4;
(dom (f `| N)) /\ ((dom (g `| N)) \ ((g `| N) " {0 })) c= (dom (g `| N)) \ ((g `| N) " {0 }) by XBOOLE_1:17;
then A44: [.x0,x.] c= (dom (g `| N)) \ ((g `| N) " {0 }) by A43, XBOOLE_1:1;
A45: t in [.x0,x.] by A18, A31;
then A46: ( t in dom (g `| N) & not t in (g `| N) " {0 } ) by A44, XBOOLE_0:def 5;

now

assume diff g,t = 0 ; :: thesis:
then (g `| N) . t = 0 by A1, A11, A45, FDIFF_1:def 8;
then (g `| N) . t in {0 } by TARSKI:def 1;
hence contradiction by A46, FUNCT_1:def 13; :: thesis:

end;

then (f . x) / (g . x) = (diff f,t) / (diff g,t) by A35, A41, 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 A36, A39, RFUNCT_1:def 4;
then (f / g) . x = ((f `| N) . t) * ((diff g,t) " ) by A1, A11, A45, FDIFF_1:def 8;
then (f / g) . x = ((f `| N) . t) * (((g `| N) . t) " ) by A1, A11, A45, FDIFF_1:def 8;
hence ( t in ].x0,x.[ & (f / g) . x = ((f `| N) / (g `| N)) . t ) by A31, A42, A45, RFUNCT_1:def 4; :: thesis:

end;

for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom (f / g) & g2 < r2 & x0 < g2 & g2 in dom (f / g) ) by A1, Th4;
then A47: ( ( for r1 being Real st x0 < r1 holds
ex t being Real st
( t < r1 & x0 < t & t in dom (f / g) ) ) & ( for r1 being Real st r1 < x0 holds
ex t being Real st
( r1 < t & t < x0 & t in dom (f / g) ) ) ) by LIMFUNC3:8;
for a being Real_Sequence st a is convergent & lim a = x0 & rng a c= (dom (f / g)) /\ (right_open_halfline x0) holds
(f / g) /* a is divergent_to+infty

proof

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

A50: now

let n be Element of NAT ; :: thesis:
A51: (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 right_open_halfline x0 by A48, XBOOLE_0:def 4;
then a . (n + k) in { g1 where g1 is Real : x0 < g1 } by XXREAL_1:230;
then ex g1 being Real st
( a . (n + k) = g1 & x0 < g1 ) ;
hence x0 < (a ^\ k) . n by NAT_1:def 3; :: thesis:
k <= n + k by NAT_1:12;
hence (a ^\ k) . n < x0 + r by A49, A51; :: thesis:

end;

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

proof

let n be Element of NAT ; :: thesis:
( x0 < (a ^\ k) . n & (a ^\ k) . n < x0 + r ) by A50;
then consider c being Real such that
A53: ( c in ].x0,((a ^\ k) . n).[ & (f / g) . ((a ^\ k) . n) = ((f `| N) / (g `| N)) . c ) by A4;
take c ; :: thesis:
A54: (dom (f / g)) /\ (right_open_halfline x0) c= dom (f / g) by XBOOLE_1:17;
then A55: rng a c= dom (f / g) by A48, XBOOLE_1:1;
rng (a ^\ k) c= rng a by VALUED_0:21;
then ((f / g) /* (a ^\ k)) . n = ((f `| N) / (g `| N)) . c by A53, A55, FUNCT_2:185, XBOOLE_1:1;
hence S₁[n,c] by A48, A53, A54, VALUED_0:27, XBOOLE_1:1; :: thesis:

end;

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

A60: now

let n be Element of NAT ; :: thesis:
b . n in ].x0,((a ^\ k) . n).[ by A56;
then b . n in { g1 where g1 is Real : ( x0 < g1 & g1 < (a ^\ k) . n ) } by RCOMP_1:def 2;
then ex g1 being Real st
( g1 = b . n & x0 < g1 & g1 < (a ^\ k) . n ) ;
hence ( d . n <= b . n & b . n <= (a ^\ k) . n ) by FUNCOP_1:13; :: thesis:

end;

then A61: b is convergent by A58, A59, SEQ_2:33;
A62: lim b = x0 by A58, A59, A60, SEQ_2:34;
A63: x0 - r < x0 by A2, XREAL_1:46;
x0 < x0 + r by A2, XREAL_1:31;
then x0 in { g2 where g2 is Real : ( x0 - r < g2 & g2 < x0 + r ) } by A63;
then A64: x0 in ].(x0 - r),(x0 + r).[ by RCOMP_1:def 2;
A65: rng b c= (dom ((f `| N) / (g `| N))) \ {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
A66: x = b . n by FUNCT_2:190;
A67: ( x0 < (a ^\ k) . n & (a ^\ k) . n < x0 + r ) by A50;
A68: x in ].x0,((a ^\ k) . n).[ by A56, A66;
then x in { g1 where g1 is Real : ( x0 < g1 & g1 < (a ^\ k) . n ) } by RCOMP_1:def 2;
then A69: ex g1 being Real st
( g1 = x & x0 < g1 & g1 < (a ^\ k) . n ) ;
A70: ].x0,((a ^\ k) . n).[ c= [.x0,((a ^\ k) . n).] by XXREAL_1:25;
x0 - r < (a ^\ k) . n by A63, A67, XXREAL_0:2;
then (a ^\ k) . n in { g3 where g3 is Real : ( x0 - r < g3 & g3 < x0 + r ) } by A67;
then (a ^\ k) . n in ].(x0 - r),(x0 + r).[ by RCOMP_1:def 2;
then [.x0,((a ^\ k) . n).] c= ].(x0 - r),(x0 + r).[ by A64, XXREAL_2:def 12;
then ].x0,((a ^\ k) . n).[ c= ].(x0 - r),(x0 + r).[ by A70, XBOOLE_1:1;
then A71: ].x0,((a ^\ k) . n).[ c= dom ((f `| N) / (g `| N)) by A1, A2, XBOOLE_1:1;
not x in {x0} by A69, TARSKI:def 1;
hence x in (dom ((f `| N) / (g `| N))) \ {x0} by A68, A71, XBOOLE_0:def 5; :: thesis:

end;

A72: (dom ((f `| N) / (g `| N))) \ {x0} c= dom ((f `| N) / (g `| N)) by XBOOLE_1:36;
A73: ((f `| N) / (g `| N)) /* b is divergent_to+infty by A1, A61, A62, A65, LIMFUNC3:def 2;

now

let n be Element of NAT ; :: thesis:
(((f / g) /* a) ^\ k) . n = ((f `| N) / (g `| N)) . (b . n) by A56;
hence (((f `| N) / (g `| N)) /* b) . n <= (((f / g) /* a) ^\ k) . n by A65, A72, FUNCT_2:185, XBOOLE_1:1; :: thesis:

end;

then ((f / g) /* a) ^\ k is divergent_to+infty by A73, LIMFUNC1:69;
hence (f / g) /* a is divergent_to+infty by LIMFUNC1:34; :: thesis:

end;

then A74: f / g is_right_divergent_to+infty_in x0 by A47, LIMFUNC2:def 5;
A75: for x being Real st x0 - r < x & x < x0 holds
ex c being Real st
( c in ].x,x0.[ & (f / g) . x = ((f `| N) / (g `| N)) . c )

proof

let x be Real; :: thesis:
assume A76: ( x0 - r < x & x < x0 ) ; :: thesis:
A77: f | N is continuous by A1, FDIFF_1:33;
A79: x0 - r < x0 by A2, XREAL_1:46;
A80: x0 + 0 < x0 + r by A2, XREAL_1:10;
then x0 in { g1 where g1 is Real : ( x0 - r < g1 & g1 < x0 + r ) } by A79;
then A81: x0 in ].(x0 - r),(x0 + r).[ by RCOMP_1:def 2;
x < x0 + r by A76, A80, XXREAL_0:2;
then x in { g1 where g1 is Real : ( x0 - r < g1 & g1 < x0 + r ) } by A76;
then x in ].(x0 - r),(x0 + r).[ by RCOMP_1:def 2;
then A83: [.x,x0.] c= N by A2, A81, XXREAL_2:def 12;
then XX: ( [.x,x0.] c= dom f & [.x,x0.] c= dom g ) by A0, XBOOLE_1:1;
f | [.x,x0.] is continuous by A77, A83, FCONT_1:17;
then A84: ((g . x) (#) f) | [.x,x0.] is continuous by XX, FCONT_1:21;
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;
g | N is continuous by A1, FDIFF_1:33;
then g | [.x,x0.] is continuous by A83, FCONT_1:17;
then ((f . x) (#) g) | [.x,x0.] is continuous by XX, FCONT_1:21;
then A85: (((f . x) (#) g) - ((g . x) (#) f)) | [.x,x0.] is continuous by A84, D85, B85, HA, FCONT_1:19;
A86: dom ((g . x) (#) f) = dom f by VALUED_1:def 5;
A87: dom ((f . x) (#) g) = dom g by VALUED_1:def 5;
A88: N c= dom ((g . x) (#) f) by A86, A0;
A89: N c= dom ((f . x) (#) g) by A87, A0;
A90: ].x,x0.[ c= [.x,x0.] by XXREAL_1:25;
then A91: ].x,x0.[ c= N by A83, XBOOLE_1:1;
A92: f is_differentiable_on ].x,x0.[ by A1, A83, A90, FDIFF_1:34, XBOOLE_1:1;
A93: ].x,x0.[ c= dom ((g . x) (#) f) by A88, A91, XBOOLE_1:1;
then A94: (g . x) (#) f is_differentiable_on ].x,x0.[ by A92, FDIFF_1:28;
A95: ].x,x0.[ c= dom ((f . x) (#) g) by A89, A91, XBOOLE_1:1;
then ].x,x0.[ c= (dom ((f . x) (#) g)) /\ (dom ((g . x) (#) f)) by A93, XBOOLE_1:19;
then A96: ].x,x0.[ c= dom (((f . x) (#) g) - ((g . x) (#) f)) by VALUED_1:12;
g is_differentiable_on ].x,x0.[ by A1, A83, A90, FDIFF_1:34, XBOOLE_1:1;
then A97: (f . x) (#) g is_differentiable_on ].x,x0.[ by A95, FDIFF_1:28;
then A98: ((f . x) (#) g) - ((g . x) (#) f) is_differentiable_on ].x,x0.[ by A94, A96, FDIFF_1:27;
set f1 = ((f . x) (#) g) - ((g . x) (#) f);
A99: [.x,x0.] c= dom (((f . x) (#) g) - ((g . x) (#) f)) by B85;
A100: ( x0 in [.x,x0.] & x in [.x,x0.] ) by A76, XXREAL_1:1;
then ( x0 in dom (((f . x) (#) g) - ((g . x) (#) f)) & x in dom (((f . x) (#) g) - ((g . x) (#) f)) ) by A99;
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 A101: ( 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;
A102: (((f . x) (#) g) - ((g . x) (#) f)) . x0 = (((f . x) (#) g) . x0) - (((g . x) (#) f) . x0) by A99, A100, VALUED_1:13
.= ((f . x) * (g . x0)) - (((g . x) (#) f) . x0) by A101, VALUED_1:def 5
.= 0 - ((g . x) * 0 ) by A1, A101, VALUED_1:def 5
.= 0 ;
(((f . x) (#) g) - ((g . x) (#) f)) . x = (((f . x) (#) g) . x) - (((g . x) (#) f) . x) by A99, A100, VALUED_1:13
.= ((f . x) * (g . x)) - (((g . x) (#) f) . x) by A101, VALUED_1:def 5
.= ((g . x) * (f . x)) - ((g . x) * (f . x)) by A101, VALUED_1:def 5
.= 0 ;
then consider t being Real such that
A103: ( t in ].x,x0.[ & diff (((f . x) (#) g) - ((g . x) (#) f)),t = 0 ) by A76, A85, A98, A102, A99, ROLLE:1;
take t ; :: thesis:
A104: (f . x) (#) g is_differentiable_in t by A97, A103, FDIFF_1:16;
(g . x) (#) f is_differentiable_in t by A94, A103, FDIFF_1:16;
then A105: 0 = (diff ((f . x) (#) g),t) - (diff ((g . x) (#) f),t) by A103, A104, FDIFF_1:22;
A106: g is_differentiable_in t by A1, A91, A103, FDIFF_1:16;
f is_differentiable_in t by A1, A91, A103, FDIFF_1:16;
then 0 = (diff ((f . x) (#) g),t) - ((g . x) * (diff f,t)) by A105, FDIFF_1:23;
then A107: 0 = ((f . x) * (diff g,t)) - ((g . x) * (diff f,t)) by A106, FDIFF_1:23;
[.x,x0.] \ {x0} c= N \ {x0} by A83, XBOOLE_1:33;
then A108: [.x,x0.] \ {x0} c= dom (f / g) by A1, XBOOLE_1:1;
then A109: [.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 A110: [.x,x0.] \ {x0} c= (dom g) \ (g " {0 }) by A109, XBOOLE_1:1;
not x in {x0} by A76, TARSKI:def 1;
then A111: x in [.x,x0.] \ {x0} by A100, XBOOLE_0:def 5;
then A112: ( x in dom g & not x in g " {0 } ) by A110, XBOOLE_0:def 5;

A113: now

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

end;

A114: [.x,x0.] c= dom ((f `| N) / (g `| N)) by A1, A83, XBOOLE_1:1;
then A115: [.x,x0.] c= (dom (f `| N)) /\ ((dom (g `| N)) \ ((g `| N) " {0 })) by RFUNCT_1:def 4;
(dom (f `| N)) /\ ((dom (g `| N)) \ ((g `| N) " {0 })) c= (dom (g `| N)) \ ((g `| N) " {0 }) by XBOOLE_1:17;
then A116: [.x,x0.] c= (dom (g `| N)) \ ((g `| N) " {0 }) by A115, XBOOLE_1:1;
A117: t in [.x,x0.] by A90, A103;
then A118: ( t in dom (g `| N) & not t in (g `| N) " {0 } ) by A116, XBOOLE_0:def 5;

now

assume diff g,t = 0 ; :: thesis:
then (g `| N) . t = 0 by A1, A83, A117, FDIFF_1:def 8;
then (g `| N) . t in {0 } by TARSKI:def 1;
hence contradiction by A118, FUNCT_1:def 13; :: thesis:

end;

then (f . x) / (g . x) = (diff f,t) / (diff g,t) by A107, A113, 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 A108, A111, RFUNCT_1:def 4;
then (f / g) . x = ((f `| N) . t) * ((diff g,t) " ) by A1, A83, A117, FDIFF_1:def 8;
then (f / g) . x = ((f `| N) . t) * (((g `| N) . t) " ) by A1, A83, A117, FDIFF_1:def 8;
hence ( t in ].x,x0.[ & (f / g) . x = ((f `| N) / (g `| N)) . t ) by A103, A114, A117, RFUNCT_1:def 4; :: thesis:

end;

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 divergent_to+infty

proof

let a be Real_Sequence; :: thesis:
assume A119: ( 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
A120: for n being Element of NAT st k <= n holds
( x0 - r < a . n & a . n < x0 + r ) by A2, A3, LIMFUNC3:7;
set a1 = a ^\ k;

A121: now

let n be Element of NAT ; :: thesis:
A122: (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 A119, 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 A120, A122; :: thesis:

end;

defpred S₁[ Element of NAT , real number ] means ( $2 in ].((a ^\ k) . $1),x0.[ & (((f / g) /* a) ^\ k) . $1 = ((f `| N) / (g `| N)) . $2 );
A123: 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 A121;
then consider c being Real such that
A124: ( c in ].((a ^\ k) . n),x0.[ & (f / g) . ((a ^\ k) . n) = ((f `| N) / (g `| N)) . c ) by A75;
take c ; :: thesis:
A125: (dom (f / g)) /\ (left_open_halfline x0) c= dom (f / g) by XBOOLE_1:17;
then A126: rng a c= dom (f / g) by A119, XBOOLE_1:1;
rng (a ^\ k) c= rng a by VALUED_0:21;
then ((f / g) /* (a ^\ k)) . n = ((f `| N) / (g `| N)) . c by A124, A126, FUNCT_2:185, XBOOLE_1:1;
hence S₁[n,c] by A119, A124, A125, VALUED_0:27, XBOOLE_1:1; :: thesis:

end;

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

A131: now

let n be Element of NAT ; :: thesis:
b . n in ].((a ^\ k) . n),x0.[ by A127;
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 A132: b is convergent by A129, A130, SEQ_2:33;
A133: lim b = x0 by A129, A130, A131, SEQ_2:34;
A134: x0 - r < x0 by A2, XREAL_1:46;
A135: x0 < x0 + r by A2, XREAL_1:31;
then x0 in { g2 where g2 is Real : ( x0 - r < g2 & g2 < x0 + r ) } by A134;
then A136: x0 in ].(x0 - r),(x0 + r).[ by RCOMP_1:def 2;
A137: rng b c= (dom ((f `| N) / (g `| N))) \ {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
A138: x = b . n by FUNCT_2:190;
A139: ( x0 - r < (a ^\ k) . n & (a ^\ k) . n < x0 ) by A121;
A140: x in ].((a ^\ k) . n),x0.[ by A127, A138;
then x in { g1 where g1 is Real : ( (a ^\ k) . n < g1 & g1 < x0 ) } by RCOMP_1:def 2;
then A141: ex g1 being Real st
( g1 = x & (a ^\ k) . n < g1 & g1 < x0 ) ;
A142: ].((a ^\ k) . n),x0.[ c= [.((a ^\ k) . n),x0.] by XXREAL_1:25;
(a ^\ k) . n < x0 + r by A135, A139, XXREAL_0:2;
then (a ^\ k) . n in { g3 where g3 is Real : ( x0 - r < g3 & g3 < x0 + r ) } by A139;
then (a ^\ k) . n in ].(x0 - r),(x0 + r).[ by RCOMP_1:def 2;
then [.((a ^\ k) . n),x0.] c= ].(x0 - r),(x0 + r).[ by A136, XXREAL_2:def 12;
then ].((a ^\ k) . n),x0.[ c= ].(x0 - r),(x0 + r).[ by A142, XBOOLE_1:1;
then A143: ].((a ^\ k) . n),x0.[ c= dom ((f `| N) / (g `| N)) by A1, A2, XBOOLE_1:1;
not x in {x0} by A141, TARSKI:def 1;
hence x in (dom ((f `| N) / (g `| N))) \ {x0} by A140, A143, XBOOLE_0:def 5; :: thesis:

end;

A144: (dom ((f `| N) / (g `| N))) \ {x0} c= dom ((f `| N) / (g `| N)) by XBOOLE_1:36;
A145: ((f `| N) / (g `| N)) /* b is divergent_to+infty by A1, A132, A133, A137, LIMFUNC3:def 2;

now

let n be Element of NAT ; :: thesis:
(((f / g) /* a) ^\ k) . n = ((f `| N) / (g `| N)) . (b . n) by A127;
hence (((f `| N) / (g `| N)) /* b) . n <= (((f / g) /* a) ^\ k) . n by A137, A144, FUNCT_2:185, XBOOLE_1:1; :: thesis:

end;

then ((f / g) /* a) ^\ k is divergent_to+infty by A145, LIMFUNC1:69;
hence (f / g) /* a is divergent_to+infty by LIMFUNC1:34; :: thesis:

end;

then f / g is_left_divergent_to+infty_in x0 by A47, LIMFUNC2:def 2;
hence f / g is_divergent_to+infty_in x0 by A74, LIMFUNC3:15; :: thesis: