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_continuous_in x0 ; :: thesis:
consider r being Real such that
A9: 0 < r and
A10: N = ].(x0 - r),(x0 + r).[ by RCOMP_1:def 6;
A11: 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

A51: now :: thesis:

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

end;

A52: [.x,x0.] c= dom ((f `| N) / (g `| N)) by A6, A20;
then [.x,x0.] c= (dom (f `| N)) /\ ((dom (g `| N)) \ ((g `| N) " {0})) by RFUNCT_1:def 1;
then [.x,x0.] c= (dom (g `| N)) \ ((g `| N) " {0}) by A14;
then A53: ( t in dom (g `| N) & not t in (g `| N) " {0} ) by A48, XBOOLE_0:def 5;

A54: now :: thesis:

assume diff (g,t) = 0 ; :: thesis:
then (g `| N) . t = 0 by A4, A20, A48, FDIFF_1:def 7;
then (g `| N) . t in {0} by TARSKI:def 1;
hence contradiction by A53, FUNCT_1:def 7; :: thesis:

end;

g is_differentiable_in t by A4, A27, A43, FDIFF_1:9;
then 0 = ((f . x) * (diff (g,t))) - ((g . x) * (diff (f,t))) by A47, FDIFF_1:15;
then (f . x) / (g . x) = (diff (f,t)) / (diff (g,t)) by A51, A54, 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 A49, A37, RFUNCT_1:def 1;
then (f / g) . x = ((f `| N) . t) * ((diff (g,t)) ") by A3, A20, A48, FDIFF_1:def 7;
then (f / g) . x = ((f `| N) . t) * (((g `| N) . t) ") by A4, A20, A48, FDIFF_1:def 7;
hence ( t in ].x,x0.[ & (f / g) . x = ((f `| N) / (g `| N)) . t ) by A43, A52, A48, RFUNCT_1:def 1; :: thesis:

end;

A55: 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) = (diff (f,x0)) / (diff (g,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
A56: a is convergent and
A57: lim a = x0 and
A58: rng a c= (dom (f / g)) /\ (left_open_halfline x0) ; :: thesis:
consider k being Element of NAT such that
A59: for n being Element of NAT st k <= n holds
( x0 - r < a . n & a . n < x0 + r ) by A9, A56, A57, 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 `| N) / (g `| N)) . $2 );

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

end;

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

proof

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

end;

consider b being Real_Sequence such that
A66: for n being Element of NAT holds S₁[n,b . n] from FUNCT_2:sch 3(A61);
A67: x0 < x0 + r by A9, XREAL_1:29;
x0 - r < x0 by A9, XREAL_1:44;
then x0 in { g2 where g2 is Real : ( x0 - r < g2 & g2 < x0 + r ) } by A67;
then A68: x0 in ].(x0 - r),(x0 + r).[ by RCOMP_1:def 2;
A69: rng b c= (dom ((f `| N) / (g `| N))) /\ (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
A70: x = b . n by FUNCT_2:113;
(a ^\ k) . n < x0 by A60;
then A71: (a ^\ k) . n < x0 + r by A67, XXREAL_0:2;
x0 - r < (a ^\ k) . n by A60;
then (a ^\ k) . n in { g3 where g3 is Real : ( x0 - r < g3 & g3 < x0 + r ) } by A71;
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 A68, XXREAL_1:25, XXREAL_2:def 12;
then ].((a ^\ k) . n),x0.[ c= ].(x0 - r),(x0 + r).[ ;
then A72: ].((a ^\ k) . n),x0.[ c= dom ((f `| N) / (g `| N)) by A6, A10;
A73: x in ].((a ^\ k) . n),x0.[ by A66, A70;
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 `| N) / (g `| N))) /\ (left_open_halfline x0) by A73, A72, XBOOLE_0:def 4; :: thesis:

end;

A74: now :: thesis:

let n be Nat; :: thesis:
A75: n in NAT by ORDINAL1:def 12;
b . n in ].((a ^\ k) . n),x0.[ by A66, 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 <= (seq_const x0) . n ) by SEQ_1:57; :: thesis:

end;

A76: lim (seq_const x0) = (seq_const x0) . 0 by SEQ_4:26
.= x0 by SEQ_1:57 ;
lim (a ^\ k) = x0 by A56, A57, SEQ_4:20;
then A77: ( b is convergent & lim b = x0 ) by A56, A76, A74, SEQ_2:19, SEQ_2:20;
A78: (dom ((f `| N) / (g `| N))) /\ (left_open_halfline x0) c= dom ((f `| N) / (g `| N)) by XBOOLE_1:17;
then A79: rng b c= dom ((f `| N) / (g `| N)) by A69;
then A80: ((f `| N) / (g `| N)) /* b is convergent by A8, A77, FCONT_1:def 1;

A81: now :: thesis:

reconsider m = 0 as Nat ;
take m = m; :: thesis:
let n be Nat; :: thesis:
assume m <= n ; :: thesis:
A82: n in NAT by ORDINAL1:def 12;
(((f / g) /* a) ^\ k) . n = ((f `| N) / (g `| N)) . (b . n) by A66, A82;
hence (((f / g) /* a) ^\ k) . n = (((f `| N) / (g `| N)) /* b) . n by A69, A78, FUNCT_2:108, XBOOLE_1:1, A82; :: thesis:

end;

lim (((f `| N) / (g `| N)) /* b) = ((f `| N) / (g `| N)) . x0 by A8, A77, A79, FCONT_1:def 1;
then lim (((f `| N) / (g `| N)) /* b) = ((f `| N) . x0) * (((g `| N) . x0) ") by A6, A10, A68, RFUNCT_1:def 1
.= (diff (f,x0)) * (((g `| N) . x0) ") by A3, A10, A68, FDIFF_1:def 7
.= (diff (f,x0)) * ((diff (g,x0)) ") by A4, A10, A68, FDIFF_1:def 7 ;
then lim (((f / g) /* a) ^\ k) = (diff (f,x0)) * ((diff (g,x0)) ") by A80, A81, SEQ_4:19;
then A83: lim (((f / g) /* a) ^\ k) = (diff (f,x0)) / (diff (g,x0)) by XCMPLX_0:def 9;
((f / g) /* a) ^\ k is convergent by A80, A81, SEQ_4:18;
hence ( (f / g) /* a is convergent & lim ((f / g) /* a) = (diff (f,x0)) / (diff (g,x0)) ) by A83, SEQ_4:21, SEQ_4:22; :: thesis:

end;

A84: 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 A85: ( f / g is_left_convergent_in x0 & lim_left ((f / g),x0) = (diff (f,x0)) / (diff (g,x0)) ) by A55, Th3;
A86: 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

A126: now :: thesis:

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

end;

A127: [.x0,x.] c= dom ((f `| N) / (g `| N)) by A6, A95;
then [.x0,x.] c= (dom (f `| N)) /\ ((dom (g `| N)) \ ((g `| N) " {0})) by RFUNCT_1:def 1;
then [.x0,x.] c= (dom (g `| N)) \ ((g `| N) " {0}) by A89;
then A128: ( t in dom (g `| N) & not t in (g `| N) " {0} ) by A123, XBOOLE_0:def 5;

A129: now :: thesis:

assume diff (g,t) = 0 ; :: thesis:
then (g `| N) . t = 0 by A4, A95, A123, FDIFF_1:def 7;
then (g `| N) . t in {0} by TARSKI:def 1;
hence contradiction by A128, FUNCT_1:def 7; :: thesis:

end;

g is_differentiable_in t by A4, A102, A118, FDIFF_1:9;
then 0 = ((f . x) * (diff (g,t))) - ((g . x) * (diff (f,t))) by A122, FDIFF_1:15;
then (f . x) / (g . x) = (diff (f,t)) / (diff (g,t)) by A126, A129, 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 A124, A112, RFUNCT_1:def 1;
then (f / g) . x = ((f `| N) . t) * ((diff (g,t)) ") by A3, A95, A123, FDIFF_1:def 7;
then (f / g) . x = ((f `| N) . t) * (((g `| N) . t) ") by A4, A95, A123, FDIFF_1:def 7;
hence ( t in ].x0,x.[ & (f / g) . x = ((f `| N) / (g `| N)) . t ) by A118, A127, A123, RFUNCT_1:def 1; :: thesis:

end;

A130: 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 convergent & lim ((f / g) /* a) = (diff (f,x0)) / (diff (g,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
A131: a is convergent and
A132: lim a = x0 and
A133: rng a c= (dom (f / g)) /\ (right_open_halfline x0) ; :: thesis:
consider k being Element of NAT such that
A134: for n being Element of NAT st k <= n holds
( x0 - r < a . n & a . n < x0 + r ) by A9, A131, A132, LIMFUNC3:7;
set a1 = a ^\ k;
defpred S₁[ Element of NAT , Real] means ( $2 in ].x0,((a ^\ k) . $1).[ & (((f / g) /* a) ^\ k) . $1 = ((f `| N) / (g `| N)) . $2 );

A135: now :: thesis:

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 A133, 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 A134; :: thesis:

end;

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

proof

let n be Element of NAT ; :: thesis:
A137: rng (a ^\ k) c= rng a by VALUED_0:21;
( x0 < (a ^\ k) . n & (a ^\ k) . n < x0 + r ) by A135;
then consider c being Real such that
A138: c in ].x0,((a ^\ k) . n).[ and
A139: (f / g) . ((a ^\ k) . n) = ((f `| N) / (g `| N)) . c by A86;
take c ; :: thesis:
A140: (dom (f / g)) /\ (right_open_halfline x0) c= dom (f / g) by XBOOLE_1:17;
then rng a c= dom (f / g) by A133;
then ((f / g) /* (a ^\ k)) . n = ((f `| N) / (g `| N)) . c by A139, A137, FUNCT_2:108, XBOOLE_1:1;
hence ( c is set & c is Element of REAL & S₁[n,c] ) by A133, A138, A140, VALUED_0:27, XBOOLE_1:1; :: thesis:

end;

consider b being Real_Sequence such that
A141: for n being Element of NAT holds S₁[n,b . n] from FUNCT_2:sch 3(A136);
A142: x0 - r < x0 by A9, XREAL_1:44;
x0 < x0 + r by A9, XREAL_1:29;
then x0 in { g2 where g2 is Real : ( x0 - r < g2 & g2 < x0 + r ) } by A142;
then A143: x0 in ].(x0 - r),(x0 + r).[ by RCOMP_1:def 2;
A144: rng b c= (dom ((f `| N) / (g `| N))) /\ (right_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
A145: x = b . n by FUNCT_2:113;
x0 < (a ^\ k) . n by A135;
then A146: x0 - r < (a ^\ k) . n by A142, XXREAL_0:2;
(a ^\ k) . n < x0 + r by A135;
then (a ^\ k) . n in { g3 where g3 is Real : ( x0 - r < g3 & g3 < x0 + r ) } by A146;
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 A143, XXREAL_1:25, XXREAL_2:def 12;
then ].x0,((a ^\ k) . n).[ c= ].(x0 - r),(x0 + r).[ ;
then A147: ].x0,((a ^\ k) . n).[ c= dom ((f `| N) / (g `| N)) by A6, A10;
A148: x in ].x0,((a ^\ k) . n).[ by A141, A145;
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 x in { g2 where g2 is Real : x0 < g2 } ;
then x in right_open_halfline x0 by XXREAL_1:230;
hence x in (dom ((f `| N) / (g `| N))) /\ (right_open_halfline x0) by A148, A147, XBOOLE_0:def 4; :: thesis:

end;

A149: now :: thesis:

let n be Nat; :: thesis:
A150: n in NAT by ORDINAL1:def 12;
b . n in ].x0,((a ^\ k) . n).[ by A141, A150;
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 ( (seq_const x0) . n <= b . n & b . n <= (a ^\ k) . n ) by SEQ_1:57; :: thesis:

end;

A151: lim (seq_const x0) = (seq_const x0) . 0 by SEQ_4:26
.= x0 by SEQ_1:57 ;
lim (a ^\ k) = x0 by A131, A132, SEQ_4:20;
then A152: ( b is convergent & lim b = x0 ) by A131, A151, A149, SEQ_2:19, SEQ_2:20;
A153: (dom ((f `| N) / (g `| N))) /\ (right_open_halfline x0) c= dom ((f `| N) / (g `| N)) by XBOOLE_1:17;
then A154: rng b c= dom ((f `| N) / (g `| N)) by A144;
then A155: ((f `| N) / (g `| N)) /* b is convergent by A8, A152, FCONT_1:def 1;

A156: now :: thesis:

reconsider m = 0 as Nat ;
take m = m; :: thesis:
let n be Nat; :: thesis:
assume m <= n ; :: thesis:
A157: n in NAT by ORDINAL1:def 12;
(((f / g) /* a) ^\ k) . n = ((f `| N) / (g `| N)) . (b . n) by A141, A157;
hence (((f / g) /* a) ^\ k) . n = (((f `| N) / (g `| N)) /* b) . n by A144, A153, FUNCT_2:108, XBOOLE_1:1, A157; :: thesis:

end;

lim (((f `| N) / (g `| N)) /* b) = ((f `| N) / (g `| N)) . x0 by A8, A152, A154, FCONT_1:def 1;
then lim (((f `| N) / (g `| N)) /* b) = ((f `| N) . x0) * (((g `| N) . x0) ") by A6, A10, A143, RFUNCT_1:def 1
.= (diff (f,x0)) * (((g `| N) . x0) ") by A3, A10, A143, FDIFF_1:def 7
.= (diff (f,x0)) * ((diff (g,x0)) ") by A4, A10, A143, FDIFF_1:def 7 ;
then lim (((f / g) /* a) ^\ k) = (diff (f,x0)) * ((diff (g,x0)) ") by A155, A156, SEQ_4:19;
then A158: lim (((f / g) /* a) ^\ k) = (diff (f,x0)) / (diff (g,x0)) by XCMPLX_0:def 9;
((f / g) /* a) ^\ k is convergent by A155, A156, SEQ_4:18;
hence ( (f / g) /* a is convergent & lim ((f / g) /* a) = (diff (f,x0)) / (diff (g,x0)) ) by A158, SEQ_4:21, SEQ_4:22; :: 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 A84, LIMFUNC3:8;
then ( f / g is_right_convergent_in x0 & lim_right ((f / g),x0) = (diff (f,x0)) / (diff (g,x0)) ) by A130, Th2;
hence ( f / g is_convergent_in x0 & lim ((f / g),x0) = (diff (f,x0)) / (diff (g,x0)) ) by A85, LIMFUNC3:30; :: thesis: