:: L_HOSPIT semantic presentation begin theorem :: L_HOSPIT:1 for f being PartFunc of REAL,REAL for x0 being Real st f is_continuous_in x0 & ( 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 & g2 < r2 & x0 < g2 & g2 in dom f ) ) holds f is_convergent_in x0 proof let f be PartFunc of REAL,REAL; ::_thesis: for x0 being Real st f is_continuous_in x0 & ( 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 & g2 < r2 & x0 < g2 & g2 in dom f ) ) holds f is_convergent_in x0 let x0 be Real; ::_thesis: ( f is_continuous_in x0 & ( 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 & g2 < r2 & x0 < g2 & g2 in dom f ) ) implies f is_convergent_in x0 ) assume that A1: f is_continuous_in x0 and A2: 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 & g2 < r2 & x0 < g2 & g2 in dom f ) ; ::_thesis: f is_convergent_in x0 now__::_thesis:_for_s_being_Real_Sequence_st_s_is_convergent_&_lim_s_=_x0_&_rng_s_c=_(dom_f)_\_{x0}_holds_ (_f_/*_s_is_convergent_&_lim_(f_/*_s)_=_f_._x0_) let s be Real_Sequence; ::_thesis: ( s is convergent & lim s = x0 & rng s c= (dom f) \ {x0} implies ( f /* s is convergent & lim (f /* s) = f . x0 ) ) assume that A3: ( s is convergent & lim s = x0 ) and A4: rng s c= (dom f) \ {x0} ; ::_thesis: ( f /* s is convergent & lim (f /* s) = f . x0 ) (dom f) \ {x0} c= dom f by XBOOLE_1:36; then rng s c= dom f by A4, XBOOLE_1:1; hence ( f /* s is convergent & lim (f /* s) = f . x0 ) by A1, A3, FCONT_1:def_1; ::_thesis: verum end; hence f is_convergent_in x0 by A2, LIMFUNC3:def_1; ::_thesis: verum end; theorem Th2: :: L_HOSPIT:2 for f being PartFunc of REAL,REAL for x0, t being Real holds ( f is_right_convergent_in x0 & lim_right (f,x0) = t iff ( ( for r being Real st x0 < r holds ex t being Real st ( t < r & x0 < t & t in dom f ) ) & ( for a being Real_Sequence st a is convergent & lim a = x0 & rng a c= (dom f) /\ (right_open_halfline x0) holds ( f /* a is convergent & lim (f /* a) = t ) ) ) ) proof let f be PartFunc of REAL,REAL; ::_thesis: for x0, t being Real holds ( f is_right_convergent_in x0 & lim_right (f,x0) = t iff ( ( for r being Real st x0 < r holds ex t being Real st ( t < r & x0 < t & t in dom f ) ) & ( for a being Real_Sequence st a is convergent & lim a = x0 & rng a c= (dom f) /\ (right_open_halfline x0) holds ( f /* a is convergent & lim (f /* a) = t ) ) ) ) let x0, t be Real; ::_thesis: ( f is_right_convergent_in x0 & lim_right (f,x0) = t iff ( ( for r being Real st x0 < r holds ex t being Real st ( t < r & x0 < t & t in dom f ) ) & ( for a being Real_Sequence st a is convergent & lim a = x0 & rng a c= (dom f) /\ (right_open_halfline x0) holds ( f /* a is convergent & lim (f /* a) = t ) ) ) ) thus ( f is_right_convergent_in x0 & lim_right (f,x0) = t implies ( ( for r being Real st x0 < r holds ex t being Real st ( t < r & x0 < t & t in dom f ) ) & ( for a being Real_Sequence st a is convergent & lim a = x0 & rng a c= (dom f) /\ (right_open_halfline x0) holds ( f /* a is convergent & lim (f /* a) = t ) ) ) ) by LIMFUNC2:def_4, LIMFUNC2:def_8; ::_thesis: ( ( for r being Real st x0 < r holds ex t being Real st ( t < r & x0 < t & t in dom f ) ) & ( for a being Real_Sequence st a is convergent & lim a = x0 & rng a c= (dom f) /\ (right_open_halfline x0) holds ( f /* a is convergent & lim (f /* a) = t ) ) implies ( f is_right_convergent_in x0 & lim_right (f,x0) = t ) ) thus ( ( for r being Real st x0 < r holds ex t being Real st ( t < r & x0 < t & t in dom f ) ) & ( for a being Real_Sequence st a is convergent & lim a = x0 & rng a c= (dom f) /\ (right_open_halfline x0) holds ( f /* a is convergent & lim (f /* a) = t ) ) implies ( f is_right_convergent_in x0 & lim_right (f,x0) = t ) ) ::_thesis: verum proof assume that A1: for r being Real st x0 < r holds ex t being Real st ( t < r & x0 < t & t in dom f ) and A2: for a being Real_Sequence st a is convergent & lim a = x0 & rng a c= (dom f) /\ (right_open_halfline x0) holds ( f /* a is convergent & lim (f /* a) = t ) ; ::_thesis: ( f is_right_convergent_in x0 & lim_right (f,x0) = t ) thus f is_right_convergent_in x0 by A1, A2, LIMFUNC2:def_4; ::_thesis: lim_right (f,x0) = t hence lim_right (f,x0) = t by A2, LIMFUNC2:def_8; ::_thesis: verum end; end; theorem Th3: :: L_HOSPIT:3 for f being PartFunc of REAL,REAL for x0, t being Real holds ( f is_left_convergent_in x0 & lim_left (f,x0) = t iff ( ( for r being Real st r < x0 holds ex t being Real st ( r < t & t < x0 & t in dom f ) ) & ( for a being Real_Sequence st a is convergent & lim a = x0 & rng a c= (dom f) /\ (left_open_halfline x0) holds ( f /* a is convergent & lim (f /* a) = t ) ) ) ) proof let f be PartFunc of REAL,REAL; ::_thesis: for x0, t being Real holds ( f is_left_convergent_in x0 & lim_left (f,x0) = t iff ( ( for r being Real st r < x0 holds ex t being Real st ( r < t & t < x0 & t in dom f ) ) & ( for a being Real_Sequence st a is convergent & lim a = x0 & rng a c= (dom f) /\ (left_open_halfline x0) holds ( f /* a is convergent & lim (f /* a) = t ) ) ) ) let x0, t be Real; ::_thesis: ( f is_left_convergent_in x0 & lim_left (f,x0) = t iff ( ( for r being Real st r < x0 holds ex t being Real st ( r < t & t < x0 & t in dom f ) ) & ( for a being Real_Sequence st a is convergent & lim a = x0 & rng a c= (dom f) /\ (left_open_halfline x0) holds ( f /* a is convergent & lim (f /* a) = t ) ) ) ) thus ( f is_left_convergent_in x0 & lim_left (f,x0) = t implies ( ( for r being Real st r < x0 holds ex t being Real st ( r < t & t < x0 & t in dom f ) ) & ( for a being Real_Sequence st a is convergent & lim a = x0 & rng a c= (dom f) /\ (left_open_halfline x0) holds ( f /* a is convergent & lim (f /* a) = t ) ) ) ) by LIMFUNC2:def_1, LIMFUNC2:def_7; ::_thesis: ( ( for r being Real st r < x0 holds ex t being Real st ( r < t & t < x0 & t in dom f ) ) & ( for a being Real_Sequence st a is convergent & lim a = x0 & rng a c= (dom f) /\ (left_open_halfline x0) holds ( f /* a is convergent & lim (f /* a) = t ) ) implies ( f is_left_convergent_in x0 & lim_left (f,x0) = t ) ) thus ( ( for r being Real st r < x0 holds ex t being Real st ( r < t & t < x0 & t in dom f ) ) & ( for a being Real_Sequence st a is convergent & lim a = x0 & rng a c= (dom f) /\ (left_open_halfline x0) holds ( f /* a is convergent & lim (f /* a) = t ) ) implies ( f is_left_convergent_in x0 & lim_left (f,x0) = t ) ) ::_thesis: verum proof assume that A1: for r being Real st r < x0 holds ex t being Real st ( r < t & t < x0 & t in dom f ) and A2: for a being Real_Sequence st a is convergent & lim a = x0 & rng a c= (dom f) /\ (left_open_halfline x0) holds ( f /* a is convergent & lim (f /* a) = t ) ; ::_thesis: ( f is_left_convergent_in x0 & lim_left (f,x0) = t ) thus f is_left_convergent_in x0 by A1, A2, LIMFUNC2:def_1; ::_thesis: lim_left (f,x0) = t hence lim_left (f,x0) = t by A2, LIMFUNC2:def_7; ::_thesis: verum end; end; theorem Th4: :: L_HOSPIT:4 for f being PartFunc of REAL,REAL for x0 being Real st ex N being Neighbourhood of x0 st N \ {x0} c= dom f holds 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 & g2 < r2 & x0 < g2 & g2 in dom f ) proof let f be PartFunc of REAL,REAL; ::_thesis: for x0 being Real st ex N being Neighbourhood of x0 st N \ {x0} c= dom f holds 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 & g2 < r2 & x0 < g2 & g2 in dom f ) let x0 be Real; ::_thesis: ( ex N being Neighbourhood of x0 st N \ {x0} c= dom f implies 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 & g2 < r2 & x0 < g2 & g2 in dom f ) ) given N being Neighbourhood of x0 such that A1: N \ {x0} c= dom f ; ::_thesis: 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 & g2 < r2 & x0 < g2 & g2 in dom f ) consider r being real number such that A2: 0 < r and A3: N = ].(x0 - r),(x0 + r).[ by RCOMP_1:def_6; A4: r is Real by XREAL_0:def_1; then N \ {x0} = ].(x0 - r),x0.[ \/ ].x0,(x0 + r).[ by A2, A3, LIMFUNC3:4; hence 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 & g2 < r2 & x0 < g2 & g2 in dom f ) by A1, A2, A4, LIMFUNC3:5; ::_thesis: verum end; theorem :: L_HOSPIT:5 for f, g being PartFunc of REAL,REAL 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_divergent_to+infty_in x0 ) holds f / g is_divergent_to+infty_in x0 proof 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_divergent_to+infty_in x0 ) holds f / g is_divergent_to+infty_in 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_divergent_to+infty_in x0 ) implies f / g is_divergent_to+infty_in x0 ) 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: f / g is_divergent_to+infty_in x0 consider r being real number such that A9: 0 < r and A10: N = ].(x0 - r),(x0 + r).[ by RCOMP_1:def_6; 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 A13: x0 + 0 < x0 + r by A9, XREAL_1:8; x0 - r < x0 by A9, XREAL_1:44; then x0 in { g1 where g1 is Real : ( x0 - r < g1 & g1 < x0 + r ) } by A13; then A14: x0 in ].(x0 - r),(x0 + r).[ by RCOMP_1:def_2; A15: (dom (f `| N)) /\ ((dom (g `| N)) \ ((g `| N) " {0})) c= (dom (g `| N)) \ ((g `| N) " {0}) by XBOOLE_1:17; A16: (dom f) /\ ((dom g) \ (g " {0})) c= (dom g) \ (g " {0}) by XBOOLE_1:17; 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 that A17: x0 - r < x and A18: x < x0 ; ::_thesis: ex c being Real st ( c in ].x,x0.[ & (f / g) . x = ((f `| N) / (g `| N)) . c ) set f1 = ((f . x) (#) g) - ((g . x) (#) f); A19: ( dom ((f . x) (#) g) = dom g & dom ((g . x) (#) f) = dom f ) by VALUED_1:def_5; then A20: dom (((f . x) (#) g) - ((g . x) (#) f)) = (dom f) /\ (dom g) by VALUED_1:12; x < x0 + r by A18, A13, XXREAL_0:2; then x in { g1 where g1 is Real : ( x0 - r < g1 & g1 < x0 + r ) } by A17; then x in ].(x0 - r),(x0 + r).[ by RCOMP_1:def_2; then A21: [.x,x0.] c= N by A10, A14, XXREAL_2:def_12; then A22: ( [.x,x0.] c= dom f & [.x,x0.] c= dom g ) by A1, A2, XBOOLE_1:1; then A23: [.x,x0.] c= dom (((f . x) (#) g) - ((g . x) (#) f)) by A20, XBOOLE_1:19; g | N is continuous by A4, FDIFF_1:25; then g | [.x,x0.] is continuous by A21, FCONT_1:16; then A24: ((f . x) (#) g) | [.x,x0.] is continuous by A2, A21, FCONT_1:20, XBOOLE_1:1; f | N is continuous by A3, FDIFF_1:25; then f | [.x,x0.] is continuous by A21, FCONT_1:16; then A25: ((g . x) (#) f) | [.x,x0.] is continuous by A1, A21, FCONT_1:20, XBOOLE_1:1; [.x,x0.] c= dom (((f . x) (#) g) - ((g . x) (#) f)) by A22, A20, XBOOLE_1:19; then A26: (((f . x) (#) g) - ((g . x) (#) f)) | [.x,x0.] is continuous by A25, A19, A20, A24, FCONT_1:18; A27: ].x,x0.[ c= [.x,x0.] by XXREAL_1:25; then A28: ].x,x0.[ c= N by A21, XBOOLE_1:1; A29: x in [.x,x0.] by A18, XXREAL_1:1; then x in dom (((f . x) (#) g) - ((g . x) (#) f)) by A23; then A30: x in (dom ((f . x) (#) g)) /\ (dom ((g . x) (#) f)) by VALUED_1:12; then A31: x in dom ((f . x) (#) g) by XBOOLE_0:def_4; A32: x0 in [.x,x0.] by A18, XXREAL_1:1; then x0 in dom (((f . x) (#) g) - ((g . x) (#) f)) by A23; then A33: x0 in (dom ((f . x) (#) g)) /\ (dom ((g . x) (#) f)) by VALUED_1:12; then A34: x0 in dom ((f . x) (#) g) by XBOOLE_0:def_4; A35: x in dom ((g . x) (#) f) by A30, XBOOLE_0:def_4; A36: (((f . x) (#) g) - ((g . x) (#) f)) . x = (((f . x) (#) g) . x) - (((g . x) (#) f) . x) by A23, A29, VALUED_1:13 .= ((f . x) * (g . x)) - (((g . x) (#) f) . x) by A31, VALUED_1:def_5 .= ((g . x) * (f . x)) - ((g . x) * (f . x)) by A35, VALUED_1:def_5 .= 0 ; A37: x0 in dom ((g . x) (#) f) by A33, XBOOLE_0:def_4; not x in {x0} by A18, TARSKI:def_1; then A38: x in [.x,x0.] \ {x0} by A29, XBOOLE_0:def_5; N c= dom ((f . x) (#) g) by A2, VALUED_1:def_5; then A39: ].x,x0.[ c= dom ((f . x) (#) g) by A28, XBOOLE_1:1; N c= dom ((g . x) (#) f) by A1, VALUED_1:def_5; then A40: ].x,x0.[ c= dom ((g . x) (#) f) by A28, XBOOLE_1:1; then ].x,x0.[ c= (dom ((f . x) (#) g)) /\ (dom ((g . x) (#) f)) by A39, XBOOLE_1:19; then A41: ].x,x0.[ c= dom (((f . x) (#) g) - ((g . x) (#) f)) by VALUED_1:12; f is_differentiable_on ].x,x0.[ by A3, A21, A27, FDIFF_1:26, XBOOLE_1:1; then A42: (g . x) (#) f is_differentiable_on ].x,x0.[ by A40, FDIFF_1:20; g is_differentiable_on ].x,x0.[ by A4, A21, A27, FDIFF_1:26, XBOOLE_1:1; then A43: (f . x) (#) g is_differentiable_on ].x,x0.[ by A39, FDIFF_1:20; (((f . x) (#) g) - ((g . x) (#) f)) . x0 = (((f . x) (#) g) . x0) - (((g . x) (#) f) . x0) by A23, A32, VALUED_1:13 .= ((f . x) * (g . x0)) - (((g . x) (#) f) . x0) by A34, VALUED_1:def_5 .= 0 - ((g . x) * 0) by A7, A37, VALUED_1:def_5 .= 0 ; then consider t being Real such that A44: t in ].x,x0.[ and A45: diff ((((f . x) (#) g) - ((g . x) (#) f)),t) = 0 by A18, A26, A42, A41, A43, A23, A36, FDIFF_1:19, ROLLE:1; A46: (g . x) (#) f is_differentiable_in t by A42, A44, FDIFF_1:9; A47: f is_differentiable_in t by A3, A28, A44, FDIFF_1:9; (f . x) (#) g is_differentiable_in t by A43, A44, FDIFF_1:9; then 0 = (diff (((f . x) (#) g),t)) - (diff (((g . x) (#) f),t)) by A45, A46, FDIFF_1:14; then A48: 0 = (diff (((f . x) (#) g),t)) - ((g . x) * (diff (f,t))) by A47, FDIFF_1:15; take t ; ::_thesis: ( t in ].x,x0.[ & (f / g) . x = ((f `| N) / (g `| N)) . t ) A49: t in [.x,x0.] by A27, A44; [.x,x0.] \ {x0} c= N \ {x0} by A21, XBOOLE_1:33; then A50: [.x,x0.] \ {x0} c= dom (f / g) by A5, XBOOLE_1:1; then [.x,x0.] \ {x0} c= (dom f) /\ ((dom g) \ (g " {0})) by RFUNCT_1:def_1; then [.x,x0.] \ {x0} c= (dom g) \ (g " {0}) by A16, XBOOLE_1:1; then A51: ( x in dom g & not x in g " {0} ) by A38, XBOOLE_0:def_5; A52: now__::_thesis:_not_g_._x_=_0 assume g . x = 0 ; ::_thesis: contradiction then g . x in {0} by TARSKI:def_1; hence contradiction by A51, FUNCT_1:def_7; ::_thesis: verum 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_1; 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__::_thesis:_not_diff_(g,t)_=_0 assume diff (g,t) = 0 ; ::_thesis: contradiction then (g `| N) . t = 0 by A4, A21, A49, FDIFF_1:def_7; then (g `| N) . t in {0} by TARSKI:def_1; hence contradiction by A54, FUNCT_1:def_7; ::_thesis: verum end; g is_differentiable_in t by A4, A28, A44, FDIFF_1:9; then 0 = ((f . x) * (diff (g,t))) - ((g . x) * (diff (f,t))) by A48, FDIFF_1:15; then (f . x) / (g . x) = (diff (f,t)) / (diff (g,t)) by A52, A55, 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 A50, A38, RFUNCT_1:def_1; then (f / g) . x = ((f `| N) . t) * ((diff (g,t)) ") by A3, A21, A49, FDIFF_1:def_7; then (f / g) . x = ((f `| N) . t) * (((g `| N) . t) ") by A4, A21, A49, FDIFF_1:def_7; hence ( t in ].x,x0.[ & (f / g) . x = ((f `| N) / (g `| N)) . t ) by A44, A53, A49, RFUNCT_1:def_1; ::_thesis: verum 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: ( a is convergent & lim a = x0 & rng a c= (dom (f / g)) /\ (left_open_halfline x0) implies (f / g) /* a is divergent_to+infty ) assume that A57: a is convergent and A58: lim a = x0 and A59: rng a c= (dom (f / g)) /\ (left_open_halfline x0) ; ::_thesis: (f / g) /* a is divergent_to+infty 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 S1[ Element of NAT , real number ] means ( $2 in ].((a ^\ k) . $1),x0.[ & (((f / g) /* a) ^\ k) . $1 = ((f `| N) / (g `| N)) . $2 ); A61: now__::_thesis:_for_n_being_Element_of_NAT_holds_ (_(a_^\_k)_._n_<_x0_&_x0_-_r_<_(a_^\_k)_._n_) let n be Element of NAT ; ::_thesis: ( (a ^\ k) . n < x0 & x0 - r < (a ^\ k) . n ) 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: x0 - r < (a ^\ k) . n ( (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: verum end; A62: 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] 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: S1[n,c] 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:108, XBOOLE_1:1; hence S1[n,c] by A59, A64, A66, VALUED_0:27, XBOOLE_1:1; ::_thesis: verum end; consider b being Real_Sequence such that A67: for n being Element of NAT holds S1[n,b . n] from FUNCT_2:sch_3(A62); A68: now__::_thesis:_for_n_being_Element_of_NAT_holds_ (_(a_^\_k)_._n_<=_b_._n_&_b_._n_<=_d_._n_) let n be Element of NAT ; ::_thesis: ( (a ^\ k) . n <= b . n & b . n <= d . n ) 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:7; ::_thesis: verum end; A69: lim d = d . 0 by SEQ_4:26 .= x0 by FUNCOP_1:7 ; A70: 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 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: ( 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 A73: x = b . n by FUNCT_2:113; (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: verum end; A77: (dom ((f `| N) / (g `| N))) \ {x0} c= dom ((f `| N) / (g `| N)) by XBOOLE_1:36; A78: now__::_thesis:_for_n_being_Element_of_NAT_holds_(((f_`|_N)_/_(g_`|_N))_/*_b)_._n_<=_(((f_/_g)_/*_a)_^\_k)_._n let n be Element of NAT ; ::_thesis: (((f `| N) / (g `| N)) /* b) . n <= (((f / g) /* a) ^\ k) . n (((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:108, XBOOLE_1:1; ::_thesis: verum end; lim (a ^\ k) = x0 by A57, A58, SEQ_4:20; then ( b is convergent & lim b = x0 ) by A57, A69, A68, SEQ_2:19, SEQ_2:20; 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:42; hence (f / g) /* a is divergent_to+infty by LIMFUNC1:7; ::_thesis: verum 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 A82: x0 - r < x0 by A9, XREAL_1:44; x0 + 0 < x0 + r by A9, XREAL_1:8; then x0 in { g1 where g1 is Real : ( x0 - r < g1 & g1 < x0 + r ) } by A82; then A83: x0 in ].(x0 - r),(x0 + r).[ by RCOMP_1:def_2; A84: (dom (f `| N)) /\ ((dom (g `| N)) \ ((g `| N) " {0})) c= (dom (g `| N)) \ ((g `| N) " {0}) by XBOOLE_1:17; A85: (dom f) /\ ((dom g) \ (g " {0})) c= (dom g) \ (g " {0}) by XBOOLE_1:17; 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 that A86: x0 < x and A87: x < x0 + r ; ::_thesis: ex c being Real st ( c in ].x0,x.[ & (f / g) . x = ((f `| N) / (g `| N)) . c ) set f1 = ((f . x) (#) g) - ((g . x) (#) f); A88: ( dom ((f . x) (#) g) = dom g & dom ((g . x) (#) f) = dom f ) by VALUED_1:def_5; x0 - r < x by A86, A82, XXREAL_0:2; then x in { g1 where g1 is Real : ( x0 - r < g1 & g1 < x0 + r ) } by A87; then x in ].(x0 - r),(x0 + r).[ by RCOMP_1:def_2; then A89: [.x0,x.] c= N by A10, A83, XXREAL_2:def_12; then ( [.x0,x.] c= dom f & [.x0,x.] c= dom g ) by A1, A2, XBOOLE_1:1; then A90: [.x0,x.] c= (dom f) /\ (dom g) by XBOOLE_1:19; then A91: [.x0,x.] c= dom (((f . x) (#) g) - ((g . x) (#) f)) by A88, VALUED_1:12; g | N is continuous by A4, FDIFF_1:25; then g | [.x0,x.] is continuous by A89, FCONT_1:16; then A92: ((f . x) (#) g) | [.x0,x.] is continuous by A2, A89, FCONT_1:20, XBOOLE_1:1; f | N is continuous by A3, FDIFF_1:25; then f | [.x0,x.] is continuous by A89, FCONT_1:16; then ((g . x) (#) f) | [.x0,x.] is continuous by A1, A89, FCONT_1:20, XBOOLE_1:1; then A93: (((f . x) (#) g) - ((g . x) (#) f)) | [.x0,x.] is continuous by A90, A88, A92, FCONT_1:18; A94: ].x0,x.[ c= [.x0,x.] by XXREAL_1:25; then A95: ].x0,x.[ c= N by A89, XBOOLE_1:1; A96: x in [.x0,x.] by A86, XXREAL_1:1; then x in dom (((f . x) (#) g) - ((g . x) (#) f)) by A91; then A97: x in (dom ((f . x) (#) g)) /\ (dom ((g . x) (#) f)) by VALUED_1:12; then A98: x in dom ((f . x) (#) g) by XBOOLE_0:def_4; A99: x0 in [.x0,x.] by A86, XXREAL_1:1; then x0 in dom (((f . x) (#) g) - ((g . x) (#) f)) by A91; then A100: x0 in (dom ((f . x) (#) g)) /\ (dom ((g . x) (#) f)) by VALUED_1:12; then A101: x0 in dom ((f . x) (#) g) by XBOOLE_0:def_4; A102: x in dom ((g . x) (#) f) by A97, XBOOLE_0:def_4; A103: (((f . x) (#) g) - ((g . x) (#) f)) . x = (((f . x) (#) g) . x) - (((g . x) (#) f) . x) by A91, A96, VALUED_1:13 .= ((f . x) * (g . x)) - (((g . x) (#) f) . x) by A98, VALUED_1:def_5 .= ((g . x) * (f . x)) - ((g . x) * (f . x)) by A102, VALUED_1:def_5 .= 0 ; A104: x0 in dom ((g . x) (#) f) by A100, XBOOLE_0:def_4; not x in {x0} by A86, TARSKI:def_1; then A105: x in [.x0,x.] \ {x0} by A96, XBOOLE_0:def_5; N c= dom ((f . x) (#) g) by A2, VALUED_1:def_5; then A106: ].x0,x.[ c= dom ((f . x) (#) g) by A95, XBOOLE_1:1; N c= dom ((g . x) (#) f) by A1, VALUED_1:def_5; then A107: ].x0,x.[ c= dom ((g . x) (#) f) by A95, XBOOLE_1:1; then ].x0,x.[ c= (dom ((f . x) (#) g)) /\ (dom ((g . x) (#) f)) by A106, XBOOLE_1:19; then A108: ].x0,x.[ c= dom (((f . x) (#) g) - ((g . x) (#) f)) by VALUED_1:12; f is_differentiable_on ].x0,x.[ by A3, A89, A94, FDIFF_1:26, XBOOLE_1:1; then A109: (g . x) (#) f is_differentiable_on ].x0,x.[ by A107, FDIFF_1:20; g is_differentiable_on ].x0,x.[ by A4, A89, A94, FDIFF_1:26, XBOOLE_1:1; then A110: (f . x) (#) g is_differentiable_on ].x0,x.[ by A106, FDIFF_1:20; (((f . x) (#) g) - ((g . x) (#) f)) . x0 = (((f . x) (#) g) . x0) - (((g . x) (#) f) . x0) by A91, A99, VALUED_1:13 .= ((f . x) * (g . x0)) - (((g . x) (#) f) . x0) by A101, VALUED_1:def_5 .= 0 - ((g . x) * 0) by A7, A104, VALUED_1:def_5 .= 0 ; then consider t being Real such that A111: t in ].x0,x.[ and A112: diff ((((f . x) (#) g) - ((g . x) (#) f)),t) = 0 by A86, A93, A109, A108, A110, A91, A103, FDIFF_1:19, ROLLE:1; A113: (g . x) (#) f is_differentiable_in t by A109, A111, FDIFF_1:9; A114: f is_differentiable_in t by A3, A95, A111, FDIFF_1:9; (f . x) (#) g is_differentiable_in t by A110, A111, FDIFF_1:9; then 0 = (diff (((f . x) (#) g),t)) - (diff (((g . x) (#) f),t)) by A112, A113, FDIFF_1:14; then A115: 0 = (diff (((f . x) (#) g),t)) - ((g . x) * (diff (f,t))) by A114, FDIFF_1:15; take t ; ::_thesis: ( t in ].x0,x.[ & (f / g) . x = ((f `| N) / (g `| N)) . t ) A116: t in [.x0,x.] by A94, A111; [.x0,x.] \ {x0} c= N \ {x0} by A89, XBOOLE_1:33; then A117: [.x0,x.] \ {x0} c= dom (f / g) by A5, XBOOLE_1:1; then [.x0,x.] \ {x0} c= (dom f) /\ ((dom g) \ (g " {0})) by RFUNCT_1:def_1; then [.x0,x.] \ {x0} c= (dom g) \ (g " {0}) by A85, XBOOLE_1:1; then A118: ( x in dom g & not x in g " {0} ) by A105, XBOOLE_0:def_5; A119: now__::_thesis:_not_g_._x_=_0 assume g . x = 0 ; ::_thesis: contradiction then g . x in {0} by TARSKI:def_1; hence contradiction by A118, FUNCT_1:def_7; ::_thesis: verum 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_1; 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__::_thesis:_not_diff_(g,t)_=_0 assume diff (g,t) = 0 ; ::_thesis: contradiction then (g `| N) . t = 0 by A4, A89, A116, FDIFF_1:def_7; then (g `| N) . t in {0} by TARSKI:def_1; hence contradiction by A121, FUNCT_1:def_7; ::_thesis: verum end; g is_differentiable_in t by A4, A95, A111, FDIFF_1:9; then 0 = ((f . x) * (diff (g,t))) - ((g . x) * (diff (f,t))) by A115, FDIFF_1:15; then (f . x) / (g . x) = (diff (f,t)) / (diff (g,t)) by A119, A122, 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 A117, A105, RFUNCT_1:def_1; then (f / g) . x = ((f `| N) . t) * ((diff (g,t)) ") by A3, A89, A116, FDIFF_1:def_7; then (f / g) . x = ((f `| N) . t) * (((g `| N) . t) ") by A4, A89, A116, FDIFF_1:def_7; hence ( t in ].x0,x.[ & (f / g) . x = ((f `| N) / (g `| N)) . t ) by A111, A120, A116, RFUNCT_1:def_1; ::_thesis: verum 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: ( a is convergent & lim a = x0 & rng a c= (dom (f / g)) /\ (right_open_halfline x0) implies (f / g) /* a is divergent_to+infty ) assume that A124: a is convergent and A125: lim a = x0 and A126: rng a c= (dom (f / g)) /\ (right_open_halfline x0) ; ::_thesis: (f / g) /* a is divergent_to+infty 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 S1[ Element of NAT , real number ] means ( $2 in ].x0,((a ^\ k) . $1).[ & (((f / g) /* a) ^\ k) . $1 = ((f `| N) / (g `| N)) . $2 ); A128: now__::_thesis:_for_n_being_Element_of_NAT_holds_ (_x0_<_(a_^\_k)_._n_&_(a_^\_k)_._n_<_x0_+_r_) let n be Element of NAT ; ::_thesis: ( x0 < (a ^\ k) . n & (a ^\ k) . n < x0 + r ) 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 < x0 + r ( (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: verum end; A129: 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] 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: S1[n,c] 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:108, XBOOLE_1:1; hence S1[n,c] by A126, A131, A133, VALUED_0:27, XBOOLE_1:1; ::_thesis: verum end; consider b being Real_Sequence such that A134: for n being Element of NAT holds S1[n,b . n] from FUNCT_2:sch_3(A129); A135: now__::_thesis:_for_n_being_Element_of_NAT_holds_ (_d_._n_<=_b_._n_&_b_._n_<=_(a_^\_k)_._n_) let n be Element of NAT ; ::_thesis: ( d . n <= b . n & b . n <= (a ^\ k) . n ) 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:7; ::_thesis: verum end; A136: lim d = d . 0 by SEQ_4:26 .= x0 by FUNCOP_1:7 ; A137: 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 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: ( 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:113; 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: verum end; A144: (dom ((f `| N) / (g `| N))) \ {x0} c= dom ((f `| N) / (g `| N)) by XBOOLE_1:36; A145: now__::_thesis:_for_n_being_Element_of_NAT_holds_(((f_`|_N)_/_(g_`|_N))_/*_b)_._n_<=_(((f_/_g)_/*_a)_^\_k)_._n let n be Element of NAT ; ::_thesis: (((f `| N) / (g `| N)) /* b) . n <= (((f / g) /* a) ^\ k) . n (((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:108, XBOOLE_1:1; ::_thesis: verum end; lim (a ^\ k) = x0 by A124, A125, SEQ_4:20; then ( b is convergent & lim b = x0 ) by A124, A136, A135, SEQ_2:19, SEQ_2:20; 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:42; hence (f / g) /* a is divergent_to+infty by LIMFUNC1:7; ::_thesis: verum 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:12; ::_thesis: verum end; theorem :: L_HOSPIT:6 for f, g being PartFunc of REAL,REAL 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_divergent_to-infty_in x0 ) holds f / g is_divergent_to-infty_in x0 proof 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_divergent_to-infty_in x0 ) holds f / g is_divergent_to-infty_in 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_divergent_to-infty_in x0 ) implies f / g is_divergent_to-infty_in x0 ) 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: f / g is_divergent_to-infty_in x0 consider r being real number such that A9: 0 < r and A10: N = ].(x0 - r),(x0 + r).[ by RCOMP_1:def_6; 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 A13: x0 + 0 < x0 + r by A9, XREAL_1:8; x0 - r < x0 by A9, XREAL_1:44; then x0 in { g1 where g1 is Real : ( x0 - r < g1 & g1 < x0 + r ) } by A13; then A14: x0 in ].(x0 - r),(x0 + r).[ by RCOMP_1:def_2; A15: (dom (f `| N)) /\ ((dom (g `| N)) \ ((g `| N) " {0})) c= (dom (g `| N)) \ ((g `| N) " {0}) by XBOOLE_1:17; A16: (dom f) /\ ((dom g) \ (g " {0})) c= (dom g) \ (g " {0}) by XBOOLE_1:17; 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 that A17: x0 - r < x and A18: x < x0 ; ::_thesis: ex c being Real st ( c in ].x,x0.[ & (f / g) . x = ((f `| N) / (g `| N)) . c ) set f1 = ((f . x) (#) g) - ((g . x) (#) f); A19: ( dom ((f . x) (#) g) = dom g & dom ((g . x) (#) f) = dom f ) by VALUED_1:def_5; then A20: dom (((f . x) (#) g) - ((g . x) (#) f)) = (dom f) /\ (dom g) by VALUED_1:12; x < x0 + r by A18, A13, XXREAL_0:2; then x in { g1 where g1 is Real : ( x0 - r < g1 & g1 < x0 + r ) } by A17; then x in ].(x0 - r),(x0 + r).[ by RCOMP_1:def_2; then A21: [.x,x0.] c= N by A10, A14, XXREAL_2:def_12; then A22: ( [.x,x0.] c= dom f & [.x,x0.] c= dom g ) by A1, A2, XBOOLE_1:1; then A23: [.x,x0.] c= dom (((f . x) (#) g) - ((g . x) (#) f)) by A20, XBOOLE_1:19; g | N is continuous by A4, FDIFF_1:25; then g | [.x,x0.] is continuous by A21, FCONT_1:16; then A24: ((f . x) (#) g) | [.x,x0.] is continuous by A2, A21, FCONT_1:20, XBOOLE_1:1; f | N is continuous by A3, FDIFF_1:25; then f | [.x,x0.] is continuous by A21, FCONT_1:16; then A25: ((g . x) (#) f) | [.x,x0.] is continuous by A1, A21, FCONT_1:20, XBOOLE_1:1; [.x,x0.] c= dom (((f . x) (#) g) - ((g . x) (#) f)) by A22, A20, XBOOLE_1:19; then A26: (((f . x) (#) g) - ((g . x) (#) f)) | [.x,x0.] is continuous by A19, A20, A25, A24, FCONT_1:18; A27: ].x,x0.[ c= [.x,x0.] by XXREAL_1:25; then A28: ].x,x0.[ c= N by A21, XBOOLE_1:1; A29: x in [.x,x0.] by A18, XXREAL_1:1; then x in dom (((f . x) (#) g) - ((g . x) (#) f)) by A23; then A30: x in (dom ((f . x) (#) g)) /\ (dom ((g . x) (#) f)) by VALUED_1:12; then A31: x in dom ((f . x) (#) g) by XBOOLE_0:def_4; A32: x0 in [.x,x0.] by A18, XXREAL_1:1; then x0 in dom (((f . x) (#) g) - ((g . x) (#) f)) by A23; then A33: x0 in (dom ((f . x) (#) g)) /\ (dom ((g . x) (#) f)) by VALUED_1:12; then A34: x0 in dom ((f . x) (#) g) by XBOOLE_0:def_4; A35: x in dom ((g . x) (#) f) by A30, XBOOLE_0:def_4; A36: (((f . x) (#) g) - ((g . x) (#) f)) . x = (((f . x) (#) g) . x) - (((g . x) (#) f) . x) by A23, A29, VALUED_1:13 .= ((f . x) * (g . x)) - (((g . x) (#) f) . x) by A31, VALUED_1:def_5 .= ((g . x) * (f . x)) - ((g . x) * (f . x)) by A35, VALUED_1:def_5 .= 0 ; A37: x0 in dom ((g . x) (#) f) by A33, XBOOLE_0:def_4; not x in {x0} by A18, TARSKI:def_1; then A38: x in [.x,x0.] \ {x0} by A29, XBOOLE_0:def_5; N c= dom ((f . x) (#) g) by A2, VALUED_1:def_5; then A39: ].x,x0.[ c= dom ((f . x) (#) g) by A28, XBOOLE_1:1; N c= dom ((g . x) (#) f) by A1, VALUED_1:def_5; then A40: ].x,x0.[ c= dom ((g . x) (#) f) by A28, XBOOLE_1:1; then ].x,x0.[ c= (dom ((f . x) (#) g)) /\ (dom ((g . x) (#) f)) by A39, XBOOLE_1:19; then A41: ].x,x0.[ c= dom (((f . x) (#) g) - ((g . x) (#) f)) by VALUED_1:12; f is_differentiable_on ].x,x0.[ by A3, A21, A27, FDIFF_1:26, XBOOLE_1:1; then A42: (g . x) (#) f is_differentiable_on ].x,x0.[ by A40, FDIFF_1:20; g is_differentiable_on ].x,x0.[ by A4, A21, A27, FDIFF_1:26, XBOOLE_1:1; then A43: (f . x) (#) g is_differentiable_on ].x,x0.[ by A39, FDIFF_1:20; (((f . x) (#) g) - ((g . x) (#) f)) . x0 = (((f . x) (#) g) . x0) - (((g . x) (#) f) . x0) by A23, A32, VALUED_1:13 .= ((f . x) * (g . x0)) - (((g . x) (#) f) . x0) by A34, VALUED_1:def_5 .= 0 - ((g . x) * 0) by A7, A37, VALUED_1:def_5 .= 0 ; then consider t being Real such that A44: t in ].x,x0.[ and A45: diff ((((f . x) (#) g) - ((g . x) (#) f)),t) = 0 by A18, A26, A42, A41, A43, A23, A36, FDIFF_1:19, ROLLE:1; A46: (g . x) (#) f is_differentiable_in t by A42, A44, FDIFF_1:9; A47: f is_differentiable_in t by A3, A28, A44, FDIFF_1:9; (f . x) (#) g is_differentiable_in t by A43, A44, FDIFF_1:9; then 0 = (diff (((f . x) (#) g),t)) - (diff (((g . x) (#) f),t)) by A45, A46, FDIFF_1:14; then A48: 0 = (diff (((f . x) (#) g),t)) - ((g . x) * (diff (f,t))) by A47, FDIFF_1:15; take t ; ::_thesis: ( t in ].x,x0.[ & (f / g) . x = ((f `| N) / (g `| N)) . t ) A49: t in [.x,x0.] by A27, A44; [.x,x0.] \ {x0} c= N \ {x0} by A21, XBOOLE_1:33; then A50: [.x,x0.] \ {x0} c= dom (f / g) by A5, XBOOLE_1:1; then [.x,x0.] \ {x0} c= (dom f) /\ ((dom g) \ (g " {0})) by RFUNCT_1:def_1; then [.x,x0.] \ {x0} c= (dom g) \ (g " {0}) by A16, XBOOLE_1:1; then A51: ( x in dom g & not x in g " {0} ) by A38, XBOOLE_0:def_5; A52: now__::_thesis:_not_g_._x_=_0 assume g . x = 0 ; ::_thesis: contradiction then g . x in {0} by TARSKI:def_1; hence contradiction by A51, FUNCT_1:def_7; ::_thesis: verum 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_1; 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__::_thesis:_not_diff_(g,t)_=_0 assume diff (g,t) = 0 ; ::_thesis: contradiction then (g `| N) . t = 0 by A4, A21, A49, FDIFF_1:def_7; then (g `| N) . t in {0} by TARSKI:def_1; hence contradiction by A54, FUNCT_1:def_7; ::_thesis: verum end; g is_differentiable_in t by A4, A28, A44, FDIFF_1:9; then 0 = ((f . x) * (diff (g,t))) - ((g . x) * (diff (f,t))) by A48, FDIFF_1:15; then (f . x) / (g . x) = (diff (f,t)) / (diff (g,t)) by A52, A55, 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 A50, A38, RFUNCT_1:def_1; then (f / g) . x = ((f `| N) . t) * ((diff (g,t)) ") by A3, A21, A49, FDIFF_1:def_7; then (f / g) . x = ((f `| N) . t) * (((g `| N) . t) ") by A4, A21, A49, FDIFF_1:def_7; hence ( t in ].x,x0.[ & (f / g) . x = ((f `| N) / (g `| N)) . t ) by A44, A53, A49, RFUNCT_1:def_1; ::_thesis: verum 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: ( a is convergent & lim a = x0 & rng a c= (dom (f / g)) /\ (left_open_halfline x0) implies (f / g) /* a is divergent_to-infty ) assume that A57: a is convergent and A58: lim a = x0 and A59: rng a c= (dom (f / g)) /\ (left_open_halfline x0) ; ::_thesis: (f / g) /* a is divergent_to-infty 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 S1[ Element of NAT , real number ] means ( $2 in ].((a ^\ k) . $1),x0.[ & (((f / g) /* a) ^\ k) . $1 = ((f `| N) / (g `| N)) . $2 ); A61: now__::_thesis:_for_n_being_Element_of_NAT_holds_ (_(a_^\_k)_._n_<_x0_&_x0_-_r_<_(a_^\_k)_._n_) let n be Element of NAT ; ::_thesis: ( (a ^\ k) . n < x0 & x0 - r < (a ^\ k) . n ) 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: x0 - r < (a ^\ k) . n ( (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: verum end; A62: 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] 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: S1[n,c] 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:108, XBOOLE_1:1; hence S1[n,c] by A59, A64, A66, VALUED_0:27, XBOOLE_1:1; ::_thesis: verum end; consider b being Real_Sequence such that A67: for n being Element of NAT holds S1[n,b . n] from FUNCT_2:sch_3(A62); A68: now__::_thesis:_for_n_being_Element_of_NAT_holds_ (_(a_^\_k)_._n_<=_b_._n_&_b_._n_<=_d_._n_) let n be Element of NAT ; ::_thesis: ( (a ^\ k) . n <= b . n & b . n <= d . n ) 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:7; ::_thesis: verum end; A69: lim d = d . 0 by SEQ_4:26 .= x0 by FUNCOP_1:7 ; A70: 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 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: ( 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 A73: x = b . n by FUNCT_2:113; (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: verum end; A77: (dom ((f `| N) / (g `| N))) \ {x0} c= dom ((f `| N) / (g `| N)) by XBOOLE_1:36; A78: now__::_thesis:_for_n_being_Element_of_NAT_holds_(((f_/_g)_/*_a)_^\_k)_._n_<=_(((f_`|_N)_/_(g_`|_N))_/*_b)_._n let n be Element of NAT ; ::_thesis: (((f / g) /* a) ^\ k) . n <= (((f `| N) / (g `| N)) /* b) . n (((f / g) /* a) ^\ k) . n = ((f `| N) / (g `| N)) . (b . n) by A67; hence (((f / g) /* a) ^\ k) . n <= (((f `| N) / (g `| N)) /* b) . n by A72, A77, FUNCT_2:108, XBOOLE_1:1; ::_thesis: verum end; lim (a ^\ k) = x0 by A57, A58, SEQ_4:20; then ( b is convergent & lim b = x0 ) by A57, A69, A68, SEQ_2:19, SEQ_2:20; then ((f `| N) / (g `| N)) /* b is divergent_to-infty by A8, A72, LIMFUNC3:def_3; then ((f / g) /* a) ^\ k is divergent_to-infty by A78, LIMFUNC1:43; hence (f / g) /* a is divergent_to-infty by LIMFUNC1:7; ::_thesis: verum 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_3; 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 A82: (dom (f `| N)) /\ ((dom (g `| N)) \ ((g `| N) " {0})) c= (dom (g `| N)) \ ((g `| N) " {0}) by XBOOLE_1:17; A83: x0 - r < x0 by A9, XREAL_1:44; x0 + 0 < x0 + r by A9, XREAL_1:8; then x0 in { g1 where g1 is Real : ( x0 - r < g1 & g1 < x0 + r ) } by A83; then A84: x0 in ].(x0 - r),(x0 + r).[ by RCOMP_1:def_2; 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 that A85: x0 < x and A86: x < x0 + r ; ::_thesis: ex c being Real st ( c in ].x0,x.[ & (f / g) . x = ((f `| N) / (g `| N)) . c ) x0 - r < x by A85, A83, XXREAL_0:2; then x in { g1 where g1 is Real : ( x0 - r < g1 & g1 < x0 + r ) } by A86; then x in ].(x0 - r),(x0 + r).[ by RCOMP_1:def_2; then A87: [.x0,x.] c= N by A10, A84, XXREAL_2:def_12; then A88: ( [.x0,x.] c= dom f & [.x0,x.] c= dom g ) by A1, A2, XBOOLE_1:1; g | N is continuous by A4, FDIFF_1:25; then g | [.x0,x.] is continuous by A87, FCONT_1:16; then A89: ((f . x) (#) g) | [.x0,x.] is continuous by A2, A87, FCONT_1:20, XBOOLE_1:1; f | N is continuous by A3, FDIFF_1:25; then f | [.x0,x.] is continuous by A87, FCONT_1:16; then A90: ((g . x) (#) f) | [.x0,x.] is continuous by A1, A87, FCONT_1:20, XBOOLE_1:1; A91: ( dom ((f . x) (#) g) = dom g & dom ((g . x) (#) f) = dom f ) by VALUED_1:def_5; then A92: dom (((f . x) (#) g) - ((g . x) (#) f)) = (dom f) /\ (dom g) by VALUED_1:12; then [.x0,x.] c= dom (((f . x) (#) g) - ((g . x) (#) f)) by A88, XBOOLE_1:19; then A93: (((f . x) (#) g) - ((g . x) (#) f)) | [.x0,x.] is continuous by A91, A92, A90, A89, FCONT_1:18; A94: ].x0,x.[ c= [.x0,x.] by XXREAL_1:25; then A95: ].x0,x.[ c= N by A87, XBOOLE_1:1; N c= dom ((f . x) (#) g) by A2, VALUED_1:def_5; then A96: ].x0,x.[ c= dom ((f . x) (#) g) by A95, XBOOLE_1:1; g is_differentiable_on ].x0,x.[ by A4, A87, A94, FDIFF_1:26, XBOOLE_1:1; then A97: (f . x) (#) g is_differentiable_on ].x0,x.[ by A96, FDIFF_1:20; N c= dom ((g . x) (#) f) by A1, VALUED_1:def_5; then A98: ].x0,x.[ c= dom ((g . x) (#) f) by A95, XBOOLE_1:1; then ].x0,x.[ c= (dom ((f . x) (#) g)) /\ (dom ((g . x) (#) f)) by A96, XBOOLE_1:19; then A99: ].x0,x.[ c= dom (((f . x) (#) g) - ((g . x) (#) f)) by VALUED_1:12; f is_differentiable_on ].x0,x.[ by A3, A87, A94, FDIFF_1:26, XBOOLE_1:1; then A100: (g . x) (#) f is_differentiable_on ].x0,x.[ by A98, FDIFF_1:20; set f1 = ((f . x) (#) g) - ((g . x) (#) f); A101: (dom f) /\ ((dom g) \ (g " {0})) c= (dom g) \ (g " {0}) by XBOOLE_1:17; ( dom ((f . x) (#) g) = dom g & dom ((g . x) (#) f) = dom f ) by VALUED_1:def_5; then dom (((f . x) (#) g) - ((g . x) (#) f)) = (dom f) /\ (dom g) by VALUED_1:12; then A102: [.x0,x.] c= dom (((f . x) (#) g) - ((g . x) (#) f)) by A88, XBOOLE_1:19; A103: x in [.x0,x.] by A85, XXREAL_1:1; then x in dom (((f . x) (#) g) - ((g . x) (#) f)) by A102; then A104: x in (dom ((f . x) (#) g)) /\ (dom ((g . x) (#) f)) by VALUED_1:12; then A105: x in dom ((f . x) (#) g) by XBOOLE_0:def_4; A106: x0 in [.x0,x.] by A85, XXREAL_1:1; then x0 in dom (((f . x) (#) g) - ((g . x) (#) f)) by A102; then A107: x0 in (dom ((f . x) (#) g)) /\ (dom ((g . x) (#) f)) by VALUED_1:12; then A108: x0 in dom ((f . x) (#) g) by XBOOLE_0:def_4; A109: x in dom ((g . x) (#) f) by A104, XBOOLE_0:def_4; A110: (((f . x) (#) g) - ((g . x) (#) f)) . x = (((f . x) (#) g) . x) - (((g . x) (#) f) . x) by A102, A103, VALUED_1:13 .= ((f . x) * (g . x)) - (((g . x) (#) f) . x) by A105, VALUED_1:def_5 .= ((g . x) * (f . x)) - ((g . x) * (f . x)) by A109, VALUED_1:def_5 .= 0 ; A111: x0 in dom ((g . x) (#) f) by A107, XBOOLE_0:def_4; not x in {x0} by A85, TARSKI:def_1; then A112: x in [.x0,x.] \ {x0} by A103, XBOOLE_0:def_5; (((f . x) (#) g) - ((g . x) (#) f)) . x0 = (((f . x) (#) g) . x0) - (((g . x) (#) f) . x0) by A102, A106, VALUED_1:13 .= ((f . x) * (g . x0)) - (((g . x) (#) f) . x0) by A108, VALUED_1:def_5 .= 0 - ((g . x) * 0) by A7, A111, VALUED_1:def_5 .= 0 ; then consider t being Real such that A113: t in ].x0,x.[ and A114: diff ((((f . x) (#) g) - ((g . x) (#) f)),t) = 0 by A85, A93, A100, A99, A97, A102, A110, FDIFF_1:19, ROLLE:1; A115: (g . x) (#) f is_differentiable_in t by A100, A113, FDIFF_1:9; A116: f is_differentiable_in t by A3, A95, A113, FDIFF_1:9; (f . x) (#) g is_differentiable_in t by A97, A113, FDIFF_1:9; then 0 = (diff (((f . x) (#) g),t)) - (diff (((g . x) (#) f),t)) by A114, A115, FDIFF_1:14; then A117: 0 = (diff (((f . x) (#) g),t)) - ((g . x) * (diff (f,t))) by A116, FDIFF_1:15; take t ; ::_thesis: ( t in ].x0,x.[ & (f / g) . x = ((f `| N) / (g `| N)) . t ) A118: t in [.x0,x.] by A94, A113; [.x0,x.] \ {x0} c= N \ {x0} by A87, XBOOLE_1:33; then A119: [.x0,x.] \ {x0} c= dom (f / g) by A5, XBOOLE_1:1; then [.x0,x.] \ {x0} c= (dom f) /\ ((dom g) \ (g " {0})) by RFUNCT_1:def_1; then [.x0,x.] \ {x0} c= (dom g) \ (g " {0}) by A101, XBOOLE_1:1; then A120: ( x in dom g & not x in g " {0} ) by A112, XBOOLE_0:def_5; A121: now__::_thesis:_not_g_._x_=_0 assume g . x = 0 ; ::_thesis: contradiction then g . x in {0} by TARSKI:def_1; hence contradiction by A120, FUNCT_1:def_7; ::_thesis: verum end; A122: [.x0,x.] c= dom ((f `| N) / (g `| N)) by A6, A87, XBOOLE_1:1; 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 A82, XBOOLE_1:1; then A123: ( t in dom (g `| N) & not t in (g `| N) " {0} ) by A118, XBOOLE_0:def_5; A124: now__::_thesis:_not_diff_(g,t)_=_0 assume diff (g,t) = 0 ; ::_thesis: contradiction then (g `| N) . t = 0 by A4, A87, A118, FDIFF_1:def_7; then (g `| N) . t in {0} by TARSKI:def_1; hence contradiction by A123, FUNCT_1:def_7; ::_thesis: verum end; g is_differentiable_in t by A4, A95, A113, FDIFF_1:9; then 0 = ((f . x) * (diff (g,t))) - ((g . x) * (diff (f,t))) by A117, FDIFF_1:15; then (f . x) / (g . x) = (diff (f,t)) / (diff (g,t)) by A121, A124, 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 A119, A112, RFUNCT_1:def_1; then (f / g) . x = ((f `| N) . t) * ((diff (g,t)) ") by A3, A87, A118, FDIFF_1:def_7; then (f / g) . x = ((f `| N) . t) * (((g `| N) . t) ") by A4, A87, A118, FDIFF_1:def_7; hence ( t in ].x0,x.[ & (f / g) . x = ((f `| N) / (g `| N)) . t ) by A113, A122, A118, RFUNCT_1:def_1; ::_thesis: verum end; A125: 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: ( a is convergent & lim a = x0 & rng a c= (dom (f / g)) /\ (right_open_halfline x0) implies (f / g) /* a is divergent_to-infty ) assume that A126: a is convergent and A127: lim a = x0 and A128: rng a c= (dom (f / g)) /\ (right_open_halfline x0) ; ::_thesis: (f / g) /* a is divergent_to-infty consider k being Element of NAT such that A129: for n being Element of NAT st k <= n holds ( x0 - r < a . n & a . n < x0 + r ) by A9, A11, A126, A127, LIMFUNC3:7; set a1 = a ^\ k; defpred S1[ Element of NAT , real number ] means ( $2 in ].x0,((a ^\ k) . $1).[ & (((f / g) /* a) ^\ k) . $1 = ((f `| N) / (g `| N)) . $2 ); A130: now__::_thesis:_for_n_being_Element_of_NAT_holds_ (_x0_<_(a_^\_k)_._n_&_(a_^\_k)_._n_<_x0_+_r_) let n be Element of NAT ; ::_thesis: ( x0 < (a ^\ k) . n & (a ^\ k) . n < x0 + r ) a . (n + k) in rng a by VALUED_0:28; then a . (n + k) in right_open_halfline x0 by A128, 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 ( (a ^\ k) . n = a . (n + k) & k <= n + k ) by NAT_1:12, NAT_1:def_3; hence (a ^\ k) . n < x0 + r by A129; ::_thesis: verum end; A131: 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] A132: rng (a ^\ k) c= rng a by VALUED_0:21; ( x0 < (a ^\ k) . n & (a ^\ k) . n < x0 + r ) by A130; then consider c being Real such that A133: c in ].x0,((a ^\ k) . n).[ and A134: (f / g) . ((a ^\ k) . n) = ((f `| N) / (g `| N)) . c by A81; take c ; ::_thesis: S1[n,c] A135: (dom (f / g)) /\ (right_open_halfline x0) c= dom (f / g) by XBOOLE_1:17; then rng a c= dom (f / g) by A128, XBOOLE_1:1; then ((f / g) /* (a ^\ k)) . n = ((f `| N) / (g `| N)) . c by A134, A132, FUNCT_2:108, XBOOLE_1:1; hence S1[n,c] by A128, A133, A135, VALUED_0:27, XBOOLE_1:1; ::_thesis: verum end; consider b being Real_Sequence such that A136: for n being Element of NAT holds S1[n,b . n] from FUNCT_2:sch_3(A131); A137: now__::_thesis:_for_n_being_Element_of_NAT_holds_ (_d_._n_<=_b_._n_&_b_._n_<=_(a_^\_k)_._n_) let n be Element of NAT ; ::_thesis: ( d . n <= b . n & b . n <= (a ^\ k) . n ) b . n in ].x0,((a ^\ k) . n).[ by A136; 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:7; ::_thesis: verum end; A138: lim d = d . 0 by SEQ_4:26 .= x0 by FUNCOP_1:7 ; A139: 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 A139; then A140: x0 in ].(x0 - r),(x0 + r).[ by RCOMP_1:def_2; A141: 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 A142: x = b . n by FUNCT_2:113; x0 < (a ^\ k) . n by A130; then A143: x0 - r < (a ^\ k) . n by A139, XXREAL_0:2; (a ^\ k) . n < x0 + r by A130; then (a ^\ k) . n in { g3 where g3 is Real : ( x0 - r < g3 & g3 < x0 + r ) } by A143; 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 A140, XXREAL_1:25, XXREAL_2:def_12; then ].x0,((a ^\ k) . n).[ c= ].(x0 - r),(x0 + r).[ by XBOOLE_1:1; then A144: ].x0,((a ^\ k) . n).[ c= dom ((f `| N) / (g `| N)) by A6, A10, XBOOLE_1:1; A145: x in ].x0,((a ^\ k) . n).[ by A136, A142; 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 A145, A144, XBOOLE_0:def_5; ::_thesis: verum end; A146: (dom ((f `| N) / (g `| N))) \ {x0} c= dom ((f `| N) / (g `| N)) by XBOOLE_1:36; A147: now__::_thesis:_for_n_being_Element_of_NAT_holds_(((f_/_g)_/*_a)_^\_k)_._n_<=_(((f_`|_N)_/_(g_`|_N))_/*_b)_._n let n be Element of NAT ; ::_thesis: (((f / g) /* a) ^\ k) . n <= (((f `| N) / (g `| N)) /* b) . n (((f / g) /* a) ^\ k) . n = ((f `| N) / (g `| N)) . (b . n) by A136; hence (((f / g) /* a) ^\ k) . n <= (((f `| N) / (g `| N)) /* b) . n by A141, A146, FUNCT_2:108, XBOOLE_1:1; ::_thesis: verum end; lim (a ^\ k) = x0 by A126, A127, SEQ_4:20; then ( b is convergent & lim b = x0 ) by A126, A138, A137, SEQ_2:19, SEQ_2:20; then ((f `| N) / (g `| N)) /* b is divergent_to-infty by A8, A141, LIMFUNC3:def_3; then ((f / g) /* a) ^\ k is divergent_to-infty by A147, LIMFUNC1:43; hence (f / g) /* a is divergent_to-infty by LIMFUNC1:7; ::_thesis: verum 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 A125, LIMFUNC2:def_6; hence f / g is_divergent_to-infty_in x0 by A80, LIMFUNC3:13; ::_thesis: verum end; theorem :: L_HOSPIT:7 for f, g being PartFunc of REAL,REAL for x0 being Real st x0 in (dom f) /\ (dom g) & ex r being Real st ( r > 0 & [.x0,(x0 + r).] c= dom f & [.x0,(x0 + r).] c= dom g & f is_differentiable_on ].x0,(x0 + r).[ & g is_differentiable_on ].x0,(x0 + r).[ & ].x0,(x0 + r).[ c= dom (f / g) & [.x0,(x0 + r).] c= dom ((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)) & f . x0 = 0 & g . x0 = 0 & f is_continuous_in x0 & g is_continuous_in x0 & (f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[) is_right_convergent_in x0 ) holds ( f / g is_right_convergent_in x0 & ex r being Real st ( r > 0 & lim_right ((f / g),x0) = lim_right (((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)),x0) ) ) proof let f, g be PartFunc of REAL,REAL; ::_thesis: for x0 being Real st x0 in (dom f) /\ (dom g) & ex r being Real st ( r > 0 & [.x0,(x0 + r).] c= dom f & [.x0,(x0 + r).] c= dom g & f is_differentiable_on ].x0,(x0 + r).[ & g is_differentiable_on ].x0,(x0 + r).[ & ].x0,(x0 + r).[ c= dom (f / g) & [.x0,(x0 + r).] c= dom ((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)) & f . x0 = 0 & g . x0 = 0 & f is_continuous_in x0 & g is_continuous_in x0 & (f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[) is_right_convergent_in x0 ) holds ( f / g is_right_convergent_in x0 & ex r being Real st ( r > 0 & lim_right ((f / g),x0) = lim_right (((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)),x0) ) ) let x0 be Real; ::_thesis: ( x0 in (dom f) /\ (dom g) & ex r being Real st ( r > 0 & [.x0,(x0 + r).] c= dom f & [.x0,(x0 + r).] c= dom g & f is_differentiable_on ].x0,(x0 + r).[ & g is_differentiable_on ].x0,(x0 + r).[ & ].x0,(x0 + r).[ c= dom (f / g) & [.x0,(x0 + r).] c= dom ((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)) & f . x0 = 0 & g . x0 = 0 & f is_continuous_in x0 & g is_continuous_in x0 & (f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[) is_right_convergent_in x0 ) implies ( f / g is_right_convergent_in x0 & ex r being Real st ( r > 0 & lim_right ((f / g),x0) = lim_right (((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)),x0) ) ) ) assume A1: x0 in (dom f) /\ (dom g) ; ::_thesis: ( for r being Real holds ( not r > 0 or not [.x0,(x0 + r).] c= dom f or not [.x0,(x0 + r).] c= dom g or not f is_differentiable_on ].x0,(x0 + r).[ or not g is_differentiable_on ].x0,(x0 + r).[ or not ].x0,(x0 + r).[ c= dom (f / g) or not [.x0,(x0 + r).] c= dom ((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)) or not f . x0 = 0 or not g . x0 = 0 or not f is_continuous_in x0 or not g is_continuous_in x0 or not (f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[) is_right_convergent_in x0 ) or ( f / g is_right_convergent_in x0 & ex r being Real st ( r > 0 & lim_right ((f / g),x0) = lim_right (((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)),x0) ) ) ) given r being Real such that A2: r > 0 and A3: [.x0,(x0 + r).] c= dom f and A4: [.x0,(x0 + r).] c= dom g and A5: f is_differentiable_on ].x0,(x0 + r).[ and A6: g is_differentiable_on ].x0,(x0 + r).[ and A7: ].x0,(x0 + r).[ c= dom (f / g) and A8: [.x0,(x0 + r).] c= dom ((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)) and A9: ( f . x0 = 0 & g . x0 = 0 ) and A10: f is_continuous_in x0 and A11: g is_continuous_in x0 and A12: (f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[) is_right_convergent_in x0 ; ::_thesis: ( f / g is_right_convergent_in x0 & ex r being Real st ( r > 0 & lim_right ((f / g),x0) = lim_right (((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)),x0) ) ) A13: ].x0,(x0 + r).[ c= [.x0,(x0 + r).] by XXREAL_1:25; then A14: ].x0,(x0 + r).[ c= dom g by A4, XBOOLE_1:1; A15: ].x0,(x0 + r).[ c= dom f by A3, A13, XBOOLE_1:1; A16: for x being Real st x0 < x & x < x0 + r holds ex c being Real st ( c in ].x0,x.[ & (f / g) . x = ((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)) . 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 `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)) . c ) ) assume that A17: x0 < x and A18: x < x0 + r ; ::_thesis: ex c being Real st ( c in ].x0,x.[ & (f / g) . x = ((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)) . c ) set f1 = ((f . x) (#) g) - ((g . x) (#) f); A19: dom ((g . x) (#) f) = dom f by VALUED_1:def_5; A20: dom ((f . x) (#) g) = dom g by VALUED_1:def_5; then A21: dom (((f . x) (#) g) - ((g . x) (#) f)) = (dom f) /\ (dom g) by A19, VALUED_1:12; A22: [.x0,x.] c= [.x0,(x0 + r).] proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in [.x0,x.] or y in [.x0,(x0 + r).] ) assume A23: y in [.x0,x.] ; ::_thesis: y in [.x0,(x0 + r).] then reconsider y = y as real number ; y <= x by A23, XXREAL_1:1; then A24: y <= x0 + r by A18, XXREAL_0:2; x0 <= y by A23, XXREAL_1:1; hence y in [.x0,(x0 + r).] by A24, XXREAL_1:1; ::_thesis: verum end; then A25: ( [.x0,x.] c= dom f & [.x0,x.] c= dom g ) by A3, A4, XBOOLE_1:1; then A26: [.x0,x.] c= dom (((f . x) (#) g) - ((g . x) (#) f)) by A21, XBOOLE_1:19; A27: x in [.x0,x.] by A17, XXREAL_1:1; then x in dom (((f . x) (#) g) - ((g . x) (#) f)) by A26; then A28: x in (dom ((f . x) (#) g)) /\ (dom ((g . x) (#) f)) by VALUED_1:12; then A29: x in dom ((f . x) (#) g) by XBOOLE_0:def_4; A30: x in dom ((g . x) (#) f) by A28, XBOOLE_0:def_4; A31: (((f . x) (#) g) - ((g . x) (#) f)) . x = (((f . x) (#) g) . x) - (((g . x) (#) f) . x) by A26, A27, 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 A30, VALUED_1:def_5 .= 0 ; A32: ].x0,(x0 + r).[ c= dom f by A3, A13, XBOOLE_1:1; not x in {x0} by A17, TARSKI:def_1; then A33: x in [.x0,x.] \ {x0} by A27, XBOOLE_0:def_5; x in { g1 where g1 is Real : ( x0 < g1 & g1 < x0 + r ) } by A17, A18; then A34: x in ].x0,(x0 + r).[ by RCOMP_1:def_2; A35: x0 in [.x0,x.] by A17, XXREAL_1:1; then x0 in dom (((f . x) (#) g) - ((g . x) (#) f)) by A26; then A36: x0 in (dom ((f . x) (#) g)) /\ (dom ((g . x) (#) f)) by VALUED_1:12; then A37: x0 in dom ((f . x) (#) g) by XBOOLE_0:def_4; A38: [.x0,x.] c= dom (((f . x) (#) g) - ((g . x) (#) f)) by A25, A21, XBOOLE_1:19; A39: x0 in dom ((g . x) (#) f) by A36, XBOOLE_0:def_4; A40: ].x0,(x0 + r).[ c= dom g by A4, A13, XBOOLE_1:1; A41: ].x0,x.[ c= ].x0,(x0 + r).[ proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in ].x0,x.[ or y in ].x0,(x0 + r).[ ) assume y in ].x0,x.[ ; ::_thesis: y in ].x0,(x0 + r).[ then y in { g2 where g2 is Real : ( x0 < g2 & g2 < x ) } by RCOMP_1:def_2; then consider g2 being Real such that A42: ( g2 = y & x0 < g2 ) and A43: g2 < x ; g2 < x0 + r by A18, A43, XXREAL_0:2; then y in { g3 where g3 is Real : ( x0 < g3 & g3 < x0 + r ) } by A42; hence y in ].x0,(x0 + r).[ by RCOMP_1:def_2; ::_thesis: verum end; then A44: ].x0,x.[ c= dom ((f . x) (#) g) by A14, A20, XBOOLE_1:1; x0 in dom f by A1, XBOOLE_0:def_4; then A45: {x0,x} c= dom f by A34, A32, ZFMISC_1:32; ].x0,x.[ c= dom f by A41, A32, XBOOLE_1:1; then ].x0,x.[ \/ {x0,x} c= dom f by A45, XBOOLE_1:8; then A46: [.x0,x.] c= dom f by A17, XXREAL_1:128; x0 in dom g by A1, XBOOLE_0:def_4; then A47: {x0,x} c= dom g by A34, A40, ZFMISC_1:32; ].x0,x.[ c= dom g by A41, A40, XBOOLE_1:1; then ].x0,x.[ \/ {x0,x} c= dom g by A47, XBOOLE_1:8; then A48: [.x0,x.] c= dom g by A17, XXREAL_1:128; g is_differentiable_in x by A6, A34, FDIFF_1:9; then A49: g is_continuous_in x by FDIFF_1:24; for s being Real_Sequence st rng s c= [.x0,x.] & s is convergent & lim s in [.x0,x.] holds ( g /* s is convergent & g . (lim s) = lim (g /* s) ) proof let s be Real_Sequence; ::_thesis: ( rng s c= [.x0,x.] & s is convergent & lim s in [.x0,x.] implies ( g /* s is convergent & g . (lim s) = lim (g /* s) ) ) assume that A50: rng s c= [.x0,x.] and A51: s is convergent and A52: lim s in [.x0,x.] ; ::_thesis: ( g /* s is convergent & g . (lim s) = lim (g /* s) ) set z = lim s; A53: rng s c= dom g by A48, A50, XBOOLE_1:1; A54: lim s in ].x0,x.[ \/ {x0,x} by A17, A52, XXREAL_1:128; now__::_thesis:_(_g_/*_s_is_convergent_&_g_._(lim_s)_=_lim_(g_/*_s)_) percases ( lim s in ].x0,x.[ or lim s in {x0,x} ) by A54, XBOOLE_0:def_3; suppose lim s in ].x0,x.[ ; ::_thesis: ( g /* s is convergent & g . (lim s) = lim (g /* s) ) then g is_differentiable_in lim s by A6, A41, FDIFF_1:9; then g is_continuous_in lim s by FDIFF_1:24; hence ( g /* s is convergent & g . (lim s) = lim (g /* s) ) by A51, A53, FCONT_1:def_1; ::_thesis: verum end; supposeA55: lim s in {x0,x} ; ::_thesis: ( g /* s is convergent & g . (lim s) = lim (g /* s) ) now__::_thesis:_(_g_/*_s_is_convergent_&_g_._(lim_s)_=_lim_(g_/*_s)_) percases ( lim s = x0 or lim s = x ) by A55, TARSKI:def_2; suppose lim s = x0 ; ::_thesis: ( g /* s is convergent & g . (lim s) = lim (g /* s) ) hence ( g /* s is convergent & g . (lim s) = lim (g /* s) ) by A11, A51, A53, FCONT_1:def_1; ::_thesis: verum end; suppose lim s = x ; ::_thesis: ( g /* s is convergent & g . (lim s) = lim (g /* s) ) hence ( g /* s is convergent & g . (lim s) = lim (g /* s) ) by A49, A51, A53, FCONT_1:def_1; ::_thesis: verum end; end; end; hence ( g /* s is convergent & g . (lim s) = lim (g /* s) ) ; ::_thesis: verum end; end; end; hence ( g /* s is convergent & g . (lim s) = lim (g /* s) ) ; ::_thesis: verum end; then g | [.x0,x.] is continuous by A48, FCONT_1:13; then A56: ((f . x) (#) g) | [.x0,x.] is continuous by A4, A22, FCONT_1:20, XBOOLE_1:1; f is_differentiable_in x by A5, A34, FDIFF_1:9; then A57: f is_continuous_in x by FDIFF_1:24; for s being Real_Sequence st rng s c= [.x0,x.] & s is convergent & lim s in [.x0,x.] holds ( f /* s is convergent & f . (lim s) = lim (f /* s) ) proof let s be Real_Sequence; ::_thesis: ( rng s c= [.x0,x.] & s is convergent & lim s in [.x0,x.] implies ( f /* s is convergent & f . (lim s) = lim (f /* s) ) ) assume that A58: rng s c= [.x0,x.] and A59: s is convergent and A60: lim s in [.x0,x.] ; ::_thesis: ( f /* s is convergent & f . (lim s) = lim (f /* s) ) set z = lim s; A61: rng s c= dom f by A46, A58, XBOOLE_1:1; A62: lim s in ].x0,x.[ \/ {x0,x} by A17, A60, XXREAL_1:128; now__::_thesis:_(_f_/*_s_is_convergent_&_f_._(lim_s)_=_lim_(f_/*_s)_) percases ( lim s in ].x0,x.[ or lim s in {x0,x} ) by A62, XBOOLE_0:def_3; suppose lim s in ].x0,x.[ ; ::_thesis: ( f /* s is convergent & f . (lim s) = lim (f /* s) ) then f is_differentiable_in lim s by A5, A41, FDIFF_1:9; then f is_continuous_in lim s by FDIFF_1:24; hence ( f /* s is convergent & f . (lim s) = lim (f /* s) ) by A59, A61, FCONT_1:def_1; ::_thesis: verum end; supposeA63: lim s in {x0,x} ; ::_thesis: ( f /* s is convergent & f . (lim s) = lim (f /* s) ) now__::_thesis:_(_f_/*_s_is_convergent_&_f_._(lim_s)_=_lim_(f_/*_s)_) percases ( lim s = x0 or lim s = x ) by A63, TARSKI:def_2; suppose lim s = x0 ; ::_thesis: ( f /* s is convergent & f . (lim s) = lim (f /* s) ) hence ( f /* s is convergent & f . (lim s) = lim (f /* s) ) by A10, A59, A61, FCONT_1:def_1; ::_thesis: verum end; suppose lim s = x ; ::_thesis: ( f /* s is convergent & f . (lim s) = lim (f /* s) ) hence ( f /* s is convergent & f . (lim s) = lim (f /* s) ) by A57, A59, A61, FCONT_1:def_1; ::_thesis: verum end; end; end; hence ( f /* s is convergent & f . (lim s) = lim (f /* s) ) ; ::_thesis: verum end; end; end; hence ( f /* s is convergent & f . (lim s) = lim (f /* s) ) ; ::_thesis: verum end; then f | [.x0,x.] is continuous by A46, FCONT_1:13; then ((g . x) (#) f) | [.x0,x.] is continuous by A3, A22, FCONT_1:20, XBOOLE_1:1; then A64: (((f . x) (#) g) - ((g . x) (#) f)) | [.x0,x.] is continuous by A20, A19, A21, A38, A56, FCONT_1:18; g is_differentiable_on ].x0,x.[ by A6, A41, FDIFF_1:26; then A65: (f . x) (#) g is_differentiable_on ].x0,x.[ by A44, FDIFF_1:20; A66: ].x0,x.[ c= dom ((g . x) (#) f) by A15, A41, A19, XBOOLE_1:1; then ].x0,x.[ c= (dom ((f . x) (#) g)) /\ (dom ((g . x) (#) f)) by A44, XBOOLE_1:19; then A67: ].x0,x.[ c= dom (((f . x) (#) g) - ((g . x) (#) f)) by VALUED_1:12; f is_differentiable_on ].x0,x.[ by A5, A41, FDIFF_1:26; then A68: (g . x) (#) f is_differentiable_on ].x0,x.[ by A66, FDIFF_1:20; (((f . x) (#) g) - ((g . x) (#) f)) . x0 = (((f . x) (#) g) . x0) - (((g . x) (#) f) . x0) by A26, A35, VALUED_1:13 .= ((f . x) * (g . x0)) - (((g . x) (#) f) . x0) by A37, VALUED_1:def_5 .= 0 - ((g . x) * 0) by A9, A39, VALUED_1:def_5 .= 0 ; then consider t being Real such that A69: t in ].x0,x.[ and A70: diff ((((f . x) (#) g) - ((g . x) (#) f)),t) = 0 by A17, A64, A68, A67, A65, A26, A31, FDIFF_1:19, ROLLE:1; A71: (g . x) (#) f is_differentiable_in t by A68, A69, FDIFF_1:9; A72: f is_differentiable_in t by A5, A41, A69, FDIFF_1:9; (f . x) (#) g is_differentiable_in t by A65, A69, FDIFF_1:9; then 0 = (diff (((f . x) (#) g),t)) - (diff (((g . x) (#) f),t)) by A70, A71, FDIFF_1:14; then A73: 0 = (diff (((f . x) (#) g),t)) - ((g . x) * (diff (f,t))) by A72, FDIFF_1:15; A74: (dom (f `| ].x0,(x0 + r).[)) /\ ((dom (g `| ].x0,(x0 + r).[)) \ ((g `| ].x0,(x0 + r).[) " {0})) c= (dom (g `| ].x0,(x0 + r).[)) \ ((g `| ].x0,(x0 + r).[) " {0}) by XBOOLE_1:17; A75: (dom f) /\ ((dom g) \ (g " {0})) c= (dom g) \ (g " {0}) by XBOOLE_1:17; now__::_thesis:_for_y_being_set_st_y_in_[.x0,x.]_\_{x0}_holds_ y_in_].x0,(x0_+_r).[ let y be set ; ::_thesis: ( y in [.x0,x.] \ {x0} implies y in ].x0,(x0 + r).[ ) assume A76: y in [.x0,x.] \ {x0} ; ::_thesis: y in ].x0,(x0 + r).[ then y in [.x0,x.] by XBOOLE_0:def_5; then y in { g4 where g4 is Real : ( x0 <= g4 & g4 <= x ) } by RCOMP_1:def_1; then consider g4 being Real such that A77: g4 = y and A78: x0 <= g4 and A79: g4 <= x ; not y in {x0} by A76, XBOOLE_0:def_5; then x0 <> g4 by A77, TARSKI:def_1; then A80: x0 < g4 by A78, XXREAL_0:1; g4 < x0 + r by A18, A79, XXREAL_0:2; then y in { g5 where g5 is Real : ( x0 < g5 & g5 < x0 + r ) } by A77, A80; hence y in ].x0,(x0 + r).[ by RCOMP_1:def_2; ::_thesis: verum end; then [.x0,x.] \ {x0} c= ].x0,(x0 + r).[ by TARSKI:def_3; then A81: [.x0,x.] \ {x0} c= dom (f / g) by A7, XBOOLE_1:1; then [.x0,x.] \ {x0} c= (dom f) /\ ((dom g) \ (g " {0})) by RFUNCT_1:def_1; then [.x0,x.] \ {x0} c= (dom g) \ (g " {0}) by A75, XBOOLE_1:1; then A82: ( x in dom g & not x in g " {0} ) by A33, XBOOLE_0:def_5; A83: now__::_thesis:_not_g_._x_=_0 assume g . x = 0 ; ::_thesis: contradiction then g . x in {0} by TARSKI:def_1; hence contradiction by A82, FUNCT_1:def_7; ::_thesis: verum end; take t ; ::_thesis: ( t in ].x0,x.[ & (f / g) . x = ((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)) . t ) ].x0,x.[ c= [.x0,x.] by XXREAL_1:25; then A84: t in [.x0,x.] by A69; x0 <= x0 + r by A2, XREAL_1:29; then x0 in { g6 where g6 is Real : ( x0 <= g6 & g6 <= x0 + r ) } ; then ( ].x0,(x0 + r).[ c= [.x0,(x0 + r).] & x0 in [.x0,(x0 + r).] ) by RCOMP_1:def_1, XXREAL_1:25; then [.x0,x.] c= [.x0,(x0 + r).] by A34, XXREAL_2:def_12; then A85: [.x0,x.] c= dom ((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)) by A8, XBOOLE_1:1; then [.x0,x.] c= (dom (f `| ].x0,(x0 + r).[)) /\ ((dom (g `| ].x0,(x0 + r).[)) \ ((g `| ].x0,(x0 + r).[) " {0})) by RFUNCT_1:def_1; then [.x0,x.] c= (dom (g `| ].x0,(x0 + r).[)) \ ((g `| ].x0,(x0 + r).[) " {0}) by A74, XBOOLE_1:1; then A86: ( t in dom (g `| ].x0,(x0 + r).[) & not t in (g `| ].x0,(x0 + r).[) " {0} ) by A84, XBOOLE_0:def_5; A87: now__::_thesis:_not_diff_(g,t)_=_0 assume diff (g,t) = 0 ; ::_thesis: contradiction then (g `| ].x0,(x0 + r).[) . t = 0 by A6, A41, A69, FDIFF_1:def_7; then (g `| ].x0,(x0 + r).[) . t in {0} by TARSKI:def_1; hence contradiction by A86, FUNCT_1:def_7; ::_thesis: verum end; g is_differentiable_in t by A6, A41, A69, FDIFF_1:9; then 0 = ((f . x) * (diff (g,t))) - ((g . x) * (diff (f,t))) by A73, FDIFF_1:15; then (f . x) / (g . x) = (diff (f,t)) / (diff (g,t)) by A83, A87, 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 A81, A33, RFUNCT_1:def_1; then (f / g) . x = ((f `| ].x0,(x0 + r).[) . t) * ((diff (g,t)) ") by A5, A41, A69, FDIFF_1:def_7; then (f / g) . x = ((f `| ].x0,(x0 + r).[) . t) * (((g `| ].x0,(x0 + r).[) . t) ") by A6, A41, A69, FDIFF_1:def_7; hence ( t in ].x0,x.[ & (f / g) . x = ((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)) . t ) by A69, A85, A84, RFUNCT_1:def_1; ::_thesis: verum end; A88: 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_right (((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)),x0) ) proof reconsider d = NAT --> x0 as Real_Sequence ; 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_right (((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)),x0) ) ) assume that A89: a is convergent and A90: lim a = x0 and A91: rng a c= (dom (f / g)) /\ (right_open_halfline x0) ; ::_thesis: ( (f / g) /* a is convergent & lim ((f / g) /* a) = lim_right (((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)),x0) ) consider k being Element of NAT such that A92: for n being Element of NAT st k <= n holds ( x0 - r < a . n & a . n < x0 + r ) by A2, A89, A90, LIMFUNC3:7; set a1 = a ^\ k; defpred S1[ Element of NAT , real number ] means ( $2 in ].x0,((a ^\ k) . $1).[ & (((f / g) /* a) ^\ k) . $1 = ((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)) . $2 ); A93: now__::_thesis:_for_n_being_Element_of_NAT_holds_ (_x0_<_(a_^\_k)_._n_&_(a_^\_k)_._n_<_x0_+_r_) let n be Element of NAT ; ::_thesis: ( x0 < (a ^\ k) . n & (a ^\ k) . n < x0 + r ) a . (n + k) in rng a by VALUED_0:28; then a . (n + k) in right_open_halfline x0 by A91, 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 ( (a ^\ k) . n = a . (n + k) & k <= n + k ) by NAT_1:12, NAT_1:def_3; hence (a ^\ k) . n < x0 + r by A92; ::_thesis: verum end; A94: 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] A95: rng (a ^\ k) c= rng a by VALUED_0:21; ( x0 < (a ^\ k) . n & (a ^\ k) . n < x0 + r ) by A93; then consider c being Real such that A96: c in ].x0,((a ^\ k) . n).[ and A97: (f / g) . ((a ^\ k) . n) = ((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)) . c by A16; take c ; ::_thesis: S1[n,c] A98: (dom (f / g)) /\ (right_open_halfline x0) c= dom (f / g) by XBOOLE_1:17; then rng a c= dom (f / g) by A91, XBOOLE_1:1; then ((f / g) /* (a ^\ k)) . n = ((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)) . c by A97, A95, FUNCT_2:108, XBOOLE_1:1; hence S1[n,c] by A91, A96, A98, VALUED_0:27, XBOOLE_1:1; ::_thesis: verum end; consider b being Real_Sequence such that A99: for n being Element of NAT holds S1[n,b . n] from FUNCT_2:sch_3(A94); A100: rng b c= (dom ((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[))) /\ (right_open_halfline x0) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng b or x in (dom ((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[))) /\ (right_open_halfline x0) ) assume x in rng b ; ::_thesis: x in (dom ((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[))) /\ (right_open_halfline x0) then consider n being Element of NAT such that A101: x = b . n by FUNCT_2:113; x0 <= x0 + r by A2, XREAL_1:29; then x0 in { g3 where g3 is Real : ( x0 <= g3 & g3 <= x0 + r ) } ; then A102: x0 in [.x0,(x0 + r).] by RCOMP_1:def_1; ( x0 < (a ^\ k) . n & (a ^\ k) . n < x0 + r ) by A93; then (a ^\ k) . n in { g4 where g4 is Real : ( x0 <= g4 & g4 <= x0 + r ) } ; then (a ^\ k) . n in [.x0,(x0 + r).] by RCOMP_1:def_1; then ( ].x0,((a ^\ k) . n).[ c= [.x0,((a ^\ k) . n).] & [.x0,((a ^\ k) . n).] c= [.x0,(x0 + r).] ) by A102, XXREAL_1:25, XXREAL_2:def_12; then ].x0,((a ^\ k) . n).[ c= [.x0,(x0 + r).] by XBOOLE_1:1; then A103: ].x0,((a ^\ k) . n).[ c= dom ((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)) by A8, XBOOLE_1:1; A104: x in ].x0,((a ^\ k) . n).[ by A99, A101; 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 `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[))) /\ (right_open_halfline x0) by A104, A103, XBOOLE_0:def_4; ::_thesis: verum end; A105: now__::_thesis:_for_n_being_Element_of_NAT_holds_ (_d_._n_<=_b_._n_&_b_._n_<=_(a_^\_k)_._n_) let n be Element of NAT ; ::_thesis: ( d . n <= b . n & b . n <= (a ^\ k) . n ) b . n in ].x0,((a ^\ k) . n).[ by A99; 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:7; ::_thesis: verum end; A106: lim d = d . 0 by SEQ_4:26 .= x0 by FUNCOP_1:7 ; lim (a ^\ k) = x0 by A89, A90, SEQ_4:20; then A107: ( b is convergent & lim b = x0 ) by A89, A106, A105, SEQ_2:19, SEQ_2:20; A108: (dom ((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[))) /\ (right_open_halfline x0) c= dom ((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)) by XBOOLE_1:17; A109: now__::_thesis:_ex_m_being_Element_of_NAT_st_ for_n_being_Element_of_NAT_st_m_<=_n_holds_ (((f_/_g)_/*_a)_^\_k)_._n_=_(((f_`|_].x0,(x0_+_r).[)_/_(g_`|_].x0,(x0_+_r).[))_/*_b)_._n take m = 0 ; ::_thesis: for n being Element of NAT st m <= n holds (((f / g) /* a) ^\ k) . n = (((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)) /* b) . n let n be Element of NAT ; ::_thesis: ( m <= n implies (((f / g) /* a) ^\ k) . n = (((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)) /* b) . n ) assume m <= n ; ::_thesis: (((f / g) /* a) ^\ k) . n = (((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)) /* b) . n (((f / g) /* a) ^\ k) . n = ((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)) . (b . n) by A99; hence (((f / g) /* a) ^\ k) . n = (((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)) /* b) . n by A100, A108, FUNCT_2:108, XBOOLE_1:1; ::_thesis: verum end; lim_right (((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)),x0) = lim_right (((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)),x0) ; then A110: ((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)) /* b is convergent by A12, A107, A100, LIMFUNC2:def_8; then A111: ((f / g) /* a) ^\ k is convergent by A109, SEQ_4:18; lim (((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)) /* b) = lim_right (((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)),x0) by A12, A107, A100, LIMFUNC2:def_8; then lim (((f / g) /* a) ^\ k) = lim_right (((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)),x0) by A110, A109, SEQ_4:19; hence ( (f / g) /* a is convergent & lim ((f / g) /* a) = lim_right (((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)),x0) ) by A111, SEQ_4:21, SEQ_4:22; ::_thesis: verum end; A112: for r1 being Real st x0 < r1 holds ex t being Real st ( t < r1 & x0 < t & t in dom (f / g) ) by A2, A7, LIMFUNC2:4; hence f / g is_right_convergent_in x0 by A88, Th2; ::_thesis: ex r being Real st ( r > 0 & lim_right ((f / g),x0) = lim_right (((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)),x0) ) take r ; ::_thesis: ( r > 0 & lim_right ((f / g),x0) = lim_right (((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)),x0) ) thus r > 0 by A2; ::_thesis: lim_right ((f / g),x0) = lim_right (((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)),x0) thus lim_right ((f / g),x0) = lim_right (((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)),x0) by A112, A88, Th2; ::_thesis: verum end; theorem :: L_HOSPIT:8 for f, g being PartFunc of REAL,REAL for x0 being Real st x0 in (dom f) /\ (dom g) & ex r being Real st ( 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 ) holds ( f / g is_left_convergent_in x0 & ex r being Real st ( r > 0 & lim_left ((f / g),x0) = lim_left (((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[)),x0) ) ) proof let f, g be PartFunc of REAL,REAL; ::_thesis: for x0 being Real st x0 in (dom f) /\ (dom g) & ex r being Real st ( 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 ) holds ( f / g is_left_convergent_in x0 & ex r being Real st ( r > 0 & lim_left ((f / g),x0) = lim_left (((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[)),x0) ) ) let x0 be Real; ::_thesis: ( x0 in (dom f) /\ (dom g) & ex r being Real st ( 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 ) implies ( f / g is_left_convergent_in x0 & ex r being Real st ( r > 0 & lim_left ((f / g),x0) = lim_left (((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[)),x0) ) ) ) assume A1: x0 in (dom f) /\ (dom g) ; ::_thesis: ( for r being Real holds ( not r > 0 or not [.(x0 - r),x0.] c= dom f or not [.(x0 - r),x0.] c= dom g or not f is_differentiable_on ].(x0 - r),x0.[ or not g is_differentiable_on ].(x0 - r),x0.[ or not ].(x0 - r),x0.[ c= dom (f / g) or not [.(x0 - r),x0.] c= dom ((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[)) or not f . x0 = 0 or not g . x0 = 0 or not f is_continuous_in x0 or not g is_continuous_in x0 or not (f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[) is_left_convergent_in x0 ) or ( f / g is_left_convergent_in x0 & ex r being Real st ( r > 0 & lim_left ((f / g),x0) = lim_left (((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[)),x0) ) ) ) given r being Real such that A2: r > 0 and A3: [.(x0 - r),x0.] c= dom f and A4: [.(x0 - r),x0.] c= dom g and A5: f is_differentiable_on ].(x0 - r),x0.[ and A6: g is_differentiable_on ].(x0 - r),x0.[ and A7: ].(x0 - r),x0.[ c= dom (f / g) and A8: [.(x0 - r),x0.] c= dom ((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[)) and A9: ( f . x0 = 0 & g . x0 = 0 ) and A10: f is_continuous_in x0 and A11: g is_continuous_in x0 and A12: (f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[) is_left_convergent_in x0 ; ::_thesis: ( f / g is_left_convergent_in x0 & ex r being Real st ( r > 0 & lim_left ((f / g),x0) = lim_left (((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[)),x0) ) ) A13: ].(x0 - r),x0.[ c= [.(x0 - r),x0.] by XXREAL_1:25; then A14: ].(x0 - r),x0.[ c= dom g by A4, XBOOLE_1:1; A15: ].(x0 - r),x0.[ c= dom f by A3, A13, XBOOLE_1:1; A16: 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: ( x0 - r < x & x < x0 implies ex c being Real st ( c in ].x,x0.[ & (f / g) . x = ((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[)) . c ) ) assume that A17: x0 - r < x and A18: x < x0 ; ::_thesis: ex c being Real st ( c in ].x,x0.[ & (f / g) . x = ((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[)) . c ) x in { g1 where g1 is Real : ( x0 - r < g1 & g1 < x0 ) } by A17, A18; then A19: x in ].(x0 - r),x0.[ by RCOMP_1:def_2; ( ].(x0 - r),x0.[ c= dom f & x0 in dom f ) by A1, A3, A13, XBOOLE_0:def_4, XBOOLE_1:1; then A20: {x,x0} c= dom f by A19, ZFMISC_1:32; A21: ].x,x0.[ c= ].(x0 - r),x0.[ proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in ].x,x0.[ or y in ].(x0 - r),x0.[ ) assume y in ].x,x0.[ ; ::_thesis: y in ].(x0 - r),x0.[ then y in { g2 where g2 is Real : ( x < g2 & g2 < x0 ) } by RCOMP_1:def_2; then consider g2 being Real such that A22: g2 = y and A23: x < g2 and A24: g2 < x0 ; x0 - r < g2 by A17, A23, XXREAL_0:2; then y in { g3 where g3 is Real : ( x0 - r < g3 & g3 < x0 ) } by A22, A24; hence y in ].(x0 - r),x0.[ by RCOMP_1:def_2; ::_thesis: verum end; then ].x,x0.[ c= dom f by A15, XBOOLE_1:1; then ].x,x0.[ \/ {x,x0} c= dom f by A20, XBOOLE_1:8; then A25: [.x,x0.] c= dom f by A18, XXREAL_1:128; ].(x0 - r),x0.[ c= dom ((f . x) (#) g) by A14, VALUED_1:def_5; then A26: ].x,x0.[ c= dom ((f . x) (#) g) by A21, XBOOLE_1:1; ].(x0 - r),x0.[ c= dom ((g . x) (#) f) by A15, VALUED_1:def_5; then A27: ].x,x0.[ c= dom ((g . x) (#) f) by A21, XBOOLE_1:1; then ].x,x0.[ c= (dom ((f . x) (#) g)) /\ (dom ((g . x) (#) f)) by A26, XBOOLE_1:19; then A28: ].x,x0.[ c= dom (((f . x) (#) g) - ((g . x) (#) f)) by VALUED_1:12; f is_differentiable_on ].x,x0.[ by A5, A21, FDIFF_1:26; then A29: (g . x) (#) f is_differentiable_on ].x,x0.[ by A27, FDIFF_1:20; ( ].(x0 - r),x0.[ c= dom g & x0 in dom g ) by A1, A4, A13, XBOOLE_0:def_4, XBOOLE_1:1; then A30: {x,x0} c= dom g by A19, ZFMISC_1:32; set f1 = ((f . x) (#) g) - ((g . x) (#) f); A31: ( dom ((f . x) (#) g) = dom g & dom ((g . x) (#) f) = dom f ) by VALUED_1:def_5; then A32: dom (((f . x) (#) g) - ((g . x) (#) f)) = (dom f) /\ (dom g) by VALUED_1:12; A33: [.x,x0.] c= [.(x0 - r),x0.] proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in [.x,x0.] or y in [.(x0 - r),x0.] ) assume A34: y in [.x,x0.] ; ::_thesis: y in [.(x0 - r),x0.] then reconsider y = y as real number ; x <= y by A34, XXREAL_1:1; then A35: x0 - r <= y by A17, XXREAL_0:2; y <= x0 by A34, XXREAL_1:1; hence y in [.(x0 - r),x0.] by A35, XXREAL_1:1; ::_thesis: verum end; then A36: ( [.x,x0.] c= dom f & [.x,x0.] c= dom g ) by A3, A4, XBOOLE_1:1; then A37: [.x,x0.] c= dom (((f . x) (#) g) - ((g . x) (#) f)) by A32, XBOOLE_1:19; A38: x in [.x,x0.] by A18, XXREAL_1:1; then x in dom (((f . x) (#) g) - ((g . x) (#) f)) by A37; then A39: x in (dom ((f . x) (#) g)) /\ (dom ((g . x) (#) f)) by VALUED_1:12; then A40: x in dom ((f . x) (#) g) by XBOOLE_0:def_4; A41: x0 in [.x,x0.] by A18, XXREAL_1:1; then x0 in dom (((f . x) (#) g) - ((g . x) (#) f)) by A37; then A42: x0 in (dom ((f . x) (#) g)) /\ (dom ((g . x) (#) f)) by VALUED_1:12; then A43: x0 in dom ((f . x) (#) g) by XBOOLE_0:def_4; A44: x in dom ((g . x) (#) f) by A39, XBOOLE_0:def_4; A45: (((f . x) (#) g) - ((g . x) (#) f)) . x = (((f . x) (#) g) . x) - (((g . x) (#) f) . x) by A37, A38, VALUED_1:13 .= ((f . x) * (g . x)) - (((g . x) (#) f) . x) by A40, VALUED_1:def_5 .= ((g . x) * (f . x)) - ((g . x) * (f . x)) by A44, VALUED_1:def_5 .= 0 ; A46: x0 in dom ((g . x) (#) f) by A42, XBOOLE_0:def_4; not x in {x0} by A18, TARSKI:def_1; then A47: x in [.x,x0.] \ {x0} by A38, XBOOLE_0:def_5; ].x,x0.[ c= dom g by A14, A21, XBOOLE_1:1; then ].x,x0.[ \/ {x,x0} c= dom g by A30, XBOOLE_1:8; then A48: [.x,x0.] c= dom g by A18, XXREAL_1:128; g is_differentiable_in x by A6, A19, FDIFF_1:9; then A49: g is_continuous_in x by FDIFF_1:24; 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: ( rng s c= [.x,x0.] & s is convergent & lim s in [.x,x0.] implies ( g /* s is convergent & g . (lim s) = lim (g /* s) ) ) assume that A50: rng s c= [.x,x0.] and A51: s is convergent and A52: lim s in [.x,x0.] ; ::_thesis: ( g /* s is convergent & g . (lim s) = lim (g /* s) ) set z = lim s; A53: rng s c= dom g by A48, A50, XBOOLE_1:1; A54: lim s in ].x,x0.[ \/ {x,x0} by A18, A52, XXREAL_1:128; now__::_thesis:_(_g_/*_s_is_convergent_&_g_._(lim_s)_=_lim_(g_/*_s)_) percases ( lim s in ].x,x0.[ or lim s in {x,x0} ) by A54, XBOOLE_0:def_3; suppose lim s in ].x,x0.[ ; ::_thesis: ( g /* s is convergent & g . (lim s) = lim (g /* s) ) then g is_differentiable_in lim s by A6, A21, FDIFF_1:9; then g is_continuous_in lim s by FDIFF_1:24; hence ( g /* s is convergent & g . (lim s) = lim (g /* s) ) by A51, A53, FCONT_1:def_1; ::_thesis: verum end; supposeA55: lim s in {x,x0} ; ::_thesis: ( g /* s is convergent & g . (lim s) = lim (g /* s) ) now__::_thesis:_(_g_/*_s_is_convergent_&_g_._(lim_s)_=_lim_(g_/*_s)_) percases ( lim s = x0 or lim s = x ) by A55, TARSKI:def_2; suppose lim s = x0 ; ::_thesis: ( g /* s is convergent & g . (lim s) = lim (g /* s) ) hence ( g /* s is convergent & g . (lim s) = lim (g /* s) ) by A11, A51, A53, FCONT_1:def_1; ::_thesis: verum end; suppose lim s = x ; ::_thesis: ( g /* s is convergent & g . (lim s) = lim (g /* s) ) hence ( g /* s is convergent & g . (lim s) = lim (g /* s) ) by A49, A51, A53, FCONT_1:def_1; ::_thesis: verum end; end; end; hence ( g /* s is convergent & g . (lim s) = lim (g /* s) ) ; ::_thesis: verum end; end; end; hence ( g /* s is convergent & g . (lim s) = lim (g /* s) ) ; ::_thesis: verum end; then g | [.x,x0.] is continuous by A48, FCONT_1:13; then A56: ((f . x) (#) g) | [.x,x0.] is continuous by A4, A33, FCONT_1:20, XBOOLE_1:1; A57: [.x,x0.] c= dom (((f . x) (#) g) - ((g . x) (#) f)) by A36, A32, XBOOLE_1:19; f is_differentiable_in x by A5, A19, FDIFF_1:9; then A58: f is_continuous_in x by FDIFF_1:24; 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: ( rng s c= [.x,x0.] & s is convergent & lim s in [.x,x0.] implies ( f /* s is convergent & f . (lim s) = lim (f /* s) ) ) assume that A59: rng s c= [.x,x0.] and A60: s is convergent and A61: lim s in [.x,x0.] ; ::_thesis: ( f /* s is convergent & f . (lim s) = lim (f /* s) ) set z = lim s; A62: rng s c= dom f by A25, A59, XBOOLE_1:1; A63: lim s in ].x,x0.[ \/ {x,x0} by A18, A61, XXREAL_1:128; now__::_thesis:_(_f_/*_s_is_convergent_&_f_._(lim_s)_=_lim_(f_/*_s)_) percases ( lim s in ].x,x0.[ or lim s in {x,x0} ) by A63, XBOOLE_0:def_3; suppose lim s in ].x,x0.[ ; ::_thesis: ( f /* s is convergent & f . (lim s) = lim (f /* s) ) then f is_differentiable_in lim s by A5, A21, FDIFF_1:9; then f is_continuous_in lim s by FDIFF_1:24; hence ( f /* s is convergent & f . (lim s) = lim (f /* s) ) by A60, A62, FCONT_1:def_1; ::_thesis: verum end; supposeA64: lim s in {x,x0} ; ::_thesis: ( f /* s is convergent & f . (lim s) = lim (f /* s) ) now__::_thesis:_(_f_/*_s_is_convergent_&_f_._(lim_s)_=_lim_(f_/*_s)_) percases ( lim s = x0 or lim s = x ) by A64, TARSKI:def_2; suppose lim s = x0 ; ::_thesis: ( f /* s is convergent & f . (lim s) = lim (f /* s) ) hence ( f /* s is convergent & f . (lim s) = lim (f /* s) ) by A10, A60, A62, FCONT_1:def_1; ::_thesis: verum end; suppose lim s = x ; ::_thesis: ( f /* s is convergent & f . (lim s) = lim (f /* s) ) hence ( f /* s is convergent & f . (lim s) = lim (f /* s) ) by A58, A60, A62, FCONT_1:def_1; ::_thesis: verum end; end; end; hence ( f /* s is convergent & f . (lim s) = lim (f /* s) ) ; ::_thesis: verum end; end; end; hence ( f /* s is convergent & f . (lim s) = lim (f /* s) ) ; ::_thesis: verum end; then f | [.x,x0.] is continuous by A25, FCONT_1:13; then ((g . x) (#) f) | [.x,x0.] is continuous by A3, A33, FCONT_1:20, XBOOLE_1:1; then A65: (((f . x) (#) g) - ((g . x) (#) f)) | [.x,x0.] is continuous by A31, A32, A57, A56, FCONT_1:18; g is_differentiable_on ].x,x0.[ by A6, A21, FDIFF_1:26; then A66: (f . x) (#) g is_differentiable_on ].x,x0.[ by A26, FDIFF_1:20; (((f . x) (#) g) - ((g . x) (#) f)) . x0 = (((f . x) (#) g) . x0) - (((g . x) (#) f) . x0) by A37, A41, VALUED_1:13 .= ((f . x) * (g . x0)) - (((g . x) (#) f) . x0) by A43, VALUED_1:def_5 .= 0 - ((g . x) * 0) by A9, A46, VALUED_1:def_5 .= 0 ; then consider t being Real such that A67: t in ].x,x0.[ and A68: diff ((((f . x) (#) g) - ((g . x) (#) f)),t) = 0 by A18, A65, A29, A28, A66, A37, A45, FDIFF_1:19, ROLLE:1; A69: (g . x) (#) f is_differentiable_in t by A29, A67, FDIFF_1:9; A70: f is_differentiable_in t by A5, A21, A67, FDIFF_1:9; (f . x) (#) g is_differentiable_in t by A66, A67, FDIFF_1:9; then 0 = (diff (((f . x) (#) g),t)) - (diff (((g . x) (#) f),t)) by A68, A69, FDIFF_1:14; then A71: 0 = (diff (((f . x) (#) g),t)) - ((g . x) * (diff (f,t))) by A70, FDIFF_1:15; A72: (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; A73: (dom f) /\ ((dom g) \ (g " {0})) c= (dom g) \ (g " {0}) by XBOOLE_1:17; now__::_thesis:_for_y_being_set_st_y_in_[.x,x0.]_\_{x0}_holds_ y_in_].(x0_-_r),x0.[ let y be set ; ::_thesis: ( y in [.x,x0.] \ {x0} implies y in ].(x0 - r),x0.[ ) assume A74: y in [.x,x0.] \ {x0} ; ::_thesis: y in ].(x0 - r),x0.[ then y in [.x,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 A75: g4 = y and A76: x <= g4 and A77: g4 <= x0 ; not y in {x0} by A74, XBOOLE_0:def_5; then x0 <> g4 by A75, TARSKI:def_1; then A78: g4 < x0 by A77, XXREAL_0:1; x0 - r < g4 by A17, A76, XXREAL_0:2; then y in { g5 where g5 is Real : ( x0 - r < g5 & g5 < x0 ) } by A75, A78; hence y in ].(x0 - r),x0.[ by RCOMP_1:def_2; ::_thesis: verum end; then [.x,x0.] \ {x0} c= ].(x0 - r),x0.[ by TARSKI:def_3; then A79: [.x,x0.] \ {x0} c= dom (f / g) by A7, XBOOLE_1:1; then [.x,x0.] \ {x0} c= (dom f) /\ ((dom g) \ (g " {0})) by RFUNCT_1:def_1; then [.x,x0.] \ {x0} c= (dom g) \ (g " {0}) by A73, XBOOLE_1:1; then A80: ( x in dom g & not x in g " {0} ) by A47, XBOOLE_0:def_5; A81: now__::_thesis:_not_g_._x_=_0 assume g . x = 0 ; ::_thesis: contradiction then g . x in {0} by TARSKI:def_1; hence contradiction by A80, FUNCT_1:def_7; ::_thesis: verum end; take t ; ::_thesis: ( t in ].x,x0.[ & (f / g) . x = ((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[)) . t ) ].x,x0.[ c= [.x,x0.] by XXREAL_1:25; then A82: t in [.x,x0.] by A67; x0 - r <= x0 by A2, XREAL_1:44; then x0 in { g6 where g6 is Real : ( x0 - r <= g6 & g6 <= x0 ) } ; then ( ].(x0 - r),x0.[ c= [.(x0 - r),x0.] & x0 in [.(x0 - r),x0.] ) by RCOMP_1:def_1, XXREAL_1:25; then [.x,x0.] c= [.(x0 - r),x0.] by A19, XXREAL_2:def_12; then A83: [.x,x0.] c= dom ((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[)) by A8, XBOOLE_1:1; then [.x,x0.] c= (dom (f `| ].(x0 - r),x0.[)) /\ ((dom (g `| ].(x0 - r),x0.[)) \ ((g `| ].(x0 - r),x0.[) " {0})) by RFUNCT_1:def_1; then [.x,x0.] c= (dom (g `| ].(x0 - r),x0.[)) \ ((g `| ].(x0 - r),x0.[) " {0}) by A72, XBOOLE_1:1; then A84: ( t in dom (g `| ].(x0 - r),x0.[) & not t in (g `| ].(x0 - r),x0.[) " {0} ) by A82, XBOOLE_0:def_5; A85: now__::_thesis:_not_diff_(g,t)_=_0 assume diff (g,t) = 0 ; ::_thesis: contradiction then (g `| ].(x0 - r),x0.[) . t = 0 by A6, A21, A67, FDIFF_1:def_7; then (g `| ].(x0 - r),x0.[) . t in {0} by TARSKI:def_1; hence contradiction by A84, FUNCT_1:def_7; ::_thesis: verum end; g is_differentiable_in t by A6, A21, A67, FDIFF_1:9; then 0 = ((f . x) * (diff (g,t))) - ((g . x) * (diff (f,t))) by A71, FDIFF_1:15; then (f . x) / (g . x) = (diff (f,t)) / (diff (g,t)) by A81, A85, 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 A79, A47, RFUNCT_1:def_1; then (f / g) . x = ((f `| ].(x0 - r),x0.[) . t) * ((diff (g,t)) ") by A5, A21, A67, FDIFF_1:def_7; then (f / g) . x = ((f `| ].(x0 - r),x0.[) . t) * (((g `| ].(x0 - r),x0.[) . t) ") by A6, A21, A67, FDIFF_1:def_7; hence ( t in ].x,x0.[ & (f / g) . x = ((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[)) . t ) by A67, A83, A82, RFUNCT_1:def_1; ::_thesis: verum end; A86: 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 reconsider d = NAT --> x0 as Real_Sequence ; 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_left (((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[)),x0) ) ) assume that A87: a is convergent and A88: lim a = x0 and A89: rng a c= (dom (f / g)) /\ (left_open_halfline x0) ; ::_thesis: ( (f / g) /* a is convergent & lim ((f / g) /* a) = lim_left (((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[)),x0) ) consider k being Element of NAT such that A90: for n being Element of NAT st k <= n holds ( x0 - r < a . n & a . n < x0 + r ) by A2, A87, A88, LIMFUNC3:7; set a1 = a ^\ k; defpred S1[ 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 ); A91: now__::_thesis:_for_n_being_Element_of_NAT_holds_ (_(a_^\_k)_._n_<_x0_&_x0_-_r_<_(a_^\_k)_._n_) let n be Element of NAT ; ::_thesis: ( (a ^\ k) . n < x0 & x0 - r < (a ^\ k) . n ) a . (n + k) in rng a by VALUED_0:28; then a . (n + k) in left_open_halfline x0 by A89, 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 ( (a ^\ k) . n = a . (n + k) & k <= n + k ) by NAT_1:12, NAT_1:def_3; hence x0 - r < (a ^\ k) . n by A90; ::_thesis: verum end; A92: 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] A93: rng (a ^\ k) c= rng a by VALUED_0:21; ( x0 - r < (a ^\ k) . n & (a ^\ k) . n < x0 ) by A91; then consider c being Real such that A94: c in ].((a ^\ k) . n),x0.[ and A95: (f / g) . ((a ^\ k) . n) = ((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[)) . c by A16; take c ; ::_thesis: S1[n,c] A96: (dom (f / g)) /\ (left_open_halfline x0) c= dom (f / g) by XBOOLE_1:17; then rng a c= dom (f / g) by A89, XBOOLE_1:1; then ((f / g) /* (a ^\ k)) . n = ((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[)) . c by A95, A93, FUNCT_2:108, XBOOLE_1:1; hence S1[n,c] by A89, A94, A96, VALUED_0:27, XBOOLE_1:1; ::_thesis: verum end; consider b being Real_Sequence such that A97: for n being Element of NAT holds S1[n,b . n] from FUNCT_2:sch_3(A92); A98: 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: ( not x in rng b or x in (dom ((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[))) /\ (left_open_halfline x0) ) assume x in rng b ; ::_thesis: x in (dom ((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[))) /\ (left_open_halfline x0) then consider n being Element of NAT such that A99: x = b . n by FUNCT_2:113; x0 - r <= x0 by A2, XREAL_1:44; then x0 in { g3 where g3 is Real : ( x0 - r <= g3 & g3 <= x0 ) } ; then A100: x0 in [.(x0 - r),x0.] by RCOMP_1:def_1; ( x0 - r < (a ^\ k) . n & (a ^\ k) . n < x0 ) by A91; then (a ^\ k) . n in { g4 where g4 is Real : ( x0 - r <= g4 & g4 <= x0 ) } ; then (a ^\ k) . n in [.(x0 - r),x0.] by RCOMP_1:def_1; then ( ].((a ^\ k) . n),x0.[ c= [.((a ^\ k) . n),x0.] & [.((a ^\ k) . n),x0.] c= [.(x0 - r),x0.] ) by A100, XXREAL_1:25, XXREAL_2:def_12; then ].((a ^\ k) . n),x0.[ c= [.(x0 - r),x0.] by XBOOLE_1:1; then A101: ].((a ^\ k) . n),x0.[ c= dom ((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[)) by A8, XBOOLE_1:1; A102: x in ].((a ^\ k) . n),x0.[ by A97, A99; 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 `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[))) /\ (left_open_halfline x0) by A102, A101, XBOOLE_0:def_4; ::_thesis: verum end; A103: now__::_thesis:_for_n_being_Element_of_NAT_holds_ (_(a_^\_k)_._n_<=_b_._n_&_b_._n_<=_d_._n_) let n be Element of NAT ; ::_thesis: ( (a ^\ k) . n <= b . n & b . n <= d . n ) b . n in ].((a ^\ k) . n),x0.[ by A97; 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:7; ::_thesis: verum end; A104: lim d = d . 0 by SEQ_4:26 .= x0 by FUNCOP_1:7 ; lim (a ^\ k) = x0 by A87, A88, SEQ_4:20; then A105: ( b is convergent & lim b = x0 ) by A87, A104, A103, SEQ_2:19, SEQ_2:20; A106: (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; A107: now__::_thesis:_ex_m_being_Element_of_NAT_st_ for_n_being_Element_of_NAT_st_m_<=_n_holds_ (((f_/_g)_/*_a)_^\_k)_._n_=_(((f_`|_].(x0_-_r),x0.[)_/_(g_`|_].(x0_-_r),x0.[))_/*_b)_._n take m = 0 ; ::_thesis: for n being Element of NAT st m <= n holds (((f / g) /* a) ^\ k) . n = (((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[)) /* b) . n let n be Element of NAT ; ::_thesis: ( m <= n implies (((f / g) /* a) ^\ k) . n = (((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[)) /* b) . n ) assume m <= n ; ::_thesis: (((f / g) /* a) ^\ k) . n = (((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[)) /* b) . n (((f / g) /* a) ^\ k) . n = ((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[)) . (b . n) by A97; hence (((f / g) /* a) ^\ k) . n = (((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[)) /* b) . n by A98, A106, FUNCT_2:108, XBOOLE_1:1; ::_thesis: verum end; lim_left (((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[)),x0) = lim_left (((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[)),x0) ; then A108: ((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[)) /* b is convergent by A12, A105, A98, LIMFUNC2:def_7; then A109: ((f / g) /* a) ^\ k is convergent by A107, SEQ_4:18; lim (((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[)) /* b) = lim_left (((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[)),x0) by A12, A105, A98, LIMFUNC2:def_7; then lim (((f / g) /* a) ^\ k) = lim_left (((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[)),x0) by A108, A107, SEQ_4:19; hence ( (f / g) /* a is convergent & lim ((f / g) /* a) = lim_left (((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[)),x0) ) by A109, SEQ_4:21, SEQ_4:22; ::_thesis: verum end; A110: for r1 being Real st r1 < x0 holds ex t being Real st ( r1 < t & t < x0 & t in dom (f / g) ) by A2, A7, LIMFUNC2:3; hence f / g is_left_convergent_in x0 by A86, Th3; ::_thesis: ex r being Real st ( r > 0 & lim_left ((f / g),x0) = lim_left (((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[)),x0) ) take r ; ::_thesis: ( r > 0 & lim_left ((f / g),x0) = lim_left (((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[)),x0) ) thus r > 0 by A2; ::_thesis: lim_left ((f / g),x0) = lim_left (((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[)),x0) thus lim_left ((f / g),x0) = lim_left (((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[)),x0) by A110, A86, Th3; ::_thesis: verum end; theorem :: L_HOSPIT:9 for f, g being PartFunc of REAL,REAL 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) ) proof 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 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_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 A9: 0 < r and A10: N = ].(x0 - r),(x0 + r).[ by RCOMP_1:def_6; A11: r is Real by XREAL_0:def_1; A12: 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 A13: x0 - r < x0 by A9, XREAL_1:44; x0 + 0 < x0 + r by A9, XREAL_1:8; then x0 in { g1 where g1 is Real : ( x0 - r < g1 & g1 < x0 + r ) } by A13; then A14: x0 in ].(x0 - r),(x0 + r).[ by RCOMP_1:def_2; A15: (dom (f `| N)) /\ ((dom (g `| N)) \ ((g `| N) " {0})) c= (dom (g `| N)) \ ((g `| N) " {0}) by XBOOLE_1:17; A16: (dom f) /\ ((dom g) \ (g " {0})) c= (dom g) \ (g " {0}) by XBOOLE_1:17; 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 that A17: x0 < x and A18: x < x0 + r ; ::_thesis: ex c being Real st ( c in ].x0,x.[ & (f / g) . x = ((f `| N) / (g `| N)) . c ) set f1 = ((f . x) (#) g) - ((g . x) (#) f); A19: ( dom ((f . x) (#) g) = dom g & dom ((g . x) (#) f) = dom f ) by VALUED_1:def_5; then A20: dom (((f . x) (#) g) - ((g . x) (#) f)) = (dom f) /\ (dom g) by VALUED_1:12; x0 - r < x by A17, A13, XXREAL_0:2; then x in { g1 where g1 is Real : ( x0 - r < g1 & g1 < x0 + r ) } by A18; then x in ].(x0 - r),(x0 + r).[ by RCOMP_1:def_2; then A21: [.x0,x.] c= N by A10, A14, XXREAL_2:def_12; then A22: ( [.x0,x.] c= dom f & [.x0,x.] c= dom g ) by A1, A2, XBOOLE_1:1; then A23: [.x0,x.] c= dom (((f . x) (#) g) - ((g . x) (#) f)) by A20, XBOOLE_1:19; g | N is continuous by A4, FDIFF_1:25; then g | [.x0,x.] is continuous by A21, FCONT_1:16; then A24: ((f . x) (#) g) | [.x0,x.] is continuous by A2, A21, FCONT_1:20, XBOOLE_1:1; f | N is continuous by A3, FDIFF_1:25; then f | [.x0,x.] is continuous by A21, FCONT_1:16; then A25: ((g . x) (#) f) | [.x0,x.] is continuous by A1, A21, FCONT_1:20, XBOOLE_1:1; [.x0,x.] c= dom (((f . x) (#) g) - ((g . x) (#) f)) by A22, A20, XBOOLE_1:19; then A26: (((f . x) (#) g) - ((g . x) (#) f)) | [.x0,x.] is continuous by A19, A20, A25, A24, FCONT_1:18; A27: ].x0,x.[ c= [.x0,x.] by XXREAL_1:25; then A28: ].x0,x.[ c= N by A21, XBOOLE_1:1; A29: x in [.x0,x.] by A17, XXREAL_1:1; then x in dom (((f . x) (#) g) - ((g . x) (#) f)) by A23; then A30: x in (dom ((f . x) (#) g)) /\ (dom ((g . x) (#) f)) by VALUED_1:12; then A31: x in dom ((f . x) (#) g) by XBOOLE_0:def_4; A32: x0 in [.x0,x.] by A17, XXREAL_1:1; then x0 in dom (((f . x) (#) g) - ((g . x) (#) f)) by A23; then A33: x0 in (dom ((f . x) (#) g)) /\ (dom ((g . x) (#) f)) by VALUED_1:12; then A34: x0 in dom ((f . x) (#) g) by XBOOLE_0:def_4; A35: x in dom ((g . x) (#) f) by A30, XBOOLE_0:def_4; A36: (((f . x) (#) g) - ((g . x) (#) f)) . x = (((f . x) (#) g) . x) - (((g . x) (#) f) . x) by A23, A29, VALUED_1:13 .= ((f . x) * (g . x)) - (((g . x) (#) f) . x) by A31, VALUED_1:def_5 .= ((g . x) * (f . x)) - ((g . x) * (f . x)) by A35, VALUED_1:def_5 .= 0 ; A37: x0 in dom ((g . x) (#) f) by A33, XBOOLE_0:def_4; not x in {x0} by A17, TARSKI:def_1; then A38: x in [.x0,x.] \ {x0} by A29, XBOOLE_0:def_5; N c= dom ((f . x) (#) g) by A2, VALUED_1:def_5; then A39: ].x0,x.[ c= dom ((f . x) (#) g) by A28, XBOOLE_1:1; N c= dom ((g . x) (#) f) by A1, VALUED_1:def_5; then A40: ].x0,x.[ c= dom ((g . x) (#) f) by A28, XBOOLE_1:1; then ].x0,x.[ c= (dom ((f . x) (#) g)) /\ (dom ((g . x) (#) f)) by A39, XBOOLE_1:19; then A41: ].x0,x.[ c= dom (((f . x) (#) g) - ((g . x) (#) f)) by VALUED_1:12; f is_differentiable_on ].x0,x.[ by A3, A21, A27, FDIFF_1:26, XBOOLE_1:1; then A42: (g . x) (#) f is_differentiable_on ].x0,x.[ by A40, FDIFF_1:20; g is_differentiable_on ].x0,x.[ by A4, A21, A27, FDIFF_1:26, XBOOLE_1:1; then A43: (f . x) (#) g is_differentiable_on ].x0,x.[ by A39, FDIFF_1:20; (((f . x) (#) g) - ((g . x) (#) f)) . x0 = (((f . x) (#) g) . x0) - (((g . x) (#) f) . x0) by A23, A32, VALUED_1:13 .= ((f . x) * (g . x0)) - (((g . x) (#) f) . x0) by A34, VALUED_1:def_5 .= 0 - ((g . x) * 0) by A7, A37, VALUED_1:def_5 .= 0 ; then consider t being Real such that A44: t in ].x0,x.[ and A45: diff ((((f . x) (#) g) - ((g . x) (#) f)),t) = 0 by A17, A26, A42, A41, A43, A23, A36, FDIFF_1:19, ROLLE:1; A46: (g . x) (#) f is_differentiable_in t by A42, A44, FDIFF_1:9; A47: f is_differentiable_in t by A3, A28, A44, FDIFF_1:9; (f . x) (#) g is_differentiable_in t by A43, A44, FDIFF_1:9; then 0 = (diff (((f . x) (#) g),t)) - (diff (((g . x) (#) f),t)) by A45, A46, FDIFF_1:14; then A48: 0 = (diff (((f . x) (#) g),t)) - ((g . x) * (diff (f,t))) by A47, FDIFF_1:15; take t ; ::_thesis: ( t in ].x0,x.[ & (f / g) . x = ((f `| N) / (g `| N)) . t ) A49: t in [.x0,x.] by A27, A44; [.x0,x.] \ {x0} c= N \ {x0} by A21, XBOOLE_1:33; then A50: [.x0,x.] \ {x0} c= dom (f / g) by A5, XBOOLE_1:1; then [.x0,x.] \ {x0} c= (dom f) /\ ((dom g) \ (g " {0})) by RFUNCT_1:def_1; then [.x0,x.] \ {x0} c= (dom g) \ (g " {0}) by A16, XBOOLE_1:1; then A51: ( x in dom g & not x in g " {0} ) by A38, XBOOLE_0:def_5; A52: now__::_thesis:_not_g_._x_=_0 assume g . x = 0 ; ::_thesis: contradiction then g . x in {0} by TARSKI:def_1; hence contradiction by A51, FUNCT_1:def_7; ::_thesis: verum end; A53: [.x0,x.] c= dom ((f `| N) / (g `| N)) by A6, A21, XBOOLE_1:1; 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 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__::_thesis:_not_diff_(g,t)_=_0 assume diff (g,t) = 0 ; ::_thesis: contradiction then (g `| N) . t = 0 by A4, A21, A49, FDIFF_1:def_7; then (g `| N) . t in {0} by TARSKI:def_1; hence contradiction by A54, FUNCT_1:def_7; ::_thesis: verum end; g is_differentiable_in t by A4, A28, A44, FDIFF_1:9; then 0 = ((f . x) * (diff (g,t))) - ((g . x) * (diff (f,t))) by A48, FDIFF_1:15; then (f . x) / (g . x) = (diff (f,t)) / (diff (g,t)) by A52, A55, 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 A50, A38, RFUNCT_1:def_1; then (f / g) . x = ((f `| N) . t) * ((diff (g,t)) ") by A3, A21, A49, FDIFF_1:def_7; then (f / g) . x = ((f `| N) . t) * (((g `| N) . t) ") by A4, A21, A49, FDIFF_1:def_7; hence ( t in ].x0,x.[ & (f / g) . x = ((f `| N) / (g `| N)) . t ) by A44, A53, A49, RFUNCT_1:def_1; ::_thesis: verum end; A56: 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 reconsider d = NAT --> x0 as Real_Sequence ; 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 that A57: a is convergent and A58: lim a = x0 and A59: 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) ) 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 S1[ Element of NAT , real number ] means ( $2 in ].x0,((a ^\ k) . $1).[ & (((f / g) /* a) ^\ k) . $1 = ((f `| N) / (g `| N)) . $2 ); A61: now__::_thesis:_for_n_being_Element_of_NAT_holds_ (_x0_<_(a_^\_k)_._n_&_(a_^\_k)_._n_<_x0_+_r_) let n be Element of NAT ; ::_thesis: ( x0 < (a ^\ k) . n & (a ^\ k) . n < x0 + r ) a . (n + k) in rng a by VALUED_0:28; then a . (n + k) in right_open_halfline x0 by A59, 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 ( (a ^\ k) . n = a . (n + k) & k <= n + k ) by NAT_1:12, NAT_1:def_3; hence (a ^\ k) . n < x0 + r by A60; ::_thesis: verum end; A62: 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] A63: rng (a ^\ k) c= rng a by VALUED_0:21; ( x0 < (a ^\ k) . n & (a ^\ k) . n < x0 + r ) by A61; then consider c being Real such that A64: c in ].x0,((a ^\ k) . n).[ and A65: (f / g) . ((a ^\ k) . n) = ((f `| N) / (g `| N)) . c by A12; take c ; ::_thesis: S1[n,c] A66: (dom (f / g)) /\ (right_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:108, XBOOLE_1:1; hence S1[n,c] by A59, A64, A66, VALUED_0:27, XBOOLE_1:1; ::_thesis: verum end; consider b being Real_Sequence such that A67: for n being Element of NAT holds S1[n,b . n] from FUNCT_2:sch_3(A62); A68: now__::_thesis:_for_n_being_Element_of_NAT_holds_ (_d_._n_<=_b_._n_&_b_._n_<=_(a_^\_k)_._n_) let n be Element of NAT ; ::_thesis: ( d . n <= b . n & b . n <= (a ^\ k) . n ) b . n in ].x0,((a ^\ k) . n).[ by A67; 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:7; ::_thesis: verum end; A69: lim d = d . 0 by SEQ_4:26 .= x0 by FUNCOP_1:7 ; lim (a ^\ k) = x0 by A57, A58, SEQ_4:20; then A70: ( b is convergent & lim b = x0 ) by A57, A69, A68, SEQ_2:19, SEQ_2:20; A71: 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 A71; then A72: x0 in ].(x0 - r),(x0 + r).[ by RCOMP_1:def_2; A73: 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 A74: x = b . n by FUNCT_2:113; x0 < (a ^\ k) . n by A61; then A75: x0 - r < (a ^\ k) . n by A71, XXREAL_0:2; (a ^\ k) . n < x0 + r by A61; then (a ^\ k) . n in { g3 where g3 is Real : ( x0 - r < g3 & g3 < x0 + r ) } by A75; 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 A72, XXREAL_1:25, XXREAL_2:def_12; then ].x0,((a ^\ k) . n).[ c= ].(x0 - r),(x0 + r).[ by XBOOLE_1:1; then A76: ].x0,((a ^\ k) . n).[ c= dom ((f `| N) / (g `| N)) by A6, A10, XBOOLE_1:1; A77: x in ].x0,((a ^\ k) . n).[ by A67, A74; 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 A77, A76, XBOOLE_0:def_5; ::_thesis: verum end; A78: (dom ((f `| N) / (g `| N))) \ {x0} c= dom ((f `| N) / (g `| N)) by XBOOLE_1:36; A79: now__::_thesis:_ex_m_being_Element_of_NAT_st_ for_n_being_Element_of_NAT_st_m_<=_n_holds_ (((f_/_g)_/*_a)_^\_k)_._n_=_(((f_`|_N)_/_(g_`|_N))_/*_b)_._n 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 A67; hence (((f / g) /* a) ^\ k) . n = (((f `| N) / (g `| N)) /* b) . n by A73, A78, FUNCT_2:108, XBOOLE_1:1; ::_thesis: verum end; lim (((f `| N) / (g `| N)),x0) = lim (((f `| N) / (g `| N)),x0) ; then A80: ((f `| N) / (g `| N)) /* b is convergent by A8, A70, A73, LIMFUNC3:def_4; then A81: ((f / g) /* a) ^\ k is convergent by A79, SEQ_4:18; lim (((f `| N) / (g `| N)) /* b) = lim (((f `| N) / (g `| N)),x0) by A8, A70, A73, LIMFUNC3:def_4; then lim (((f / g) /* a) ^\ k) = lim (((f `| N) / (g `| N)),x0) by A80, A79, SEQ_4:19; hence ( (f / g) /* a is convergent & lim ((f / g) /* a) = lim (((f `| N) / (g `| N)),x0) ) by A81, SEQ_4:21, SEQ_4:22; ::_thesis: verum end; A82: 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 x0 < r1 holds ex t being Real st ( t < r1 & x0 < t & t in dom (f / g) ) by LIMFUNC3:8; then A83: ( f / g is_right_convergent_in x0 & lim_right ((f / g),x0) = lim (((f `| N) / (g `| N)),x0) ) by A56, Th2; A84: 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 A85: x0 + 0 < x0 + r by A9, XREAL_1:8; x0 - r < x0 by A9, XREAL_1:44; then x0 in { g1 where g1 is Real : ( x0 - r < g1 & g1 < x0 + r ) } by A85; then A86: x0 in ].(x0 - r),(x0 + r).[ by RCOMP_1:def_2; A87: (dom (f `| N)) /\ ((dom (g `| N)) \ ((g `| N) " {0})) c= (dom (g `| N)) \ ((g `| N) " {0}) by XBOOLE_1:17; A88: (dom f) /\ ((dom g) \ (g " {0})) c= (dom g) \ (g " {0}) by XBOOLE_1:17; 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 that A89: x0 - r < x and A90: x < x0 ; ::_thesis: ex c being Real st ( c in ].x,x0.[ & (f / g) . x = ((f `| N) / (g `| N)) . c ) set f1 = ((f . x) (#) g) - ((g . x) (#) f); A91: ( dom ((f . x) (#) g) = dom g & dom ((g . x) (#) f) = dom f ) by VALUED_1:def_5; then A92: dom (((f . x) (#) g) - ((g . x) (#) f)) = (dom f) /\ (dom g) by VALUED_1:12; x < x0 + r by A90, A85, XXREAL_0:2; then x in { g1 where g1 is Real : ( x0 - r < g1 & g1 < x0 + r ) } by A89; then x in ].(x0 - r),(x0 + r).[ by RCOMP_1:def_2; then A93: [.x,x0.] c= N by A10, A86, XXREAL_2:def_12; then A94: ( [.x,x0.] c= dom f & [.x,x0.] c= dom g ) by A1, A2, XBOOLE_1:1; then A95: [.x,x0.] c= dom (((f . x) (#) g) - ((g . x) (#) f)) by A92, XBOOLE_1:19; g | N is continuous by A4, FDIFF_1:25; then g | [.x,x0.] is continuous by A93, FCONT_1:16; then A96: ((f . x) (#) g) | [.x,x0.] is continuous by A2, A93, FCONT_1:20, XBOOLE_1:1; f | N is continuous by A3, FDIFF_1:25; then f | [.x,x0.] is continuous by A93, FCONT_1:16; then A97: ((g . x) (#) f) | [.x,x0.] is continuous by A1, A93, FCONT_1:20, XBOOLE_1:1; [.x,x0.] c= dom (((f . x) (#) g) - ((g . x) (#) f)) by A94, A92, XBOOLE_1:19; then A98: (((f . x) (#) g) - ((g . x) (#) f)) | [.x,x0.] is continuous by A91, A92, A97, A96, FCONT_1:18; A99: ].x,x0.[ c= [.x,x0.] by XXREAL_1:25; then A100: ].x,x0.[ c= N by A93, XBOOLE_1:1; A101: x in [.x,x0.] by A90, XXREAL_1:1; then x in dom (((f . x) (#) g) - ((g . x) (#) f)) by A95; then A102: x in (dom ((f . x) (#) g)) /\ (dom ((g . x) (#) f)) by VALUED_1:12; then A103: x in dom ((f . x) (#) g) by XBOOLE_0:def_4; A104: x0 in [.x,x0.] by A90, XXREAL_1:1; then x0 in dom (((f . x) (#) g) - ((g . x) (#) f)) by A95; then A105: x0 in (dom ((f . x) (#) g)) /\ (dom ((g . x) (#) f)) by VALUED_1:12; then A106: x0 in dom ((f . x) (#) g) by XBOOLE_0:def_4; A107: x in dom ((g . x) (#) f) by A102, XBOOLE_0:def_4; A108: (((f . x) (#) g) - ((g . x) (#) f)) . x = (((f . x) (#) g) . x) - (((g . x) (#) f) . x) by A95, A101, 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 A107, VALUED_1:def_5 .= 0 ; A109: x0 in dom ((g . x) (#) f) by A105, XBOOLE_0:def_4; not x in {x0} by A90, TARSKI:def_1; then A110: x in [.x,x0.] \ {x0} by A101, XBOOLE_0:def_5; N c= dom ((f . x) (#) g) by A2, VALUED_1:def_5; then A111: ].x,x0.[ c= dom ((f . x) (#) g) by A100, XBOOLE_1:1; N c= dom ((g . x) (#) f) by A1, VALUED_1:def_5; then A112: ].x,x0.[ c= dom ((g . x) (#) f) by A100, XBOOLE_1:1; then ].x,x0.[ c= (dom ((f . x) (#) g)) /\ (dom ((g . x) (#) f)) by A111, XBOOLE_1:19; then A113: ].x,x0.[ c= dom (((f . x) (#) g) - ((g . x) (#) f)) by VALUED_1:12; f is_differentiable_on ].x,x0.[ by A3, A93, A99, FDIFF_1:26, XBOOLE_1:1; then A114: (g . x) (#) f is_differentiable_on ].x,x0.[ by A112, FDIFF_1:20; g is_differentiable_on ].x,x0.[ by A4, A93, A99, FDIFF_1:26, XBOOLE_1:1; then A115: (f . x) (#) g is_differentiable_on ].x,x0.[ by A111, FDIFF_1:20; (((f . x) (#) g) - ((g . x) (#) f)) . x0 = (((f . x) (#) g) . x0) - (((g . x) (#) f) . x0) by A95, A104, VALUED_1:13 .= ((f . x) * (g . x0)) - (((g . x) (#) f) . x0) by A106, VALUED_1:def_5 .= 0 - ((g . x) * 0) by A7, A109, VALUED_1:def_5 .= 0 ; then consider t being Real such that A116: t in ].x,x0.[ and A117: diff ((((f . x) (#) g) - ((g . x) (#) f)),t) = 0 by A90, A98, A114, A113, A115, A95, A108, FDIFF_1:19, ROLLE:1; A118: (g . x) (#) f is_differentiable_in t by A114, A116, FDIFF_1:9; A119: f is_differentiable_in t by A3, A100, A116, FDIFF_1:9; (f . x) (#) g is_differentiable_in t by A115, A116, FDIFF_1:9; then 0 = (diff (((f . x) (#) g),t)) - (diff (((g . x) (#) f),t)) by A117, A118, FDIFF_1:14; then A120: 0 = (diff (((f . x) (#) g),t)) - ((g . x) * (diff (f,t))) by A119, FDIFF_1:15; take t ; ::_thesis: ( t in ].x,x0.[ & (f / g) . x = ((f `| N) / (g `| N)) . t ) A121: t in [.x,x0.] by A99, A116; [.x,x0.] \ {x0} c= N \ {x0} by A93, XBOOLE_1:33; then A122: [.x,x0.] \ {x0} c= dom (f / g) by A5, XBOOLE_1:1; then [.x,x0.] \ {x0} c= (dom f) /\ ((dom g) \ (g " {0})) by RFUNCT_1:def_1; then [.x,x0.] \ {x0} c= (dom g) \ (g " {0}) by A88, XBOOLE_1:1; then A123: ( x in dom g & not x in g " {0} ) by A110, XBOOLE_0:def_5; A124: now__::_thesis:_not_g_._x_=_0 assume g . x = 0 ; ::_thesis: contradiction then g . x in {0} by TARSKI:def_1; hence contradiction by A123, FUNCT_1:def_7; ::_thesis: verum end; A125: [.x,x0.] c= dom ((f `| N) / (g `| N)) by A6, A93, XBOOLE_1:1; 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 A87, XBOOLE_1:1; then A126: ( t in dom (g `| N) & not t in (g `| N) " {0} ) by A121, XBOOLE_0:def_5; A127: now__::_thesis:_not_diff_(g,t)_=_0 assume diff (g,t) = 0 ; ::_thesis: contradiction then (g `| N) . t = 0 by A4, A93, A121, FDIFF_1:def_7; then (g `| N) . t in {0} by TARSKI:def_1; hence contradiction by A126, FUNCT_1:def_7; ::_thesis: verum end; g is_differentiable_in t by A4, A100, A116, FDIFF_1:9; then 0 = ((f . x) * (diff (g,t))) - ((g . x) * (diff (f,t))) by A120, FDIFF_1:15; then (f . x) / (g . x) = (diff (f,t)) / (diff (g,t)) by A124, A127, 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 A122, A110, RFUNCT_1:def_1; then (f / g) . x = ((f `| N) . t) * ((diff (g,t)) ") by A3, A93, A121, FDIFF_1:def_7; then (f / g) . x = ((f `| N) . t) * (((g `| N) . t) ") by A4, A93, A121, FDIFF_1:def_7; hence ( t in ].x,x0.[ & (f / g) . x = ((f `| N) / (g `| N)) . t ) by A116, A125, A121, RFUNCT_1:def_1; ::_thesis: verum end; A128: 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 reconsider d = NAT --> x0 as Real_Sequence ; 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 that A129: a is convergent and A130: lim a = x0 and A131: 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) ) consider k being Element of NAT such that A132: for n being Element of NAT st k <= n holds ( x0 - r < a . n & a . n < x0 + r ) by A9, A11, A129, A130, LIMFUNC3:7; set a1 = a ^\ k; defpred S1[ Element of NAT , real number ] means ( $2 in ].((a ^\ k) . $1),x0.[ & (((f / g) /* a) ^\ k) . $1 = ((f `| N) / (g `| N)) . $2 ); A133: now__::_thesis:_for_n_being_Element_of_NAT_holds_ (_(a_^\_k)_._n_<_x0_&_x0_-_r_<_(a_^\_k)_._n_) let n be Element of NAT ; ::_thesis: ( (a ^\ k) . n < x0 & x0 - r < (a ^\ k) . n ) a . (n + k) in rng a by VALUED_0:28; then a . (n + k) in left_open_halfline x0 by A131, 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 ( (a ^\ k) . n = a . (n + k) & k <= n + k ) by NAT_1:12, NAT_1:def_3; hence x0 - r < (a ^\ k) . n by A132; ::_thesis: verum end; A134: 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] A135: rng (a ^\ k) c= rng a by VALUED_0:21; ( x0 - r < (a ^\ k) . n & (a ^\ k) . n < x0 ) by A133; then consider c being Real such that A136: c in ].((a ^\ k) . n),x0.[ and A137: (f / g) . ((a ^\ k) . n) = ((f `| N) / (g `| N)) . c by A84; take c ; ::_thesis: S1[n,c] A138: (dom (f / g)) /\ (left_open_halfline x0) c= dom (f / g) by XBOOLE_1:17; then rng a c= dom (f / g) by A131, XBOOLE_1:1; then ((f / g) /* (a ^\ k)) . n = ((f `| N) / (g `| N)) . c by A137, A135, FUNCT_2:108, XBOOLE_1:1; hence S1[n,c] by A131, A136, A138, VALUED_0:27, XBOOLE_1:1; ::_thesis: verum end; consider b being Real_Sequence such that A139: for n being Element of NAT holds S1[n,b . n] from FUNCT_2:sch_3(A134); A140: now__::_thesis:_for_n_being_Element_of_NAT_holds_ (_(a_^\_k)_._n_<=_b_._n_&_b_._n_<=_d_._n_) let n be Element of NAT ; ::_thesis: ( (a ^\ k) . n <= b . n & b . n <= d . n ) b . n in ].((a ^\ k) . n),x0.[ by A139; 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:7; ::_thesis: verum end; A141: lim d = d . 0 by SEQ_4:26 .= x0 by FUNCOP_1:7 ; lim (a ^\ k) = x0 by A129, A130, SEQ_4:20; then A142: ( b is convergent & lim b = x0 ) by A129, A141, A140, SEQ_2:19, SEQ_2:20; A143: 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 A143; then A144: x0 in ].(x0 - r),(x0 + r).[ by RCOMP_1:def_2; A145: 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 A146: x = b . n by FUNCT_2:113; (a ^\ k) . n < x0 by A133; then A147: (a ^\ k) . n < x0 + r by A143, XXREAL_0:2; x0 - r < (a ^\ k) . n by A133; then (a ^\ k) . n in { g3 where g3 is Real : ( x0 - r < g3 & g3 < x0 + r ) } by A147; 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 A144, XXREAL_1:25, XXREAL_2:def_12; then ].((a ^\ k) . n),x0.[ c= ].(x0 - r),(x0 + r).[ by XBOOLE_1:1; then A148: ].((a ^\ k) . n),x0.[ c= dom ((f `| N) / (g `| N)) by A6, A10, XBOOLE_1:1; A149: x in ].((a ^\ k) . n),x0.[ by A139, A146; 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 A149, A148, XBOOLE_0:def_5; ::_thesis: verum end; A150: (dom ((f `| N) / (g `| N))) \ {x0} c= dom ((f `| N) / (g `| N)) by XBOOLE_1:36; A151: now__::_thesis:_ex_m_being_Element_of_NAT_st_ for_n_being_Element_of_NAT_st_m_<=_n_holds_ (((f_/_g)_/*_a)_^\_k)_._n_=_(((f_`|_N)_/_(g_`|_N))_/*_b)_._n 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 A139; hence (((f / g) /* a) ^\ k) . n = (((f `| N) / (g `| N)) /* b) . n by A145, A150, FUNCT_2:108, XBOOLE_1:1; ::_thesis: verum end; lim (((f `| N) / (g `| N)),x0) = lim (((f `| N) / (g `| N)),x0) ; then A152: ((f `| N) / (g `| N)) /* b is convergent by A8, A142, A145, LIMFUNC3:def_4; then A153: ((f / g) /* a) ^\ k is convergent by A151, SEQ_4:18; lim (((f `| N) / (g `| N)) /* b) = lim (((f `| N) / (g `| N)),x0) by A8, A142, A145, LIMFUNC3:def_4; then lim (((f / g) /* a) ^\ k) = lim (((f `| N) / (g `| N)),x0) by A152, A151, SEQ_4:19; hence ( (f / g) /* a is convergent & lim ((f / g) /* a) = lim (((f `| N) / (g `| N)),x0) ) by A153, SEQ_4:21, SEQ_4:22; ::_thesis: verum end; for r1 being Real st r1 < x0 holds ex t being Real st ( r1 < t & t < x0 & t in dom (f / g) ) by A82, LIMFUNC3:8; then A154: ( f / g is_left_convergent_in x0 & lim_left ((f / g),x0) = lim (((f `| N) / (g `| N)),x0) ) by A128, Th3; hence f / g is_convergent_in x0 by A83, LIMFUNC3:30; ::_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 A83, A154, LIMFUNC3:30; ::_thesis: verum end; theorem :: L_HOSPIT:10 for f, g being PartFunc of REAL,REAL 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_continuous_in x0 ) holds ( f / g is_convergent_in x0 & lim ((f / g),x0) = (diff (f,x0)) / (diff (g,x0)) ) proof 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_continuous_in x0 ) holds ( f / g is_convergent_in x0 & lim ((f / g),x0) = (diff (f,x0)) / (diff (g,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_continuous_in x0 ) implies ( f / g is_convergent_in x0 & lim ((f / g),x0) = (diff (f,x0)) / (diff (g,x0)) ) ) 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: ( f / g is_convergent_in x0 & lim ((f / g),x0) = (diff (f,x0)) / (diff (g,x0)) ) consider r being real number such that A9: 0 < r and A10: N = ].(x0 - r),(x0 + r).[ by RCOMP_1:def_6; 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 A13: x0 + 0 < x0 + r by A9, XREAL_1:8; x0 - r < x0 by A9, XREAL_1:44; then x0 in { g1 where g1 is Real : ( x0 - r < g1 & g1 < x0 + r ) } by A13; then A14: x0 in ].(x0 - r),(x0 + r).[ by RCOMP_1:def_2; A15: (dom (f `| N)) /\ ((dom (g `| N)) \ ((g `| N) " {0})) c= (dom (g `| N)) \ ((g `| N) " {0}) by XBOOLE_1:17; A16: (dom f) /\ ((dom g) \ (g " {0})) c= (dom g) \ (g " {0}) by XBOOLE_1:17; 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 that A17: x0 - r < x and A18: x < x0 ; ::_thesis: ex c being Real st ( c in ].x,x0.[ & (f / g) . x = ((f `| N) / (g `| N)) . c ) set f1 = ((f . x) (#) g) - ((g . x) (#) f); A19: ( dom ((f . x) (#) g) = dom g & dom ((g . x) (#) f) = dom f ) by VALUED_1:def_5; then A20: dom (((f . x) (#) g) - ((g . x) (#) f)) = (dom f) /\ (dom g) by VALUED_1:12; x < x0 + r by A18, A13, XXREAL_0:2; then x in { g1 where g1 is Real : ( x0 - r < g1 & g1 < x0 + r ) } by A17; then x in ].(x0 - r),(x0 + r).[ by RCOMP_1:def_2; then A21: [.x,x0.] c= N by A10, A14, XXREAL_2:def_12; then A22: ( [.x,x0.] c= dom f & [.x,x0.] c= dom g ) by A1, A2, XBOOLE_1:1; then A23: [.x,x0.] c= dom (((f . x) (#) g) - ((g . x) (#) f)) by A20, XBOOLE_1:19; g | N is continuous by A4, FDIFF_1:25; then g | [.x,x0.] is continuous by A21, FCONT_1:16; then A24: ((f . x) (#) g) | [.x,x0.] is continuous by A2, A21, FCONT_1:20, XBOOLE_1:1; f | N is continuous by A3, FDIFF_1:25; then f | [.x,x0.] is continuous by A21, FCONT_1:16; then A25: ((g . x) (#) f) | [.x,x0.] is continuous by A1, A21, FCONT_1:20, XBOOLE_1:1; [.x,x0.] c= dom (((f . x) (#) g) - ((g . x) (#) f)) by A22, A20, XBOOLE_1:19; then A26: (((f . x) (#) g) - ((g . x) (#) f)) | [.x,x0.] is continuous by A19, A20, A25, A24, FCONT_1:18; A27: ].x,x0.[ c= [.x,x0.] by XXREAL_1:25; then A28: ].x,x0.[ c= N by A21, XBOOLE_1:1; A29: x in [.x,x0.] by A18, XXREAL_1:1; then x in dom (((f . x) (#) g) - ((g . x) (#) f)) by A23; then A30: x in (dom ((f . x) (#) g)) /\ (dom ((g . x) (#) f)) by VALUED_1:12; then A31: x in dom ((f . x) (#) g) by XBOOLE_0:def_4; A32: x0 in [.x,x0.] by A18, XXREAL_1:1; then x0 in dom (((f . x) (#) g) - ((g . x) (#) f)) by A23; then A33: x0 in (dom ((f . x) (#) g)) /\ (dom ((g . x) (#) f)) by VALUED_1:12; then A34: x0 in dom ((f . x) (#) g) by XBOOLE_0:def_4; A35: x in dom ((g . x) (#) f) by A30, XBOOLE_0:def_4; A36: (((f . x) (#) g) - ((g . x) (#) f)) . x = (((f . x) (#) g) . x) - (((g . x) (#) f) . x) by A23, A29, VALUED_1:13 .= ((f . x) * (g . x)) - (((g . x) (#) f) . x) by A31, VALUED_1:def_5 .= ((g . x) * (f . x)) - ((g . x) * (f . x)) by A35, VALUED_1:def_5 .= 0 ; A37: x0 in dom ((g . x) (#) f) by A33, XBOOLE_0:def_4; not x in {x0} by A18, TARSKI:def_1; then A38: x in [.x,x0.] \ {x0} by A29, XBOOLE_0:def_5; N c= dom ((f . x) (#) g) by A2, VALUED_1:def_5; then A39: ].x,x0.[ c= dom ((f . x) (#) g) by A28, XBOOLE_1:1; N c= dom ((g . x) (#) f) by A1, VALUED_1:def_5; then A40: ].x,x0.[ c= dom ((g . x) (#) f) by A28, XBOOLE_1:1; then ].x,x0.[ c= (dom ((f . x) (#) g)) /\ (dom ((g . x) (#) f)) by A39, XBOOLE_1:19; then A41: ].x,x0.[ c= dom (((f . x) (#) g) - ((g . x) (#) f)) by VALUED_1:12; f is_differentiable_on ].x,x0.[ by A3, A21, A27, FDIFF_1:26, XBOOLE_1:1; then A42: (g . x) (#) f is_differentiable_on ].x,x0.[ by A40, FDIFF_1:20; g is_differentiable_on ].x,x0.[ by A4, A21, A27, FDIFF_1:26, XBOOLE_1:1; then A43: (f . x) (#) g is_differentiable_on ].x,x0.[ by A39, FDIFF_1:20; (((f . x) (#) g) - ((g . x) (#) f)) . x0 = (((f . x) (#) g) . x0) - (((g . x) (#) f) . x0) by A23, A32, VALUED_1:13 .= ((f . x) * (g . x0)) - (((g . x) (#) f) . x0) by A34, VALUED_1:def_5 .= 0 - ((g . x) * 0) by A7, A37, VALUED_1:def_5 .= 0 ; then consider t being Real such that A44: t in ].x,x0.[ and A45: diff ((((f . x) (#) g) - ((g . x) (#) f)),t) = 0 by A18, A26, A42, A41, A43, A23, A36, FDIFF_1:19, ROLLE:1; A46: (g . x) (#) f is_differentiable_in t by A42, A44, FDIFF_1:9; A47: f is_differentiable_in t by A3, A28, A44, FDIFF_1:9; (f . x) (#) g is_differentiable_in t by A43, A44, FDIFF_1:9; then 0 = (diff (((f . x) (#) g),t)) - (diff (((g . x) (#) f),t)) by A45, A46, FDIFF_1:14; then A48: 0 = (diff (((f . x) (#) g),t)) - ((g . x) * (diff (f,t))) by A47, FDIFF_1:15; take t ; ::_thesis: ( t in ].x,x0.[ & (f / g) . x = ((f `| N) / (g `| N)) . t ) A49: t in [.x,x0.] by A27, A44; [.x,x0.] \ {x0} c= N \ {x0} by A21, XBOOLE_1:33; then A50: [.x,x0.] \ {x0} c= dom (f / g) by A5, XBOOLE_1:1; then [.x,x0.] \ {x0} c= (dom f) /\ ((dom g) \ (g " {0})) by RFUNCT_1:def_1; then [.x,x0.] \ {x0} c= (dom g) \ (g " {0}) by A16, XBOOLE_1:1; then A51: ( x in dom g & not x in g " {0} ) by A38, XBOOLE_0:def_5; A52: now__::_thesis:_not_g_._x_=_0 assume g . x = 0 ; ::_thesis: contradiction then g . x in {0} by TARSKI:def_1; hence contradiction by A51, FUNCT_1:def_7; ::_thesis: verum 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_1; 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__::_thesis:_not_diff_(g,t)_=_0 assume diff (g,t) = 0 ; ::_thesis: contradiction then (g `| N) . t = 0 by A4, A21, A49, FDIFF_1:def_7; then (g `| N) . t in {0} by TARSKI:def_1; hence contradiction by A54, FUNCT_1:def_7; ::_thesis: verum end; g is_differentiable_in t by A4, A28, A44, FDIFF_1:9; then 0 = ((f . x) * (diff (g,t))) - ((g . x) * (diff (f,t))) by A48, FDIFF_1:15; then (f . x) / (g . x) = (diff (f,t)) / (diff (g,t)) by A52, A55, 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 A50, A38, RFUNCT_1:def_1; then (f / g) . x = ((f `| N) . t) * ((diff (g,t)) ") by A3, A21, A49, FDIFF_1:def_7; then (f / g) . x = ((f `| N) . t) * (((g `| N) . t) ") by A4, A21, A49, FDIFF_1:def_7; hence ( t in ].x,x0.[ & (f / g) . x = ((f `| N) / (g `| N)) . t ) by A44, A53, A49, RFUNCT_1:def_1; ::_thesis: verum 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 convergent & lim ((f / g) /* a) = (diff (f,x0)) / (diff (g,x0)) ) proof reconsider d = NAT --> x0 as Real_Sequence ; 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) = (diff (f,x0)) / (diff (g,x0)) ) ) assume that A57: a is convergent and A58: lim a = x0 and A59: rng a c= (dom (f / g)) /\ (left_open_halfline x0) ; ::_thesis: ( (f / g) /* a is convergent & lim ((f / g) /* a) = (diff (f,x0)) / (diff (g,x0)) ) 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 S1[ Element of NAT , real number ] means ( $2 in ].((a ^\ k) . $1),x0.[ & (((f / g) /* a) ^\ k) . $1 = ((f `| N) / (g `| N)) . $2 ); A61: now__::_thesis:_for_n_being_Element_of_NAT_holds_ (_(a_^\_k)_._n_<_x0_&_x0_-_r_<_(a_^\_k)_._n_) let n be Element of NAT ; ::_thesis: ( (a ^\ k) . n < x0 & x0 - r < (a ^\ k) . n ) 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: x0 - r < (a ^\ k) . n ( (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: verum end; A62: 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] 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: S1[n,c] 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:108, XBOOLE_1:1; hence S1[n,c] by A59, A64, A66, VALUED_0:27, XBOOLE_1:1; ::_thesis: verum end; consider b being Real_Sequence such that A67: for n being Element of NAT holds S1[n,b . n] from FUNCT_2:sch_3(A62); A68: 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 A68; then A69: x0 in ].(x0 - r),(x0 + r).[ by RCOMP_1:def_2; A70: rng b c= (dom ((f `| N) / (g `| N))) /\ (left_open_halfline 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))) /\ (left_open_halfline x0) ) assume x in rng b ; ::_thesis: x in (dom ((f `| N) / (g `| N))) /\ (left_open_halfline x0) then consider n being Element of NAT such that A71: x = b . n by FUNCT_2:113; (a ^\ k) . n < x0 by A61; then A72: (a ^\ k) . n < x0 + r by A68, 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 A72; 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 A69, XXREAL_1:25, XXREAL_2:def_12; then ].((a ^\ k) . n),x0.[ c= ].(x0 - r),(x0 + r).[ by XBOOLE_1:1; then A73: ].((a ^\ k) . n),x0.[ c= dom ((f `| N) / (g `| N)) by A6, A10, XBOOLE_1:1; A74: x in ].((a ^\ k) . n),x0.[ by A67, A71; 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 A74, A73, XBOOLE_0:def_4; ::_thesis: verum end; A75: now__::_thesis:_for_n_being_Element_of_NAT_holds_ (_(a_^\_k)_._n_<=_b_._n_&_b_._n_<=_d_._n_) let n be Element of NAT ; ::_thesis: ( (a ^\ k) . n <= b . n & b . n <= d . n ) 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:7; ::_thesis: verum end; A76: lim d = d . 0 by SEQ_4:26 .= x0 by FUNCOP_1:7 ; lim (a ^\ k) = x0 by A57, A58, SEQ_4:20; then A77: ( b is convergent & lim b = x0 ) by A57, A76, A75, 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 A70, XBOOLE_1:1; then A80: ((f `| N) / (g `| N)) /* b is convergent by A8, A77, FCONT_1:def_1; A81: now__::_thesis:_ex_m_being_Element_of_NAT_st_ for_n_being_Element_of_NAT_st_m_<=_n_holds_ (((f_/_g)_/*_a)_^\_k)_._n_=_(((f_`|_N)_/_(g_`|_N))_/*_b)_._n 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 A67; hence (((f / g) /* a) ^\ k) . n = (((f `| N) / (g `| N)) /* b) . n by A70, A78, FUNCT_2:108, XBOOLE_1:1; ::_thesis: verum 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, A69, RFUNCT_1:def_1 .= (diff (f,x0)) * (((g `| N) . x0) ") by A3, A10, A69, FDIFF_1:def_7 .= (diff (f,x0)) * ((diff (g,x0)) ") by A4, A10, A69, FDIFF_1:def_7 ; then lim (((f / g) /* a) ^\ k) = (diff (f,x0)) * ((diff (g,x0)) ") by A80, A81, SEQ_4:19; then A82: 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 A82, SEQ_4:21, SEQ_4:22; ::_thesis: verum end; A83: 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 A84: ( f / g is_left_convergent_in x0 & lim_left ((f / g),x0) = (diff (f,x0)) / (diff (g,x0)) ) by A56, Th3; A85: 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 A86: x0 - r < x0 by A9, XREAL_1:44; x0 + 0 < x0 + r by A9, XREAL_1:8; then x0 in { g1 where g1 is Real : ( x0 - r < g1 & g1 < x0 + r ) } by A86; then A87: x0 in ].(x0 - r),(x0 + r).[ by RCOMP_1:def_2; A88: (dom (f `| N)) /\ ((dom (g `| N)) \ ((g `| N) " {0})) c= (dom (g `| N)) \ ((g `| N) " {0}) by XBOOLE_1:17; A89: (dom f) /\ ((dom g) \ (g " {0})) c= (dom g) \ (g " {0}) by XBOOLE_1:17; 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 that A90: x0 < x and A91: x < x0 + r ; ::_thesis: ex c being Real st ( c in ].x0,x.[ & (f / g) . x = ((f `| N) / (g `| N)) . c ) set f1 = ((f . x) (#) g) - ((g . x) (#) f); A92: ( dom ((f . x) (#) g) = dom g & dom ((g . x) (#) f) = dom f ) by VALUED_1:def_5; then A93: dom (((f . x) (#) g) - ((g . x) (#) f)) = (dom f) /\ (dom g) by VALUED_1:12; x0 - r < x by A90, A86, XXREAL_0:2; then x in { g1 where g1 is Real : ( x0 - r < g1 & g1 < x0 + r ) } by A91; then x in ].(x0 - r),(x0 + r).[ by RCOMP_1:def_2; then A94: [.x0,x.] c= N by A10, A87, XXREAL_2:def_12; then A95: ( [.x0,x.] c= dom f & [.x0,x.] c= dom g ) by A1, A2, XBOOLE_1:1; then A96: [.x0,x.] c= dom (((f . x) (#) g) - ((g . x) (#) f)) by A93, XBOOLE_1:19; g | N is continuous by A4, FDIFF_1:25; then g | [.x0,x.] is continuous by A94, FCONT_1:16; then A97: ((f . x) (#) g) | [.x0,x.] is continuous by A2, A94, FCONT_1:20, XBOOLE_1:1; f | N is continuous by A3, FDIFF_1:25; then f | [.x0,x.] is continuous by A94, FCONT_1:16; then A98: ((g . x) (#) f) | [.x0,x.] is continuous by A1, A94, FCONT_1:20, XBOOLE_1:1; [.x0,x.] c= dom (((f . x) (#) g) - ((g . x) (#) f)) by A95, A93, XBOOLE_1:19; then A99: (((f . x) (#) g) - ((g . x) (#) f)) | [.x0,x.] is continuous by A92, A93, A98, A97, FCONT_1:18; A100: ].x0,x.[ c= [.x0,x.] by XXREAL_1:25; then A101: ].x0,x.[ c= N by A94, XBOOLE_1:1; A102: x in [.x0,x.] by A90, XXREAL_1:1; then x in dom (((f . x) (#) g) - ((g . x) (#) f)) by A96; then A103: x in (dom ((f . x) (#) g)) /\ (dom ((g . x) (#) f)) by VALUED_1:12; then A104: x in dom ((f . x) (#) g) by XBOOLE_0:def_4; A105: x0 in [.x0,x.] by A90, XXREAL_1:1; then x0 in dom (((f . x) (#) g) - ((g . x) (#) f)) by A96; then A106: x0 in (dom ((f . x) (#) g)) /\ (dom ((g . x) (#) f)) by VALUED_1:12; then A107: x0 in dom ((f . x) (#) g) by XBOOLE_0:def_4; A108: x in dom ((g . x) (#) f) by A103, XBOOLE_0:def_4; A109: (((f . x) (#) g) - ((g . x) (#) f)) . x = (((f . x) (#) g) . x) - (((g . x) (#) f) . x) by A96, A102, VALUED_1:13 .= ((f . x) * (g . x)) - (((g . x) (#) f) . x) by A104, VALUED_1:def_5 .= ((g . x) * (f . x)) - ((g . x) * (f . x)) by A108, VALUED_1:def_5 .= 0 ; A110: x0 in dom ((g . x) (#) f) by A106, XBOOLE_0:def_4; not x in {x0} by A90, TARSKI:def_1; then A111: x in [.x0,x.] \ {x0} by A102, XBOOLE_0:def_5; N c= dom ((f . x) (#) g) by A2, VALUED_1:def_5; then A112: ].x0,x.[ c= dom ((f . x) (#) g) by A101, XBOOLE_1:1; N c= dom ((g . x) (#) f) by A1, VALUED_1:def_5; then A113: ].x0,x.[ c= dom ((g . x) (#) f) by A101, XBOOLE_1:1; then ].x0,x.[ c= (dom ((f . x) (#) g)) /\ (dom ((g . x) (#) f)) by A112, XBOOLE_1:19; then A114: ].x0,x.[ c= dom (((f . x) (#) g) - ((g . x) (#) f)) by VALUED_1:12; f is_differentiable_on ].x0,x.[ by A3, A94, A100, FDIFF_1:26, XBOOLE_1:1; then A115: (g . x) (#) f is_differentiable_on ].x0,x.[ by A113, FDIFF_1:20; g is_differentiable_on ].x0,x.[ by A4, A94, A100, FDIFF_1:26, XBOOLE_1:1; then A116: (f . x) (#) g is_differentiable_on ].x0,x.[ by A112, FDIFF_1:20; (((f . x) (#) g) - ((g . x) (#) f)) . x0 = (((f . x) (#) g) . x0) - (((g . x) (#) f) . x0) by A96, A105, VALUED_1:13 .= ((f . x) * (g . x0)) - (((g . x) (#) f) . x0) by A107, VALUED_1:def_5 .= 0 - ((g . x) * 0) by A7, A110, VALUED_1:def_5 .= 0 ; then consider t being Real such that A117: t in ].x0,x.[ and A118: diff ((((f . x) (#) g) - ((g . x) (#) f)),t) = 0 by A90, A99, A115, A114, A116, A96, A109, FDIFF_1:19, ROLLE:1; A119: (g . x) (#) f is_differentiable_in t by A115, A117, FDIFF_1:9; A120: f is_differentiable_in t by A3, A101, A117, FDIFF_1:9; (f . x) (#) g is_differentiable_in t by A116, A117, FDIFF_1:9; then 0 = (diff (((f . x) (#) g),t)) - (diff (((g . x) (#) f),t)) by A118, A119, FDIFF_1:14; then A121: 0 = (diff (((f . x) (#) g),t)) - ((g . x) * (diff (f,t))) by A120, FDIFF_1:15; take t ; ::_thesis: ( t in ].x0,x.[ & (f / g) . x = ((f `| N) / (g `| N)) . t ) A122: t in [.x0,x.] by A100, A117; [.x0,x.] \ {x0} c= N \ {x0} by A94, XBOOLE_1:33; then A123: [.x0,x.] \ {x0} c= dom (f / g) by A5, XBOOLE_1:1; then [.x0,x.] \ {x0} c= (dom f) /\ ((dom g) \ (g " {0})) by RFUNCT_1:def_1; then [.x0,x.] \ {x0} c= (dom g) \ (g " {0}) by A89, XBOOLE_1:1; then A124: ( x in dom g & not x in g " {0} ) by A111, XBOOLE_0:def_5; A125: now__::_thesis:_not_g_._x_=_0 assume g . x = 0 ; ::_thesis: contradiction then g . x in {0} by TARSKI:def_1; hence contradiction by A124, FUNCT_1:def_7; ::_thesis: verum end; A126: [.x0,x.] c= dom ((f `| N) / (g `| N)) by A6, A94, XBOOLE_1:1; 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 A88, XBOOLE_1:1; then A127: ( t in dom (g `| N) & not t in (g `| N) " {0} ) by A122, XBOOLE_0:def_5; A128: now__::_thesis:_not_diff_(g,t)_=_0 assume diff (g,t) = 0 ; ::_thesis: contradiction then (g `| N) . t = 0 by A4, A94, A122, FDIFF_1:def_7; then (g `| N) . t in {0} by TARSKI:def_1; hence contradiction by A127, FUNCT_1:def_7; ::_thesis: verum end; g is_differentiable_in t by A4, A101, A117, FDIFF_1:9; then 0 = ((f . x) * (diff (g,t))) - ((g . x) * (diff (f,t))) by A121, FDIFF_1:15; then (f . x) / (g . x) = (diff (f,t)) / (diff (g,t)) by A125, A128, 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 A123, A111, RFUNCT_1:def_1; then (f / g) . x = ((f `| N) . t) * ((diff (g,t)) ") by A3, A94, A122, FDIFF_1:def_7; then (f / g) . x = ((f `| N) . t) * (((g `| N) . t) ") by A4, A94, A122, FDIFF_1:def_7; hence ( t in ].x0,x.[ & (f / g) . x = ((f `| N) / (g `| N)) . t ) by A117, A126, A122, RFUNCT_1:def_1; ::_thesis: verum end; A129: 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 d = NAT --> x0 as Real_Sequence ; 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) = (diff (f,x0)) / (diff (g,x0)) ) ) assume that A130: a is convergent and A131: lim a = x0 and A132: rng a c= (dom (f / g)) /\ (right_open_halfline x0) ; ::_thesis: ( (f / g) /* a is convergent & lim ((f / g) /* a) = (diff (f,x0)) / (diff (g,x0)) ) consider k being Element of NAT such that A133: for n being Element of NAT st k <= n holds ( x0 - r < a . n & a . n < x0 + r ) by A9, A11, A130, A131, LIMFUNC3:7; set a1 = a ^\ k; defpred S1[ Element of NAT , real number ] means ( $2 in ].x0,((a ^\ k) . $1).[ & (((f / g) /* a) ^\ k) . $1 = ((f `| N) / (g `| N)) . $2 ); A134: now__::_thesis:_for_n_being_Element_of_NAT_holds_ (_x0_<_(a_^\_k)_._n_&_(a_^\_k)_._n_<_x0_+_r_) let n be Element of NAT ; ::_thesis: ( x0 < (a ^\ k) . n & (a ^\ k) . n < x0 + r ) a . (n + k) in rng a by VALUED_0:28; then a . (n + k) in right_open_halfline x0 by A132, 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 ( (a ^\ k) . n = a . (n + k) & k <= n + k ) by NAT_1:12, NAT_1:def_3; hence (a ^\ k) . n < x0 + r by A133; ::_thesis: verum end; A135: 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] A136: rng (a ^\ k) c= rng a by VALUED_0:21; ( x0 < (a ^\ k) . n & (a ^\ k) . n < x0 + r ) by A134; then consider c being Real such that A137: c in ].x0,((a ^\ k) . n).[ and A138: (f / g) . ((a ^\ k) . n) = ((f `| N) / (g `| N)) . c by A85; take c ; ::_thesis: S1[n,c] A139: (dom (f / g)) /\ (right_open_halfline x0) c= dom (f / g) by XBOOLE_1:17; then rng a c= dom (f / g) by A132, XBOOLE_1:1; then ((f / g) /* (a ^\ k)) . n = ((f `| N) / (g `| N)) . c by A138, A136, FUNCT_2:108, XBOOLE_1:1; hence S1[n,c] by A132, A137, A139, VALUED_0:27, XBOOLE_1:1; ::_thesis: verum end; consider b being Real_Sequence such that A140: for n being Element of NAT holds S1[n,b . n] from FUNCT_2:sch_3(A135); A141: 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 A141; then A142: x0 in ].(x0 - r),(x0 + r).[ by RCOMP_1:def_2; A143: rng b c= (dom ((f `| N) / (g `| N))) /\ (right_open_halfline 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))) /\ (right_open_halfline x0) ) assume x in rng b ; ::_thesis: x in (dom ((f `| N) / (g `| N))) /\ (right_open_halfline x0) then consider n being Element of NAT such that A144: x = b . n by FUNCT_2:113; x0 < (a ^\ k) . n by A134; then A145: x0 - r < (a ^\ k) . n by A141, XXREAL_0:2; (a ^\ k) . n < x0 + r by A134; then (a ^\ k) . n in { g3 where g3 is Real : ( x0 - r < g3 & g3 < x0 + r ) } by A145; 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 A142, XXREAL_1:25, XXREAL_2:def_12; then ].x0,((a ^\ k) . n).[ c= ].(x0 - r),(x0 + r).[ by XBOOLE_1:1; then A146: ].x0,((a ^\ k) . n).[ c= dom ((f `| N) / (g `| N)) by A6, A10, XBOOLE_1:1; A147: x in ].x0,((a ^\ k) . n).[ by A140, A144; 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 A147, A146, XBOOLE_0:def_4; ::_thesis: verum end; A148: now__::_thesis:_for_n_being_Element_of_NAT_holds_ (_d_._n_<=_b_._n_&_b_._n_<=_(a_^\_k)_._n_) let n be Element of NAT ; ::_thesis: ( d . n <= b . n & b . n <= (a ^\ k) . n ) b . n in ].x0,((a ^\ k) . n).[ by A140; 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:7; ::_thesis: verum end; A149: lim d = d . 0 by SEQ_4:26 .= x0 by FUNCOP_1:7 ; lim (a ^\ k) = x0 by A130, A131, SEQ_4:20; then A150: ( b is convergent & lim b = x0 ) by A130, A149, A148, SEQ_2:19, SEQ_2:20; A151: (dom ((f `| N) / (g `| N))) /\ (right_open_halfline x0) c= dom ((f `| N) / (g `| N)) by XBOOLE_1:17; then A152: rng b c= dom ((f `| N) / (g `| N)) by A143, XBOOLE_1:1; then A153: ((f `| N) / (g `| N)) /* b is convergent by A8, A150, FCONT_1:def_1; A154: now__::_thesis:_ex_m_being_Element_of_NAT_st_ for_n_being_Element_of_NAT_st_m_<=_n_holds_ (((f_/_g)_/*_a)_^\_k)_._n_=_(((f_`|_N)_/_(g_`|_N))_/*_b)_._n 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 A140; hence (((f / g) /* a) ^\ k) . n = (((f `| N) / (g `| N)) /* b) . n by A143, A151, FUNCT_2:108, XBOOLE_1:1; ::_thesis: verum end; lim (((f `| N) / (g `| N)) /* b) = ((f `| N) / (g `| N)) . x0 by A8, A150, A152, FCONT_1:def_1; then lim (((f `| N) / (g `| N)) /* b) = ((f `| N) . x0) * (((g `| N) . x0) ") by A6, A10, A142, RFUNCT_1:def_1 .= (diff (f,x0)) * (((g `| N) . x0) ") by A3, A10, A142, FDIFF_1:def_7 .= (diff (f,x0)) * ((diff (g,x0)) ") by A4, A10, A142, FDIFF_1:def_7 ; then lim (((f / g) /* a) ^\ k) = (diff (f,x0)) * ((diff (g,x0)) ") by A153, A154, SEQ_4:19; then A155: lim (((f / g) /* a) ^\ k) = (diff (f,x0)) / (diff (g,x0)) by XCMPLX_0:def_9; ((f / g) /* a) ^\ k is convergent by A153, A154, SEQ_4:18; hence ( (f / g) /* a is convergent & lim ((f / g) /* a) = (diff (f,x0)) / (diff (g,x0)) ) by A155, SEQ_4:21, SEQ_4:22; ::_thesis: verum end; for r1 being Real st x0 < r1 holds ex t being Real st ( t < r1 & x0 < t & t in dom (f / g) ) by A83, LIMFUNC3:8; then ( f / g is_right_convergent_in x0 & lim_right ((f / g),x0) = (diff (f,x0)) / (diff (g,x0)) ) by A129, Th2; hence ( f / g is_convergent_in x0 & lim ((f / g),x0) = (diff (f,x0)) / (diff (g,x0)) ) by A84, LIMFUNC3:30; ::_thesis: verum end;