l_hospit.miz



    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 :: L_HOSPIT:1

    f is_continuous_in x0 & (for r1, r2 st r1 < x0 & x0 < r2 holds 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 holds 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;

        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 :: L_HOSPIT:2

    

     Th2: f is_right_convergent_in x0 & ( lim_right (f,x0)) = t iff (for r st x0 < r holds 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 holds 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, LIMFUNC2:def 8;

      reconsider t as Real;

      (for r st x0 < r holds 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 holds 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;

      hence thesis;

    end;

    theorem :: L_HOSPIT:3

    

     Th3: f is_left_convergent_in x0 & ( lim_left (f,x0)) = t iff (for r st r < x0 holds 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 holds 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, LIMFUNC2:def 7;

      reconsider t as Real;

      (for r st r < x0 holds 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 holds 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;

      hence thesis;

    end;

    theorem :: L_HOSPIT:4

    

     Th4: (ex N be Neighbourhood of x0 st (N \ {x0}) c= ( dom f)) implies for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom f) & g2 < r2 & x0 < g2 & g2 in ( dom f)

    proof

      given N be Neighbourhood of x0 such that

       A1: (N \ {x0}) c= ( dom f);

      consider r be Real such that

       A2: 0 < r and

       A3: N = ].(x0 - r), (x0 + r).[ by RCOMP_1:def 6;

      (N \ {x0}) = ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[) by A2, A3, LIMFUNC3: 4;

      hence thesis by A1, A2, LIMFUNC3: 5;

    end;

    theorem :: L_HOSPIT:5

    (ex N be 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 be 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 such that

       A9: 0 < r and

       A10: N = ].(x0 - r), (x0 + r).[ by RCOMP_1:def 6;

      

       A11: for x st (x0 - r) < x & x < x0 holds ex c st c in ].x, x0.[ & ((f / g) . x) = (((f `| N) / (g `| N)) . c)

      proof

        

         A12: (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 A12;

        then

         A13: x0 in ].(x0 - r), (x0 + r).[ by RCOMP_1:def 2;

        

         A14: (( dom (f `| N)) /\ (( dom (g `| N)) \ ((g `| N) " { 0 }))) c= (( dom (g `| N)) \ ((g `| N) " { 0 })) by XBOOLE_1: 17;

        

         A15: (( dom f) /\ (( dom g) \ (g " { 0 }))) c= (( dom g) \ (g " { 0 })) by XBOOLE_1: 17;

        let x such that

         A16: (x0 - r) < x and

         A17: x < x0;

        set f1 = (((f . x) (#) g) - ((g . x) (#) f));

        

         A18: ( dom ((f . x) (#) g)) = ( dom g) & ( dom ((g . x) (#) f)) = ( dom f) by VALUED_1:def 5;

        then

         A19: ( dom (((f . x) (#) g) - ((g . x) (#) f))) = (( dom f) /\ ( dom g)) by VALUED_1: 12;

        x < (x0 + r) by A17, A12, XXREAL_0: 2;

        then x in { g1 : (x0 - r) < g1 & g1 < (x0 + r) } by A16;

        then x in ].(x0 - r), (x0 + r).[ by RCOMP_1:def 2;

        then

         A20: [.x, x0.] c= N by A10, A13, XXREAL_2:def 12;

        then

         A21: [.x, x0.] c= ( dom f) & [.x, x0.] c= ( dom g) by A1, A2;

        then

         A22: [.x, x0.] c= ( dom f1) by A19, XBOOLE_1: 19;

        (g | N) is continuous by A4, FDIFF_1: 25;

        then (g | [.x, x0.]) is continuous by A20, FCONT_1: 16;

        then

         A23: (((f . x) (#) g) | [.x, x0.]) is continuous by A2, A20, FCONT_1: 20, XBOOLE_1: 1;

        (f | N) is continuous by A3, FDIFF_1: 25;

        then (f | [.x, x0.]) is continuous by A20, FCONT_1: 16;

        then

         A24: (((g . x) (#) f) | [.x, x0.]) is continuous by A1, A20, FCONT_1: 20, XBOOLE_1: 1;

         [.x, x0.] c= ( dom (((f . x) (#) g) - ((g . x) (#) f))) by A21, A19, XBOOLE_1: 19;

        then

         A25: ((((f . x) (#) g) - ((g . x) (#) f)) | [.x, x0.]) is continuous by A24, A18, A19, A23, FCONT_1: 18;

        

         A26: ].x, x0.[ c= [.x, x0.] by XXREAL_1: 25;

        then

         A27: ].x, x0.[ c= N by A20;

        

         A28: x in [.x, x0.] by A17, XXREAL_1: 1;

        then x in ( dom f1) by A22;

        then

         A29: x in (( dom ((f . x) (#) g)) /\ ( dom ((g . x) (#) f))) by VALUED_1: 12;

        then

         A30: x in ( dom ((f . x) (#) g)) by XBOOLE_0:def 4;

        

         A31: x0 in [.x, x0.] by A17, XXREAL_1: 1;

        then x0 in ( dom f1) by A22;

        then

         A32: x0 in (( dom ((f . x) (#) g)) /\ ( dom ((g . x) (#) f))) by VALUED_1: 12;

        then

         A33: x0 in ( dom ((f . x) (#) g)) by XBOOLE_0:def 4;

        

         A34: x in ( dom ((g . x) (#) f)) by A29, XBOOLE_0:def 4;

        

         A35: (f1 . x) = ((((f . x) (#) g) . x) - (((g . x) (#) f) . x)) by A22, A28, VALUED_1: 13

        .= (((f . x) * (g . x)) - (((g . x) (#) f) . x)) by A30, VALUED_1:def 5

        .= (((g . x) * (f . x)) - ((g . x) * (f . x))) by A34, VALUED_1:def 5

        .= 0 ;

        

         A36: x0 in ( dom ((g . x) (#) f)) by A32, XBOOLE_0:def 4;

         not x in {x0} by A17, TARSKI:def 1;

        then

         A37: x in ( [.x, x0.] \ {x0}) by A28, XBOOLE_0:def 5;

        N c= ( dom ((f . x) (#) g)) by A2, VALUED_1:def 5;

        then

         A38: ].x, x0.[ c= ( dom ((f . x) (#) g)) by A27;

        N c= ( dom ((g . x) (#) f)) by A1, VALUED_1:def 5;

        then

         A39: ].x, x0.[ c= ( dom ((g . x) (#) f)) by A27;

        then ].x, x0.[ c= (( dom ((f . x) (#) g)) /\ ( dom ((g . x) (#) f))) by A38, XBOOLE_1: 19;

        then

         A40: ].x, x0.[ c= ( dom (((f . x) (#) g) - ((g . x) (#) f))) by VALUED_1: 12;

        f is_differentiable_on ].x, x0.[ by A3, A20, A26, FDIFF_1: 26, XBOOLE_1: 1;

        then

         A41: ((g . x) (#) f) is_differentiable_on ].x, x0.[ by A39, FDIFF_1: 20;

        g is_differentiable_on ].x, x0.[ by A4, A20, A26, FDIFF_1: 26, XBOOLE_1: 1;

        then

         A42: ((f . x) (#) g) is_differentiable_on ].x, x0.[ by A38, FDIFF_1: 20;

        (f1 . x0) = ((((f . x) (#) g) . x0) - (((g . x) (#) f) . x0)) by A22, A31, VALUED_1: 13

        .= (((f . x) * (g . x0)) - (((g . x) (#) f) . x0)) by A33, VALUED_1:def 5

        .= ( 0 - ((g . x) * 0 )) by A7, A36, VALUED_1:def 5

        .= 0 ;

        then

        consider t such that

         A43: t in ].x, x0.[ and

         A44: ( diff (f1,t)) = 0 by A17, A25, A41, A40, A42, A22, A35, FDIFF_1: 19, ROLLE: 1;

        

         A45: ((g . x) (#) f) is_differentiable_in t by A41, A43, FDIFF_1: 9;

        

         A46: f is_differentiable_in t by A3, A27, A43, FDIFF_1: 9;

        ((f . x) (#) g) is_differentiable_in t by A42, A43, FDIFF_1: 9;

        then 0 = (( diff (((f . x) (#) g),t)) - ( diff (((g . x) (#) f),t))) by A44, A45, FDIFF_1: 14;

        then

         A47: 0 = (( diff (((f . x) (#) g),t)) - ((g . x) * ( diff (f,t)))) by A46, FDIFF_1: 15;

        take t;

        

         A48: t in [.x, x0.] by A26, A43;

        ( [.x, x0.] \ {x0}) c= (N \ {x0}) by A20, XBOOLE_1: 33;

        then

         A49: ( [.x, x0.] \ {x0}) c= ( dom (f / g)) by A5;

        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 A15;

        then

         A50: x in ( dom g) & not x in (g " { 0 }) by A37, XBOOLE_0:def 5;

         A51:

        now

          assume (g . x) = 0 ;

          then (g . x) in { 0 } by TARSKI:def 1;

          hence contradiction by A50, FUNCT_1:def 7;

        end;

        

         A52: [.x, x0.] c= ( dom ((f `| N) / (g `| N))) by A6, A20;

        then [.x, x0.] c= (( dom (f `| N)) /\ (( dom (g `| N)) \ ((g `| N) " { 0 }))) by RFUNCT_1:def 1;

        then [.x, x0.] c= (( dom (g `| N)) \ ((g `| N) " { 0 })) by A14;

        then

         A53: t in ( dom (g `| N)) & not t in ((g `| N) " { 0 }) by A48, XBOOLE_0:def 5;

         A54:

        now

          assume ( diff (g,t)) = 0 ;

          then ((g `| N) . t) = 0 by A4, A20, A48, FDIFF_1:def 7;

          then ((g `| N) . t) in { 0 } by TARSKI:def 1;

          hence contradiction by A53, FUNCT_1:def 7;

        end;

        g is_differentiable_in t by A4, A27, A43, FDIFF_1: 9;

        then 0 = (((f . x) * ( diff (g,t))) - ((g . x) * ( diff (f,t)))) by A47, FDIFF_1: 15;

        then ((f . x) / (g . x)) = (( diff (f,t)) / ( diff (g,t))) by A51, A54, XCMPLX_1: 94;

        then ((f . x) * ((g . x) " )) = (( diff (f,t)) / ( diff (g,t))) by XCMPLX_0:def 9;

        then ((f . x) * ((g . x) " )) = (( diff (f,t)) * (( diff (g,t)) " )) by XCMPLX_0:def 9;

        then ((f / g) . x) = (( diff (f,t)) * (( diff (g,t)) " )) by A49, A37, RFUNCT_1:def 1;

        then ((f / g) . x) = (((f `| N) . t) * (( diff (g,t)) " )) by A3, A20, A48, FDIFF_1:def 7;

        then ((f / g) . x) = (((f `| N) . t) * (((g `| N) . t) " )) by A4, A20, A48, FDIFF_1:def 7;

        hence thesis by A43, A52, A48, RFUNCT_1:def 1;

      end;

      

       A55: 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 xx0 = x0 as Element of REAL by XREAL_0:def 1;

        set d = ( seq_const x0);

        let a;

        assume that

         A56: a is convergent and

         A57: ( lim a) = x0 and

         A58: ( rng a) c= (( dom (f / g)) /\ ( left_open_halfline x0));

        consider k such that

         A59: for n st k <= n holds (x0 - r) < (a . n) & (a . n) < (x0 + r) by A9, A56, A57, LIMFUNC3: 7;

        set a1 = (a ^\ k);

        defpred X[ Element of NAT , Real] means $2 in ].(a1 . $1), x0.[ & ((((f / g) /* a) ^\ k) . $1) = (((f `| N) / (g `| N)) . $2);

         A60:

        now

          let n;

          (a . (n + k)) in ( rng a) by VALUED_0: 28;

          then (a . (n + k)) in ( left_open_halfline x0) by A58, XBOOLE_0:def 4;

          then (a . (n + k)) in { g1 : 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, NAT_1:def 3;

          hence (x0 - r) < (a1 . n) by A59;

        end;

        

         A61: for n holds ex c be Element of REAL st X[n, c]

        proof

          let n;

          

           A62: ( rng a1) c= ( rng a) by VALUED_0: 21;

          (x0 - r) < (a1 . n) & (a1 . n) < x0 by A60;

          then

          consider c such that

           A63: c in ].(a1 . n), x0.[ and

           A64: ((f / g) . (a1 . n)) = (((f `| N) / (g `| N)) . c) by A11;

          take c;

          

           A65: (( dom (f / g)) /\ ( left_open_halfline x0)) c= ( dom (f / g)) by XBOOLE_1: 17;

          then ( rng a) c= ( dom (f / g)) by A58;

          then (((f / g) /* (a ^\ k)) . n) = (((f `| N) / (g `| N)) . c) by A64, A62, FUNCT_2: 108, XBOOLE_1: 1;

          hence thesis by A58, A63, A65, VALUED_0: 27, XBOOLE_1: 1;

        end;

        consider b such that

         A66: for n holds X[n, (b . n)] from FUNCT_2:sch 3( A61);

         A67:

        now

          let n be Nat;

          n in NAT by ORDINAL1:def 12;

          then (b . n) in ].(a1 . n), x0.[ by A66;

          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 SEQ_1: 57;

        end;

        

         A68: ( lim d) = (d . 0 ) by SEQ_4: 26

        .= x0 by SEQ_1: 57;

        

         A69: 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 A69;

        then

         A70: x0 in ].(x0 - r), (x0 + r).[ by RCOMP_1:def 2;

        

         A71: ( rng b) c= (( dom ((f `| N) / (g `| N))) \ {x0})

        proof

          let x be object;

          assume x in ( rng b);

          then

          consider n such that

           A72: x = (b . n) by FUNCT_2: 113;

          (a1 . n) < x0 by A60;

          then

           A73: (a1 . n) < (x0 + r) by A69, XXREAL_0: 2;

          (x0 - r) < (a1 . n) by A60;

          then (a1 . n) in { g3 : (x0 - r) < g3 & g3 < (x0 + r) } by A73;

          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 A70, XXREAL_1: 25, XXREAL_2:def 12;

          then ].(a1 . n), x0.[ c= ].(x0 - r), (x0 + r).[;

          then

           A74: ].(a1 . n), x0.[ c= ( dom ((f `| N) / (g `| N))) by A6, A10;

          

           A75: x in ].(a1 . n), x0.[ by A66, A72;

          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 A75, A74, XBOOLE_0:def 5;

        end;

        

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

         A77:

        now

          let n be Nat;

          

           A78: n in NAT by ORDINAL1:def 12;

          ((((f / g) /* a) ^\ k) . n) = (((f `| N) / (g `| N)) . (b . n)) by A66, A78;

          hence ((((f `| N) / (g `| N)) /* b) . n) <= ((((f / g) /* a) ^\ k) . n) by A71, A76, FUNCT_2: 108, XBOOLE_1: 1, A78;

        end;

        ( lim a1) = x0 by A56, A57, SEQ_4: 20;

        then b is convergent & ( lim b) = x0 by A56, A68, A67, SEQ_2: 19, SEQ_2: 20;

        then (((f `| N) / (g `| N)) /* b) is divergent_to+infty by A8, A71, LIMFUNC3:def 2;

        then (((f / g) /* a) ^\ k) is divergent_to+infty by A77, LIMFUNC1: 42;

        hence thesis by LIMFUNC1: 7;

      end;

      

       A79: for r1, r2 st r1 < x0 & x0 < r2 holds 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 holds 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 A55, LIMFUNC2:def 2;

      

       A81: for x st x0 < x & x < (x0 + r) holds 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;

        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;

        

         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;

        N c= ( dom ((g . x) (#) f)) by A1, VALUED_1:def 5;

        then

         A107: ].x0, x.[ c= ( dom ((g . x) (#) f)) by A95;

        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;

        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;

        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;

        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;

        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 xx0 = x0 as Element of REAL by XREAL_0:def 1;

        set d = ( seq_const x0);

        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, A124, A125, LIMFUNC3: 7;

        set a1 = (a ^\ k);

        defpred X[ Element of NAT , Real] 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, NAT_1:def 3;

          hence (a1 . n) < (x0 + r) by A127;

        end;

        

         A129: for n holds ex c be Element of 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;

          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 be Nat;

          n in NAT by ORDINAL1:def 12;

          then (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 SEQ_1: 57;

        end;

        

         A136: ( lim d) = (d . 0 ) by SEQ_4: 26

        .= x0 by SEQ_1: 57;

        

         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 object;

          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).[;

          then

           A142: ].x0, (a1 . n).[ c= ( dom ((f `| N) / (g `| N))) by A6, A10;

          

           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 be Nat;

          

           A146: n in NAT by ORDINAL1:def 12;

          ((((f / g) /* a) ^\ k) . n) = (((f `| N) / (g `| N)) . (b . n)) by A134, A146;

          hence ((((f `| N) / (g `| N)) /* b) . n) <= ((((f / g) /* a) ^\ k) . n) by A139, A144, FUNCT_2: 108, XBOOLE_1: 1, A146;

        end;

        ( lim a1) = x0 by A124, A125, SEQ_4: 20;

        then b is convergent & ( lim b) = x0 by A124, A136, A135, SEQ_2: 19, SEQ_2: 20;

        then (((f `| N) / (g `| N)) /* b) is divergent_to+infty by A8, A139, LIMFUNC3:def 2;

        then (((f / g) /* a) ^\ k) is divergent_to+infty by A145, LIMFUNC1: 42;

        hence thesis by LIMFUNC1: 7;

      end;

      for r1 st x0 < r1 holds 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 :: L_HOSPIT:6

    (ex N be 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 be 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 such that

       A9: 0 < r and

       A10: N = ].(x0 - r), (x0 + r).[ by RCOMP_1:def 6;

      

       A11: for x st (x0 - r) < x & x < x0 holds ex c st c in ].x, x0.[ & ((f / g) . x) = (((f `| N) / (g `| N)) . c)

      proof

        

         A12: (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 A12;

        then

         A13: x0 in ].(x0 - r), (x0 + r).[ by RCOMP_1:def 2;

        

         A14: (( dom (f `| N)) /\ (( dom (g `| N)) \ ((g `| N) " { 0 }))) c= (( dom (g `| N)) \ ((g `| N) " { 0 })) by XBOOLE_1: 17;

        

         A15: (( dom f) /\ (( dom g) \ (g " { 0 }))) c= (( dom g) \ (g " { 0 })) by XBOOLE_1: 17;

        let x such that

         A16: (x0 - r) < x and

         A17: x < x0;

        set f1 = (((f . x) (#) g) - ((g . x) (#) f));

        

         A18: ( dom ((f . x) (#) g)) = ( dom g) & ( dom ((g . x) (#) f)) = ( dom f) by VALUED_1:def 5;

        then

         A19: ( dom (((f . x) (#) g) - ((g . x) (#) f))) = (( dom f) /\ ( dom g)) by VALUED_1: 12;

        x < (x0 + r) by A17, A12, XXREAL_0: 2;

        then x in { g1 : (x0 - r) < g1 & g1 < (x0 + r) } by A16;

        then x in ].(x0 - r), (x0 + r).[ by RCOMP_1:def 2;

        then

         A20: [.x, x0.] c= N by A10, A13, XXREAL_2:def 12;

        then

         A21: [.x, x0.] c= ( dom f) & [.x, x0.] c= ( dom g) by A1, A2;

        then

         A22: [.x, x0.] c= ( dom f1) by A19, XBOOLE_1: 19;

        (g | N) is continuous by A4, FDIFF_1: 25;

        then (g | [.x, x0.]) is continuous by A20, FCONT_1: 16;

        then

         A23: (((f . x) (#) g) | [.x, x0.]) is continuous by A2, A20, FCONT_1: 20, XBOOLE_1: 1;

        (f | N) is continuous by A3, FDIFF_1: 25;

        then (f | [.x, x0.]) is continuous by A20, FCONT_1: 16;

        then

         A24: (((g . x) (#) f) | [.x, x0.]) is continuous by A1, A20, FCONT_1: 20, XBOOLE_1: 1;

         [.x, x0.] c= ( dom (((f . x) (#) g) - ((g . x) (#) f))) by A21, A19, XBOOLE_1: 19;

        then

         A25: ((((f . x) (#) g) - ((g . x) (#) f)) | [.x, x0.]) is continuous by A18, A19, A24, A23, FCONT_1: 18;

        

         A26: ].x, x0.[ c= [.x, x0.] by XXREAL_1: 25;

        then

         A27: ].x, x0.[ c= N by A20;

        

         A28: x in [.x, x0.] by A17, XXREAL_1: 1;

        then x in ( dom f1) by A22;

        then

         A29: x in (( dom ((f . x) (#) g)) /\ ( dom ((g . x) (#) f))) by VALUED_1: 12;

        then

         A30: x in ( dom ((f . x) (#) g)) by XBOOLE_0:def 4;

        

         A31: x0 in [.x, x0.] by A17, XXREAL_1: 1;

        then x0 in ( dom f1) by A22;

        then

         A32: x0 in (( dom ((f . x) (#) g)) /\ ( dom ((g . x) (#) f))) by VALUED_1: 12;

        then

         A33: x0 in ( dom ((f . x) (#) g)) by XBOOLE_0:def 4;

        

         A34: x in ( dom ((g . x) (#) f)) by A29, XBOOLE_0:def 4;

        

         A35: (f1 . x) = ((((f . x) (#) g) . x) - (((g . x) (#) f) . x)) by A22, A28, VALUED_1: 13

        .= (((f . x) * (g . x)) - (((g . x) (#) f) . x)) by A30, VALUED_1:def 5

        .= (((g . x) * (f . x)) - ((g . x) * (f . x))) by A34, VALUED_1:def 5

        .= 0 ;

        

         A36: x0 in ( dom ((g . x) (#) f)) by A32, XBOOLE_0:def 4;

         not x in {x0} by A17, TARSKI:def 1;

        then

         A37: x in ( [.x, x0.] \ {x0}) by A28, XBOOLE_0:def 5;

        N c= ( dom ((f . x) (#) g)) by A2, VALUED_1:def 5;

        then

         A38: ].x, x0.[ c= ( dom ((f . x) (#) g)) by A27;

        N c= ( dom ((g . x) (#) f)) by A1, VALUED_1:def 5;

        then

         A39: ].x, x0.[ c= ( dom ((g . x) (#) f)) by A27;

        then ].x, x0.[ c= (( dom ((f . x) (#) g)) /\ ( dom ((g . x) (#) f))) by A38, XBOOLE_1: 19;

        then

         A40: ].x, x0.[ c= ( dom (((f . x) (#) g) - ((g . x) (#) f))) by VALUED_1: 12;

        f is_differentiable_on ].x, x0.[ by A3, A20, A26, FDIFF_1: 26, XBOOLE_1: 1;

        then

         A41: ((g . x) (#) f) is_differentiable_on ].x, x0.[ by A39, FDIFF_1: 20;

        g is_differentiable_on ].x, x0.[ by A4, A20, A26, FDIFF_1: 26, XBOOLE_1: 1;

        then

         A42: ((f . x) (#) g) is_differentiable_on ].x, x0.[ by A38, FDIFF_1: 20;

        (f1 . x0) = ((((f . x) (#) g) . x0) - (((g . x) (#) f) . x0)) by A22, A31, VALUED_1: 13

        .= (((f . x) * (g . x0)) - (((g . x) (#) f) . x0)) by A33, VALUED_1:def 5

        .= ( 0 - ((g . x) * 0 )) by A7, A36, VALUED_1:def 5

        .= 0 ;

        then

        consider t such that

         A43: t in ].x, x0.[ and

         A44: ( diff (f1,t)) = 0 by A17, A25, A41, A40, A42, A22, A35, FDIFF_1: 19, ROLLE: 1;

        

         A45: ((g . x) (#) f) is_differentiable_in t by A41, A43, FDIFF_1: 9;

        

         A46: f is_differentiable_in t by A3, A27, A43, FDIFF_1: 9;

        ((f . x) (#) g) is_differentiable_in t by A42, A43, FDIFF_1: 9;

        then 0 = (( diff (((f . x) (#) g),t)) - ( diff (((g . x) (#) f),t))) by A44, A45, FDIFF_1: 14;

        then

         A47: 0 = (( diff (((f . x) (#) g),t)) - ((g . x) * ( diff (f,t)))) by A46, FDIFF_1: 15;

        take t;

        

         A48: t in [.x, x0.] by A26, A43;

        ( [.x, x0.] \ {x0}) c= (N \ {x0}) by A20, XBOOLE_1: 33;

        then

         A49: ( [.x, x0.] \ {x0}) c= ( dom (f / g)) by A5;

        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 A15;

        then

         A50: x in ( dom g) & not x in (g " { 0 }) by A37, XBOOLE_0:def 5;

         A51:

        now

          assume (g . x) = 0 ;

          then (g . x) in { 0 } by TARSKI:def 1;

          hence contradiction by A50, FUNCT_1:def 7;

        end;

        

         A52: [.x, x0.] c= ( dom ((f `| N) / (g `| N))) by A6, A20;

        then [.x, x0.] c= (( dom (f `| N)) /\ (( dom (g `| N)) \ ((g `| N) " { 0 }))) by RFUNCT_1:def 1;

        then [.x, x0.] c= (( dom (g `| N)) \ ((g `| N) " { 0 })) by A14;

        then

         A53: t in ( dom (g `| N)) & not t in ((g `| N) " { 0 }) by A48, XBOOLE_0:def 5;

         A54:

        now

          assume ( diff (g,t)) = 0 ;

          then ((g `| N) . t) = 0 by A4, A20, A48, FDIFF_1:def 7;

          then ((g `| N) . t) in { 0 } by TARSKI:def 1;

          hence contradiction by A53, FUNCT_1:def 7;

        end;

        g is_differentiable_in t by A4, A27, A43, FDIFF_1: 9;

        then 0 = (((f . x) * ( diff (g,t))) - ((g . x) * ( diff (f,t)))) by A47, FDIFF_1: 15;

        then ((f . x) / (g . x)) = (( diff (f,t)) / ( diff (g,t))) by A51, A54, XCMPLX_1: 94;

        then ((f . x) * ((g . x) " )) = (( diff (f,t)) / ( diff (g,t))) by XCMPLX_0:def 9;

        then ((f . x) * ((g . x) " )) = (( diff (f,t)) * (( diff (g,t)) " )) by XCMPLX_0:def 9;

        then ((f / g) . x) = (( diff (f,t)) * (( diff (g,t)) " )) by A49, A37, RFUNCT_1:def 1;

        then ((f / g) . x) = (((f `| N) . t) * (( diff (g,t)) " )) by A3, A20, A48, FDIFF_1:def 7;

        then ((f / g) . x) = (((f `| N) . t) * (((g `| N) . t) " )) by A4, A20, A48, FDIFF_1:def 7;

        hence thesis by A43, A52, A48, RFUNCT_1:def 1;

      end;

      

       A55: 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 xx0 = x0 as Element of REAL by XREAL_0:def 1;

        set d = ( seq_const x0);

        let a;

        assume that

         A56: a is convergent and

         A57: ( lim a) = x0 and

         A58: ( rng a) c= (( dom (f / g)) /\ ( left_open_halfline x0));

        consider k such that

         A59: for n st k <= n holds (x0 - r) < (a . n) & (a . n) < (x0 + r) by A9, A56, A57, LIMFUNC3: 7;

        set a1 = (a ^\ k);

        defpred X[ Element of NAT , Real] means $2 in ].(a1 . $1), x0.[ & ((((f / g) /* a) ^\ k) . $1) = (((f `| N) / (g `| N)) . $2);

         A60:

        now

          let n;

          (a . (n + k)) in ( rng a) by VALUED_0: 28;

          then (a . (n + k)) in ( left_open_halfline x0) by A58, XBOOLE_0:def 4;

          then (a . (n + k)) in { g1 : 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, NAT_1:def 3;

          hence (x0 - r) < (a1 . n) by A59;

        end;

        

         A61: for n holds ex c be Element of REAL st X[n, c]

        proof

          let n;

          

           A62: ( rng a1) c= ( rng a) by VALUED_0: 21;

          (x0 - r) < (a1 . n) & (a1 . n) < x0 by A60;

          then

          consider c such that

           A63: c in ].(a1 . n), x0.[ and

           A64: ((f / g) . (a1 . n)) = (((f `| N) / (g `| N)) . c) by A11;

          take c;

          

           A65: (( dom (f / g)) /\ ( left_open_halfline x0)) c= ( dom (f / g)) by XBOOLE_1: 17;

          then ( rng a) c= ( dom (f / g)) by A58;

          then (((f / g) /* (a ^\ k)) . n) = (((f `| N) / (g `| N)) . c) by A64, A62, FUNCT_2: 108, XBOOLE_1: 1;

          hence thesis by A58, A63, A65, VALUED_0: 27, XBOOLE_1: 1;

        end;

        consider b such that

         A66: for n holds X[n, (b . n)] from FUNCT_2:sch 3( A61);

         A67:

        now

          let n be Nat;

          

           A68: n in NAT by ORDINAL1:def 12;

          (b . n) in ].(a1 . n), x0.[ by A66, A68;

          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 SEQ_1: 57;

        end;

        

         A69: ( lim d) = (d . 0 ) by SEQ_4: 26

        .= x0 by SEQ_1: 57;

        

         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 object;

          assume x in ( rng b);

          then

          consider n such that

           A73: x = (b . n) by FUNCT_2: 113;

          (a1 . n) < x0 by A60;

          then

           A74: (a1 . n) < (x0 + r) by A70, XXREAL_0: 2;

          (x0 - r) < (a1 . n) by A60;

          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).[;

          then

           A75: ].(a1 . n), x0.[ c= ( dom ((f `| N) / (g `| N))) by A6, A10;

          

           A76: x in ].(a1 . n), x0.[ by A66, 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 be Nat;

          

           A79: n in NAT by ORDINAL1:def 12;

          ((((f / g) /* a) ^\ k) . n) = (((f `| N) / (g `| N)) . (b . n)) by A66, A79;

          hence ((((f / g) /* a) ^\ k) . n) <= ((((f `| N) / (g `| N)) /* b) . n) by A72, A77, FUNCT_2: 108, XBOOLE_1: 1, A79;

        end;

        ( lim a1) = x0 by A56, A57, SEQ_4: 20;

        then b is convergent & ( lim b) = x0 by A56, A69, A67, SEQ_2: 19, SEQ_2: 20;

        then (((f `| N) / (g `| N)) /* b) is divergent_to-infty by A8, A72, LIMFUNC3:def 3;

        then (((f / g) /* a) ^\ k) is divergent_to-infty by A78, LIMFUNC1: 43;

        hence thesis by LIMFUNC1: 7;

      end;

      

       A80: for r1, r2 st r1 < x0 & x0 < r2 holds 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 holds ex t st r1 < t & t < x0 & t in ( dom (f / g)) by LIMFUNC3: 8;

      then

       A81: (f / g) is_left_divergent_to-infty_in x0 by A55, LIMFUNC2:def 3;

      

       A82: for x st x0 < x & x < (x0 + r) holds ex c st c in ].x0, x.[ & ((f / g) . x) = (((f `| N) / (g `| N)) . c)

      proof

        

         A83: (( dom (f `| N)) /\ (( dom (g `| N)) \ ((g `| N) " { 0 }))) c= (( dom (g `| N)) \ ((g `| N) " { 0 })) by XBOOLE_1: 17;

        

         A84: (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 A84;

        then

         A85: x0 in ].(x0 - r), (x0 + r).[ by RCOMP_1:def 2;

        let x such that

         A86: x0 < x and

         A87: x < (x0 + r);

        (x0 - r) < x by A86, A84, 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

         A88: [.x0, x.] c= N by A10, A85, XXREAL_2:def 12;

        then

         A89: [.x0, x.] c= ( dom f) & [.x0, x.] c= ( dom g) by A1, A2;

        (g | N) is continuous by A4, FDIFF_1: 25;

        then (g | [.x0, x.]) is continuous by A88, FCONT_1: 16;

        then

         A90: (((f . x) (#) g) | [.x0, x.]) is continuous by A2, A88, FCONT_1: 20, XBOOLE_1: 1;

        (f | N) is continuous by A3, FDIFF_1: 25;

        then (f | [.x0, x.]) is continuous by A88, FCONT_1: 16;

        then

         A91: (((g . x) (#) f) | [.x0, x.]) is continuous by A1, A88, FCONT_1: 20, XBOOLE_1: 1;

        

         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;

        then [.x0, x.] c= ( dom (((f . x) (#) g) - ((g . x) (#) f))) by A89, XBOOLE_1: 19;

        then

         A94: ((((f . x) (#) g) - ((g . x) (#) f)) | [.x0, x.]) is continuous by A92, A93, A91, A90, FCONT_1: 18;

        

         A95: ].x0, x.[ c= [.x0, x.] by XXREAL_1: 25;

        then

         A96: ].x0, x.[ c= N by A88;

        N c= ( dom ((f . x) (#) g)) by A2, VALUED_1:def 5;

        then

         A97: ].x0, x.[ c= ( dom ((f . x) (#) g)) by A96;

        g is_differentiable_on ].x0, x.[ by A4, A88, A95, FDIFF_1: 26, XBOOLE_1: 1;

        then

         A98: ((f . x) (#) g) is_differentiable_on ].x0, x.[ by A97, FDIFF_1: 20;

        N c= ( dom ((g . x) (#) f)) by A1, VALUED_1:def 5;

        then

         A99: ].x0, x.[ c= ( dom ((g . x) (#) f)) by A96;

        then ].x0, x.[ c= (( dom ((f . x) (#) g)) /\ ( dom ((g . x) (#) f))) by A97, XBOOLE_1: 19;

        then

         A100: ].x0, x.[ c= ( dom (((f . x) (#) g) - ((g . x) (#) f))) by VALUED_1: 12;

        f is_differentiable_on ].x0, x.[ by A3, A88, A95, FDIFF_1: 26, XBOOLE_1: 1;

        then

         A101: ((g . x) (#) f) is_differentiable_on ].x0, x.[ by A99, FDIFF_1: 20;

        set f1 = (((f . x) (#) g) - ((g . x) (#) f));

        

         A102: (( 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

         A103: [.x0, x.] c= ( dom f1) by A89, XBOOLE_1: 19;

        

         A104: x in [.x0, x.] by A86, XXREAL_1: 1;

        then x in ( dom f1) by A103;

        then

         A105: x in (( dom ((f . x) (#) g)) /\ ( dom ((g . x) (#) f))) by VALUED_1: 12;

        then

         A106: x in ( dom ((f . x) (#) g)) by XBOOLE_0:def 4;

        

         A107: x0 in [.x0, x.] by A86, XXREAL_1: 1;

        then x0 in ( dom f1) by A103;

        then

         A108: x0 in (( dom ((f . x) (#) g)) /\ ( dom ((g . x) (#) f))) by VALUED_1: 12;

        then

         A109: x0 in ( dom ((f . x) (#) g)) by XBOOLE_0:def 4;

        

         A110: x in ( dom ((g . x) (#) f)) by A105, XBOOLE_0:def 4;

        

         A111: (f1 . x) = ((((f . x) (#) g) . x) - (((g . x) (#) f) . x)) by A103, A104, VALUED_1: 13

        .= (((f . x) * (g . x)) - (((g . x) (#) f) . x)) by A106, VALUED_1:def 5

        .= (((g . x) * (f . x)) - ((g . x) * (f . x))) by A110, VALUED_1:def 5

        .= 0 ;

        

         A112: x0 in ( dom ((g . x) (#) f)) by A108, XBOOLE_0:def 4;

         not x in {x0} by A86, TARSKI:def 1;

        then

         A113: x in ( [.x0, x.] \ {x0}) by A104, XBOOLE_0:def 5;

        (f1 . x0) = ((((f . x) (#) g) . x0) - (((g . x) (#) f) . x0)) by A103, A107, VALUED_1: 13

        .= (((f . x) * (g . x0)) - (((g . x) (#) f) . x0)) by A109, VALUED_1:def 5

        .= ( 0 - ((g . x) * 0 )) by A7, A112, VALUED_1:def 5

        .= 0 ;

        then

        consider t such that

         A114: t in ].x0, x.[ and

         A115: ( diff (f1,t)) = 0 by A86, A94, A101, A100, A98, A103, A111, FDIFF_1: 19, ROLLE: 1;

        

         A116: ((g . x) (#) f) is_differentiable_in t by A101, A114, FDIFF_1: 9;

        

         A117: f is_differentiable_in t by A3, A96, A114, FDIFF_1: 9;

        ((f . x) (#) g) is_differentiable_in t by A98, A114, FDIFF_1: 9;

        then 0 = (( diff (((f . x) (#) g),t)) - ( diff (((g . x) (#) f),t))) by A115, A116, FDIFF_1: 14;

        then

         A118: 0 = (( diff (((f . x) (#) g),t)) - ((g . x) * ( diff (f,t)))) by A117, FDIFF_1: 15;

        take t;

        

         A119: t in [.x0, x.] by A95, A114;

        ( [.x0, x.] \ {x0}) c= (N \ {x0}) by A88, XBOOLE_1: 33;

        then

         A120: ( [.x0, x.] \ {x0}) c= ( dom (f / g)) by A5;

        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 A102;

        then

         A121: x in ( dom g) & not x in (g " { 0 }) by A113, XBOOLE_0:def 5;

         A122:

        now

          assume (g . x) = 0 ;

          then (g . x) in { 0 } by TARSKI:def 1;

          hence contradiction by A121, FUNCT_1:def 7;

        end;

        

         A123: [.x0, x.] c= ( dom ((f `| N) / (g `| N))) by A6, A88;

        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 A83;

        then

         A124: t in ( dom (g `| N)) & not t in ((g `| N) " { 0 }) by A119, XBOOLE_0:def 5;

         A125:

        now

          assume ( diff (g,t)) = 0 ;

          then ((g `| N) . t) = 0 by A4, A88, A119, FDIFF_1:def 7;

          then ((g `| N) . t) in { 0 } by TARSKI:def 1;

          hence contradiction by A124, FUNCT_1:def 7;

        end;

        g is_differentiable_in t by A4, A96, A114, FDIFF_1: 9;

        then 0 = (((f . x) * ( diff (g,t))) - ((g . x) * ( diff (f,t)))) by A118, FDIFF_1: 15;

        then ((f . x) / (g . x)) = (( diff (f,t)) / ( diff (g,t))) by A122, A125, 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 A120, A113, RFUNCT_1:def 1;

        then ((f / g) . x) = (((f `| N) . t) * (( diff (g,t)) " )) by A3, A88, A119, FDIFF_1:def 7;

        then ((f / g) . x) = (((f `| N) . t) * (((g `| N) . t) " )) by A4, A88, A119, FDIFF_1:def 7;

        hence thesis by A114, A123, A119, RFUNCT_1:def 1;

      end;

      

       A126: 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 xx0 = x0 as Element of REAL by XREAL_0:def 1;

        set d = ( seq_const x0);

        let a;

        assume that

         A127: a is convergent and

         A128: ( lim a) = x0 and

         A129: ( rng a) c= (( dom (f / g)) /\ ( right_open_halfline x0));

        consider k such that

         A130: for n st k <= n holds (x0 - r) < (a . n) & (a . n) < (x0 + r) by A9, A127, A128, LIMFUNC3: 7;

        set a1 = (a ^\ k);

        defpred X[ Element of NAT , Real] means $2 in ].x0, (a1 . $1).[ & ((((f / g) /* a) ^\ k) . $1) = (((f `| N) / (g `| N)) . $2);

         A131:

        now

          let n;

          (a . (n + k)) in ( rng a) by VALUED_0: 28;

          then (a . (n + k)) in ( right_open_halfline x0) by A129, 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, NAT_1:def 3;

          hence (a1 . n) < (x0 + r) by A130;

        end;

        

         A132: for n holds ex c be Element of REAL st X[n, c]

        proof

          let n;

          

           A133: ( rng a1) c= ( rng a) by VALUED_0: 21;

          x0 < (a1 . n) & (a1 . n) < (x0 + r) by A131;

          then

          consider c such that

           A134: c in ].x0, (a1 . n).[ and

           A135: ((f / g) . (a1 . n)) = (((f `| N) / (g `| N)) . c) by A82;

          take c;

          

           A136: (( dom (f / g)) /\ ( right_open_halfline x0)) c= ( dom (f / g)) by XBOOLE_1: 17;

          then ( rng a) c= ( dom (f / g)) by A129;

          then (((f / g) /* (a ^\ k)) . n) = (((f `| N) / (g `| N)) . c) by A135, A133, FUNCT_2: 108, XBOOLE_1: 1;

          hence thesis by A129, A134, A136, VALUED_0: 27, XBOOLE_1: 1;

        end;

        consider b such that

         A137: for n holds X[n, (b . n)] from FUNCT_2:sch 3( A132);

         A138:

        now

          let n be Nat;

          

           A139: n in NAT by ORDINAL1:def 12;

          (b . n) in ].x0, (a1 . n).[ by A137, A139;

          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 SEQ_1: 57;

        end;

        

         A140: ( lim d) = (d . 0 ) by SEQ_4: 26

        .= x0 by SEQ_1: 57;

        

         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))) \ {x0})

        proof

          let x be object;

          assume x in ( rng b);

          then

          consider n such that

           A144: x = (b . n) by FUNCT_2: 113;

          x0 < (a1 . n) by A131;

          then

           A145: (x0 - r) < (a1 . n) by A141, XXREAL_0: 2;

          (a1 . n) < (x0 + r) by A131;

          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).[;

          then

           A146: ].x0, (a1 . n).[ c= ( dom ((f `| N) / (g `| N))) by A6, A10;

          

           A147: x in ].x0, (a1 . n).[ by A137, 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 not x in {x0} by TARSKI:def 1;

          hence thesis by A147, A146, XBOOLE_0:def 5;

        end;

        

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

         A149:

        now

          let n be Nat;

          

           A150: n in NAT by ORDINAL1:def 12;

          ((((f / g) /* a) ^\ k) . n) = (((f `| N) / (g `| N)) . (b . n)) by A137, A150;

          hence ((((f / g) /* a) ^\ k) . n) <= ((((f `| N) / (g `| N)) /* b) . n) by A143, A148, FUNCT_2: 108, XBOOLE_1: 1, A150;

        end;

        ( lim a1) = x0 by A127, A128, SEQ_4: 20;

        then b is convergent & ( lim b) = x0 by A127, A140, A138, SEQ_2: 19, SEQ_2: 20;

        then (((f `| N) / (g `| N)) /* b) is divergent_to-infty by A8, A143, LIMFUNC3:def 3;

        then (((f / g) /* a) ^\ k) is divergent_to-infty by A149, LIMFUNC1: 43;

        hence thesis by LIMFUNC1: 7;

      end;

      for r1 st x0 < r1 holds ex t st t < r1 & x0 < t & t in ( dom (f / g)) by A80, LIMFUNC3: 8;

      then (f / g) is_right_divergent_to-infty_in x0 by A126, LIMFUNC2:def 6;

      hence thesis by A81, LIMFUNC3: 13;

    end;

    theorem :: L_HOSPIT:7

    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;

      

       A15: ].x0, (x0 + r).[ c= ( dom f) by A3, A13;

      

       A16: for x st x0 < x & x < (x0 + r) holds 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 object;

          assume

           A23: y in [.x0, x.];

          then

          reconsider y as Real;

          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;

        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;

         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;

        

         A41: ].x0, x.[ c= ].x0, (x0 + r).[

        proof

          let y be object;

          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;

        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;

        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;

        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;

          

           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;

          

           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;

        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 object;

          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).[;

        then

         A81: ( [.x0, x.] \ {x0}) c= ( dom (f / g)) by A7;

        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;

        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;

        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;

        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 xx0 = x0 as Element of REAL by XREAL_0:def 1;

        set d = ( seq_const x0);

        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] 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, NAT_1:def 3;

          hence (a1 . n) < (x0 + r) by A92;

        end;

        

         A94: for n holds ex c be Element of 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;

          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 object;

          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).];

          then

           A103: ].x0, (a1 . n).[ c= ( dom ((f `| ].x0, (x0 + r).[) / (g `| ].x0, (x0 + r).[))) by A8;

          

           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 be Nat;

          

           A106: n in NAT by ORDINAL1:def 12;

          (b . n) in ].x0, (a1 . n).[ by A99, A106;

          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 SEQ_1: 57;

        end;

        

         A107: ( lim d) = (d . 0 ) by SEQ_4: 26

        .= x0 by SEQ_1: 57;

        ( lim a1) = x0 by A89, A90, SEQ_4: 20;

        then

         A108: b is convergent & ( lim b) = x0 by A89, A107, A105, SEQ_2: 19, SEQ_2: 20;

        

         A109: (( 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;

         A110:

        now

          reconsider m = 0 as Nat;

          take m;

          let n be Nat such that m <= n;

          

           A111: n in NAT by ORDINAL1:def 12;

          ((((f / g) /* a) ^\ k) . n) = (((f `| ].x0, (x0 + r).[) / (g `| ].x0, (x0 + r).[)) . (b . n)) by A99, A111;

          hence ((((f / g) /* a) ^\ k) . n) = ((((f `| ].x0, (x0 + r).[) / (g `| ].x0, (x0 + r).[)) /* b) . n) by A100, A109, FUNCT_2: 108, XBOOLE_1: 1, A111;

        end;

        ( lim_right (((f `| ].x0, (x0 + r).[) / (g `| ].x0, (x0 + r).[)),x0)) = ( lim_right (((f `| ].x0, (x0 + r).[) / (g `| ].x0, (x0 + r).[)),x0));

        then

         A112: (((f `| ].x0, (x0 + r).[) / (g `| ].x0, (x0 + r).[)) /* b) is convergent by A12, A108, A100, LIMFUNC2:def 8;

        then

         A113: (((f / g) /* a) ^\ k) is convergent by A110, 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, A108, A100, LIMFUNC2:def 8;

        then ( lim (((f / g) /* a) ^\ k)) = ( lim_right (((f `| ].x0, (x0 + r).[) / (g `| ].x0, (x0 + r).[)),x0)) by A112, A110, SEQ_4: 19;

        hence thesis by A113, SEQ_4: 21, SEQ_4: 22;

      end;

      

       A114: for r1 st x0 < r1 holds 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 A114, A88, Th2;

    end;

    theorem :: L_HOSPIT:8

    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;

      

       A15: ].(x0 - r), x0.[ c= ( dom f) by A3, A13;

      

       A16: for x st (x0 - r) < x & x < x0 holds 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;

        then

         A20: {x, x0} c= ( dom f) by A19, ZFMISC_1: 32;

        

         A21: ].x, x0.[ c= ].(x0 - r), x0.[

        proof

          let y be object;

          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;

        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;

         ].(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;

        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;

        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 object;

          assume

           A34: y in [.x, x0.];

          then

          reconsider y as Real;

          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;

        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;

        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;

          

           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;

          

           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 object;

          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.[;

        then

         A79: ( [.x, x0.] \ {x0}) c= ( dom (f / g)) by A7;

        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;

        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;

        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;

        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 xx0 = x0 as Element of REAL by XREAL_0:def 1;

        set d = ( seq_const x0);

        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] 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, NAT_1:def 3;

          hence (x0 - r) < (a1 . n) by A90;

        end;

        

         A92: for n holds ex c be Element of 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;

          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 object;

          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.];

          then

           A101: ].(a1 . n), x0.[ c= ( dom ((f `| ].(x0 - r), x0.[) / (g `| ].(x0 - r), x0.[))) by A8;

          

           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 be Nat;

          

           A104: n in NAT by ORDINAL1:def 12;

          (b . n) in ].(a1 . n), x0.[ by A97, A104;

          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 SEQ_1: 57;

        end;

        

         A105: ( lim d) = (d . 0 ) by SEQ_4: 26

        .= x0 by SEQ_1: 57;

        ( lim a1) = x0 by A87, A88, SEQ_4: 20;

        then

         A106: b is convergent & ( lim b) = x0 by A87, A105, A103, SEQ_2: 19, SEQ_2: 20;

        

         A107: (( 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;

         A108:

        now

          reconsider m = 0 as Nat;

          take m;

          let n be Nat such that m <= n;

          

           A109: n in NAT by ORDINAL1:def 12;

          ((((f / g) /* a) ^\ k) . n) = (((f `| ].(x0 - r), x0.[) / (g `| ].(x0 - r), x0.[)) . (b . n)) by A97, A109;

          hence ((((f / g) /* a) ^\ k) . n) = ((((f `| ].(x0 - r), x0.[) / (g `| ].(x0 - r), x0.[)) /* b) . n) by A98, A107, FUNCT_2: 108, XBOOLE_1: 1, A109;

        end;

        ( lim_left (((f `| ].(x0 - r), x0.[) / (g `| ].(x0 - r), x0.[)),x0)) = ( lim_left (((f `| ].(x0 - r), x0.[) / (g `| ].(x0 - r), x0.[)),x0));

        then

         A110: (((f `| ].(x0 - r), x0.[) / (g `| ].(x0 - r), x0.[)) /* b) is convergent by A12, A106, A98, LIMFUNC2:def 7;

        then

         A111: (((f / g) /* a) ^\ k) is convergent by A108, 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, A106, A98, LIMFUNC2:def 7;

        then ( lim (((f / g) /* a) ^\ k)) = ( lim_left (((f `| ].(x0 - r), x0.[) / (g `| ].(x0 - r), x0.[)),x0)) by A110, A108, SEQ_4: 19;

        hence thesis by A111, SEQ_4: 21, SEQ_4: 22;

      end;

      

       A112: for r1 st r1 < x0 holds 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 A112, A86, Th3;

    end;

    theorem :: L_HOSPIT:9

    (ex N be 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 be Neighbourhood of x0 st ( lim ((f / g),x0)) = ( lim (((f `| N) / (g `| N)),x0))

    proof

      given N be 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 such that

       A9: 0 < r and

       A10: N = ].(x0 - r), (x0 + r).[ by RCOMP_1:def 6;

      

       A11: for x st x0 < x & x < (x0 + r) holds ex c st c in ].x0, x.[ & ((f / g) . x) = (((f `| N) / (g `| N)) . c)

      proof

        

         A12: (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 A12;

        then

         A13: x0 in ].(x0 - r), (x0 + r).[ by RCOMP_1:def 2;

        

         A14: (( dom (f `| N)) /\ (( dom (g `| N)) \ ((g `| N) " { 0 }))) c= (( dom (g `| N)) \ ((g `| N) " { 0 })) by XBOOLE_1: 17;

        

         A15: (( dom f) /\ (( dom g) \ (g " { 0 }))) c= (( dom g) \ (g " { 0 })) by XBOOLE_1: 17;

        let x such that

         A16: x0 < x and

         A17: x < (x0 + r);

        set f1 = (((f . x) (#) g) - ((g . x) (#) f));

        

         A18: ( dom ((f . x) (#) g)) = ( dom g) & ( dom ((g . x) (#) f)) = ( dom f) by VALUED_1:def 5;

        then

         A19: ( dom (((f . x) (#) g) - ((g . x) (#) f))) = (( dom f) /\ ( dom g)) by VALUED_1: 12;

        (x0 - r) < x by A16, A12, 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

         A20: [.x0, x.] c= N by A10, A13, XXREAL_2:def 12;

        then

         A21: [.x0, x.] c= ( dom f) & [.x0, x.] c= ( dom g) by A1, A2;

        then

         A22: [.x0, x.] c= ( dom f1) by A19, XBOOLE_1: 19;

        (g | N) is continuous by A4, FDIFF_1: 25;

        then (g | [.x0, x.]) is continuous by A20, FCONT_1: 16;

        then

         A23: (((f . x) (#) g) | [.x0, x.]) is continuous by A2, A20, FCONT_1: 20, XBOOLE_1: 1;

        (f | N) is continuous by A3, FDIFF_1: 25;

        then (f | [.x0, x.]) is continuous by A20, FCONT_1: 16;

        then

         A24: (((g . x) (#) f) | [.x0, x.]) is continuous by A1, A20, FCONT_1: 20, XBOOLE_1: 1;

         [.x0, x.] c= ( dom (((f . x) (#) g) - ((g . x) (#) f))) by A21, A19, XBOOLE_1: 19;

        then

         A25: ((((f . x) (#) g) - ((g . x) (#) f)) | [.x0, x.]) is continuous by A18, A19, A24, A23, FCONT_1: 18;

        

         A26: ].x0, x.[ c= [.x0, x.] by XXREAL_1: 25;

        then

         A27: ].x0, x.[ c= N by A20;

        

         A28: x in [.x0, x.] by A16, XXREAL_1: 1;

        then x in ( dom f1) by A22;

        then

         A29: x in (( dom ((f . x) (#) g)) /\ ( dom ((g . x) (#) f))) by VALUED_1: 12;

        then

         A30: x in ( dom ((f . x) (#) g)) by XBOOLE_0:def 4;

        

         A31: x0 in [.x0, x.] by A16, XXREAL_1: 1;

        then x0 in ( dom f1) by A22;

        then

         A32: x0 in (( dom ((f . x) (#) g)) /\ ( dom ((g . x) (#) f))) by VALUED_1: 12;

        then

         A33: x0 in ( dom ((f . x) (#) g)) by XBOOLE_0:def 4;

        

         A34: x in ( dom ((g . x) (#) f)) by A29, XBOOLE_0:def 4;

        

         A35: (f1 . x) = ((((f . x) (#) g) . x) - (((g . x) (#) f) . x)) by A22, A28, VALUED_1: 13

        .= (((f . x) * (g . x)) - (((g . x) (#) f) . x)) by A30, VALUED_1:def 5

        .= (((g . x) * (f . x)) - ((g . x) * (f . x))) by A34, VALUED_1:def 5

        .= 0 ;

        

         A36: x0 in ( dom ((g . x) (#) f)) by A32, XBOOLE_0:def 4;

         not x in {x0} by A16, TARSKI:def 1;

        then

         A37: x in ( [.x0, x.] \ {x0}) by A28, XBOOLE_0:def 5;

        N c= ( dom ((f . x) (#) g)) by A2, VALUED_1:def 5;

        then

         A38: ].x0, x.[ c= ( dom ((f . x) (#) g)) by A27;

        N c= ( dom ((g . x) (#) f)) by A1, VALUED_1:def 5;

        then

         A39: ].x0, x.[ c= ( dom ((g . x) (#) f)) by A27;

        then ].x0, x.[ c= (( dom ((f . x) (#) g)) /\ ( dom ((g . x) (#) f))) by A38, XBOOLE_1: 19;

        then

         A40: ].x0, x.[ c= ( dom (((f . x) (#) g) - ((g . x) (#) f))) by VALUED_1: 12;

        f is_differentiable_on ].x0, x.[ by A3, A20, A26, FDIFF_1: 26, XBOOLE_1: 1;

        then

         A41: ((g . x) (#) f) is_differentiable_on ].x0, x.[ by A39, FDIFF_1: 20;

        g is_differentiable_on ].x0, x.[ by A4, A20, A26, FDIFF_1: 26, XBOOLE_1: 1;

        then

         A42: ((f . x) (#) g) is_differentiable_on ].x0, x.[ by A38, FDIFF_1: 20;

        (f1 . x0) = ((((f . x) (#) g) . x0) - (((g . x) (#) f) . x0)) by A22, A31, VALUED_1: 13

        .= (((f . x) * (g . x0)) - (((g . x) (#) f) . x0)) by A33, VALUED_1:def 5

        .= ( 0 - ((g . x) * 0 )) by A7, A36, VALUED_1:def 5

        .= 0 ;

        then

        consider t such that

         A43: t in ].x0, x.[ and

         A44: ( diff (f1,t)) = 0 by A16, A25, A41, A40, A42, A22, A35, FDIFF_1: 19, ROLLE: 1;

        

         A45: ((g . x) (#) f) is_differentiable_in t by A41, A43, FDIFF_1: 9;

        

         A46: f is_differentiable_in t by A3, A27, A43, FDIFF_1: 9;

        ((f . x) (#) g) is_differentiable_in t by A42, A43, FDIFF_1: 9;

        then 0 = (( diff (((f . x) (#) g),t)) - ( diff (((g . x) (#) f),t))) by A44, A45, FDIFF_1: 14;

        then

         A47: 0 = (( diff (((f . x) (#) g),t)) - ((g . x) * ( diff (f,t)))) by A46, FDIFF_1: 15;

        take t;

        

         A48: t in [.x0, x.] by A26, A43;

        ( [.x0, x.] \ {x0}) c= (N \ {x0}) by A20, XBOOLE_1: 33;

        then

         A49: ( [.x0, x.] \ {x0}) c= ( dom (f / g)) by A5;

        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 A15;

        then

         A50: x in ( dom g) & not x in (g " { 0 }) by A37, XBOOLE_0:def 5;

         A51:

        now

          assume (g . x) = 0 ;

          then (g . x) in { 0 } by TARSKI:def 1;

          hence contradiction by A50, FUNCT_1:def 7;

        end;

        

         A52: [.x0, x.] c= ( dom ((f `| N) / (g `| N))) by A6, A20;

        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 A14;

        then

         A53: t in ( dom (g `| N)) & not t in ((g `| N) " { 0 }) by A48, XBOOLE_0:def 5;

         A54:

        now

          assume ( diff (g,t)) = 0 ;

          then ((g `| N) . t) = 0 by A4, A20, A48, FDIFF_1:def 7;

          then ((g `| N) . t) in { 0 } by TARSKI:def 1;

          hence contradiction by A53, FUNCT_1:def 7;

        end;

        g is_differentiable_in t by A4, A27, A43, FDIFF_1: 9;

        then 0 = (((f . x) * ( diff (g,t))) - ((g . x) * ( diff (f,t)))) by A47, FDIFF_1: 15;

        then ((f . x) / (g . x)) = (( diff (f,t)) / ( diff (g,t))) by A51, A54, XCMPLX_1: 94;

        then ((f . x) * ((g . x) " )) = (( diff (f,t)) / ( diff (g,t))) by XCMPLX_0:def 9;

        then ((f . x) * ((g . x) " )) = (( diff (f,t)) * (( diff (g,t)) " )) by XCMPLX_0:def 9;

        then ((f / g) . x) = (( diff (f,t)) * (( diff (g,t)) " )) by A49, A37, RFUNCT_1:def 1;

        then ((f / g) . x) = (((f `| N) . t) * (( diff (g,t)) " )) by A3, A20, A48, FDIFF_1:def 7;

        then ((f / g) . x) = (((f `| N) . t) * (((g `| N) . t) " )) by A4, A20, A48, FDIFF_1:def 7;

        hence thesis by A43, A52, A48, RFUNCT_1:def 1;

      end;

      

       A55: 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 xx0 = x0 as Element of REAL by XREAL_0:def 1;

        set d = ( seq_const x0);

        let a;

        assume that

         A56: a is convergent and

         A57: ( lim a) = x0 and

         A58: ( rng a) c= (( dom (f / g)) /\ ( right_open_halfline x0));

        consider k such that

         A59: for n st k <= n holds (x0 - r) < (a . n) & (a . n) < (x0 + r) by A9, A56, A57, LIMFUNC3: 7;

        set a1 = (a ^\ k);

        defpred X[ Element of NAT , Real] means $2 in ].x0, (a1 . $1).[ & ((((f / g) /* a) ^\ k) . $1) = (((f `| N) / (g `| N)) . $2);

         A60:

        now

          let n;

          (a . (n + k)) in ( rng a) by VALUED_0: 28;

          then (a . (n + k)) in ( right_open_halfline x0) by A58, 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, NAT_1:def 3;

          hence (a1 . n) < (x0 + r) by A59;

        end;

        

         A61: for n holds ex c be Element of REAL st X[n, c]

        proof

          let n;

          

           A62: ( rng a1) c= ( rng a) by VALUED_0: 21;

          x0 < (a1 . n) & (a1 . n) < (x0 + r) by A60;

          then

          consider c such that

           A63: c in ].x0, (a1 . n).[ and

           A64: ((f / g) . (a1 . n)) = (((f `| N) / (g `| N)) . c) by A11;

          take c;

          

           A65: (( dom (f / g)) /\ ( right_open_halfline x0)) c= ( dom (f / g)) by XBOOLE_1: 17;

          then ( rng a) c= ( dom (f / g)) by A58;

          then (((f / g) /* (a ^\ k)) . n) = (((f `| N) / (g `| N)) . c) by A64, A62, FUNCT_2: 108, XBOOLE_1: 1;

          hence thesis by A58, A63, A65, VALUED_0: 27, XBOOLE_1: 1;

        end;

        consider b such that

         A66: for n holds X[n, (b . n)] from FUNCT_2:sch 3( A61);

         A67:

        now

          let n be Nat;

          

           A68: n in NAT by ORDINAL1:def 12;

          (b . n) in ].x0, (a1 . n).[ by A66, A68;

          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 SEQ_1: 57;

        end;

        

         A69: ( lim d) = (d . 0 ) by SEQ_4: 26

        .= x0 by SEQ_1: 57;

        ( lim a1) = x0 by A56, A57, SEQ_4: 20;

        then

         A70: b is convergent & ( lim b) = x0 by A56, A69, A67, SEQ_2: 19, SEQ_2: 20;

        

         A71: (x0 - r) < x0 by A9, XREAL_1: 44;

        x0 < (x0 + r) by A9, XREAL_1: 29;

        then x0 in { g2 : (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 object;

          assume x in ( rng b);

          then

          consider n such that

           A74: x = (b . n) by FUNCT_2: 113;

          x0 < (a1 . n) by A60;

          then

           A75: (x0 - r) < (a1 . n) by A71, XXREAL_0: 2;

          (a1 . n) < (x0 + r) by A60;

          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).[;

          then

           A76: ].x0, (a1 . n).[ c= ( dom ((f `| N) / (g `| N))) by A6, A10;

          

           A77: x in ].x0, (a1 . n).[ by A66, 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

          reconsider m = 0 as Nat;

          take m;

          let n be Nat such that m <= n;

          

           A80: n in NAT by ORDINAL1:def 12;

          ((((f / g) /* a) ^\ k) . n) = (((f `| N) / (g `| N)) . (b . n)) by A66, A80;

          hence ((((f / g) /* a) ^\ k) . n) = ((((f `| N) / (g `| N)) /* b) . n) by A73, A78, FUNCT_2: 108, XBOOLE_1: 1, A80;

        end;

        ( lim (((f `| N) / (g `| N)),x0)) = ( lim (((f `| N) / (g `| N)),x0));

        then

         A81: (((f `| N) / (g `| N)) /* b) is convergent by A8, A70, A73, LIMFUNC3:def 4;

        then

         A82: (((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 A81, A79, SEQ_4: 19;

        hence thesis by A82, SEQ_4: 21, SEQ_4: 22;

      end;

      

       A83: for r1, r2 st r1 < x0 & x0 < r2 holds 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 holds ex t st t < r1 & x0 < t & t in ( dom (f / g)) by LIMFUNC3: 8;

      then

       A84: (f / g) is_right_convergent_in x0 & ( lim_right ((f / g),x0)) = ( lim (((f `| N) / (g `| N)),x0)) by A55, Th2;

      

       A85: for x st (x0 - r) < x & x < x0 holds ex c st c in ].x, x0.[ & ((f / g) . x) = (((f `| N) / (g `| N)) . c)

      proof

        

         A86: (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 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 - r) < x and

         A91: x < x0;

        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;

        x < (x0 + r) by A91, A86, XXREAL_0: 2;

        then x in { g1 : (x0 - r) < g1 & g1 < (x0 + r) } by A90;

        then x in ].(x0 - r), (x0 + r).[ by RCOMP_1:def 2;

        then

         A94: [.x, x0.] c= N by A10, A87, XXREAL_2:def 12;

        then

         A95: [.x, x0.] c= ( dom f) & [.x, x0.] c= ( dom g) by A1, A2;

        then

         A96: [.x, x0.] c= ( dom f1) by A93, XBOOLE_1: 19;

        (g | N) is continuous by A4, FDIFF_1: 25;

        then (g | [.x, x0.]) is continuous by A94, FCONT_1: 16;

        then

         A97: (((f . x) (#) g) | [.x, x0.]) is continuous by A2, A94, FCONT_1: 20, XBOOLE_1: 1;

        (f | N) is continuous by A3, FDIFF_1: 25;

        then (f | [.x, x0.]) is continuous by A94, FCONT_1: 16;

        then

         A98: (((g . x) (#) f) | [.x, x0.]) is continuous by A1, A94, FCONT_1: 20, XBOOLE_1: 1;

         [.x, x0.] c= ( dom (((f . x) (#) g) - ((g . x) (#) f))) by A95, A93, XBOOLE_1: 19;

        then

         A99: ((((f . x) (#) g) - ((g . x) (#) f)) | [.x, x0.]) is continuous by A92, A93, A98, A97, FCONT_1: 18;

        

         A100: ].x, x0.[ c= [.x, x0.] by XXREAL_1: 25;

        then

         A101: ].x, x0.[ c= N by A94;

        

         A102: x in [.x, x0.] by A91, 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 [.x, x0.] by A91, 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 A91, TARSKI:def 1;

        then

         A111: x in ( [.x, x0.] \ {x0}) by A102, XBOOLE_0:def 5;

        N c= ( dom ((f . x) (#) g)) by A2, VALUED_1:def 5;

        then

         A112: ].x, x0.[ c= ( dom ((f . x) (#) g)) by A101;

        N c= ( dom ((g . x) (#) f)) by A1, VALUED_1:def 5;

        then

         A113: ].x, x0.[ c= ( dom ((g . x) (#) f)) by A101;

        then ].x, x0.[ c= (( dom ((f . x) (#) g)) /\ ( dom ((g . x) (#) f))) by A112, XBOOLE_1: 19;

        then

         A114: ].x, x0.[ c= ( dom (((f . x) (#) g) - ((g . x) (#) f))) by VALUED_1: 12;

        f is_differentiable_on ].x, x0.[ by A3, A94, A100, FDIFF_1: 26, XBOOLE_1: 1;

        then

         A115: ((g . x) (#) f) is_differentiable_on ].x, x0.[ by A113, FDIFF_1: 20;

        g is_differentiable_on ].x, x0.[ by A4, A94, A100, FDIFF_1: 26, XBOOLE_1: 1;

        then

         A116: ((f . x) (#) g) is_differentiable_on ].x, x0.[ 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 ].x, x0.[ and

         A118: ( diff (f1,t)) = 0 by A91, 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 [.x, x0.] by A100, A117;

        ( [.x, x0.] \ {x0}) c= (N \ {x0}) by A94, XBOOLE_1: 33;

        then

         A123: ( [.x, x0.] \ {x0}) c= ( dom (f / g)) by A5;

        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 A89;

        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: [.x, x0.] c= ( dom ((f `| N) / (g `| N))) by A6, A94;

        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 A88;

        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)) /\ ( left_open_halfline x0)) holds ((f / g) /* a) is convergent & ( lim ((f / g) /* a)) = ( lim (((f `| N) / (g `| N)),x0))

      proof

        reconsider xx0 = x0 as Element of REAL by XREAL_0:def 1;

        set d = ( seq_const x0);

        let a;

        assume that

         A130: a is convergent and

         A131: ( lim a) = x0 and

         A132: ( rng a) c= (( dom (f / g)) /\ ( left_open_halfline x0));

        consider k such that

         A133: for n st k <= n holds (x0 - r) < (a . n) & (a . n) < (x0 + r) by A9, A130, A131, LIMFUNC3: 7;

        set a1 = (a ^\ k);

        defpred X[ Element of NAT , Real] means $2 in ].(a1 . $1), x0.[ & ((((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 ( left_open_halfline x0) by A132, 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, NAT_1:def 3;

          hence (x0 - r) < (a1 . n) by A133;

        end;

        

         A135: for n holds ex c be Element of REAL st X[n, c]

        proof

          let n;

          

           A136: ( rng a1) c= ( rng a) by VALUED_0: 21;

          (x0 - r) < (a1 . n) & (a1 . n) < x0 by A134;

          then

          consider c such that

           A137: c in ].(a1 . n), x0.[ and

           A138: ((f / g) . (a1 . n)) = (((f `| N) / (g `| N)) . c) by A85;

          take c;

          

           A139: (( dom (f / g)) /\ ( left_open_halfline x0)) c= ( dom (f / g)) by XBOOLE_1: 17;

          then ( rng a) c= ( dom (f / g)) by A132;

          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:

        now

          let n be Nat;

          

           A142: n in NAT by ORDINAL1:def 12;

          (b . n) in ].(a1 . n), x0.[ by A140, A142;

          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 SEQ_1: 57;

        end;

        

         A143: ( lim d) = (d . 0 ) by SEQ_4: 26

        .= x0 by SEQ_1: 57;

        ( lim a1) = x0 by A130, A131, SEQ_4: 20;

        then

         A144: b is convergent & ( lim b) = x0 by A130, A143, A141, SEQ_2: 19, SEQ_2: 20;

        

         A145: 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 A145;

        then

         A146: x0 in ].(x0 - r), (x0 + r).[ by RCOMP_1:def 2;

        

         A147: ( rng b) c= (( dom ((f `| N) / (g `| N))) \ {x0})

        proof

          let x be object;

          assume x in ( rng b);

          then

          consider n such that

           A148: x = (b . n) by FUNCT_2: 113;

          (a1 . n) < x0 by A134;

          then

           A149: (a1 . n) < (x0 + r) by A145, XXREAL_0: 2;

          (x0 - r) < (a1 . n) by A134;

          then (a1 . n) in { g3 : (x0 - r) < g3 & g3 < (x0 + r) } by A149;

          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 A146, XXREAL_1: 25, XXREAL_2:def 12;

          then ].(a1 . n), x0.[ c= ].(x0 - r), (x0 + r).[;

          then

           A150: ].(a1 . n), x0.[ c= ( dom ((f `| N) / (g `| N))) by A6, A10;

          

           A151: x in ].(a1 . n), x0.[ by A140, A148;

          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 A151, A150, XBOOLE_0:def 5;

        end;

        

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

         A153:

        now

          reconsider m = 0 as Nat;

          take m;

          let n be Nat such that m <= n;

          

           A154: n in NAT by ORDINAL1:def 12;

          ((((f / g) /* a) ^\ k) . n) = (((f `| N) / (g `| N)) . (b . n)) by A140, A154;

          hence ((((f / g) /* a) ^\ k) . n) = ((((f `| N) / (g `| N)) /* b) . n) by A147, A152, FUNCT_2: 108, XBOOLE_1: 1, A154;

        end;

        ( lim (((f `| N) / (g `| N)),x0)) = ( lim (((f `| N) / (g `| N)),x0));

        then

         A155: (((f `| N) / (g `| N)) /* b) is convergent by A8, A144, A147, LIMFUNC3:def 4;

        then

         A156: (((f / g) /* a) ^\ k) is convergent by A153, SEQ_4: 18;

        ( lim (((f `| N) / (g `| N)) /* b)) = ( lim (((f `| N) / (g `| N)),x0)) by A8, A144, A147, LIMFUNC3:def 4;

        then ( lim (((f / g) /* a) ^\ k)) = ( lim (((f `| N) / (g `| N)),x0)) by A155, A153, SEQ_4: 19;

        hence thesis by A156, SEQ_4: 21, SEQ_4: 22;

      end;

      for r1 st r1 < x0 holds ex t st r1 < t & t < x0 & t in ( dom (f / g)) by A83, LIMFUNC3: 8;

      then

       A157: (f / g) is_left_convergent_in x0 & ( lim_left ((f / g),x0)) = ( lim (((f `| N) / (g `| N)),x0)) by A129, Th3;

      hence (f / g) is_convergent_in x0 by A84, LIMFUNC3: 30;

      take N;

      thus thesis by A84, A157, LIMFUNC3: 30;

    end;

    ::$Notion-Name

    theorem :: L_HOSPIT:10

    (ex N be 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 be 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 such that

       A9: 0 < r and

       A10: N = ].(x0 - r), (x0 + r).[ by RCOMP_1:def 6;

      

       A11: for x st (x0 - r) < x & x < x0 holds ex c st c in ].x, x0.[ & ((f / g) . x) = (((f `| N) / (g `| N)) . c)

      proof

        

         A12: (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 A12;

        then

         A13: x0 in ].(x0 - r), (x0 + r).[ by RCOMP_1:def 2;

        

         A14: (( dom (f `| N)) /\ (( dom (g `| N)) \ ((g `| N) " { 0 }))) c= (( dom (g `| N)) \ ((g `| N) " { 0 })) by XBOOLE_1: 17;

        

         A15: (( dom f) /\ (( dom g) \ (g " { 0 }))) c= (( dom g) \ (g " { 0 })) by XBOOLE_1: 17;

        let x such that

         A16: (x0 - r) < x and

         A17: x < x0;

        set f1 = (((f . x) (#) g) - ((g . x) (#) f));

        

         A18: ( dom ((f . x) (#) g)) = ( dom g) & ( dom ((g . x) (#) f)) = ( dom f) by VALUED_1:def 5;

        then

         A19: ( dom (((f . x) (#) g) - ((g . x) (#) f))) = (( dom f) /\ ( dom g)) by VALUED_1: 12;

        x < (x0 + r) by A17, A12, XXREAL_0: 2;

        then x in { g1 : (x0 - r) < g1 & g1 < (x0 + r) } by A16;

        then x in ].(x0 - r), (x0 + r).[ by RCOMP_1:def 2;

        then

         A20: [.x, x0.] c= N by A10, A13, XXREAL_2:def 12;

        then

         A21: [.x, x0.] c= ( dom f) & [.x, x0.] c= ( dom g) by A1, A2;

        then

         A22: [.x, x0.] c= ( dom f1) by A19, XBOOLE_1: 19;

        (g | N) is continuous by A4, FDIFF_1: 25;

        then (g | [.x, x0.]) is continuous by A20, FCONT_1: 16;

        then

         A23: (((f . x) (#) g) | [.x, x0.]) is continuous by A2, A20, FCONT_1: 20, XBOOLE_1: 1;

        (f | N) is continuous by A3, FDIFF_1: 25;

        then (f | [.x, x0.]) is continuous by A20, FCONT_1: 16;

        then

         A24: (((g . x) (#) f) | [.x, x0.]) is continuous by A1, A20, FCONT_1: 20, XBOOLE_1: 1;

         [.x, x0.] c= ( dom (((f . x) (#) g) - ((g . x) (#) f))) by A21, A19, XBOOLE_1: 19;

        then

         A25: ((((f . x) (#) g) - ((g . x) (#) f)) | [.x, x0.]) is continuous by A18, A19, A24, A23, FCONT_1: 18;

        

         A26: ].x, x0.[ c= [.x, x0.] by XXREAL_1: 25;

        then

         A27: ].x, x0.[ c= N by A20;

        

         A28: x in [.x, x0.] by A17, XXREAL_1: 1;

        then x in ( dom f1) by A22;

        then

         A29: x in (( dom ((f . x) (#) g)) /\ ( dom ((g . x) (#) f))) by VALUED_1: 12;

        then

         A30: x in ( dom ((f . x) (#) g)) by XBOOLE_0:def 4;

        

         A31: x0 in [.x, x0.] by A17, XXREAL_1: 1;

        then x0 in ( dom f1) by A22;

        then

         A32: x0 in (( dom ((f . x) (#) g)) /\ ( dom ((g . x) (#) f))) by VALUED_1: 12;

        then

         A33: x0 in ( dom ((f . x) (#) g)) by XBOOLE_0:def 4;

        

         A34: x in ( dom ((g . x) (#) f)) by A29, XBOOLE_0:def 4;

        

         A35: (f1 . x) = ((((f . x) (#) g) . x) - (((g . x) (#) f) . x)) by A22, A28, VALUED_1: 13

        .= (((f . x) * (g . x)) - (((g . x) (#) f) . x)) by A30, VALUED_1:def 5

        .= (((g . x) * (f . x)) - ((g . x) * (f . x))) by A34, VALUED_1:def 5

        .= 0 ;

        

         A36: x0 in ( dom ((g . x) (#) f)) by A32, XBOOLE_0:def 4;

         not x in {x0} by A17, TARSKI:def 1;

        then

         A37: x in ( [.x, x0.] \ {x0}) by A28, XBOOLE_0:def 5;

        N c= ( dom ((f . x) (#) g)) by A2, VALUED_1:def 5;

        then

         A38: ].x, x0.[ c= ( dom ((f . x) (#) g)) by A27;

        N c= ( dom ((g . x) (#) f)) by A1, VALUED_1:def 5;

        then

         A39: ].x, x0.[ c= ( dom ((g . x) (#) f)) by A27;

        then ].x, x0.[ c= (( dom ((f . x) (#) g)) /\ ( dom ((g . x) (#) f))) by A38, XBOOLE_1: 19;

        then

         A40: ].x, x0.[ c= ( dom (((f . x) (#) g) - ((g . x) (#) f))) by VALUED_1: 12;

        f is_differentiable_on ].x, x0.[ by A3, A20, A26, FDIFF_1: 26, XBOOLE_1: 1;

        then

         A41: ((g . x) (#) f) is_differentiable_on ].x, x0.[ by A39, FDIFF_1: 20;

        g is_differentiable_on ].x, x0.[ by A4, A20, A26, FDIFF_1: 26, XBOOLE_1: 1;

        then

         A42: ((f . x) (#) g) is_differentiable_on ].x, x0.[ by A38, FDIFF_1: 20;

        (f1 . x0) = ((((f . x) (#) g) . x0) - (((g . x) (#) f) . x0)) by A22, A31, VALUED_1: 13

        .= (((f . x) * (g . x0)) - (((g . x) (#) f) . x0)) by A33, VALUED_1:def 5

        .= ( 0 - ((g . x) * 0 )) by A7, A36, VALUED_1:def 5

        .= 0 ;

        then

        consider t such that

         A43: t in ].x, x0.[ and

         A44: ( diff (f1,t)) = 0 by A17, A25, A41, A40, A42, A22, A35, FDIFF_1: 19, ROLLE: 1;

        

         A45: ((g . x) (#) f) is_differentiable_in t by A41, A43, FDIFF_1: 9;

        

         A46: f is_differentiable_in t by A3, A27, A43, FDIFF_1: 9;

        ((f . x) (#) g) is_differentiable_in t by A42, A43, FDIFF_1: 9;

        then 0 = (( diff (((f . x) (#) g),t)) - ( diff (((g . x) (#) f),t))) by A44, A45, FDIFF_1: 14;

        then

         A47: 0 = (( diff (((f . x) (#) g),t)) - ((g . x) * ( diff (f,t)))) by A46, FDIFF_1: 15;

        take t;

        

         A48: t in [.x, x0.] by A26, A43;

        ( [.x, x0.] \ {x0}) c= (N \ {x0}) by A20, XBOOLE_1: 33;

        then

         A49: ( [.x, x0.] \ {x0}) c= ( dom (f / g)) by A5;

        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 A15;

        then

         A50: x in ( dom g) & not x in (g " { 0 }) by A37, XBOOLE_0:def 5;

         A51:

        now

          assume (g . x) = 0 ;

          then (g . x) in { 0 } by TARSKI:def 1;

          hence contradiction by A50, FUNCT_1:def 7;

        end;

        

         A52: [.x, x0.] c= ( dom ((f `| N) / (g `| N))) by A6, A20;

        then [.x, x0.] c= (( dom (f `| N)) /\ (( dom (g `| N)) \ ((g `| N) " { 0 }))) by RFUNCT_1:def 1;

        then [.x, x0.] c= (( dom (g `| N)) \ ((g `| N) " { 0 })) by A14;

        then

         A53: t in ( dom (g `| N)) & not t in ((g `| N) " { 0 }) by A48, XBOOLE_0:def 5;

         A54:

        now

          assume ( diff (g,t)) = 0 ;

          then ((g `| N) . t) = 0 by A4, A20, A48, FDIFF_1:def 7;

          then ((g `| N) . t) in { 0 } by TARSKI:def 1;

          hence contradiction by A53, FUNCT_1:def 7;

        end;

        g is_differentiable_in t by A4, A27, A43, FDIFF_1: 9;

        then 0 = (((f . x) * ( diff (g,t))) - ((g . x) * ( diff (f,t)))) by A47, FDIFF_1: 15;

        then ((f . x) / (g . x)) = (( diff (f,t)) / ( diff (g,t))) by A51, A54, XCMPLX_1: 94;

        then ((f . x) * ((g . x) " )) = (( diff (f,t)) / ( diff (g,t))) by XCMPLX_0:def 9;

        then ((f . x) * ((g . x) " )) = (( diff (f,t)) * (( diff (g,t)) " )) by XCMPLX_0:def 9;

        then ((f / g) . x) = (( diff (f,t)) * (( diff (g,t)) " )) by A49, A37, RFUNCT_1:def 1;

        then ((f / g) . x) = (((f `| N) . t) * (( diff (g,t)) " )) by A3, A20, A48, FDIFF_1:def 7;

        then ((f / g) . x) = (((f `| N) . t) * (((g `| N) . t) " )) by A4, A20, A48, FDIFF_1:def 7;

        hence thesis by A43, A52, A48, RFUNCT_1:def 1;

      end;

      

       A55: 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 xx0 = x0 as Element of REAL by XREAL_0:def 1;

        set d = ( seq_const x0);

        let a;

        assume that

         A56: a is convergent and

         A57: ( lim a) = x0 and

         A58: ( rng a) c= (( dom (f / g)) /\ ( left_open_halfline x0));

        consider k such that

         A59: for n st k <= n holds (x0 - r) < (a . n) & (a . n) < (x0 + r) by A9, A56, A57, LIMFUNC3: 7;

        set a1 = (a ^\ k);

        defpred X[ Element of NAT , Real] means $2 in ].(a1 . $1), x0.[ & ((((f / g) /* a) ^\ k) . $1) = (((f `| N) / (g `| N)) . $2);

         A60:

        now

          let n;

          (a . (n + k)) in ( rng a) by VALUED_0: 28;

          then (a . (n + k)) in ( left_open_halfline x0) by A58, XBOOLE_0:def 4;

          then (a . (n + k)) in { g1 : 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, NAT_1:def 3;

          hence (x0 - r) < (a1 . n) by A59;

        end;

        

         A61: for n holds ex c be Element of REAL st X[n, c]

        proof

          let n;

          

           A62: ( rng a1) c= ( rng a) by VALUED_0: 21;

          (x0 - r) < (a1 . n) & (a1 . n) < x0 by A60;

          then

          consider c such that

           A63: c in ].(a1 . n), x0.[ and

           A64: ((f / g) . (a1 . n)) = (((f `| N) / (g `| N)) . c) by A11;

          take c;

          

           A65: (( dom (f / g)) /\ ( left_open_halfline x0)) c= ( dom (f / g)) by XBOOLE_1: 17;

          then ( rng a) c= ( dom (f / g)) by A58;

          then (((f / g) /* (a ^\ k)) . n) = (((f `| N) / (g `| N)) . c) by A64, A62, FUNCT_2: 108, XBOOLE_1: 1;

          hence thesis by A58, A63, A65, VALUED_0: 27, XBOOLE_1: 1;

        end;

        consider b such that

         A66: for n holds X[n, (b . n)] from FUNCT_2:sch 3( A61);

        

         A67: x0 < (x0 + r) by A9, XREAL_1: 29;

        (x0 - r) < x0 by A9, XREAL_1: 44;

        then x0 in { g2 : (x0 - r) < g2 & g2 < (x0 + r) } by A67;

        then

         A68: x0 in ].(x0 - r), (x0 + r).[ by RCOMP_1:def 2;

        

         A69: ( rng b) c= (( dom ((f `| N) / (g `| N))) /\ ( left_open_halfline x0))

        proof

          let x be object;

          assume x in ( rng b);

          then

          consider n such that

           A70: x = (b . n) by FUNCT_2: 113;

          (a1 . n) < x0 by A60;

          then

           A71: (a1 . n) < (x0 + r) by A67, XXREAL_0: 2;

          (x0 - r) < (a1 . n) by A60;

          then (a1 . n) in { g3 : (x0 - r) < g3 & g3 < (x0 + r) } by A71;

          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 A68, XXREAL_1: 25, XXREAL_2:def 12;

          then ].(a1 . n), x0.[ c= ].(x0 - r), (x0 + r).[;

          then

           A72: ].(a1 . n), x0.[ c= ( dom ((f `| N) / (g `| N))) by A6, A10;

          

           A73: x in ].(a1 . n), x0.[ by A66, A70;

          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 A73, A72, XBOOLE_0:def 4;

        end;

         A74:

        now

          let n be Nat;

          

           A75: n in NAT by ORDINAL1:def 12;

          (b . n) in ].(a1 . n), x0.[ by A66, A75;

          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 SEQ_1: 57;

        end;

        

         A76: ( lim d) = (d . 0 ) by SEQ_4: 26

        .= x0 by SEQ_1: 57;

        ( lim a1) = x0 by A56, A57, SEQ_4: 20;

        then

         A77: b is convergent & ( lim b) = x0 by A56, A76, A74, SEQ_2: 19, SEQ_2: 20;

        

         A78: (( dom ((f `| N) / (g `| N))) /\ ( left_open_halfline x0)) c= ( dom ((f `| N) / (g `| N))) by XBOOLE_1: 17;

        then

         A79: ( rng b) c= ( dom ((f `| N) / (g `| N))) by A69;

        then

         A80: (((f `| N) / (g `| N)) /* b) is convergent by A8, A77, FCONT_1:def 1;

         A81:

        now

          reconsider m = 0 as Nat;

          take m;

          let n be Nat such that m <= n;

          

           A82: n in NAT by ORDINAL1:def 12;

          ((((f / g) /* a) ^\ k) . n) = (((f `| N) / (g `| N)) . (b . n)) by A66, A82;

          hence ((((f / g) /* a) ^\ k) . n) = ((((f `| N) / (g `| N)) /* b) . n) by A69, A78, FUNCT_2: 108, XBOOLE_1: 1, A82;

        end;

        ( lim (((f `| N) / (g `| N)) /* b)) = (((f `| N) / (g `| N)) . x0) by A8, A77, A79, FCONT_1:def 1;

        

        then ( lim (((f `| N) / (g `| N)) /* b)) = (((f `| N) . x0) * (((g `| N) . x0) " )) by A6, A10, A68, RFUNCT_1:def 1

        .= (( diff (f,x0)) * (((g `| N) . x0) " )) by A3, A10, A68, FDIFF_1:def 7

        .= (( diff (f,x0)) * (( diff (g,x0)) " )) by A4, A10, A68, FDIFF_1:def 7;

        then ( lim (((f / g) /* a) ^\ k)) = (( diff (f,x0)) * (( diff (g,x0)) " )) by A80, A81, SEQ_4: 19;

        then

         A83: ( lim (((f / g) /* a) ^\ k)) = (( diff (f,x0)) / ( diff (g,x0))) by XCMPLX_0:def 9;

        (((f / g) /* a) ^\ k) is convergent by A80, A81, SEQ_4: 18;

        hence thesis by A83, SEQ_4: 21, SEQ_4: 22;

      end;

      

       A84: for r1, r2 st r1 < x0 & x0 < r2 holds 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 holds ex t st r1 < t & t < x0 & t in ( dom (f / g)) by LIMFUNC3: 8;

      then

       A85: (f / g) is_left_convergent_in x0 & ( lim_left ((f / g),x0)) = (( diff (f,x0)) / ( diff (g,x0))) by A55, Th3;

      

       A86: for x st x0 < x & x < (x0 + r) holds ex c st c in ].x0, x.[ & ((f / g) . x) = (((f `| N) / (g `| N)) . c)

      proof

        

         A87: (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 A87;

        then

         A88: x0 in ].(x0 - r), (x0 + r).[ by RCOMP_1:def 2;

        

         A89: (( dom (f `| N)) /\ (( dom (g `| N)) \ ((g `| N) " { 0 }))) c= (( dom (g `| N)) \ ((g `| N) " { 0 })) by XBOOLE_1: 17;

        

         A90: (( dom f) /\ (( dom g) \ (g " { 0 }))) c= (( dom g) \ (g " { 0 })) by XBOOLE_1: 17;

        let x such that

         A91: x0 < x and

         A92: x < (x0 + r);

        set f1 = (((f . x) (#) g) - ((g . x) (#) f));

        

         A93: ( dom ((f . x) (#) g)) = ( dom g) & ( dom ((g . x) (#) f)) = ( dom f) by VALUED_1:def 5;

        then

         A94: ( dom (((f . x) (#) g) - ((g . x) (#) f))) = (( dom f) /\ ( dom g)) by VALUED_1: 12;

        (x0 - r) < x by A91, A87, XXREAL_0: 2;

        then x in { g1 : (x0 - r) < g1 & g1 < (x0 + r) } by A92;

        then x in ].(x0 - r), (x0 + r).[ by RCOMP_1:def 2;

        then

         A95: [.x0, x.] c= N by A10, A88, XXREAL_2:def 12;

        then

         A96: [.x0, x.] c= ( dom f) & [.x0, x.] c= ( dom g) by A1, A2;

        then

         A97: [.x0, x.] c= ( dom f1) by A94, XBOOLE_1: 19;

        (g | N) is continuous by A4, FDIFF_1: 25;

        then (g | [.x0, x.]) is continuous by A95, FCONT_1: 16;

        then

         A98: (((f . x) (#) g) | [.x0, x.]) is continuous by A2, A95, FCONT_1: 20, XBOOLE_1: 1;

        (f | N) is continuous by A3, FDIFF_1: 25;

        then (f | [.x0, x.]) is continuous by A95, FCONT_1: 16;

        then

         A99: (((g . x) (#) f) | [.x0, x.]) is continuous by A1, A95, FCONT_1: 20, XBOOLE_1: 1;

         [.x0, x.] c= ( dom (((f . x) (#) g) - ((g . x) (#) f))) by A96, A94, XBOOLE_1: 19;

        then

         A100: ((((f . x) (#) g) - ((g . x) (#) f)) | [.x0, x.]) is continuous by A93, A94, A99, A98, FCONT_1: 18;

        

         A101: ].x0, x.[ c= [.x0, x.] by XXREAL_1: 25;

        then

         A102: ].x0, x.[ c= N by A95;

        

         A103: x in [.x0, x.] by A91, XXREAL_1: 1;

        then x in ( dom f1) by A97;

        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 A91, XXREAL_1: 1;

        then x0 in ( dom f1) by A97;

        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 A97, 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 A91, TARSKI:def 1;

        then

         A112: x in ( [.x0, x.] \ {x0}) by A103, XBOOLE_0:def 5;

        N c= ( dom ((f . x) (#) g)) by A2, VALUED_1:def 5;

        then

         A113: ].x0, x.[ c= ( dom ((f . x) (#) g)) by A102;

        N c= ( dom ((g . x) (#) f)) by A1, VALUED_1:def 5;

        then

         A114: ].x0, x.[ c= ( dom ((g . x) (#) f)) by A102;

        then ].x0, x.[ c= (( dom ((f . x) (#) g)) /\ ( dom ((g . x) (#) f))) by A113, XBOOLE_1: 19;

        then

         A115: ].x0, x.[ c= ( dom (((f . x) (#) g) - ((g . x) (#) f))) by VALUED_1: 12;

        f is_differentiable_on ].x0, x.[ by A3, A95, A101, FDIFF_1: 26, XBOOLE_1: 1;

        then

         A116: ((g . x) (#) f) is_differentiable_on ].x0, x.[ by A114, FDIFF_1: 20;

        g is_differentiable_on ].x0, x.[ by A4, A95, A101, FDIFF_1: 26, XBOOLE_1: 1;

        then

         A117: ((f . x) (#) g) is_differentiable_on ].x0, x.[ by A113, FDIFF_1: 20;

        (f1 . x0) = ((((f . x) (#) g) . x0) - (((g . x) (#) f) . x0)) by A97, 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

         A118: t in ].x0, x.[ and

         A119: ( diff (f1,t)) = 0 by A91, A100, A116, A115, A117, A97, A110, FDIFF_1: 19, ROLLE: 1;

        

         A120: ((g . x) (#) f) is_differentiable_in t by A116, A118, FDIFF_1: 9;

        

         A121: f is_differentiable_in t by A3, A102, A118, FDIFF_1: 9;

        ((f . x) (#) g) is_differentiable_in t by A117, A118, FDIFF_1: 9;

        then 0 = (( diff (((f . x) (#) g),t)) - ( diff (((g . x) (#) f),t))) by A119, A120, FDIFF_1: 14;

        then

         A122: 0 = (( diff (((f . x) (#) g),t)) - ((g . x) * ( diff (f,t)))) by A121, FDIFF_1: 15;

        take t;

        

         A123: t in [.x0, x.] by A101, A118;

        ( [.x0, x.] \ {x0}) c= (N \ {x0}) by A95, XBOOLE_1: 33;

        then

         A124: ( [.x0, x.] \ {x0}) c= ( dom (f / g)) by A5;

        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 A90;

        then

         A125: x in ( dom g) & not x in (g " { 0 }) by A112, XBOOLE_0:def 5;

         A126:

        now

          assume (g . x) = 0 ;

          then (g . x) in { 0 } by TARSKI:def 1;

          hence contradiction by A125, FUNCT_1:def 7;

        end;

        

         A127: [.x0, x.] c= ( dom ((f `| N) / (g `| N))) by A6, A95;

        then [.x0, x.] c= (( dom (f `| N)) /\ (( dom (g `| N)) \ ((g `| N) " { 0 }))) by RFUNCT_1:def 1;

        then [.x0, x.] c= (( dom (g `| N)) \ ((g `| N) " { 0 })) by A89;

        then

         A128: t in ( dom (g `| N)) & not t in ((g `| N) " { 0 }) by A123, XBOOLE_0:def 5;

         A129:

        now

          assume ( diff (g,t)) = 0 ;

          then ((g `| N) . t) = 0 by A4, A95, A123, FDIFF_1:def 7;

          then ((g `| N) . t) in { 0 } by TARSKI:def 1;

          hence contradiction by A128, FUNCT_1:def 7;

        end;

        g is_differentiable_in t by A4, A102, A118, FDIFF_1: 9;

        then 0 = (((f . x) * ( diff (g,t))) - ((g . x) * ( diff (f,t)))) by A122, FDIFF_1: 15;

        then ((f . x) / (g . x)) = (( diff (f,t)) / ( diff (g,t))) by A126, A129, XCMPLX_1: 94;

        then ((f . x) * ((g . x) " )) = (( diff (f,t)) / ( diff (g,t))) by XCMPLX_0:def 9;

        then ((f . x) * ((g . x) " )) = (( diff (f,t)) * (( diff (g,t)) " )) by XCMPLX_0:def 9;

        then ((f / g) . x) = (( diff (f,t)) * (( diff (g,t)) " )) by A124, A112, RFUNCT_1:def 1;

        then ((f / g) . x) = (((f `| N) . t) * (( diff (g,t)) " )) by A3, A95, A123, FDIFF_1:def 7;

        then ((f / g) . x) = (((f `| N) . t) * (((g `| N) . t) " )) by A4, A95, A123, FDIFF_1:def 7;

        hence thesis by A118, A127, A123, RFUNCT_1:def 1;

      end;

      

       A130: 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 xx0 = x0 as Element of REAL by XREAL_0:def 1;

        set d = ( seq_const x0);

        let a;

        assume that

         A131: a is convergent and

         A132: ( lim a) = x0 and

         A133: ( rng a) c= (( dom (f / g)) /\ ( right_open_halfline x0));

        consider k such that

         A134: for n st k <= n holds (x0 - r) < (a . n) & (a . n) < (x0 + r) by A9, A131, A132, LIMFUNC3: 7;

        set a1 = (a ^\ k);

        defpred X[ Element of NAT , Real] means $2 in ].x0, (a1 . $1).[ & ((((f / g) /* a) ^\ k) . $1) = (((f `| N) / (g `| N)) . $2);

         A135:

        now

          let n;

          (a . (n + k)) in ( rng a) by VALUED_0: 28;

          then (a . (n + k)) in ( right_open_halfline x0) by A133, XBOOLE_0:def 4;

          then (a . (n + k)) in { g1 : 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, NAT_1:def 3;

          hence (a1 . n) < (x0 + r) by A134;

        end;

        

         A136: for n holds ex c be Element of REAL st X[n, c]

        proof

          let n;

          

           A137: ( rng a1) c= ( rng a) by VALUED_0: 21;

          x0 < (a1 . n) & (a1 . n) < (x0 + r) by A135;

          then

          consider c such that

           A138: c in ].x0, (a1 . n).[ and

           A139: ((f / g) . (a1 . n)) = (((f `| N) / (g `| N)) . c) by A86;

          take c;

          

           A140: (( dom (f / g)) /\ ( right_open_halfline x0)) c= ( dom (f / g)) by XBOOLE_1: 17;

          then ( rng a) c= ( dom (f / g)) by A133;

          then (((f / g) /* (a ^\ k)) . n) = (((f `| N) / (g `| N)) . c) by A139, A137, FUNCT_2: 108, XBOOLE_1: 1;

          hence thesis by A133, A138, A140, VALUED_0: 27, XBOOLE_1: 1;

        end;

        consider b such that

         A141: for n holds X[n, (b . n)] from FUNCT_2:sch 3( A136);

        

         A142: (x0 - r) < x0 by A9, XREAL_1: 44;

        x0 < (x0 + r) by A9, XREAL_1: 29;

        then x0 in { g2 : (x0 - r) < g2 & g2 < (x0 + r) } by A142;

        then

         A143: x0 in ].(x0 - r), (x0 + r).[ by RCOMP_1:def 2;

        

         A144: ( rng b) c= (( dom ((f `| N) / (g `| N))) /\ ( right_open_halfline x0))

        proof

          let x be object;

          assume x in ( rng b);

          then

          consider n such that

           A145: x = (b . n) by FUNCT_2: 113;

          x0 < (a1 . n) by A135;

          then

           A146: (x0 - r) < (a1 . n) by A142, XXREAL_0: 2;

          (a1 . n) < (x0 + r) by A135;

          then (a1 . n) in { g3 : (x0 - r) < g3 & g3 < (x0 + r) } by A146;

          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 A143, XXREAL_1: 25, XXREAL_2:def 12;

          then ].x0, (a1 . n).[ c= ].(x0 - r), (x0 + r).[;

          then

           A147: ].x0, (a1 . n).[ c= ( dom ((f `| N) / (g `| N))) by A6, A10;

          

           A148: x in ].x0, (a1 . n).[ by A141, A145;

          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 A148, A147, XBOOLE_0:def 4;

        end;

         A149:

        now

          let n be Nat;

          

           A150: n in NAT by ORDINAL1:def 12;

          (b . n) in ].x0, (a1 . n).[ by A141, A150;

          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 SEQ_1: 57;

        end;

        

         A151: ( lim d) = (d . 0 ) by SEQ_4: 26

        .= x0 by SEQ_1: 57;

        ( lim a1) = x0 by A131, A132, SEQ_4: 20;

        then

         A152: b is convergent & ( lim b) = x0 by A131, A151, A149, SEQ_2: 19, SEQ_2: 20;

        

         A153: (( dom ((f `| N) / (g `| N))) /\ ( right_open_halfline x0)) c= ( dom ((f `| N) / (g `| N))) by XBOOLE_1: 17;

        then

         A154: ( rng b) c= ( dom ((f `| N) / (g `| N))) by A144;

        then

         A155: (((f `| N) / (g `| N)) /* b) is convergent by A8, A152, FCONT_1:def 1;

         A156:

        now

          reconsider m = 0 as Nat;

          take m;

          let n be Nat such that m <= n;

          

           A157: n in NAT by ORDINAL1:def 12;

          ((((f / g) /* a) ^\ k) . n) = (((f `| N) / (g `| N)) . (b . n)) by A141, A157;

          hence ((((f / g) /* a) ^\ k) . n) = ((((f `| N) / (g `| N)) /* b) . n) by A144, A153, FUNCT_2: 108, XBOOLE_1: 1, A157;

        end;

        ( lim (((f `| N) / (g `| N)) /* b)) = (((f `| N) / (g `| N)) . x0) by A8, A152, A154, FCONT_1:def 1;

        

        then ( lim (((f `| N) / (g `| N)) /* b)) = (((f `| N) . x0) * (((g `| N) . x0) " )) by A6, A10, A143, RFUNCT_1:def 1

        .= (( diff (f,x0)) * (((g `| N) . x0) " )) by A3, A10, A143, FDIFF_1:def 7

        .= (( diff (f,x0)) * (( diff (g,x0)) " )) by A4, A10, A143, FDIFF_1:def 7;

        then ( lim (((f / g) /* a) ^\ k)) = (( diff (f,x0)) * (( diff (g,x0)) " )) by A155, A156, SEQ_4: 19;

        then

         A158: ( lim (((f / g) /* a) ^\ k)) = (( diff (f,x0)) / ( diff (g,x0))) by XCMPLX_0:def 9;

        (((f / g) /* a) ^\ k) is convergent by A155, A156, SEQ_4: 18;

        hence thesis by A158, SEQ_4: 21, SEQ_4: 22;

      end;

      for r1 st x0 < r1 holds ex t st t < r1 & x0 < t & t in ( dom (f / g)) by A84, LIMFUNC3: 8;

      then (f / g) is_right_convergent_in x0 & ( lim_right ((f / g),x0)) = (( diff (f,x0)) / ( diff (g,x0))) by A130, Th2;

      hence thesis by A85, LIMFUNC3: 30;

    end;