:: The de l'Hospital Theorem
::  by Ma{\l}gorzata Korolkiewicz
::
:: Received February 20, 1992
:: Copyright (c) 1992-2012 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies PARTFUN1, NUMBERS, REAL_1, SEQ_1, SUBSET_1, FCONT_1, ARYTM_3,
      RELAT_1, LIMFUNC3, SEQ_2, ORDINAL2, TARSKI, XBOOLE_0, FUNCT_2, FUNCT_1,
      LIMFUNC2, LIMFUNC1, RCOMP_1, XREAL_0, ORDINAL1, CARD_1, XXREAL_1,
      ARYTM_1, FDIFF_1, VALUED_1, FUNCOP_1, XXREAL_0, NAT_1;
 notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XREAL_0, REAL_1,
      NAT_1, FUNCT_2, FUNCOP_1, VALUED_0, VALUED_1, SEQ_1, COMSEQ_2,
      SEQ_2, RELSET_1,
      PARTFUN1, RFUNCT_1, RCOMP_1, FCONT_1, FDIFF_1, LIMFUNC1, LIMFUNC2,
      LIMFUNC3, XXREAL_0;
 constructors PARTFUN1, FUNCOP_1, REAL_1, NAT_1, SEQ_2, SEQM_3, PROB_1,
      RCOMP_1, RFUNCT_1, RFUNCT_2, FCONT_1, LIMFUNC1, FDIFF_1, LIMFUNC2,
      LIMFUNC3, VALUED_1, SEQ_1, XXREAL_2, RELSET_1, SEQ_4, COMSEQ_2;
 registrations ORDINAL1, RELSET_1, NUMBERS, XREAL_0, MEMBERED, RCOMP_1,
      VALUED_0, XXREAL_2, FUNCOP_1, XBOOLE_0, SEQ_4, FUNCT_2, COMSEQ_2;
 requirements SUBSET, BOOLE, ARITHM;
 definitions TARSKI, PROB_1, LIMFUNC1;
 theorems TARSKI, NAT_1, RFUNCT_1, RCOMP_1, FCONT_1, FDIFF_1, ROLLE, SEQ_2,
      SEQ_4, LIMFUNC2, LIMFUNC1, LIMFUNC3, ZFMISC_1, FUNCT_1, XREAL_0,
      XBOOLE_0, XBOOLE_1, XCMPLX_0, XCMPLX_1, FUNCOP_1, XREAL_1, XXREAL_0,
      VALUED_1, XXREAL_1, XXREAL_2, FUNCT_2, VALUED_0;
 schemes FUNCT_2;

begin

reserve f,g for PartFunc of REAL,REAL,
  r,r1,r2,g1,g2,g3,g4,g5,g6,x,x0,t,c for Real,
  a,b,s for Real_Sequence,
  n,k for Element of NAT;

theorem
  f is_continuous_in x0 & (for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1
& g1<x0 & g1 in dom f & g2<r2 & x0<g2 & g2 in dom f) implies f is_convergent_in
  x0
proof
  assume that
A1: f is_continuous_in x0 and
A2: for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom f &
  g2<r2 & x0<g2 & g2 in dom f;
  now
    let s such that
A3: s is convergent & lim s=x0 and
A4: rng s c= dom 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;
  end;
  hence thesis by A2,LIMFUNC3:def 1;
end;

theorem Th2:
  f is_right_convergent_in x0 & lim_right(f,x0) = t iff (for r st
x0<r ex t st t<r & x0<t & t in dom f) & for a 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
  thus f is_right_convergent_in x0 & lim_right(f,x0) = t implies (for r st x0<
  r ex t st t<r & x0<t & t in dom f) & for a 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,def 8;
  thus (for r st x0<r ex t st t<r & x0<t & t in dom f) & (for a 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
  proof
    assume that
A1: for r st x0<r ex t st t<r & x0<t & t in dom f and
A2: for a 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 by A1,A2,LIMFUNC2:def 4;
    hence thesis by A2,LIMFUNC2:def 8;
  end;
end;

theorem Th3:
  f is_left_convergent_in x0 & lim_left(f,x0) = t iff (for r st r<
  x0 ex t st r<t & t<x0 & t in dom f) & for a 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
  thus f is_left_convergent_in x0 & lim_left(f,x0) = t implies (for r st r<x0
ex t st r<t & t<x0 & t in dom f) & for a 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,def 7;
  thus (for r st r<x0 ex t st r<t & t<x0 & t in dom f) & (for a 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
  proof
    assume that
A1: for r st r<x0 ex t st r<t & t<x0 & t in dom f and
A2: for a 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 by A1,A2,LIMFUNC2:def 1;
    hence thesis by A2,LIMFUNC2:def 7;
  end;
end;

theorem Th4:
  (ex N being Neighbourhood of x0 st N\{x0} c=dom f) implies for r1
,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom f & g2<r2 & x0<g2 &
  g2 in dom f
proof
  given N being Neighbourhood of x0 such that
A1: N\{x0} c= dom f;
  consider r be 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 thesis by A1,A2,A4,LIMFUNC3:5;
end;

theorem
  (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
proof
  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;
  consider r be 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 st x0-r<x & x<x0 ex c 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: 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 such that
A17: x0-r<x and
A18: x<x0;
    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: 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 f1 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 f1 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 f1 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: f1.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;
    f1.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 such that
A44: t in ].x,x0.[ and
A45: diff(f1,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;
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
      assume g.x=0;
      then g.x in {0} by TARSKI:def 1;
      hence contradiction by A51,FUNCT_1:def 7;
    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
      assume diff(g,t)=0;
      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;
    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 thesis by A44,A53,A49,RFUNCT_1:def 1;
  end;
A56: for a 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;
    assume that
A57: a is convergent and
A58: lim a = x0 and
A59: rng a c= dom (f/g) /\ left_open_halfline(x0);
    consider k such that
A60: for n st k<=n holds x0-r<a.n & a.n<x0+r by A9,A11,A57,A58,LIMFUNC3:7;
    set a1 = a^\k;
    defpred X[Element of NAT, real number] means $2 in ].a1.$1,x0.[ & (((f/g)
    /*a)^\k).$1=((f`|N)/(g`|N)).$2;
A61: now
      let 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:g1<x0} by XXREAL_1:229;
      then ex g1 st a.(n+k)=g1 & g1<x0;
      hence a1.n<x0 by NAT_1:def 3;
      a1.n = a.(n+k) & k<=n+k by NAT_1:12,def 3;
      hence x0-r<a1.n by A60;
    end;
A62: for n ex c be Real st X[n,c]
    proof
      let n;
A63:  rng a1 c= rng a by VALUED_0:21;
      x0-r<a1.n & a1.n<x0 by A61;
      then consider c such that
A64:  c in ].a1.n,x0.[ and
A65:  (f/g).(a1.n)=((f`|N)/(g`|N)).c by A12;
      take 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 thesis by A59,A64,A66,VALUED_0:27,XBOOLE_1:1;
    end;
    consider b such that
A67: for n holds X[n,b.n] from FUNCT_2:sch 3(A62);
A68: now
      let n;
      b.n in ].a1.n,x0.[ by A67;
      then b.n in {g1:a1.n<g1 & g1<x0} by RCOMP_1:def 2;
      then ex g1 st g1=b.n & a1.n<g1 & g1<x0;
      hence a1.n<=b.n & b.n<= d.n by FUNCOP_1:7;
    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: 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;
      assume x in rng b;
      then consider n such that
A73:  x=b.n by FUNCT_2:113;
      a1.n<x0 by A61;
      then
A74:  a1.n<x0+r by A70,XXREAL_0:2;
      x0-r<a1.n by A61;
      then a1.n in {g3: x0-r<g3 & g3<x0+r} by A74;
      then a1.n in ].x0-r,x0+r.[ by RCOMP_1:def 2;
      then ].a1.n,x0.[ c= [.a1.n,x0.] & [.a1.n,x0.] c= ].x0-r,x0+r.[ by A71,
XXREAL_1:25,XXREAL_2:def 12;
      then ].a1.n,x0.[ c= ].x0-r,x0+r.[ by XBOOLE_1:1;
      then
A75:  ].a1.n,x0.[ c= dom ((f`|N)/(g`|N)) by A6,A10,XBOOLE_1:1;
A76:  x in ].a1.n,x0.[ by A67,A73;
      then x in {g1:a1.n<g1 & g1<x0} by RCOMP_1:def 2;
      then ex g1 st g1 = x & a1.n<g1 & g1<x0;
      then not x in {x0} by TARSKI:def 1;
      hence thesis by A76,A75,XBOOLE_0:def 5;
    end;
A77: dom ((f`|N)/(g`|N)) \{x0} c= dom ((f`|N)/(g`|N)) by XBOOLE_1:36;
A78: now
      let 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;
    end;
    lim a1=x0 by A57,A58,SEQ_4:20;
    then b is convergent & lim b=x0 by A57,A69,A68,SEQ_2:19,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 thesis by LIMFUNC1:7;
  end;
A79: for r1,r2 st r1<x0 & x0<r2 ex g1,g2 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 st r1<x0 ex t 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 st x0<x & x<x0+r ex c 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: 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 such that
A86: x0<x and
A87: x<x0+r;
    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: 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 f1 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 f1 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 f1 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: f1.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;
    f1.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 such that
A111: t in ].x0,x.[ and
A112: diff(f1,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;
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
      assume g.x=0;
      then g.x in {0} by TARSKI:def 1;
      hence contradiction by A118,FUNCT_1:def 7;
    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
      assume diff(g,t)=0;
      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;
    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 thesis by A111,A120,A116,RFUNCT_1:def 1;
  end;
A123: for a 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;
    assume that
A124: a is convergent and
A125: lim a = x0 and
A126: rng a c= dom (f/g) /\ right_open_halfline(x0);
    consider k such that
A127: for n st k<=n holds x0-r<a.n & a.n<x0+r by A9,A11,A124,A125,LIMFUNC3:7;
    set a1 = a^\k;
    defpred X[Element of NAT,real number] means $2 in ].x0,a1.$1.[ & (((f/g)/*
    a)^\k).$1=((f`|N)/(g`|N)).$2;
A128: now
      let n;
      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:x0<g1} by XXREAL_1:230;
      then ex g1 st a.(n+k)=g1 & x0<g1;
      hence x0<a1.n by NAT_1:def 3;
      a1.n = a.(n+k) & k<=n+k by NAT_1:12,def 3;
      hence a1.n<x0+r by A127;
    end;
A129: for n ex c be Real st X[n,c]
    proof
      let n;
A130: rng a1 c= rng a by VALUED_0:21;
      x0<a1.n & a1.n<x0+r by A128;
      then consider c such that
A131: c in ].x0,a1.n.[ and
A132: (f/g).(a1.n)=((f`|N)/(g`|N)).c by A81;
      take 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 thesis by A126,A131,A133,VALUED_0:27,XBOOLE_1:1;
    end;
    consider b such that
A134: for n holds X[n,b.n] from FUNCT_2:sch 3(A129);
A135: now
      let n;
      b.n in ].x0,a1.n.[ by A134;
      then b.n in {g1:x0<g1 & g1<a1.n} by RCOMP_1:def 2;
      then ex g1 st g1=b.n & x0<g1 & g1<a1.n;
      hence d.n<=b.n & b.n<=a1.n by FUNCOP_1:7;
    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: 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;
      assume x in rng b;
      then consider n such that
A140: x=b.n by FUNCT_2:113;
      x0<a1.n by A128;
      then
A141: x0-r<a1.n by A137,XXREAL_0:2;
      a1.n<x0+r by A128;
      then a1.n in {g3: x0-r<g3 & g3<x0+r} by A141;
      then a1.n in ].x0-r,x0+r.[ by RCOMP_1:def 2;
      then ].x0,a1.n.[ c= [.x0,a1.n.] & [.x0,a1.n.] c= ].x0-r,x0+r.[ by A138,
XXREAL_1:25,XXREAL_2:def 12;
      then ].x0,a1.n.[ c= ].x0-r,x0+r.[ by XBOOLE_1:1;
      then
A142: ].x0,a1.n.[ c= dom ((f`|N)/(g`|N)) by A6,A10,XBOOLE_1:1;
A143: x in ].x0,a1.n.[ by A134,A140;
      then x in {g1:x0<g1 & g1<a1.n} by RCOMP_1:def 2;
      then ex g1 st g1 = x & x0<g1 & g1<a1.n;
      then not x in {x0} by TARSKI:def 1;
      hence thesis by A143,A142,XBOOLE_0:def 5;
    end;
A144: dom ((f`|N)/(g`|N)) \{x0} c= dom ((f`|N)/(g`|N)) by XBOOLE_1:36;
A145: now
      let 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;
    end;
    lim a1=x0 by A124,A125,SEQ_4:20;
    then b is convergent & lim b=x0 by A124,A136,A135,SEQ_2:19,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 thesis by LIMFUNC1:7;
  end;
  for r1 st x0<r1 ex t 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 thesis by A80,LIMFUNC3:12;
end;

theorem
  (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
proof
  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;
  consider r be 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 st x0-r<x & x<x0 ex c 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: 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 such that
A17: x0-r<x and
A18: x<x0;
    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: 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 f1 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 f1 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 f1 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: f1.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;
    f1.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 such that
A44: t in ].x,x0.[ and
A45: diff(f1,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;
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
      assume g.x=0;
      then g.x in {0} by TARSKI:def 1;
      hence contradiction by A51,FUNCT_1:def 7;
    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
      assume diff(g,t)=0;
      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;
    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 thesis by A44,A53,A49,RFUNCT_1:def 1;
  end;
A56: for a 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;
    assume that
A57: a is convergent and
A58: lim a = x0 and
A59: rng a c= dom (f/g) /\ left_open_halfline(x0);
    consider k such that
A60: for n st k<=n holds x0-r<a.n & a.n<x0+r by A9,A11,A57,A58,LIMFUNC3:7;
    set a1 = a^\k;
    defpred X[Element of NAT,real number] means $2 in ].a1.$1,x0.[ & (((f/g)/*
    a)^\k).$1=((f`|N)/(g`|N)).$2;
A61: now
      let 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:g1<x0} by XXREAL_1:229;
      then ex g1 st a.(n+k)=g1 & g1<x0;
      hence a1.n<x0 by NAT_1:def 3;
      a1.n = a.(n+k) & k<=n+k by NAT_1:12,def 3;
      hence x0-r<a1.n by A60;
    end;
A62: for n ex c be Real st X[n,c]
    proof
      let n;
A63:  rng a1 c= rng a by VALUED_0:21;
      x0-r<a1.n & a1.n<x0 by A61;
      then consider c such that
A64:  c in ].a1.n,x0.[ and
A65:  (f/g).(a1.n)=((f`|N)/(g`|N)).c by A12;
      take 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 thesis by A59,A64,A66,VALUED_0:27,XBOOLE_1:1;
    end;
    consider b such that
A67: for n holds X[n,b.n] from FUNCT_2:sch 3(A62);
A68: now
      let n;
      b.n in ].a1.n,x0.[ by A67;
      then b.n in {g1:a1.n<g1 & g1<x0} by RCOMP_1:def 2;
      then ex g1 st g1=b.n & a1.n<g1 & g1<x0;
      hence a1.n<=b.n & b.n<= d.n by FUNCOP_1:7;
    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: 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;
      assume x in rng b;
      then consider n such that
A73:  x=b.n by FUNCT_2:113;
      a1.n<x0 by A61;
      then
A74:  a1.n<x0+r by A70,XXREAL_0:2;
      x0-r<a1.n by A61;
      then a1.n in {g3: x0-r<g3 & g3<x0+r} by A74;
      then a1.n in ].x0-r,x0+r.[ by RCOMP_1:def 2;
      then ].a1.n,x0.[ c= [.a1.n,x0.] & [.a1.n,x0.] c= ].x0-r,x0+r.[ by A71,
XXREAL_1:25,XXREAL_2:def 12;
      then ].a1.n,x0.[ c= ].x0-r,x0+r.[ by XBOOLE_1:1;
      then
A75:  ].a1.n,x0.[ c= dom ((f`|N)/(g`|N)) by A6,A10,XBOOLE_1:1;
A76:  x in ].a1.n,x0.[ by A67,A73;
      then x in {g1:a1.n<g1 & g1<x0} by RCOMP_1:def 2;
      then ex g1 st g1 = x & a1.n<g1 & g1<x0;
      then not x in {x0} by TARSKI:def 1;
      hence thesis by A76,A75,XBOOLE_0:def 5;
    end;
A77: dom ((f`|N)/(g`|N)) \{x0} c= dom ((f`|N)/(g`|N)) by XBOOLE_1:36;
A78: now
      let 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;
    end;
    lim a1=x0 by A57,A58,SEQ_4:20;
    then b is convergent & lim b=x0 by A57,A69,A68,SEQ_2:19,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 thesis by LIMFUNC1:7;
  end;
A79: for r1,r2 st r1<x0 & x0<r2 ex g1,g2 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 st r1<x0 ex t 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 st x0<x & x<x0+r ex c 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: x0-r<g1 & g1<x0+r} by A83;
    then
A84: x0 in ].x0-r,x0+r.[ by RCOMP_1:def 2;
    let x such that
A85: x0<x and
A86: x<x0+r;
    x0-r<x by A85,A83,XXREAL_0:2;
    then x in {g1: 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 f1 by A88,XBOOLE_1:19;
A103: x in [.x0,x.] by A85,XXREAL_1:1;
    then x in dom f1 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 f1 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: f1.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;
    f1.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 such that
A113: t in ].x0,x.[ and
A114: diff(f1,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;
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
      assume g.x=0;
      then g.x in {0} by TARSKI:def 1;
      hence contradiction by A120,FUNCT_1:def 7;
    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
      assume diff(g,t)=0;
      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;
    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 thesis by A113,A122,A118,RFUNCT_1:def 1;
  end;
A125: for a 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;
    assume that
A126: a is convergent and
A127: lim a = x0 and
A128: rng a c= dom (f/g) /\ right_open_halfline(x0);
    consider k such that
A129: for n st k<=n holds x0-r<a.n & a.n<x0+r by A9,A11,A126,A127,LIMFUNC3:7;
    set a1 = a^\k;
    defpred X[Element of NAT,real number] means $2 in ].x0,a1.$1.[ & (((f/g)/*
    a)^\k).$1=((f`|N)/(g`|N)).$2;
A130: now
      let n;
      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:x0<g1} by XXREAL_1:230;
      then ex g1 st a.(n+k)=g1 & x0<g1;
      hence x0<a1.n by NAT_1:def 3;
      a1.n = a.(n+k) & k<=n+k by NAT_1:12,def 3;
      hence a1.n<x0+r by A129;
    end;
A131: for n ex c be Real st X[n,c]
    proof
      let n;
A132: rng a1 c= rng a by VALUED_0:21;
      x0<a1.n & a1.n<x0+r by A130;
      then consider c such that
A133: c in ].x0,a1.n.[ and
A134: (f/g).(a1.n)=((f`|N)/(g`|N)).c by A81;
      take 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 thesis by A128,A133,A135,VALUED_0:27,XBOOLE_1:1;
    end;
    consider b such that
A136: for n holds X[n,b.n] from FUNCT_2:sch 3(A131);
A137: now
      let n;
      b.n in ].x0,a1.n.[ by A136;
      then b.n in {g1:x0<g1 & g1<a1.n} by RCOMP_1:def 2;
      then ex g1 st g1=b.n & x0<g1 & g1<a1.n;
      hence d.n<=b.n & b.n<=a1.n by FUNCOP_1:7;
    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: 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;
      assume x in rng b;
      then consider n such that
A142: x=b.n by FUNCT_2:113;
      x0<a1.n by A130;
      then
A143: x0-r<a1.n by A139,XXREAL_0:2;
      a1.n<x0+r by A130;
      then a1.n in {g3: x0-r<g3 & g3<x0+r} by A143;
      then a1.n in ].x0-r,x0+r.[ by RCOMP_1:def 2;
      then ].x0,a1.n.[ c= [.x0,a1.n.] & [.x0,a1.n.] c= ].x0-r,x0+r.[ by A140,
XXREAL_1:25,XXREAL_2:def 12;
      then ].x0,a1.n.[ c= ].x0-r,x0+r.[ by XBOOLE_1:1;
      then
A144: ].x0,a1.n.[ c= dom ((f`|N)/(g`|N)) by A6,A10,XBOOLE_1:1;
A145: x in ].x0,a1.n.[ by A136,A142;
      then x in {g1:x0<g1 & g1<a1.n} by RCOMP_1:def 2;
      then ex g1 st g1 = x & x0<g1 & g1<a1.n;
      then not x in {x0} by TARSKI:def 1;
      hence thesis by A145,A144,XBOOLE_0:def 5;
    end;
A146: dom ((f`|N)/(g`|N)) \{x0} c= dom ((f`|N)/(g`|N)) by XBOOLE_1:36;
A147: now
      let 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;
    end;
    lim a1=x0 by A126,A127,SEQ_4:20;
    then b is convergent & lim b=x0 by A126,A138,A137,SEQ_2:19,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 thesis by LIMFUNC1:7;
  end;
  for r1 st x0<r1 ex t 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 thesis by A80,LIMFUNC3:13;
end;

theorem
  x0 in dom f /\ dom g & (ex r 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 st r>0
  & lim_right(f/g,x0) = lim_right(((f`|(].x0,x0+r.[))/(g`|(].x0,x0+r.[))),x0)
proof
  assume
A1: x0 in dom f /\ dom g;
  given r 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;
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 st x0<x & x<x0+r ex c st c in ].x0,x.[ & (f/g).x=((f`|].x0,x0+r.[
  )/(g`|].x0,x0+r.[)).c
  proof
    let x;
    assume that
A17: x0<x and
A18: x<x0+r;
    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;
      assume
A23:  y in [.x0,x.];
      then reconsider 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 thesis by A24,XXREAL_1:1;
    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 f1 by A21,XBOOLE_1:19;
A27: x in [.x0,x.] by A17,XXREAL_1:1;
    then x in dom f1 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: f1.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: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 f1 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;
      assume y in ].x0,x.[;
      then y in {g2:x0<g2 & g2<x} by RCOMP_1:def 2;
      then consider g2 such that
A42:  g2=y & x0<g2 and
A43:  g2<x;
      g2<x0+r by A18,A43,XXREAL_0:2;
      then y in {g3:x0<g3 & g3<x0+r} by A42;
      hence thesis by RCOMP_1:def 2;
    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 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 such that
A50:  rng s c= [.x0,x.] and
A51:  s is convergent and
A52:  lim s in [.x0,x.];
      set z = lim s;
A53:  rng s c= dom g by A48,A50,XBOOLE_1:1;
A54:  z in ].x0,x.[ \/ {x0,x} by A17,A52,XXREAL_1:128;
      now
        per cases by A54,XBOOLE_0:def 3;
        suppose
          z in ].x0,x.[;
          then g is_differentiable_in z by A6,A41,FDIFF_1:9;
          then g is_continuous_in z by FDIFF_1:24;
          hence thesis by A51,A53,FCONT_1:def 1;
        end;
        suppose
A55:      z in {x0,x};
          now
            per cases by A55,TARSKI:def 2;
            suppose
              z = x0;
              hence thesis by A11,A51,A53,FCONT_1:def 1;
            end;
            suppose
              z = x;
              hence thesis by A49,A51,A53,FCONT_1:def 1;
            end;
          end;
          hence thesis;
        end;
      end;
      hence thesis;
    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 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;
      assume that
A58:  rng s c= [.x0,x.] and
A59:  s is convergent and
A60:  lim s in [.x0,x.];
      set z = lim s;
A61:  rng s c= dom f by A46,A58,XBOOLE_1:1;
A62:  z in ].x0,x.[ \/ {x0,x} by A17,A60,XXREAL_1:128;
      now
        per cases by A62,XBOOLE_0:def 3;
        suppose
          z in ].x0,x.[;
          then f is_differentiable_in z by A5,A41,FDIFF_1:9;
          then f is_continuous_in z by FDIFF_1:24;
          hence thesis by A59,A61,FCONT_1:def 1;
        end;
        suppose
A63:      z in {x0,x};
          now
            per cases by A63,TARSKI:def 2;
            suppose
              z = x0;
              hence thesis by A10,A59,A61,FCONT_1:def 1;
            end;
            suppose
              z = x;
              hence thesis by A57,A59,A61,FCONT_1:def 1;
            end;
          end;
          hence thesis;
        end;
      end;
      hence thesis;
    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;
    f1.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 such that
A69: t in ].x0,x.[ and
A70: diff(f1,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
      let y be set;
      assume
A76:  y in [.x0,x.]\{x0};
      then y in [.x0,x.] by XBOOLE_0:def 5;
      then y in {g4: x0<=g4 & g4<=x} by RCOMP_1:def 1;
      then consider g4 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: x0<g5 & g5<x0+r} by A77,A80;
      hence y in ].x0,x0+r.[ by RCOMP_1:def 2;
    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
      assume g.x=0;
      then g.x in {0} by TARSKI:def 1;
      hence contradiction by A82,FUNCT_1:def 7;
    end;
    take 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: 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
      assume diff(g,t)=0;
      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;
    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 thesis by A69,A85,A84,RFUNCT_1:def 1;
  end;
A88: for a 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;
    assume that
A89: a is convergent and
A90: lim a = x0 and
A91: rng a c= dom (f/g) /\ right_open_halfline(x0);
    consider k such that
A92: for n st k<=n holds x0-r<a.n & a.n<x0+r by A2,A89,A90,LIMFUNC3:7;
    set a1 = a^\k;
    defpred X[Element of NAT,real number] means $2 in ].x0,a1.$1.[ & (((f/g)/*
    a)^\k).$1=((f`|].x0,x0+r.[)/(g`|].x0,x0+r.[)).$2;
A93: now
      let n;
      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:x0<g1} by XXREAL_1:230;
      then ex g1 st a.(n+k)=g1 & x0<g1;
      hence x0<a1.n by NAT_1:def 3;
      a1.n = a.(n+k) & k<=n+k by NAT_1:12,def 3;
      hence a1.n<x0+r by A92;
    end;
A94: for n ex c be Real st X[n,c]
    proof
      let n;
A95:  rng a1 c= rng a by VALUED_0:21;
      x0<a1.n & a1.n<x0+r by A93;
      then consider c such that
A96:  c in ].x0,a1.n.[ and
A97:  (f/g).(a1.n)=((f`|].x0,x0+r.[)/(g`|].x0,x0+r.[)).c by A16;
      take 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 thesis by A91,A96,A98,VALUED_0:27,XBOOLE_1:1;
    end;
    consider b such that
A99: for n holds X[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;
      assume x in rng b;
      then consider n such that
A101: x=b.n by FUNCT_2:113;
      x0<=x0+r by A2,XREAL_1:29;
      then x0 in {g3: x0<=g3 & g3<=x0+r};
      then
A102: x0 in [.x0,x0+r.] by RCOMP_1:def 1;
      x0<a1.n & a1.n<x0+r by A93;
      then a1.n in {g4: x0<=g4 & g4<=x0+r};
      then a1.n in [.x0,x0+r.] by RCOMP_1:def 1;
      then ].x0,a1.n.[ c= [.x0,a1.n.] & [.x0,a1.n.] c= [.x0,x0+r.] by A102,
XXREAL_1:25,XXREAL_2:def 12;
      then ].x0,a1.n.[ c= [.x0,x0+r.] by XBOOLE_1:1;
      then
A103: ].x0,a1.n.[ c= dom ((f`|].x0,x0+r.[)/(g`|].x0,x0+r.[)) by A8,XBOOLE_1:1;
A104: x in ].x0,a1.n.[ by A99,A101;
      then x in {g1:x0<g1 & g1<a1.n} by RCOMP_1:def 2;
      then ex g1 st g1 = x & x0<g1 & g1<a1.n;
      then x in {g2: x0<g2};
      then x in right_open_halfline(x0) by XXREAL_1:230;
      hence thesis by A104,A103,XBOOLE_0:def 4;
    end;
A105: now
      let n;
      b.n in ].x0,a1.n.[ by A99;
      then b.n in {g1:x0<g1 & g1<a1.n} by RCOMP_1:def 2;
      then ex g1 st g1=b.n & x0<g1 & g1<a1.n;
      hence d.n<=b.n & b.n<=a1.n by FUNCOP_1:7;
    end;
A106: lim d=d.0 by SEQ_4:26
      .=x0 by FUNCOP_1:7;
    lim a1=x0 by A89,A90,SEQ_4:20;
    then
A107: b is convergent & lim b=x0 by A89,A106,A105,SEQ_2:19,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
      take m = 0;
      let n such that
      m <=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;
    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 thesis by A111,SEQ_4:21,22;
  end;
A112: for r1 st x0<r1 ex t 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;
  take r;
  thus r>0 by A2;
  thus thesis by A112,A88,Th2;
end;

theorem
  x0 in dom f /\ dom g & (ex r 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 st r>0 &
  lim_left(f/g,x0) = lim_left(((f`|(].x0-r,x0.[))/(g`|(].x0-r,x0.[))),x0)
proof
  assume
A1: x0 in dom f /\ dom g;
  given r 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;
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 st x0-r<x & x<x0 ex c st c in ].x,x0.[ & (f/g).x=((f`|].x0-r,x0.[
  )/(g`|].x0-r,x0.[)).c
  proof
    let x;
    assume that
A17: x0-r<x and
A18: x<x0;
    x in {g1: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;
      assume y in ].x,x0.[;
      then y in {g2:x<g2 & g2<x0} by RCOMP_1:def 2;
      then consider g2 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:x0-r<g3 & g3<x0} by A22,A24;
      hence thesis by RCOMP_1:def 2;
    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;
      assume
A34:  y in [.x,x0.];
      then reconsider 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 thesis by A35,XXREAL_1:1;
    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 f1 by A32,XBOOLE_1:19;
A38: x in [.x,x0.] by A18,XXREAL_1:1;
    then x in dom f1 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 f1 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: f1.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 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 such that
A50:  rng s c= [.x,x0.] and
A51:  s is convergent and
A52:  lim s in [.x,x0.];
      set z = lim s;
A53:  rng s c= dom g by A48,A50,XBOOLE_1:1;
A54:  z in ].x,x0.[ \/ {x,x0} by A18,A52,XXREAL_1:128;
      now
        per cases by A54,XBOOLE_0:def 3;
        suppose
          z in ].x,x0.[;
          then g is_differentiable_in z by A6,A21,FDIFF_1:9;
          then g is_continuous_in z by FDIFF_1:24;
          hence thesis by A51,A53,FCONT_1:def 1;
        end;
        suppose
A55:      z in {x,x0};
          now
            per cases by A55,TARSKI:def 2;
            suppose
              z = x0;
              hence thesis by A11,A51,A53,FCONT_1:def 1;
            end;
            suppose
              z = x;
              hence thesis by A49,A51,A53,FCONT_1:def 1;
            end;
          end;
          hence thesis;
        end;
      end;
      hence thesis;
    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 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;
      assume that
A59:  rng s c= [.x,x0.] and
A60:  s is convergent and
A61:  lim s in [.x,x0.];
      set z = lim s;
A62:  rng s c= dom f by A25,A59,XBOOLE_1:1;
A63:  z in ].x,x0.[ \/ {x,x0} by A18,A61,XXREAL_1:128;
      now
        per cases by A63,XBOOLE_0:def 3;
        suppose
          z in ].x,x0.[;
          then f is_differentiable_in z by A5,A21,FDIFF_1:9;
          then f is_continuous_in z by FDIFF_1:24;
          hence thesis by A60,A62,FCONT_1:def 1;
        end;
        suppose
A64:      z in {x,x0};
          now
            per cases by A64,TARSKI:def 2;
            suppose
              z = x0;
              hence thesis by A10,A60,A62,FCONT_1:def 1;
            end;
            suppose
              z = x;
              hence thesis by A58,A60,A62,FCONT_1:def 1;
            end;
          end;
          hence thesis;
        end;
      end;
      hence thesis;
    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;
    f1.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 such that
A67: t in ].x,x0.[ and
A68: diff(f1,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
      let y be set;
      assume
A74:  y in [.x,x0.]\{x0};
      then y in [.x,x0.] by XBOOLE_0:def 5;
      then y in {g4: x<=g4 & g4<=x0} by RCOMP_1:def 1;
      then consider g4 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: x0-r<g5 & g5<x0} by A75,A78;
      hence y in ].x0-r,x0.[ by RCOMP_1:def 2;
    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
      assume g.x=0;
      then g.x in {0} by TARSKI:def 1;
      hence contradiction by A80,FUNCT_1:def 7;
    end;
    take 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: 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
      assume diff(g,t)=0;
      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;
    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 thesis by A67,A83,A82,RFUNCT_1:def 1;
  end;
A86: for a 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;
    assume that
A87: a is convergent and
A88: lim a = x0 and
A89: rng a c= dom (f/g) /\ left_open_halfline(x0);
    consider k such that
A90: for n st k<=n holds x0-r<a.n & a.n<x0+r by A2,A87,A88,LIMFUNC3:7;
    set a1 = a^\k;
    defpred X[Element of NAT,real number] means $2 in ].a1.$1,x0.[ & (((f/g)/*
    a)^\k).$1=((f`|].x0-r,x0.[)/(g`|].x0-r,x0.[)).$2;
A91: now
      let 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:g1<x0} by XXREAL_1:229;
      then ex g1 st a.(n+k)=g1 & g1<x0;
      hence a1.n<x0 by NAT_1:def 3;
      a1.n = a.(n+k) & k<=n+k by NAT_1:12,def 3;
      hence x0-r<a1.n by A90;
    end;
A92: for n ex c be Real st X[n,c]
    proof
      let n;
A93:  rng a1 c= rng a by VALUED_0:21;
      x0-r<a1.n & a1.n<x0 by A91;
      then consider c such that
A94:  c in ].a1.n,x0.[ and
A95:  (f/g).(a1.n)= ((f`|].x0-r,x0.[)/(g`|].x0-r,x0.[)).c by A16;
      take 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 thesis by A89,A94,A96,VALUED_0:27,XBOOLE_1:1;
    end;
    consider b such that
A97: for n holds X[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;
      assume x in rng b;
      then consider n such that
A99:  x=b.n by FUNCT_2:113;
      x0-r<=x0 by A2,XREAL_1:44;
      then x0 in {g3: x0-r<=g3 & g3<=x0};
      then
A100: x0 in [.x0-r,x0.] by RCOMP_1:def 1;
      x0-r<a1.n & a1.n<x0 by A91;
      then a1.n in {g4: x0-r<=g4 & g4<=x0};
      then a1.n in [.x0-r,x0.] by RCOMP_1:def 1;
      then ].a1.n,x0.[ c= [.a1.n,x0.] & [.a1.n,x0.] c= [.x0-r,x0.] by A100,
XXREAL_1:25,XXREAL_2:def 12;
      then ].a1.n,x0.[ c= [.x0-r,x0.] by XBOOLE_1:1;
      then
A101: ].a1.n,x0.[ c= dom ((f`|].x0-r,x0.[)/(g`|].x0-r,x0.[)) by A8,XBOOLE_1:1;
A102: x in ].a1.n,x0.[ by A97,A99;
      then x in {g1:a1.n<g1 & g1<x0} by RCOMP_1:def 2;
      then ex g1 st g1 = x & a1.n<g1 & g1<x0;
      then x in {g2: g2<x0};
      then x in left_open_halfline(x0) by XXREAL_1:229;
      hence thesis by A102,A101,XBOOLE_0:def 4;
    end;
A103: now
      let n;
      b.n in ].a1.n,x0.[ by A97;
      then b.n in {g1:a1.n<g1 & g1<x0} by RCOMP_1:def 2;
      then ex g1 st g1=b.n & a1.n<g1 & g1<x0;
      hence a1.n<=b.n & b.n<=d.n by FUNCOP_1:7;
    end;
A104: lim d=d.0 by SEQ_4:26
      .=x0 by FUNCOP_1:7;
    lim a1=x0 by A87,A88,SEQ_4:20;
    then
A105: b is convergent & lim b=x0 by A87,A104,A103,SEQ_2:19,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
      take m = 0;
      let n such that
      m <=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;
    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 thesis by A109,SEQ_4:21,22;
  end;
A110: for r1 st r1<x0 ex t 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;
  take r;
  thus r>0 by A2;
  thus thesis by A110,A86,Th3;
end;

theorem
  (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)
proof
  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;
  consider r be 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 st x0<x & x<x0+r ex c 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: 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 such that
A17: x0<x and
A18: x<x0+r;
    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: 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 f1 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 f1 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 f1 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: f1.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;
    f1.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 such that
A44: t in ].x0,x.[ and
A45: diff(f1,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;
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
      assume g.x=0;
      then g.x in {0} by TARSKI:def 1;
      hence contradiction by A51,FUNCT_1:def 7;
    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
      assume diff(g,t)=0;
      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;
    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 thesis by A44,A53,A49,RFUNCT_1:def 1;
  end;
A56: for a 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;
    assume that
A57: a is convergent and
A58: lim a = x0 and
A59: rng a c= dom (f/g) /\ right_open_halfline(x0);
    consider k such that
A60: for n st k<=n holds x0-r<a.n & a.n<x0+r by A9,A11,A57,A58,LIMFUNC3:7;
    set a1 = a^\k;
    defpred X[Element of NAT,real number] means $2 in ].x0,a1.$1.[ & (((f/g)/*
    a)^\k).$1=((f`|N)/(g`|N)).$2;
A61: now
      let n;
      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:x0<g1} by XXREAL_1:230;
      then ex g1 st a.(n+k)=g1 & x0<g1;
      hence x0<a1.n by NAT_1:def 3;
      a1.n = a.(n+k) & k<=n+k by NAT_1:12,def 3;
      hence a1.n<x0+r by A60;
    end;
A62: for n ex c be Real st X[n,c]
    proof
      let n;
A63:  rng a1 c= rng a by VALUED_0:21;
      x0<a1.n & a1.n<x0+r by A61;
      then consider c such that
A64:  c in ].x0,a1.n.[ and
A65:  (f/g).(a1.n)=((f`|N)/(g`|N)).c by A12;
      take 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 thesis by A59,A64,A66,VALUED_0:27,XBOOLE_1:1;
    end;
    consider b such that
A67: for n holds X[n,b.n] from FUNCT_2:sch 3(A62);
A68: now
      let n;
      b.n in ].x0,a1.n.[ by A67;
      then b.n in {g1:x0<g1 & g1<a1.n} by RCOMP_1:def 2;
      then ex g1 st g1=b.n & x0<g1 & g1<a1.n;
      hence d.n<=b.n & b.n<=a1.n by FUNCOP_1:7;
    end;
A69: lim d=d.0 by SEQ_4:26
      .=x0 by FUNCOP_1:7;
    lim a1=x0 by A57,A58,SEQ_4:20;
    then
A70: b is convergent & lim b=x0 by A57,A69,A68,SEQ_2:19,20;
A71: x0-r<x0 by A9,XREAL_1:44;
    x0<x0+r by A9,XREAL_1:29;
    then x0 in {g2: 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;
      assume x in rng b;
      then consider n such that
A74:  x=b.n by FUNCT_2:113;
      x0<a1.n by A61;
      then
A75:  x0-r<a1.n by A71,XXREAL_0:2;
      a1.n<x0+r by A61;
      then a1.n in {g3: x0-r<g3 & g3<x0+r} by A75;
      then a1.n in ].x0-r,x0+r.[ by RCOMP_1:def 2;
      then ].x0,a1.n.[ c= [.x0,a1.n.] & [.x0,a1.n.] c= ].x0-r,x0+r.[ by A72,
XXREAL_1:25,XXREAL_2:def 12;
      then ].x0,a1.n.[ c= ].x0-r,x0+r.[ by XBOOLE_1:1;
      then
A76:  ].x0,a1.n.[ c= dom ((f`|N)/(g`|N)) by A6,A10,XBOOLE_1:1;
A77:  x in ].x0,a1.n.[ by A67,A74;
      then x in {g1:x0<g1 & g1<a1.n} by RCOMP_1:def 2;
      then ex g1 st g1 = x & x0<g1 & g1<a1.n;
      then not x in {x0} by TARSKI:def 1;
      hence thesis by A77,A76,XBOOLE_0:def 5;
    end;
A78: dom ((f`|N)/(g`|N)) \{x0} c= dom ((f`|N)/(g`|N)) by XBOOLE_1:36;
A79: now
      take m = 0;
      let n such that
      m <=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;
    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 thesis by A81,SEQ_4:21,22;
  end;
A82: for r1,r2 st r1<x0 & x0<r2 ex g1,g2 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 st x0<r1 ex t 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 st x0-r<x & x<x0 ex c 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: 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 such that
A89: x0-r<x and
A90: x<x0;
    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: 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 f1 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 f1 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 f1 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: f1.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;
    f1.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 such that
A116: t in ].x,x0.[ and
A117: diff(f1,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;
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
      assume g.x=0;
      then g.x in {0} by TARSKI:def 1;
      hence contradiction by A123,FUNCT_1:def 7;
    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
      assume diff(g,t)=0;
      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;
    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 thesis by A116,A125,A121,RFUNCT_1:def 1;
  end;
A128: for a 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;
    assume that
A129: a is convergent and
A130: lim a = x0 and
A131: rng a c= dom (f/g) /\ left_open_halfline(x0);
    consider k such that
A132: for n st k<=n holds x0-r<a.n & a.n<x0+r by A9,A11,A129,A130,LIMFUNC3:7;
    set a1 = a^\k;
    defpred X[Element of NAT,real number] means $2 in ].a1.$1,x0.[ & (((f/g)/*
    a)^\k).$1=((f`|N)/(g`|N)).$2;
A133: now
      let 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:g1<x0} by XXREAL_1:229;
      then ex g1 st a.(n+k)=g1 & g1<x0;
      hence a1.n<x0 by NAT_1:def 3;
      a1.n = a.(n+k) & k<=n+k by NAT_1:12,def 3;
      hence x0-r<a1.n by A132;
    end;
A134: for n ex c be Real st X[n,c]
    proof
      let n;
A135: rng a1 c= rng a by VALUED_0:21;
      x0-r<a1.n & a1.n<x0 by A133;
      then consider c such that
A136: c in ].a1.n,x0.[ and
A137: (f/g).(a1.n)=((f`|N)/(g`|N)).c by A84;
      take 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 thesis by A131,A136,A138,VALUED_0:27,XBOOLE_1:1;
    end;
    consider b such that
A139: for n holds X[n,b.n] from FUNCT_2:sch 3(A134);
A140: now
      let n;
      b.n in ].a1.n,x0.[ by A139;
      then b.n in {g1:a1.n<g1 & g1<x0} by RCOMP_1:def 2;
      then ex g1 st g1=b.n & a1.n<g1 & g1<x0;
      hence a1.n<=b.n & b.n<= d.n by FUNCOP_1:7;
    end;
A141: lim d=d.0 by SEQ_4:26
      .=x0 by FUNCOP_1:7;
    lim a1=x0 by A129,A130,SEQ_4:20;
    then
A142: b is convergent & lim b=x0 by A129,A141,A140,SEQ_2:19,20;
A143: x0<x0+r by A9,XREAL_1:29;
    x0-r<x0 by A9,XREAL_1:44;
    then x0 in {g2: 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;
      assume x in rng b;
      then consider n such that
A146: x=b.n by FUNCT_2:113;
      a1.n<x0 by A133;
      then
A147: a1.n<x0+r by A143,XXREAL_0:2;
      x0-r<a1.n by A133;
      then a1.n in {g3: x0-r<g3 & g3<x0+r} by A147;
      then a1.n in ].x0-r,x0+r.[ by RCOMP_1:def 2;
      then ].a1.n,x0.[ c= [.a1.n,x0.] & [.a1.n,x0.] c= ].x0-r,x0+r.[ by A144,
XXREAL_1:25,XXREAL_2:def 12;
      then ].a1.n,x0.[ c= ].x0-r,x0+r.[ by XBOOLE_1:1;
      then
A148: ].a1.n,x0.[ c= dom ((f`|N)/(g`|N)) by A6,A10,XBOOLE_1:1;
A149: x in ].a1.n,x0.[ by A139,A146;
      then x in {g1:a1.n<g1 & g1<x0} by RCOMP_1:def 2;
      then ex g1 st g1 = x & a1.n<g1 & g1<x0;
      then not x in {x0} by TARSKI:def 1;
      hence thesis by A149,A148,XBOOLE_0:def 5;
    end;
A150: dom ((f`|N)/(g`|N)) \{x0} c= dom ((f`|N)/(g`|N)) by XBOOLE_1:36;
A151: now
      take m = 0;
      let n such that
      m <=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;
    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 thesis by A153,SEQ_4:21,22;
  end;
  for r1 st r1<x0 ex t 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;
  take N;
  thus thesis by A83,A154,LIMFUNC3:30;
end;

::$N l'Hospital Theorem
theorem
  (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)
proof
  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;
  consider r be 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 st x0-r<x & x<x0 ex c 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: 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 such that
A17: x0-r<x and
A18: x<x0;
    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: 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 f1 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 f1 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 f1 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: f1.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;
    f1.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 such that
A44: t in ].x,x0.[ and
A45: diff(f1,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;
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
      assume g.x=0;
      then g.x in {0} by TARSKI:def 1;
      hence contradiction by A51,FUNCT_1:def 7;
    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
      assume diff(g,t)=0;
      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;
    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 thesis by A44,A53,A49,RFUNCT_1:def 1;
  end;
A56: for a 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;
    assume that
A57: a is convergent and
A58: lim a = x0 and
A59: rng a c= dom (f/g) /\ left_open_halfline(x0);
    consider k such that
A60: for n st k<=n holds x0-r<a.n & a.n<x0+r by A9,A11,A57,A58,LIMFUNC3:7;
    set a1 = a^\k;
    defpred X[Element of NAT,real number] means $2 in ].a1.$1,x0.[ & (((f/g)/*
    a)^\k).$1=((f`|N)/(g`|N)).$2;
A61: now
      let 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:g1<x0} by XXREAL_1:229;
      then ex g1 st a.(n+k)=g1 & g1<x0;
      hence a1.n<x0 by NAT_1:def 3;
      a1.n = a.(n+k) & k<=n+k by NAT_1:12,def 3;
      hence x0-r<a1.n by A60;
    end;
A62: for n ex c be Real st X[n,c]
    proof
      let n;
A63:  rng a1 c= rng a by VALUED_0:21;
      x0-r<a1.n & a1.n<x0 by A61;
      then consider c such that
A64:  c in ].a1.n,x0.[ and
A65:  (f/g).(a1.n)=((f`|N)/(g`|N)).c by A12;
      take 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 thesis by A59,A64,A66,VALUED_0:27,XBOOLE_1:1;
    end;
    consider b such that
A67: for n holds X[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: 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;
      assume x in rng b;
      then consider n such that
A71:  x=b.n by FUNCT_2:113;
      a1.n<x0 by A61;
      then
A72:  a1.n<x0+r by A68,XXREAL_0:2;
      x0-r<a1.n by A61;
      then a1.n in {g3: x0-r<g3 & g3<x0+r} by A72;
      then a1.n in ].x0-r,x0+r.[ by RCOMP_1:def 2;
      then ].a1.n,x0.[ c= [.a1.n,x0.] & [.a1.n,x0.] c= ].x0-r,x0+r.[ by A69,
XXREAL_1:25,XXREAL_2:def 12;
      then ].a1.n,x0.[ c= ].x0-r,x0+r.[ by XBOOLE_1:1;
      then
A73:  ].a1.n,x0.[ c= dom ((f`|N)/(g`|N)) by A6,A10,XBOOLE_1:1;
A74:  x in ].a1.n,x0.[ by A67,A71;
      then x in {g1:a1.n<g1 & g1<x0} by RCOMP_1:def 2;
      then ex g1 st g1=x & a1.n<g1 & g1<x0;
      then x in {g2:g2<x0};
      then x in left_open_halfline(x0) by XXREAL_1:229;
      hence thesis by A74,A73,XBOOLE_0:def 4;
    end;
A75: now
      let n;
      b.n in ].a1.n,x0.[ by A67;
      then b.n in {g1:a1.n<g1 & g1<x0} by RCOMP_1:def 2;
      then ex g1 st g1=b.n & a1.n<g1 & g1<x0;
      hence a1.n<=b.n & b.n<= d.n by FUNCOP_1:7;
    end;
A76: lim d=d.0 by SEQ_4:26
      .=x0 by FUNCOP_1:7;
    lim a1=x0 by A57,A58,SEQ_4:20;
    then
A77: b is convergent & lim b=x0 by A57,A76,A75,SEQ_2:19,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
      take m = 0;
      let n such that
      m <=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;
    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 thesis by A82,SEQ_4:21,22;
  end;
A83: for r1,r2 st r1<x0 & x0<r2 ex g1,g2 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 st r1<x0 ex t 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 st x0<x & x<x0+r ex c 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: 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 such that
A90: x0<x and
A91: x<x0+r;
    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: 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 f1 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 f1 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 f1 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: f1.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;
    f1.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 such that
A117: t in ].x0,x.[ and
A118: diff(f1,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;
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
      assume g.x=0;
      then g.x in {0} by TARSKI:def 1;
      hence contradiction by A124,FUNCT_1:def 7;
    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
      assume diff(g,t)=0;
      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;
    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 thesis by A117,A126,A122,RFUNCT_1:def 1;
  end;
A129: for a 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;
    assume that
A130: a is convergent and
A131: lim a = x0 and
A132: rng a c= dom (f/g) /\ right_open_halfline(x0);
    consider k such that
A133: for n st k<=n holds x0-r<a.n & a.n<x0+r by A9,A11,A130,A131,LIMFUNC3:7;
    set a1 = a^\k;
    defpred X[Element of NAT,real number] means $2 in ].x0,a1.$1.[ & (((f/g)/*
    a)^\k).$1=((f`|N)/(g`|N)).$2;
A134: now
      let n;
      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:x0<g1} by XXREAL_1:230;
      then ex g1 st a.(n+k)=g1 & x0<g1;
      hence x0<a1.n by NAT_1:def 3;
      a1.n = a.(n+k) & k<=n+k by NAT_1:12,def 3;
      hence a1.n<x0+r by A133;
    end;
A135: for n ex c be Real st X[n,c]
    proof
      let n;
A136: rng a1 c= rng a by VALUED_0:21;
      x0<a1.n & a1.n<x0+r by A134;
      then consider c such that
A137: c in ].x0,a1.n.[ and
A138: (f/g).(a1.n)=((f`|N)/(g`|N)).c by A85;
      take 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 thesis by A132,A137,A139,VALUED_0:27,XBOOLE_1:1;
    end;
    consider b such that
A140: for n holds X[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: 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;
      assume x in rng b;
      then consider n such that
A144: x=b.n by FUNCT_2:113;
      x0<a1.n by A134;
      then
A145: x0-r<a1.n by A141,XXREAL_0:2;
      a1.n<x0+r by A134;
      then a1.n in {g3: x0-r<g3 & g3<x0+r} by A145;
      then a1.n in ].x0-r,x0+r.[ by RCOMP_1:def 2;
      then ].x0,a1.n.[ c= [.x0,a1.n.] & [.x0,a1.n.] c= ].x0-r,x0+r.[ by A142,
XXREAL_1:25,XXREAL_2:def 12;
      then ].x0,a1.n.[ c= ].x0-r,x0+r.[ by XBOOLE_1:1;
      then
A146: ].x0,a1.n.[ c= dom ((f`|N)/(g`|N)) by A6,A10,XBOOLE_1:1;
A147: x in ].x0,a1.n.[ by A140,A144;
      then x in {g1:x0<g1 & g1<a1.n} by RCOMP_1:def 2;
      then ex g1 st g1=x & x0<g1 & g1<a1.n;
      then x in {g2:x0<g2};
      then x in right_open_halfline(x0) by XXREAL_1:230;
      hence thesis by A147,A146,XBOOLE_0:def 4;
    end;
A148: now
      let n;
      b.n in ].x0,a1.n.[ by A140;
      then b.n in {g1:x0<g1 & g1<a1.n} by RCOMP_1:def 2;
      then ex g1 st g1=b.n & x0<g1 & g1<a1.n;
      hence d.n<=b.n & b.n<=a1.n by FUNCOP_1:7;
    end;
A149: lim d=d.0 by SEQ_4:26
      .=x0 by FUNCOP_1:7;
    lim a1=x0 by A130,A131,SEQ_4:20;
    then
A150: b is convergent & lim b=x0 by A130,A149,A148,SEQ_2:19,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
      take m = 0;
      let n such that
      m <=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;
    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 thesis by A155,SEQ_4:21,22;
  end;
  for r1 st x0<r1 ex t 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 thesis by A84,LIMFUNC3:30;
end;