let f, g be PartFunc of REAL ,REAL ; :: thesis: for x0 being Real st ex N being Neighbourhood of x0 st
( N c= dom f & N c= dom g & 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_convergent_in x0 ) holds
( f / g is_convergent_in x0 & ex N being Neighbourhood of x0 st lim (f / g),x0 = lim ((f `| N) / (g `| N)),x0 )
let x0 be Real; :: thesis: ( ex N being Neighbourhood of x0 st
( N c= dom f & N c= dom g & 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_convergent_in x0 ) implies ( f / g is_convergent_in x0 & ex N being Neighbourhood of x0 st lim (f / g),x0 = lim ((f `| N) / (g `| N)),x0 ) )
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_convergent_in x0 ) ; :: thesis: ( f / g is_convergent_in x0 & ex N being Neighbourhood of x0 st lim (f / g),x0 = lim ((f `| N) / (g `| N)),x0 )
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: ( x0 < x & x < x0 + r implies ex c being Real st
( c in ].x0,x.[ & (f / g) . x = ((f `| N) / (g `| N)) . c ) )
assume A5: ( x0 < x & x < x0 + r ) ; :: thesis: ex c being Real st
( c in ].x0,x.[ & (f / g) . x = ((f `| N) / (g `| N)) . c )
A6: f | N is continuous by A1, FDIFF_1:33;
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 XX: ( [.x0,x.] c= dom f & [.x0,x.] c= dom g ) by A0, 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: [.x0,x.] c= dom (((f . x) (#) g) - ((g . x) (#) f)) by XX, XBOOLE_1:19;
f | [.x0,x.] is continuous by A6, A11, FCONT_1:17;
then A12: ((g . x) (#) f) | [.x0,x.] is continuous by XX, FCONT_1:21;
g | N is continuous by A1, FDIFF_1:33;
then g | [.x0,x.] is continuous by A11, FCONT_1:17;
then ((f . x) (#) g) | [.x0,x.] is continuous by XX, FCONT_1:21;
then A13: (((f . x) (#) g) - ((g . x) (#) f)) | [.x0,x.] is continuous by A12, D85, B85, 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 A14, A0;
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 B85;
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: ( t in ].x0,x.[ & (f / g) . x = ((f `| N) / (g `| N)) . t )
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: contradiction
then g . x in {0 } by TARSKI:def 1;
hence contradiction by A40, FUNCT_1:def 13; :: thesis: verum
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: contradiction
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: verum
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: verum
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 convergent & lim ((f / g) /* a) = lim ((f `| N) / (g `| N)),x0 )
proof
let a be Real_Sequence; :: thesis: ( a is convergent & lim a = x0 & rng a c= (dom (f / g)) /\ (right_open_halfline x0) implies ( (f / g) /* a is convergent & lim ((f / g) /* a) = lim ((f `| N) / (g `| N)),x0 ) )
assume A48: ( a is convergent & lim a = x0 & rng a c= (dom (f / g)) /\ (right_open_halfline x0) ) ; :: thesis: ( (f / g) /* a is convergent & lim ((f / g) /* a) = lim ((f `| N) / (g `| N)),x0 )
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: ( x0 < (a ^\ k) . n & (a ^\ k) . n < x0 + r )
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: (a ^\ k) . n < x0 + r
k <= n + k by NAT_1:12;
hence (a ^\ k) . n < x0 + r by A49, A51; :: thesis: verum
end;
defpred S1[ 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 S1[n,c]
proof
let n be Element of NAT ; :: thesis: ex c being Real st S1[n,c]
( 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: S1[n,c]
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 S1[n,c] by A48, A53, A54, VALUED_0:27, XBOOLE_1:1; :: thesis: verum
end;
consider b being Real_Sequence such that
A56: for n being Element of NAT holds S1[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: ( d . n <= b . n & b . n <= (a ^\ k) . n )
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: verum
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: ( not x in rng b or x in (dom ((f `| N) / (g `| N))) \ {x0} )
assume x in rng b ; :: thesis: x in (dom ((f `| N) / (g `| N))) \ {x0}
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: verum
end;
A72: (dom ((f `| N) / (g `| N))) \ {x0} c= dom ((f `| N) / (g `| N)) by XBOOLE_1:36;
lim ((f `| N) / (g `| N)),x0 = lim ((f `| N) / (g `| N)),x0 ;
then A73: ( ((f `| N) / (g `| N)) /* b is convergent & lim (((f `| N) / (g `| N)) /* b) = lim ((f `| N) / (g `| N)),x0 ) by A1, A61, A62, A65, LIMFUNC3:def 4;
A74: now
take m = 0 ; :: thesis: for n being Element of NAT st m <= n holds
(((f / g) /* a) ^\ k) . n = (((f `| N) / (g `| N)) /* b) . n
let n be Element of NAT ; :: thesis: ( m <= n implies (((f / g) /* a) ^\ k) . n = (((f `| N) / (g `| N)) /* b) . n )
assume m <= n ; :: thesis: (((f / g) /* a) ^\ k) . n = (((f `| N) / (g `| N)) /* b) . n
(((f / g) /* a) ^\ k) . n = ((f `| N) / (g `| N)) . (b . n) by A56;
hence (((f / g) /* a) ^\ k) . n = (((f `| N) / (g `| N)) /* b) . n by A65, A72, FUNCT_2:185, XBOOLE_1:1; :: thesis: verum
end;
then A75: ((f / g) /* a) ^\ k is convergent by A73, SEQ_4:31;
lim (((f / g) /* a) ^\ k) = lim ((f `| N) / (g `| N)),x0 by A73, A74, SEQ_4:32;
hence ( (f / g) /* a is convergent & lim ((f / g) /* a) = lim ((f `| N) / (g `| N)),x0 ) by A75, SEQ_4:35, SEQ_4:36; :: thesis: verum
end;
then A76: ( f / g is_right_convergent_in x0 & lim_right (f / g),x0 = lim ((f `| N) / (g `| N)),x0 ) by A47, Th2;
A77: 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: ( x0 - r < x & x < x0 implies ex c being Real st
( c in ].x,x0.[ & (f / g) . x = ((f `| N) / (g `| N)) . c ) )
assume A78: ( x0 - r < x & x < x0 ) ; :: thesis: ex c being Real st
( c in ].x,x0.[ & (f / g) . x = ((f `| N) / (g `| N)) . c )
A79: f | N is continuous by A1, FDIFF_1:33;
A81: x0 - r < x0 by A2, XREAL_1:46;
A88: dom ((g . x) (#) f) = dom f by VALUED_1:def 5;
A89: dom ((f . x) (#) g) = dom g by VALUED_1:def 5;
A82: x0 + 0 < x0 + r by A2, XREAL_1:10;
then x0 in { g1 where g1 is Real : ( x0 - r < g1 & g1 < x0 + r ) } by A81;
then A83: x0 in ].(x0 - r),(x0 + r).[ by RCOMP_1:def 2;
x < x0 + r by A78, A82, XXREAL_0:2;
then x in { g1 where g1 is Real : ( x0 - r < g1 & g1 < x0 + r ) } by A78;
then x in ].(x0 - r),(x0 + r).[ by RCOMP_1:def 2;
then A85: [.x,x0.] c= N by A2, A83, XXREAL_2:def 12;
then XX: ( [.x,x0.] c= dom f & [.x,x0.] c= dom g ) by A0, 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;
f | [.x,x0.] is continuous by A79, A85, FCONT_1:17;
then A86: ((g . x) (#) f) | [.x,x0.] is continuous by XX, FCONT_1:21;
g | N is continuous by A1, FDIFF_1:33;
then g | [.x,x0.] is continuous by A85, FCONT_1:17;
then ((f . x) (#) g) | [.x,x0.] is continuous by XX, FCONT_1:21;
then A87: (((f . x) (#) g) - ((g . x) (#) f)) | [.x,x0.] is continuous by A86, D85, B85, HA, FCONT_1:19;
A90: N c= dom ((g . x) (#) f) by A88, A0;
A91: N c= dom ((f . x) (#) g) by A89, A0;
A92: ].x,x0.[ c= [.x,x0.] by XXREAL_1:25;
then A93: ].x,x0.[ c= N by A85, XBOOLE_1:1;
A94: f is_differentiable_on ].x,x0.[ by A1, A85, A92, FDIFF_1:34, XBOOLE_1:1;
A95: ].x,x0.[ c= dom ((g . x) (#) f) by A90, A93, XBOOLE_1:1;
then A96: (g . x) (#) f is_differentiable_on ].x,x0.[ by A94, FDIFF_1:28;
A97: ].x,x0.[ c= dom ((f . x) (#) g) by A91, A93, XBOOLE_1:1;
then ].x,x0.[ c= (dom ((f . x) (#) g)) /\ (dom ((g . x) (#) f)) by A95, XBOOLE_1:19;
then A98: ].x,x0.[ c= dom (((f . x) (#) g) - ((g . x) (#) f)) by VALUED_1:12;
g is_differentiable_on ].x,x0.[ by A1, A85, A92, FDIFF_1:34, XBOOLE_1:1;
then A99: (f . x) (#) g is_differentiable_on ].x,x0.[ by A97, FDIFF_1:28;
then A100: ((f . x) (#) g) - ((g . x) (#) f) is_differentiable_on ].x,x0.[ by A96, A98, FDIFF_1:27;
set f1 = ((f . x) (#) g) - ((g . x) (#) f);
A101: [.x,x0.] c= dom (((f . x) (#) g) - ((g . x) (#) f)) by B85;
A102: ( x0 in [.x,x0.] & x in [.x,x0.] ) by A78, XXREAL_1:1;
then ( x0 in dom (((f . x) (#) g) - ((g . x) (#) f)) & x in dom (((f . x) (#) g) - ((g . x) (#) f)) ) by A101;
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 A103: ( 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;
A104: (((f . x) (#) g) - ((g . x) (#) f)) . x0 = (((f . x) (#) g) . x0) - (((g . x) (#) f) . x0) by A101, A102, VALUED_1:13
.= ((f . x) * (g . x0)) - (((g . x) (#) f) . x0) by A103, VALUED_1:def 5
.= 0 - ((g . x) * 0 ) by A1, A103, VALUED_1:def 5
.= 0 ;
(((f . x) (#) g) - ((g . x) (#) f)) . x = (((f . x) (#) g) . x) - (((g . x) (#) f) . x) by A101, A102, VALUED_1:13
.= ((f . x) * (g . x)) - (((g . x) (#) f) . x) by A103, VALUED_1:def 5
.= ((g . x) * (f . x)) - ((g . x) * (f . x)) by A103, VALUED_1:def 5
.= 0 ;
then consider t being Real such that
A105: ( t in ].x,x0.[ & diff (((f . x) (#) g) - ((g . x) (#) f)),t = 0 ) by A78, A87, A100, A104, A101, ROLLE:1;
take t ; :: thesis: ( t in ].x,x0.[ & (f / g) . x = ((f `| N) / (g `| N)) . t )
A106: (f . x) (#) g is_differentiable_in t by A99, A105, FDIFF_1:16;
(g . x) (#) f is_differentiable_in t by A96, A105, FDIFF_1:16;
then A107: 0 = (diff ((f . x) (#) g),t) - (diff ((g . x) (#) f),t) by A105, A106, FDIFF_1:22;
A108: g is_differentiable_in t by A1, A93, A105, FDIFF_1:16;
f is_differentiable_in t by A1, A93, A105, FDIFF_1:16;
then 0 = (diff ((f . x) (#) g),t) - ((g . x) * (diff f,t)) by A107, FDIFF_1:23;
then A109: 0 = ((f . x) * (diff g,t)) - ((g . x) * (diff f,t)) by A108, FDIFF_1:23;
[.x,x0.] \ {x0} c= N \ {x0} by A85, XBOOLE_1:33;
then A110: [.x,x0.] \ {x0} c= dom (f / g) by A1, XBOOLE_1:1;
then A111: [.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 A112: [.x,x0.] \ {x0} c= (dom g) \ (g " {0 }) by A111, XBOOLE_1:1;
not x in {x0} by A78, TARSKI:def 1;
then A113: x in [.x,x0.] \ {x0} by A102, XBOOLE_0:def 5;
then A114: ( x in dom g & not x in g " {0 } ) by A112, XBOOLE_0:def 5;
A115: now
assume g . x = 0 ; :: thesis: contradiction
then g . x in {0 } by TARSKI:def 1;
hence contradiction by A114, FUNCT_1:def 13; :: thesis: verum
end;
A116: [.x,x0.] c= dom ((f `| N) / (g `| N)) by A1, A85, XBOOLE_1:1;
then A117: [.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 A118: [.x,x0.] c= (dom (g `| N)) \ ((g `| N) " {0 }) by A117, XBOOLE_1:1;
A119: t in [.x,x0.] by A92, A105;
then A120: ( t in dom (g `| N) & not t in (g `| N) " {0 } ) by A118, XBOOLE_0:def 5;
now
assume diff g,t = 0 ; :: thesis: contradiction
then (g `| N) . t = 0 by A1, A85, A119, FDIFF_1:def 8;
then (g `| N) . t in {0 } by TARSKI:def 1;
hence contradiction by A120, FUNCT_1:def 13; :: thesis: verum
end;
then (f . x) / (g . x) = (diff f,t) / (diff g,t) by A109, A115, 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 A110, A113, RFUNCT_1:def 4;
then (f / g) . x = ((f `| N) . t) * ((diff g,t) " ) by A1, A85, A119, FDIFF_1:def 8;
then (f / g) . x = ((f `| N) . t) * (((g `| N) . t) " ) by A1, A85, A119, FDIFF_1:def 8;
hence ( t in ].x,x0.[ & (f / g) . x = ((f `| N) / (g `| N)) . t ) by A105, A116, A119, RFUNCT_1:def 4; :: thesis: verum
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 convergent & lim ((f / g) /* a) = lim ((f `| N) / (g `| N)),x0 )
proof
let a be Real_Sequence; :: thesis: ( a is convergent & lim a = x0 & rng a c= (dom (f / g)) /\ (left_open_halfline x0) implies ( (f / g) /* a is convergent & lim ((f / g) /* a) = lim ((f `| N) / (g `| N)),x0 ) )
assume A121: ( a is convergent & lim a = x0 & rng a c= (dom (f / g)) /\ (left_open_halfline x0) ) ; :: thesis: ( (f / g) /* a is convergent & lim ((f / g) /* a) = lim ((f `| N) / (g `| N)),x0 )
then consider k being Element of NAT such that
A122: 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;
A123: now
let n be Element of NAT ; :: thesis: ( (a ^\ k) . n < x0 & x0 - r < (a ^\ k) . n )
A124: (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 A121, 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: x0 - r < (a ^\ k) . n
k <= n + k by NAT_1:12;
hence x0 - r < (a ^\ k) . n by A122, A124; :: thesis: verum
end;
defpred S1[ Element of NAT , real number ] means ( $2 in ].((a ^\ k) . $1),x0.[ & (((f / g) /* a) ^\ k) . $1 = ((f `| N) / (g `| N)) . $2 );
A125: for n being Element of NAT ex c being Real st S1[n,c]
proof
let n be Element of NAT ; :: thesis: ex c being Real st S1[n,c]
( x0 - r < (a ^\ k) . n & (a ^\ k) . n < x0 ) by A123;
then consider c being Real such that
A126: ( c in ].((a ^\ k) . n),x0.[ & (f / g) . ((a ^\ k) . n) = ((f `| N) / (g `| N)) . c ) by A77;
take c ; :: thesis: S1[n,c]
A127: (dom (f / g)) /\ (left_open_halfline x0) c= dom (f / g) by XBOOLE_1:17;
then A128: rng a c= dom (f / g) by A121, 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 A126, A128, FUNCT_2:185, XBOOLE_1:1;
hence S1[n,c] by A121, A126, A127, VALUED_0:27, XBOOLE_1:1; :: thesis: verum
end;
consider b being Real_Sequence such that
A129: for n being Element of NAT holds S1[n,b . n] from FUNCT_2:sch 3(A125);
 reconsider d = NAT --> x0 as Real_Sequence ;
A131: lim d = d . 0 by SEQ_4:41
.= x0 by FUNCOP_1:13 ;
A132: ( a ^\ k is convergent & lim (a ^\ k) = x0 ) by A121, SEQ_4:33;
A133: now
let n be Element of NAT ; :: thesis: ( (a ^\ k) . n <= b . n & b . n <= d . n )
b . n in ].((a ^\ k) . n),x0.[ by A129;
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: verum
end;
then A134: b is convergent by A131, A132, SEQ_2:33;
A135: lim b = x0 by A131, A132, A133, SEQ_2:34;
A136: x0 - r < x0 by A2, XREAL_1:46;
A137: x0 < x0 + r by A2, XREAL_1:31;
then x0 in { g2 where g2 is Real : ( x0 - r < g2 & g2 < x0 + r ) } by A136;
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: ( not x in rng b or x in (dom ((f `| N) / (g `| N))) \ {x0} )
assume x in rng b ; :: thesis: x in (dom ((f `| N) / (g `| N))) \ {x0}
then consider n being Element of NAT such that
A140: x = b . n by FUNCT_2:190;
A141: ( x0 - r < (a ^\ k) . n & (a ^\ k) . n < x0 ) by A123;
A142: x in ].((a ^\ k) . n),x0.[ by A129, A140;
then x in { g1 where g1 is Real : ( (a ^\ k) . n < g1 & g1 < x0 ) } by RCOMP_1:def 2;
then A143: ex g1 being Real st
( g1 = x & (a ^\ k) . n < g1 & g1 < x0 ) ;
A144: ].((a ^\ k) . n),x0.[ c= [.((a ^\ k) . n),x0.] by XXREAL_1:25;
(a ^\ k) . n < x0 + r by A137, A141, XXREAL_0:2;
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 [.((a ^\ k) . n),x0.] c= ].(x0 - r),(x0 + r).[ by A138, XXREAL_2:def 12;
then ].((a ^\ k) . n),x0.[ c= ].(x0 - r),(x0 + r).[ by A144, XBOOLE_1:1;
then A145: ].((a ^\ k) . n),x0.[ c= dom ((f `| N) / (g `| N)) by A1, A2, XBOOLE_1:1;
not x in {x0} by A143, TARSKI:def 1;
hence x in (dom ((f `| N) / (g `| N))) \ {x0} by A142, A145, XBOOLE_0:def 5; :: thesis: verum
end;
A146: (dom ((f `| N) / (g `| N))) \ {x0} c= dom ((f `| N) / (g `| N)) by XBOOLE_1:36;
lim ((f `| N) / (g `| N)),x0 = lim ((f `| N) / (g `| N)),x0 ;
then A147: ( ((f `| N) / (g `| N)) /* b is convergent & lim (((f `| N) / (g `| N)) /* b) = lim ((f `| N) / (g `| N)),x0 ) by A1, A134, A135, A139, LIMFUNC3:def 4;
A148: now
take m = 0 ; :: thesis: for n being Element of NAT st m <= n holds
(((f / g) /* a) ^\ k) . n = (((f `| N) / (g `| N)) /* b) . n
let n be Element of NAT ; :: thesis: ( m <= n implies (((f / g) /* a) ^\ k) . n = (((f `| N) / (g `| N)) /* b) . n )
assume m <= n ; :: thesis: (((f / g) /* a) ^\ k) . n = (((f `| N) / (g `| N)) /* b) . n
(((f / g) /* a) ^\ k) . n = ((f `| N) / (g `| N)) . (b . n) by A129;
hence (((f / g) /* a) ^\ k) . n = (((f `| N) / (g `| N)) /* b) . n by A139, A146, FUNCT_2:185, XBOOLE_1:1; :: thesis: verum
end;
then A149: ((f / g) /* a) ^\ k is convergent by A147, SEQ_4:31;
lim (((f / g) /* a) ^\ k) = lim ((f `| N) / (g `| N)),x0 by A147, A148, SEQ_4:32;
hence ( (f / g) /* a is convergent & lim ((f / g) /* a) = lim ((f `| N) / (g `| N)),x0 ) by A149, SEQ_4:35, SEQ_4:36; :: thesis: verum
end;
then A150: ( f / g is_left_convergent_in x0 & lim_left (f / g),x0 = lim ((f `| N) / (g `| N)),x0 ) by A47, Th3;
hence f / g is_convergent_in x0 by A76, LIMFUNC3:34; :: thesis: ex N being Neighbourhood of x0 st lim (f / g),x0 = lim ((f `| N) / (g `| N)),x0
take N ; :: thesis: lim (f / g),x0 = lim ((f `| N) / (g `| N)),x0
thus lim (f / g),x0 = lim ((f `| N) / (g `| N)),x0 by A76, A150, LIMFUNC3:34; :: thesis: verum