let f, g be PartFunc of REAL ,REAL ; :: thesis:
let x0 be Real; :: thesis:
given N being Neighbourhood of x0 such that A1: N c= dom f and
A2: N c= dom g and
A3: f is_differentiable_on N and
A4: g is_differentiable_on N and
A5: N \ {x0} c= dom (f / g) and
A6: N c= dom ((f `| N) / (g `| N)) and
A7: ( f . x0 = 0 & g . x0 = 0 ) and
A8: (f `| N) / (g `| N) is_divergent_to+infty_in x0 ; :: thesis:
consider r being real number such that
A9: 0 < r and
A10: N = ].(x0 - r),(x0 + r).[ by RCOMP_1:def 7;
A11: r is Real by XREAL_0:def 1;
A12: 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

A52: now

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

end;

A53: [.x,x0.] c= dom ((f `| N) / (g `| N)) by A6, A21, XBOOLE_1:1;
then [.x,x0.] c= (dom (f `| N)) /\ ((dom (g `| N)) \ ((g `| N) " {0 })) by RFUNCT_1:def 4;
then [.x,x0.] c= (dom (g `| N)) \ ((g `| N) " {0 }) by A15, XBOOLE_1:1;
then A54: ( t in dom (g `| N) & not t in (g `| N) " {0 } ) by A49, XBOOLE_0:def 5;

A55: now

assume diff g,t = 0 ; :: thesis:
then (g `| N) . t = 0 by A4, A21, A49, FDIFF_1:def 8;
then (g `| N) . t in {0 } by TARSKI:def 1;
hence contradiction by A54, FUNCT_1:def 13; :: thesis:

end;

g is_differentiable_in t by A4, A28, A44, FDIFF_1:16;
then 0 = ((f . x) * (diff g,t)) - ((g . x) * (diff f,t)) by A48, FDIFF_1:23;
then (f . x) / (g . x) = (diff f,t) / (diff g,t) by A52, A55, 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 A50, A38, RFUNCT_1:def 4;
then (f / g) . x = ((f `| N) . t) * ((diff g,t) " ) by A3, A21, A49, FDIFF_1:def 8;
then (f / g) . x = ((f `| N) . t) * (((g `| N) . t) " ) by A4, A21, A49, FDIFF_1:def 8;
hence ( t in ].x,x0.[ & (f / g) . x = ((f `| N) / (g `| N)) . t ) by A44, A53, A49, RFUNCT_1:def 4; :: thesis:

end;

A56: 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

reconsider d = NAT --> x0 as Real_Sequence ;
let a be Real_Sequence; :: thesis:
assume that
A57: a is convergent and
A58: lim a = x0 and
A59: rng a c= (dom (f / g)) /\ (left_open_halfline x0) ; :: thesis:
consider k being Element of NAT such that
A60: for n being Element of NAT st k <= n holds
( x0 - r < a . n & a . n < x0 + r ) by A9, A11, A57, A58, LIMFUNC3:7;
set a1 = a ^\ k;
defpred S₁[ Element of NAT , real number ] means ( $2 in ].((a ^\ k) . $1),x0.[ & (((f / g) /* a) ^\ k) . $1 = ((f `| N) / (g `| N)) . $2 );

A61: now

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 A59, 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 A60; :: thesis:

end;

A62: for n being Element of NAT ex c being Real st S₁[n,c]

proof

let n be Element of NAT ; :: thesis:
A63: rng (a ^\ k) c= rng a by VALUED_0:21;
( x0 - r < (a ^\ k) . n & (a ^\ k) . n < x0 ) by A61;
then consider c being Real such that
A64: c in ].((a ^\ k) . n),x0.[ and
A65: (f / g) . ((a ^\ k) . n) = ((f `| N) / (g `| N)) . c by A12;
take c ; :: thesis:
A66: (dom (f / g)) /\ (left_open_halfline x0) c= dom (f / g) by XBOOLE_1:17;
then rng a c= dom (f / g) by A59, XBOOLE_1:1;
then ((f / g) /* (a ^\ k)) . n = ((f `| N) / (g `| N)) . c by A65, A63, FUNCT_2:185, XBOOLE_1:1;
hence S₁[n,c] by A59, A64, A66, VALUED_0:27, XBOOLE_1:1; :: thesis:

end;

consider b being Real_Sequence such that
A67: for n being Element of NAT holds S₁[n,b . n] from FUNCT_2:sch 3(A62);

A68: now

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

A69: lim d = d . 0 by SEQ_4:41
.= x0 by FUNCOP_1:13 ;
A70: x0 < x0 + r by A9, XREAL_1:31;
x0 - r < x0 by A9, XREAL_1:46;
then x0 in { g2 where g2 is Real : ( x0 - r < g2 & g2 < x0 + r ) } by A70;
then A71: x0 in ].(x0 - r),(x0 + r).[ by RCOMP_1:def 2;
A72: 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
A73: x = b . n by FUNCT_2:190;
(a ^\ k) . n < x0 by A61;
then A74: (a ^\ k) . n < x0 + r by A70, XXREAL_0:2;
x0 - r < (a ^\ k) . n by A61;
then (a ^\ k) . n in { g3 where g3 is Real : ( x0 - r < g3 & g3 < x0 + r ) } by A74;
then (a ^\ k) . n in ].(x0 - r),(x0 + r).[ by RCOMP_1:def 2;
then ( ].((a ^\ k) . n),x0.[ c= [.((a ^\ k) . n),x0.] & [.((a ^\ k) . n),x0.] c= ].(x0 - r),(x0 + r).[ ) by A71, XXREAL_1:25, XXREAL_2:def 12;
then ].((a ^\ k) . n),x0.[ c= ].(x0 - r),(x0 + r).[ by XBOOLE_1:1;
then A75: ].((a ^\ k) . n),x0.[ c= dom ((f `| N) / (g `| N)) by A6, A10, XBOOLE_1:1;
A76: x in ].((a ^\ k) . n),x0.[ by A67, A73;
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 not x in {x0} by TARSKI:def 1;
hence x in (dom ((f `| N) / (g `| N))) \ {x0} by A76, A75, XBOOLE_0:def 5; :: thesis:

end;

A77: (dom ((f `| N) / (g `| N))) \ {x0} c= dom ((f `| N) / (g `| N)) by XBOOLE_1:36;

A78: now

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

end;

lim (a ^\ k) = x0 by A57, A58, SEQ_4:33;
then ( b is convergent & lim b = x0 ) by A57, A69, A68, SEQ_2:33, SEQ_2:34;
then ((f `| N) / (g `| N)) /* b is divergent_to+infty by A8, A72, LIMFUNC3:def 2;
then ((f / g) /* a) ^\ k is divergent_to+infty by A78, LIMFUNC1:69;
hence (f / g) /* a is divergent_to+infty by LIMFUNC1:34; :: thesis:

end;

A79: 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 A5, Th4;
then 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;
then A80: f / g is_left_divergent_to+infty_in x0 by A56, LIMFUNC2:def 2;
A81: 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

A119: now

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

end;

A120: [.x0,x.] c= dom ((f `| N) / (g `| N)) by A6, A89, XBOOLE_1:1;
then [.x0,x.] c= (dom (f `| N)) /\ ((dom (g `| N)) \ ((g `| N) " {0 })) by RFUNCT_1:def 4;
then [.x0,x.] c= (dom (g `| N)) \ ((g `| N) " {0 }) by A84, XBOOLE_1:1;
then A121: ( t in dom (g `| N) & not t in (g `| N) " {0 } ) by A116, XBOOLE_0:def 5;

A122: now

assume diff g,t = 0 ; :: thesis:
then (g `| N) . t = 0 by A4, A89, A116, FDIFF_1:def 8;
then (g `| N) . t in {0 } by TARSKI:def 1;
hence contradiction by A121, FUNCT_1:def 13; :: thesis:

end;

g is_differentiable_in t by A4, A95, A111, FDIFF_1:16;
then 0 = ((f . x) * (diff g,t)) - ((g . x) * (diff f,t)) by A115, FDIFF_1:23;
then (f . x) / (g . x) = (diff f,t) / (diff g,t) by A119, A122, 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 A117, A105, RFUNCT_1:def 4;
then (f / g) . x = ((f `| N) . t) * ((diff g,t) " ) by A3, A89, A116, FDIFF_1:def 8;
then (f / g) . x = ((f `| N) . t) * (((g `| N) . t) " ) by A4, A89, A116, FDIFF_1:def 8;
hence ( t in ].x0,x.[ & (f / g) . x = ((f `| N) / (g `| N)) . t ) by A111, A120, A116, RFUNCT_1:def 4; :: thesis:

end;

A123: 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

reconsider d = NAT --> x0 as Real_Sequence ;
let a be Real_Sequence; :: thesis:
assume that
A124: a is convergent and
A125: lim a = x0 and
A126: rng a c= (dom (f / g)) /\ (right_open_halfline x0) ; :: thesis:
consider k being Element of NAT such that
A127: for n being Element of NAT st k <= n holds
( x0 - r < a . n & a . n < x0 + r ) by A9, A11, A124, A125, LIMFUNC3:7;
set a1 = a ^\ k;
defpred S₁[ Element of NAT , real number ] means ( $2 in ].x0,((a ^\ k) . $1).[ & (((f / g) /* a) ^\ k) . $1 = ((f `| N) / (g `| N)) . $2 );

A128: now

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

end;

A129: for n being Element of NAT ex c being Real st S₁[n,c]

proof

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

end;

consider b being Real_Sequence such that
A134: for n being Element of NAT holds S₁[n,b . n] from FUNCT_2:sch 3(A129);

A135: now

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

A136: lim d = d . 0 by SEQ_4:41
.= x0 by FUNCOP_1:13 ;
A137: x0 - r < x0 by A9, XREAL_1:46;
x0 < x0 + r by A9, XREAL_1:31;
then x0 in { g2 where g2 is Real : ( x0 - r < g2 & g2 < x0 + r ) } by A137;
then A138: x0 in ].(x0 - r),(x0 + r).[ by RCOMP_1:def 2;
A139: 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
A140: x = b . n by FUNCT_2:190;
x0 < (a ^\ k) . n by A128;
then A141: x0 - r < (a ^\ k) . n by A137, XXREAL_0:2;
(a ^\ k) . n < x0 + r by A128;
then (a ^\ k) . n in { g3 where g3 is Real : ( x0 - r < g3 & g3 < x0 + r ) } by A141;
then (a ^\ k) . n in ].(x0 - r),(x0 + r).[ by RCOMP_1:def 2;
then ( ].x0,((a ^\ k) . n).[ c= [.x0,((a ^\ k) . n).] & [.x0,((a ^\ k) . n).] c= ].(x0 - r),(x0 + r).[ ) by A138, XXREAL_1:25, XXREAL_2:def 12;
then ].x0,((a ^\ k) . n).[ c= ].(x0 - r),(x0 + r).[ by XBOOLE_1:1;
then A142: ].x0,((a ^\ k) . n).[ c= dom ((f `| N) / (g `| N)) by A6, A10, XBOOLE_1:1;
A143: x in ].x0,((a ^\ k) . n).[ by A134, A140;
then x in { g1 where g1 is Real : ( x0 < g1 & g1 < (a ^\ k) . n ) } by RCOMP_1:def 2;
then ex g1 being Real st
( g1 = x & x0 < g1 & g1 < (a ^\ k) . n ) ;
then not x in {x0} by TARSKI:def 1;
hence x in (dom ((f `| N) / (g `| N))) \ {x0} by A143, A142, XBOOLE_0:def 5; :: thesis:

end;

A144: (dom ((f `| N) / (g `| N))) \ {x0} c= dom ((f `| N) / (g `| N)) by XBOOLE_1:36;

A145: now

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

end;

lim (a ^\ k) = x0 by A124, A125, SEQ_4:33;
then ( b is convergent & lim b = x0 ) by A124, A136, A135, SEQ_2:33, SEQ_2:34;
then ((f `| N) / (g `| N)) /* b is divergent_to+infty by A8, A139, LIMFUNC3:def 2;
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;

for r1 being Real st x0 < r1 holds
ex t being Real st
( t < r1 & x0 < t & t in dom (f / g) ) by A79, LIMFUNC3:8;
then f / g is_right_divergent_to+infty_in x0 by A123, LIMFUNC2:def 5;
hence f / g is_divergent_to+infty_in x0 by A80, LIMFUNC3:15; :: thesis: