FDIFF_3

:: Real Function One-Side Differantiability
::  by Ewa Burakowska and Beata Madras
::
:: Received December 12, 1991
:: Copyright (c) 1991-2026 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, FDIFF_1, SEQ_1, FUNCT_1, PARTFUN1, REAL_1, SUBSET_1,
      XXREAL_0, CARD_1, XXREAL_1, ARYTM_1, TARSKI, RELAT_1, ARYTM_3, VALUED_0,
      SEQ_2, ORDINAL2, VALUED_1, FUNCT_2, NAT_1, LIMFUNC1, XBOOLE_0, COMPLEX1,
      SQUARE_1, ORDINAL4, RCOMP_1, FDIFF_3, ASYMPT_1;
 notations TARSKI, ORDINAL1, SUBSET_1, NUMBERS, XXREAL_0, XREAL_0, XCMPLX_0,
      COMPLEX1, REAL_1, SQUARE_1, NAT_1, RELSET_1, PARTFUN1, FUNCT_1, FUNCT_2,
      FUNCOP_1, VALUED_0, VALUED_1, SEQ_1, COMSEQ_2, SEQ_2, RFUNCT_1, RCOMP_1,
      FDIFF_1, LIMFUNC1, RECDEF_1;
 constructors FUNCOP_1, REAL_1, SQUARE_1, NAT_1, COMPLEX1, SEQ_2, SEQM_3,
      PROB_1, RCOMP_1, RFUNCT_1, RFUNCT_2, LIMFUNC1, PARTFUN1, FDIFF_1,
      VALUED_1, RECDEF_1, XXREAL_2, SETFAM_1, RELSET_1, BINOP_2, RVSUM_1,
      COMSEQ_2, SEQ_1;
 registrations ORDINAL1, RELSET_1, NUMBERS, XREAL_0, MEMBERED, FDIFF_1,
      VALUED_0, VALUED_1, FUNCT_2, XXREAL_2, SEQ_4, SQUARE_1, NAT_1, SEQ_1,
      SEQ_2;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
 definitions TARSKI, XBOOLE_0;
 equalities XBOOLE_0, SQUARE_1, PROB_1, LIMFUNC1, VALUED_1;
 expansions TARSKI;
 theorems NAT_1, SEQ_1, SEQ_2, SEQM_3, SEQ_4, ABSVALUE, RFUNCT_1, RFUNCT_2,
      RCOMP_1, FDIFF_1, LIMFUNC2, FDIFF_2, TARSKI, SCHEME1, ZFMISC_1, FCONT_3,
      FUNCT_1, FUNCT_2, XBOOLE_0, XBOOLE_1, XCMPLX_0, XCMPLX_1, XREAL_1,
      COMPLEX1, XXREAL_0, VALUED_1, XXREAL_1, XXREAL_2, VALUED_0, ORDINAL1,
      XREAL_0;
 schemes SEQ_1, SCHEME1, FUNCT_2, FDIFF_2;

begin

reserve h,h1,h2 for 0-convergent non-zero Real_Sequence,
  c,c1 for constant Real_Sequence,
  f,f1,f2 for PartFunc of REAL,REAL,
  x0,r,r0,r1,r2,g,g1,g2 for Real,
  n0,k,n,m for Element of NAT,
  a,b,d for Real_Sequence,
  x for set;

theorem Th1:
  (ex r st r>0 & [.x0-r,x0.] c= dom f) implies ex h,c st rng c ={x0
  } & rng (h+c) c= dom f & for n being Nat holds h.n < 0
proof
  given r such that
A1: r>0 and
A2: [.x0-r,x0.] c= dom f;
  reconsider xx0 = x0 as Element of REAL by XREAL_0:def 1;
  set a = seq_const x0;
  reconsider a as constant Real_Sequence;
  deffunc F(Nat) = (-r)/($1+2);
  consider b such that
A3: for n being Nat holds b.n = F(n) from SEQ_1:sch 1;
A4: now
    let n be Nat;
    0 < r/(n+2) by A1,XREAL_1:139;
    then -(r/(n+2)) < -0 by XREAL_1:24;
    then (-r)/(n+2) < 0 by XCMPLX_1:187;
    hence b.n < 0 by A3;
  end;
  then for n being Nat holds 0 <> b.n;
  then
A5: b is non-zero by SEQ_1:5;
  b is convergent & lim b = 0 by A3,SEQ_4:31;
  then reconsider b as 0-convergent non-zero Real_Sequence
    by A5,FDIFF_1:def 1;
  take b;
  take a;
  thus rng a = {x0}
  proof
    thus rng a c= {x0}
    proof
      let x be object;
      assume x in rng a;
      then ex n st x = a.n by FUNCT_2:113;
      then x = x0 by SEQ_1:57;
      hence thesis by TARSKI:def 1;
    end;
    let x be object;
    assume x in {x0};
    then x = x0 by TARSKI:def 1
      .= a.0 by SEQ_1:57;
    hence thesis by VALUED_0:28;
  end;
  thus rng (b+a) c= dom f
  proof
    let x be object;
    assume x in rng (b+a);
    then consider n such that
A6: x = (b+a).n by FUNCT_2:113;
 0+1 < n + 2 by XREAL_1:8;
    then r*1 < r*(n+2) by A1,XREAL_1:97;
    then r * (n+2)" < r*(n + 2)*((n + 2)") by XREAL_1:68;
    then r * ((n+2)") < r*((n + 2)*(n + 2)");
    then r * (n+2)" < r * 1 by XCMPLX_0:def 7;
    then r/(n+2) < r by XCMPLX_0:def 9;
    then x0 - r < x0 - r/(n+2) by XREAL_1:15;
    then x0 - r < x0 + - r/(n+2);
    then
A7: x0 - r <= x0 + (-r)/(n+2) by XCMPLX_1:187;
    0 < r/(n+2) by A1,XREAL_1:139;
    then x0 - r/(n+2) < x0 - 0 by XREAL_1:15;
    then x0 + - r/(n+2) <= x0;
    then x0 + (-r)/(n+2) <= x0 by XCMPLX_1:187;
    then
A8: x0 + (-r)/(n+2) in {g1: x0 - r <= g1 & g1 <= x0 } by A7;
    x = b.n +a.n by A6,SEQ_1:7
      .= (-r)/(n+2) + a.n by A3
      .= x0 + (-r)/(n+2) by SEQ_1:57;
    then x in [.x0 - r, x0.] by A8,RCOMP_1:def 1;
    hence thesis by A2;
  end;
  thus thesis by A4;
end;

theorem Th2:
  (ex r st r>0 & [.x0,x0+r.] c= dom f) implies ex h,c st rng c ={x0
  } & rng (h+c) c= dom f & for n being Nat holds h.n > 0
proof
  given r such that
A1: r>0 and
A2: [.x0,x0+r.] c= dom f;
  reconsider xx0 = x0 as Element of REAL by XREAL_0:def 1;
  set a = seq_const x0;
  reconsider a as constant Real_Sequence;
  deffunc F(Nat) = r/($1+2);
  consider b such that
A3: for n being Nat holds b.n = F(n) from SEQ_1:sch 1;
A4: now
    let n be Nat;
    0 < r/(n+2) by A1,XREAL_1:139;
    hence 0 < b.n by A3;
  end;
  then for n being Nat holds 0<>b.n;
  then
A5: b is non-zero by SEQ_1:5;
  b is convergent & lim b = 0 by A3,SEQ_4:31;
  then reconsider b as 0-convergent non-zero Real_Sequence
    by A5,FDIFF_1:def 1;
  take b,a;
  thus rng a = {x0}
  proof
    thus rng a c= {x0}
    proof
      let x be object;
      assume x in rng a;
      then ex n st x = a.n by FUNCT_2:113;
      then x = x0 by SEQ_1:57;
      hence thesis by TARSKI:def 1;
    end;
    let x be object;
    assume x in {x0};
    then x = x0 by TARSKI:def 1
      .= a.0 by SEQ_1:57;
    hence thesis by VALUED_0:28;
  end;
  thus rng (b+a) c= dom f
  proof
    let x be object;
    assume x in rng (b+a);
    then consider n such that
A6: x = (b+a).n by FUNCT_2:113;
 0+1 < n + 2 by XREAL_1:8;
    then r*1 < r*(n+2) by A1,XREAL_1:97;
    then r * (n+2)" < r*(n + 2)*((n + 2)") by XREAL_1:68;
    then r * (n+2)" < r*((n + 2)*(n + 2)");
    then r * (n+2)" < r * 1 by XCMPLX_0:def 7;
    then r/(n+2) < r by XCMPLX_0:def 9;
    then
A7: x0 + r/(n+2) <= x0 + r by XREAL_1:6;
    0 < r/(n+2) by A1,XREAL_1:139;
    then x0 + 0 < x0 + r/(n+2) by XREAL_1:8;
    then
A8: x0 + r/(n+2) in {g1: x0 <= g1 & g1 <= x0 + r} by A7;
    x = b.n +a.n by A6,SEQ_1:7
      .= r/(n+2) + a.n by A3
      .= r/(n+2) + x0 by SEQ_1:57;
    then x in [.x0,x0 + r.] by A8,RCOMP_1:def 1;
    hence thesis by A2;
  end;
  thus thesis by A4;
end;

theorem Th3:
  (for h,c st rng c ={x0} & rng (h+c) c= dom f & (for n being Nat holds h.n <
0) holds h"(#)(f/*(h+c) - f/*c) is convergent) & {x0} c= dom f implies for h1,
h2,c st rng c ={x0} & rng (h1+c) c= dom f &
 (for n being Nat holds h1.n < 0) & rng (h2+c)
 c= dom f & (for n being Nat holds h2.n < 0)
holds lim (h1"(#)(f/*(h1+c) - f/*c)) = lim (
  h2"(#)(f/*(h2+c) - f/*c))
proof
  assume that
A1: for h,c st rng c ={x0} & rng (h+c) c= dom f &
   (for n being Nat holds h.n < 0)
  holds h"(#)(f/*(h+c) - f/*c) is convergent and
A2: {x0} c= dom f;
  let h1,h2,c such that
A3: rng c ={x0} and
A4: rng (h1+c) c= dom f and
A5: for n being Nat holds h1.n < 0 and
A6: rng (h2+c) c= dom f and
A7: for n being Nat holds h2.n < 0;
  deffunc G(Element of NAT) = h2.$1;
  deffunc F(Element of NAT) = h1.$1;
  consider d such that
A8: for n holds d.(2*n) = F(n) & d.(2*n + 1) = G(n) from SCHEME1:sch 2;
  now
    let n be Nat;
    consider m such that
A9: n = 2*m or n = 2*m + 1 by SCHEME1:1;
    now
      per cases by A9;
      suppose
A10:    n = 2*m;
        d.(2*m) = h1.m by A8;
        hence d.n <> 0 by A10,SEQ_1:5;
      end;
      suppose
A11:    n = 2*m + 1;
        d.(2*m + 1) = h2.m by A8;
        hence d.n <> 0 by A11,SEQ_1:5;
      end;
    end;
    hence d.n <> 0;
  end;
  then
A12: d is non-zero by SEQ_1:5;
A13: h2 is convergent & lim h2 = 0;
  h1 is convergent & lim h1 = 0;
  then d is convergent & lim d = 0 by A8,A13,FDIFF_2:1;
  then reconsider d as 0-convergent non-zero Real_Sequence
    by A12,FDIFF_1:def 1;
  deffunc F(Nat) = 2*$1;
  consider a such that
A14: for n being Nat holds a.n = F(n) from SEQ_1:sch 1;
  deffunc G(Nat) = 2*$1+1;
  consider b such that
A15: for n being Nat holds b.n = G(n) from SEQ_1:sch 1;
  for n holds b.n = G(n) by A15;
  then reconsider b as increasing sequence of NAT by FDIFF_2:3;
A16: rng (d + c) c= dom f
  proof
    let x be object;
    assume x in rng (d + c);
    then consider n such that
A17: x = (d + c).n by FUNCT_2:113;
    consider m such that
A18: n = 2*m or n = 2*m + 1 by SCHEME1:1;
A19: x = d.n + c.n by A17,SEQ_1:7;
    now
      per cases by A18;
      suppose
        n = 2*m;
        then x = h1.m + c.(2*m) by A8,A19
          .= h1.m + c.m by VALUED_0:23
          .= (h1 + c).m by SEQ_1:7;
        then x in rng (h1 + c) by VALUED_0:28;
        hence thesis by A4;
      end;
      suppose
        n = 2*m + 1;
        then x = h2.m + c.(2*m +1) by A8,A19
          .= h2.m + c.m by VALUED_0:23
          .= (h2 + c).m by SEQ_1:7;
        then x in rng (h2 + c) by VALUED_0:28;
        hence thesis by A6;
      end;
    end;
    hence thesis;
  end;
  now
    let n;
    thus ((d"(#)(f/*(d+c) - f/*c))*b).n=(d"(#)(f/*(d+c) - f/*c)).(b.n) by
FUNCT_2:15
      .= (d"(#)(f/*(d+c) - f/*c)).(2*n + 1) by A15
      .= (d").(2*n + 1)*(f/*(d+c) - f/*c).(2*n + 1) by SEQ_1:8
      .= (d").(2*n +1)*((f/*(d+c)).(2*n + 1) - (f/*c).(2*n + 1)) by RFUNCT_2:1
      .= (d.( 2*n + 1))"*((f/*(d+c)).(2*n + 1) - (f/*c).(2*n + 1)) by
VALUED_1:10
      .= (h2.n)"*((f/*(d+c)).(2*n + 1) - (f/*c).(2*n + 1)) by A8
      .= (h2").n*((f/*(d+c)).(2*n + 1) - (f/*c).(2*n + 1)) by VALUED_1:10
      .= (h2").n*(f.((d + c).(2*n + 1)) - (f/*c).(2*n + 1)) by A16,FUNCT_2:108
      .= (h2").n*(f.(d.(2*n + 1) + c.(2*n + 1)) - (f/*c).(2*n + 1)) by SEQ_1:7
      .= (h2").n*(f.(h2.n + c.(2*n + 1)) - (f/*c).(2*n + 1)) by A8
      .= (h2").n*(f.(h2.n + c.n) - (f/*c).(2*n + 1)) by VALUED_0:23
      .= (h2").n*(f.((h2 + c).n) - (f/*c).(2*n + 1)) by SEQ_1:7
      .= (h2").n*((f/*(h2+c)).n - (f/*c).(2*n + 1)) by A6,FUNCT_2:108
      .= (h2").n*((f/*(h2+c)).n - f.(c.(2*n + 1))) by A2,A3,FUNCT_2:108
      .= (h2").n*((f/*(h2+c)).n - f.(c.n)) by VALUED_0:23
      .= (h2").n*((f/*(h2+c)).n - (f/*c).n) by A2,A3,FUNCT_2:108
      .= (h2").n*(f/*(h2+c) - f/*c).n by RFUNCT_2:1
      .= (h2"(#)(f/*(h2+c) - f/*c)).n by SEQ_1:8;
  end;
  then
A20: h2"(#)(f/*(h2+c) - f/*c) is subsequence of d"(#)(f/*(d+c) - f/*c) by
FUNCT_2:63;
  now
    let n be Nat;
    consider m such that
A21: n = 2*m or n = 2*m + 1 by SCHEME1:1;
    now
      per cases by A21;
      suppose
A22:    n = 2*m;
        d.(2*m) = h1.m by A8;
        hence d.n < 0 by A5,A22;
      end;
      suppose
A23:    n = 2*m + 1;
        d.(2*m + 1) = h2.m by A8;
        hence d.n < 0 by A7,A23;
      end;
    end;
    hence d.n < 0;
  end;
  then
A24: d"(#)(f/*(d+c) - f/*c) is convergent by A1,A3,A16;
  for n holds a.n = F(n) by A14;
  then reconsider a as increasing sequence of NAT by FDIFF_2:2;
  now
    let n;
    thus ((d"(#)(f/*(d+c) - f/*c))*a).n = (d"(#)(f/*(d+c) - f/*c)).(a.n ) by
FUNCT_2:15
      .= (d"(#)(f/*(d+c) - f/*c)).(2*n) by A14
      .= (d").(2*n)*(f/*(d+c) - f/*c).(2*n) by SEQ_1:8
      .= (d").(2*n)*((f/*(d+c)).(2*n) - (f/*c).(2*n)) by RFUNCT_2:1
      .= (d.(2*n))"*((f/*(d+c)).(2*n) - (f/*c).(2*n)) by VALUED_1:10
      .= (h1.n)"*((f/*(d+c)).(2*n) - (f/*c).(2*n)) by A8
      .= (h1").n*((f/*(d+c)).(2*n) - (f/*c).(2*n)) by VALUED_1:10
      .= (h1").n*(f.((d + c).(2*n)) - (f/*c).(2*n)) by A16,FUNCT_2:108
      .= (h1").n*(f.(d.(2*n) + c.(2*n)) - (f/*c).(2*n)) by SEQ_1:7
      .= (h1").n*(f.(h1.n + c.(2*n)) - (f/*c).(2*n)) by A8
      .= (h1").n*(f.(h1.n + c.n) - (f/*c).(2*n)) by VALUED_0:23
      .= (h1").n*(f.((h1 + c).n) - (f/*c).(2*n)) by SEQ_1:7
      .= (h1").n*((f/*(h1+c)).n - (f/*c).(2*n)) by A4,FUNCT_2:108
      .= (h1").n*((f/*(h1+c)).n - f.(c.(2*n))) by A2,A3,FUNCT_2:108
      .= (h1").n*((f/*(h1+c)).n - f.(c.n)) by VALUED_0:23
      .= (h1").n*((f/*(h1+c)).n - (f/*c).n) by A2,A3,FUNCT_2:108
      .= (h1").n*(f/*(h1+c) - f/*c).n by RFUNCT_2:1
      .= (h1"(#)(f/*(h1+c) - f/*c)).n by SEQ_1:8;
  end;
  then h1"(#)(f/*(h1+c) - f/*c) is subsequence of d"(#)(f/*(d+c) - f/*c) by
FUNCT_2:63;
  then lim (h1"(#)(f/*(h1+c) - f/*c)) = lim (d"(#) (f/*(d+c) - f/*c)) by A24,
SEQ_4:17;
  hence thesis by A24,A20,SEQ_4:17;
end;

theorem Th4:
  (for h,c st rng c ={x0} & rng (h+c) c= dom f & (for n being Nat holds h.n>0
) holds h"(#)(f/*(h+c) - f/*c) is convergent) & {x0} c= dom f implies for h1,h2
,c st rng c ={x0} & rng (h1 + c)c= dom f & rng (h2 + c) c= dom f &
 (for n being Nat holds
h1.n >0) & (for n being Nat holds h2.n >0)
 holds lim (h1"(#)(f/*(h1+c) - f/*c)) = lim (h2
  "(#)(f/*(h2+c) - f/*c))
proof
  assume that
A1: for h,c st rng c ={x0} & rng (h+c) c= dom f & (for n being Nat holds h.n>0)
  holds h"(#)(f/*(h+c) - f/*c) is convergent and
A2: {x0} c= dom f;
  let h1,h2,c such that
A3: rng c ={x0} and
A4: rng (h1 + c) c= dom f and
A5: rng (h2 + c) c= dom f and
A6: for n being Nat holds h1.n >0 and
A7: for n being Nat holds h2.n >0;
  deffunc G(Element of NAT) = h2.$1;
  deffunc F(Element of NAT) = h1.$1;
  consider d such that
A8: for n holds d.(2*n)=F(n) & d.(2*n+1)=G(n) from SCHEME1:sch 2;
  now
    let n be Nat;
    consider m such that
A9: n = 2*m or n = 2*m+1 by SCHEME1:1;
    now
      per cases by A9;
      suppose
        n = 2*m;
        then d.n = h1.m by A8;
        hence d.n<>0 by SEQ_1:5;
      end;
      suppose
        n = 2*m+1;
        then d.n = h2.m by A8;
        hence d.n<>0 by SEQ_1:5;
      end;
    end;
    hence d.n<>0;
  end;
  then
A10: d is non-zero by SEQ_1:5;
A11: h2 is convergent & lim h2 =0;
  h1 is convergent & lim h1 =0;
  then d is convergent & lim d =0 by A8,A11,FDIFF_2:1;
  then reconsider d as 0-convergent non-zero Real_Sequence
    by A10,FDIFF_1:def 1;
  deffunc F(Nat) = 2*$1;
  consider a such that
A12: for n being Nat holds a.n = F(n) from SEQ_1:sch 1;
  deffunc G(Nat) = 2*$1+1;
  consider b such that
A13: for n being Nat holds b.n = G(n) from SEQ_1:sch 1;
   for n holds b.n = G(n) by A13;
  then reconsider b as increasing sequence of NAT by FDIFF_2:3;
A14: rng (d+c) c= dom f
  proof
    let x be object;
    assume x in rng (d+c);
    then consider n such that
A15: x = (d+c).n by FUNCT_2:113;
    consider m such that
A16: n=2*m or n=2*m+1 by SCHEME1:1;
    now
      per cases by A16;
      suppose
        n = 2*m;
        then x = d.(2*m) + c.(2*m) by A15,SEQ_1:7
          .= h1.m + c.(2*m) by A8
          .= h1.m + c.m by VALUED_0:23
          .= (h1+c).m by SEQ_1:7;
        then x in rng(h1+c) by VALUED_0:28;
        hence thesis by A4;
      end;
      suppose
        n = 2*m+1;
        then x = d.(2*m+1) + c.(2*m+1) by A15,SEQ_1:7
          .= h2.m + c.(2*m+1) by A8
          .= h2.m + c.m by VALUED_0:23
          .= (h2 + c).m by SEQ_1:7;
        then x in rng(h2+c) by VALUED_0:28;
        hence thesis by A5;
      end;
    end;
    hence thesis;
  end;
  now
    let n;
    thus ((d"(#)(f/*(d+c) - f/*c))*b).n = (d"(#) (f/*(d+c) - f/*c)).(b.n) by
FUNCT_2:15
      .= (d"(#)(f/*(d+c) - f/*c)).(2*n+1) by A13
      .= (d").(2*n+1) * (f/*(d+c) - f/*c).(2*n+1) by SEQ_1:8
      .= (d.(2*n+1))" * (f/*(d+c) - f/*c).(2*n+1) by VALUED_1:10
      .= (h2.n)" * (f/*(d+c) - f/*c).(2*n+1) by A8
      .= (h2").n * (f/*(d+c) - f/*c).(2*n+1) by VALUED_1:10
      .= (h2").n *((f/*(d+c)).(2*n+1) - (f/*c).(2*n+1)) by RFUNCT_2:1
      .= (h2").n *(f.((d+c).(2*n+1)) - (f/*c).(2*n+1)) by A14,FUNCT_2:108
      .= (h2").n *(f.((d+c).(2*n+1)) - f.(c.(2*n+1))) by A2,A3,FUNCT_2:108
      .= (h2").n *(f.(d.(2*n+1)+c.(2*n+1)) - f.(c.(2*n+1))) by SEQ_1:7
      .= (h2").n *(f.(h2.n+c.(2*n+1)) - f.(c.(2*n+1))) by A8
      .= (h2").n *(f.(h2.n+c.(2*n+1)) - f.(c.n)) by VALUED_0:23
      .= (h2").n *(f.(h2.n+c.n) - f.(c.n)) by VALUED_0:23
      .= (h2").n *(f.((h2+c).n) - f.(c.n)) by SEQ_1:7
      .= (h2").n *((f/*(h2+c)).n - f.(c.n)) by A5,FUNCT_2:108
      .= (h2").n *((f/*(h2+c)).n - (f/*c).n) by A2,A3,FUNCT_2:108
      .= (h2").n *(f/*(h2+c) - f/*c).n by RFUNCT_2:1
      .= (h2"(#)(f/*(h2+c) - f/*c)).n by SEQ_1:8;
  end;
  then
A17: h2"(#)(f/*(h2+c) - f/*c) is subsequence of d"(#)(f/*(d+c) - f/*c) by
FUNCT_2:63;
  for n being Nat holds d.n > 0
  proof
    let n be Nat;
    consider m such that
A18: n = 2*m or n = 2*m+1 by SCHEME1:1;
    now
      per cases by A18;
      suppose
        n = 2*m;
        then d.n = h1.m by A8;
        hence thesis by A6;
      end;
      suppose
        n = 2*m+1;
        then d.n = h2.m by A8;
        hence thesis by A7;
      end;
    end;
    hence thesis;
  end;
  then
A19: d"(#)(f/*(d+c) - f/*c) is convergent by A1,A3,A14;
  for n holds a.n = F(n) by A12;
  then reconsider a as increasing sequence of NAT by FDIFF_2:2;
  now
    let n;
    thus ((d"(#)(f/*(d+c) - f/*c))*a).n = (d"(#) (f/*(d+c) - f/*c)).(a.n) by
FUNCT_2:15
      .= (d"(#)(f/*(d+c) - f/*c)).(2*n) by A12
      .= (d").(2*n) * (f/*(d+c) - f/*c).(2*n) by SEQ_1:8
      .= (d.(2*n))" * (f/*(d+c) - f/*c).(2*n) by VALUED_1:10
      .= (h1.n)" * (f/*(d+c) - f/*c).(2*n) by A8
      .= (h1").n * (f/*(d+c) - f/*c).(2*n) by VALUED_1:10
      .= (h1").n *((f/*(d+c)).(2*n) - (f/*c).(2*n)) by RFUNCT_2:1
      .= (h1").n *(f.((d+c).(2*n)) - (f/*c).(2*n)) by A14,FUNCT_2:108
      .= (h1").n *(f.((d+c).(2*n)) - f.(c.(2*n))) by A2,A3,FUNCT_2:108
      .= (h1").n *(f.(d.(2*n)+c.(2*n)) - f.(c.(2*n))) by SEQ_1:7
      .= (h1").n *(f.(h1.n+c.(2*n)) - f.(c.(2*n))) by A8
      .= (h1").n *(f.(h1.n+c.(2*n)) - f.(c.n)) by VALUED_0:23
      .= (h1").n *(f.(h1.n+c.n) - f.(c.n)) by VALUED_0:23
      .= (h1").n *(f.((h1+c).n) - f.(c.n)) by SEQ_1:7
      .= (h1").n *((f/*(h1+c)).n - f.(c.n)) by A4,FUNCT_2:108
      .= (h1").n *((f/*(h1+c)).n - (f/*c).n) by A2,A3,FUNCT_2:108
      .= (h1").n *(f/*(h1+c) - f/*c).n by RFUNCT_2:1
      .= (h1"(#)(f/*(h1+c) - f/*c)).n by SEQ_1:8;
  end;
  then h1"(#)(f/*(h1+c) - f/*c) is subsequence of d"(#)(f/*(d+c) - f/*c) by
FUNCT_2:63;
  then lim (h1"(#)(f/*(h1+c) - f/*c)) = lim (d"(#) (f/*(d+c) -f/*c)) by A19,
SEQ_4:17;
  hence thesis by A19,A17,SEQ_4:17;
end;

definition
  let f,x0;
  pred f is_Lcontinuous_in x0 means

  x0 in dom f & for a st rng a c=
  left_open_halfline(x0) /\ dom f & a is convergent & lim a = x0 holds f/*a is
  convergent & f.x0 = lim(f/*a);
  pred f is_Rcontinuous_in x0 means

  x0 in dom f & for a st rng a c=
  right_open_halfline(x0) /\ dom f & a is convergent & lim a = x0 holds f/*a is
  convergent & f.x0 = lim(f/*a);
  pred f is_right_differentiable_in x0 means

  (ex r st r>0 & [.x0, x0+r
.] c= dom f) & for h,c st rng c ={x0} & rng (h+c) c= dom f &
  (for n being Nat holds h.n >
  0) holds h"(#)(f/*(h+c) - f/*c) is convergent;
  pred f is_left_differentiable_in x0 means

  (ex r st r>0 & [.x0-r,x0.]
  c= dom f) & for h,c st rng c ={x0} & rng (h+c) c= dom f &
   (for n being Nat holds h.n<0)
  holds h"(#)(f/*(h+c) - f/*c) is convergent;
end;

theorem Th5:
  f is_left_differentiable_in x0 implies f is_Lcontinuous_in x0
proof
  assume
A1: f is_left_differentiable_in x0;
A2: for a st rng a c= left_open_halfline(x0) /\ dom f & a is convergent &
  lim a = x0 holds f/*a is convergent & f.x0 = lim(f/*a)
  proof
  reconsider xx0 = x0 as Element of REAL by XREAL_0:def 1;
    set b = seq_const x0;
    let a such that
A3: rng a c= left_open_halfline(x0) /\ dom f and
A4: a is convergent and
A5: lim a = x0;
    consider r such that
A6: 0 < r and
A7: [.x0 - r, x0.] c= dom f by A1;
    consider n0 being Nat such that
A8: for k being Nat st k>=n0 holds x0 - r<a.k
        by A4,A5,A6,LIMFUNC2:1,XREAL_1:44;
    deffunc F(Nat) = a.$1-b.$1;
    consider d such that
A9: for n being Nat holds d.n = F(n) from SEQ_1:sch 1;
A10: d = a - b by A9,RFUNCT_2:1;
    then
A11: d is convergent by A4;
    reconsider c = b^\n0 as constant Real_Sequence;
A12: rng c = {x0}
    proof
      thus rng c c= {x0}
      proof
        let x be object;
        assume x in rng c;
        then consider n such that
A13:    x = (b^\n0).n by FUNCT_2:113;
        x = b.(n + n0) by A13,NAT_1:def 3;
        then x = x0 by SEQ_1:57;
        hence thesis by TARSKI:def 1;
      end;
      let x be object;
      assume x in {x0};
      then
A14:  x = x0 by TARSKI:def 1;
      c.0 = b.(0 + n0) by NAT_1:def 3
        .= x by A14,SEQ_1:57;
      hence thesis by VALUED_0:28;
    end;
A15: now
      let g be Real such that
A16:  0<g;
       reconsider n=0 as Nat;
      take n;
      let m be Nat such that
      n<=m;
A17:   m in NAT by ORDINAL1:def 12;
      x0 - r <= x0 by A6,XREAL_1:44;
      then x0 in [.x0 - r,x0.] by XXREAL_1:1;
      then rng c c= dom f by A7,A12,ZFMISC_1:31;
      then |.(f/*c).m-f.x0.| = |.f.(c.m)-f.x0.| by FUNCT_2:108,A17
        .= |.f.(b.(m+n0))-f.x0.| by NAT_1:def 3
        .= |.f.x0-f.x0.| by SEQ_1:57
        .= 0 by ABSVALUE:2;
      hence |.(f/*c).m-f.x0.|<g by A16;
    end;
    then
A18: f/*c is convergent by SEQ_2:def 6;
    lim b = b.0 by SEQ_4:26
      .= x0 by SEQ_1:57;
    then lim d = x0 - x0 by A4,A5,A10,SEQ_2:12
      .= 0;
    then
A19: lim (d^\n0) = 0 by A11,SEQ_4:20;
A20: for n holds d.n < 0 & d.n <> 0
    proof
      let n;
A21:  d.n = a.n - b.n by A9;
      a.n in rng a by VALUED_0:28;
      then a.n in left_open_halfline(x0) by A3,XBOOLE_0:def 4;
      then a.n in { r1: r1 < x0 } by XXREAL_1:229;
      then
A22:  ex r1 st r1 = a.n & r1 < x0;
      then a.n - x0 < x0 - x0 by XREAL_1:9;
      hence d.n < 0 by A21,SEQ_1:57;
      thus thesis by A21,A22,SEQ_1:57;
    end;
A23: for n being Nat holds (d^\n0).n < 0
    proof
      let n be Nat;
A24:    n+n0 in NAT by ORDINAL1:def 12;
      (d^\n0).n = d.(n + n0) by NAT_1:def 3;
      hence thesis by A20,A24;
    end;
    for n being Nat holds (d^\n0).n <>0
     by A23;
    then d ^\n0 is non-zero by SEQ_1:5;
    then reconsider h = d^\n0 as 0-convergent non-zero Real_Sequence
      by A11,A19,FDIFF_1:def 1;
A25: rng a c= dom f
    by A3,XBOOLE_0:def 4;
    now
      let n;
      thus (f/*(h+c)-f/*c+f/*c).n=(f/*(h+c)-f/*c).n+(f/*c).n by SEQ_1:7
        .= (f/*(h+c)).n-(f/*c).n+(f/*c).n by RFUNCT_2:1
        .= (f/*(h+c)).n;
    end;
    then
A26: f/*(h+c)-f/*c+(f/*c)=f/*(h+c) by FUNCT_2:63;
    now
      let n;
      thus (h+c).n=((a-b+b)^\n0).n by A10,SEQM_3:15
        .= (a-b+b).(n+n0) by NAT_1:def 3
        .= (a-b).(n+n0)+b.(n+n0) by SEQ_1:7
        .= a.(n+n0)-b.(n+n0)+b.(n+n0) by RFUNCT_2:1
        .= (a^\n0).n by NAT_1:def 3;
    end;
    then
A27: f/*(h+c)-f/*c+(f/*c)=f/*(a^\n0) by A26,FUNCT_2:63
      .= (f/*a)^\n0 by A25,VALUED_0:27;
A28: for n holds (a^\n0).n in [.x0 - r,x0.]
    proof
      let n;
      a.(n + n0) in rng a by VALUED_0:28;
      then (a^\n0).n in rng a by NAT_1:def 3;
      then (a^\n0).n in left_open_halfline(x0) by A3,XBOOLE_0:def 4;
      then (a^\n0).n in {g:g < x0} by XXREAL_1:229;
      then
A29:  ex g st g = (a^\n0).n & g < x0;
      0 <= n & 0 + n0 = n0;
      then n0 <= n0 + n by XREAL_1:6;
      then x0 - r <= a.(n + n0) by A8;
      then x0 - r <= (a^\n0).n by NAT_1:def 3;
      then (a^\n0).n in {g: x0 - r <= g & g <= x0} by A29;
      hence thesis by RCOMP_1:def 1;
    end;
    rng (h + c) c= [.x0 - r,x0.]
    proof
      let x be object;
      assume x in rng(h + c);
      then consider n such that
A30:  x = (h+c).n by FUNCT_2:113;
      (h+c).n=((a - b +b)^\n0).n by A10,SEQM_3:15
        .= (a - b + b) .(n + n0) by NAT_1:def 3
        .= (a - b).(n + n0) + b.(n + n0) by SEQ_1:7
        .= a.(n + n0) - b.(n + n0) + b.(n + n0) by RFUNCT_2:1
        .= (a^\n0).n by NAT_1:def 3;
      hence thesis by A28,A30;
    end;
    then rng (h + c) c= dom f by A7;
    then
A31: h"(#)(f/*(h+c) - f/*c) is convergent by A1,A23,A12;
    then
A32: lim (h(#)(h"(#)(f/*(h+c) - f/*c)))=0*lim(h"(#) (f/*(h+c) - f/*c)) by A19,
SEQ_2:15
      .=0;
    now
      let n;
A33:  h.n<>0 by A23;
      thus (h(#)(h"(#)(f/*(h+c) - f/*c))).n=h.n *(h"(#) (f/*(h+c) - f/*c)).n
      by SEQ_1:8
        .= h.n*((h").n*(f/*(h+c) - f/*c).n) by SEQ_1:8
        .= h.n*(((h.n)")*(f/*(h+c) - f/*c).n) by VALUED_1:10
        .= h.n*((h.n)")*(f/*(h+c) - f/*c).n
        .= 1*(f/*(h+c) - f/*c).n by A33,XCMPLX_0:def 7
        .= (f/*(h+c) - f/*c).n;
    end;
    then
A34: h(#)(h"(#)(f/*(h+c) - f/*c))=f/*(h+c)-f/*c by FUNCT_2:63;
    then
A35: f/*(h+c)-f/*c is convergent by A31;
    then
A36: f/*(h+c)-f/*c+f/*c is convergent by A18;
    hence f/*a is convergent by A27,SEQ_4:21;
    lim(f/*c)=f.x0 by A15,A18,SEQ_2:def 7;
    then lim(f/*(h+c)-f/*c+f/*c) = 0+f.x0 by A32,A34,A35,A18,SEQ_2:6
      .= f.x0;
    hence thesis by A36,A27,SEQ_4:22;
  end;
  x0 in dom f
  proof
    consider r such that
A37: 0 < r and
A38: [.x0 - r,x0.] c= dom f by A1;
    x0 - r <= x0 by A37,XREAL_1:44;
    then x0 in [.x0 - r,x0.] by XXREAL_1:1;
    hence thesis by A38;
  end;
  hence thesis by A2;
end;

theorem Th6:
  f is_Lcontinuous_in x0 & f.x0<>g2 & (ex r st r>0 & [.x0-r,x0.] c=
dom f) implies ex r1 st r1 > 0 & [.x0-r1,x0.] c= dom f & for g st g in [.x0-r1,
  x0.] holds f.g <> g2
proof
  assume that
A1: f is_Lcontinuous_in x0 and
A2: f.x0 <> g2;
  given r such that
A3: r>0 and
A4: [.x0-r,x0.] c= dom f;
  defpred P[Element of NAT,set] means $2 in [.x0-r/($1+1),x0.] & $2 in dom f &
  f.$2 = g2;
  assume
A5: for r1 st r1>0 & [.x0-r1,x0.] c= dom f ex g st g in [.x0-r1,x0.] & f
  .g = g2;
A6: for n ex g be Element of REAL st P[n,g]
  proof
    let n;
    x0 - r <= x0 by A3,XREAL_1:44;
    then
A7: x0 in [.x0 - r,x0.] by XXREAL_1:1;
    0 + 1 <= n + 1 by XREAL_1:7;
    then r/(n+1) <= r/1 by A3,XREAL_1:118;
    then
A8: x0 - r <= x0 - r/(n+1) by XREAL_1:13;
    x0 - r/(n+1) <= x0 by A3,XREAL_1:44,139;
    then x0 - r/(n+1) in {g1: x0 - r <= g1 & g1 <= x0} by A8;
    then x0 - r/(n+1) in [.x0 - r, x0.] by RCOMP_1:def 1;
    then [.x0 - r/(n+1),x0.] c= [.x0 - r,x0.] by A7,XXREAL_2:def 12;
    then
A9: [.x0 - r/(n+1),x0.] c= dom f by A4;
    then consider g such that
A10: g in [.x0-r/(n+1),x0.] & f.g = g2 by A3,A5,XREAL_1:139;
    take g;
    thus thesis by A9,A10;
  end;
  consider a such that
A11: for n holds P[n,a.n] from FUNCT_2:sch 3(A6);
A12: rng a c= left_open_halfline(x0) /\ dom f
  proof
    let x be object;
    assume x in rng a;
    then consider n such that
A13: x=a.n by FUNCT_2:113;
    a.n in [.x0-r/(n+1),x0.] by A11;
    then a.n in {g1: x0 - r/(n+1) <= g1 & g1 <= x0} by RCOMP_1:def 1;
    then
A14: ex g1 st g1 = a.n & x0 - r/(n+1) <= g1 & g1 <=x0;
    a.n <> x0 by A2,A11;
    then a.n < x0 by A14,XXREAL_0:1;
    then a.n in {g1: g1 < x0};
    then
A15: a.n in left_open_halfline(x0) by XXREAL_1:229;
    a.n in dom f by A11;
    hence thesis by A13,A15,XBOOLE_0:def 4;
  end;
A16: left_open_halfline(x0) /\ dom f c= dom f by XBOOLE_1:17;
A17: for n holds (f/*a).n = g2
  proof
    let n;
    thus (f/*a).n = f.(a.n) by A12,A16,FUNCT_2:108,XBOOLE_1:1
      .= g2 by A11;
  end;
  now
    let n be Nat;
    n in NAT by ORDINAL1:def 12;
    then (f/*a).n = g2 by A17;
    hence (f/*a).n =(f/*a).(n+1) by A17;
  end;
  then
A18: lim (f/*a) = (f/*a).0 by SEQ_4:26,VALUED_0:25
    .= g2 by A17;
  reconsider xx0 = x0 as Element of REAL by XREAL_0:def 1;
  set d = seq_const x0;
  deffunc F(Nat) = x0 - r/($1+1);
  consider b such that
A19: for n being Nat holds b.n = F(n) from SEQ_1:sch 1;
A20: now
    let n be Nat;
A21:  n in NAT by ORDINAL1:def 12;
    a.n in [.x0 - r/(n+1), x0.] by A11,A21;
    then a.n in {g1: x0 - r/(n+1) <= g1 & g1 <= x0} by RCOMP_1:def 1;
    then ex g1 st g1 = a.n & x0 - r/(n+1) <= g1 & g1 <=x0;
    hence b.n <= a.n & a.n <= d.n by A19,SEQ_1:57;
  end;
A22: lim d = d.0 by SEQ_4:26
    .= x0 by SEQ_1:57;
  b is convergent & lim b = x0 by A19,FCONT_3:5;
  then a is convergent & lim a = x0 by A22,A20,SEQ_2:19,20;
  hence contradiction by A1,A2,A12,A18;
end;

theorem Th7:
  f is_right_differentiable_in x0 implies f is_Rcontinuous_in x0
proof
  assume
A1: f is_right_differentiable_in x0;
  then consider r such that
A2: r>0 and
A3: [.x0,x0 + r.] c= dom f;
A4: for a st rng a c= right_open_halfline(x0) /\ dom f & a is convergent &
  lim a = x0 holds f/*a is convergent & f.x0 = lim(f/*a)
  proof
  reconsider xx0 = x0 as Element of REAL by XREAL_0:def 1;
    set b = seq_const x0;
    let a such that
A5: rng a c= right_open_halfline(x0) /\ dom f and
A6: a is convergent and
A7: lim a = x0;
    consider r such that
A8: r > 0 and
A9: [.x0, x0 + r.] c= dom f by A1;
    x0 + 0 < x0 + r by A8,XREAL_1:6;
    then consider n0 be Nat such that
A10: for k being Nat st k>=n0 holds a.k < x0 +r by A6,A7,LIMFUNC2:2;
    deffunc F(Nat) = a.$1-b.$1;
    consider d such that
A11: for n being Nat holds d.n = F(n) from SEQ_1:sch 1;
A12: d = a - b by A11,RFUNCT_2:1;
    then
A13: d is convergent by A6;
    reconsider c = b^\n0 as constant Real_Sequence;
A14: rng c = {x0}
    proof
      thus rng c c= {x0}
      proof
        let x be object;
        assume x in rng c;
        then consider n such that
A15:    x = (b^\n0).n by FUNCT_2:113;
        x = b.(n + n0) by A15,NAT_1:def 3;
        then x = x0 by SEQ_1:57;
        hence thesis by TARSKI:def 1;
      end;
      let x be object;
      assume x in {x0};
      then
A16:  x = x0 by TARSKI:def 1;
      c.0 = b.(0 + n0) by NAT_1:def 3
        .= x by A16,SEQ_1:57;
      hence thesis by VALUED_0:28;
    end;
A17: now
      let g be Real such that
A18:  0<g;
       reconsider n=0 as Nat;
      take n;
      let m be Nat such that
      n<=m;
A19:   m in NAT by ORDINAL1:def 12;
      x0 + 0 <= x0 +r by A8,XREAL_1:7;
      then x0 in [.x0, x0 + r.] by XXREAL_1:1;
      then rng c c= dom f by A9,A14,ZFMISC_1:31;
      then |.(f/*c).m-f.x0.| = |.f.(c.m)-f.x0.| by FUNCT_2:108,A19
        .= |.f.(b.(m+n0))-f.x0.| by NAT_1:def 3
        .= |.f.x0-f.x0.| by SEQ_1:57
        .= 0 by ABSVALUE:2;
      hence |.(f/*c).m-f.x0.|<g by A18;
    end;
    then
A20: f/*c is convergent by SEQ_2:def 6;
    lim b = b.0 by SEQ_4:26
      .= x0 by SEQ_1:57;
    then lim d = x0 - x0 by A6,A7,A12,SEQ_2:12
      .= 0;
    then
A21: lim (d^\n0) = 0 by A13,SEQ_4:20;
A22: for n holds d.n > 0 & d.n <> 0
    proof
      let n;
A23:  d.n = a.n - b.n by A11;
      a.n in rng a by VALUED_0:28;
      then a.n in right_open_halfline(x0) by A5,XBOOLE_0:def 4;
      then a.n in { r1: x0 < r1 } by XXREAL_1:230;
      then
A24:  ex r1 st r1 = a.n & x0 < r1;
      then a.n - x0 > x0 - x0 by XREAL_1:9;
      hence d.n > 0 by A23,SEQ_1:57;
      thus thesis by A23,A24,SEQ_1:57;
    end;
A25: for n being Nat holds (d^\n0).n > 0
    proof
      let n be Nat;
A26:    n+n0 in NAT by ORDINAL1:def 12;
      (d^\n0).n = d.(n + n0) by NAT_1:def 3;
      hence thesis by A22,A26;
    end;
    for n being Nat holds (d^\n0).n <>0
     by A25;
    then d ^\n0 is non-zero by SEQ_1:5;
    then reconsider h = d^\n0 as 0-convergent non-zero Real_Sequence
       by A13,A21,FDIFF_1:def 1;
A27: rng a c= dom f
    by A5,XBOOLE_0:def 4;
    now
      let n;
      thus (f/*(h+c)-f/*c+f/*c).n=(f/*(h+c)-f/*c).n+(f/*c).n by SEQ_1:7
        .= (f/*(h+c)).n-(f/*c).n+(f/*c).n by RFUNCT_2:1
        .= (f/*(h+c)).n;
    end;
    then
A28: f/*(h+c)-f/*c+(f/*c)=f/*(h+c) by FUNCT_2:63;
    now
      let n;
      thus (h+c).n=((a-b+b)^\n0).n by A12,SEQM_3:15
        .= (a-b+b).(n+n0) by NAT_1:def 3
        .= (a-b).(n+n0)+b.(n+n0) by SEQ_1:7
        .= a.(n+n0)-b.(n+n0)+b.(n+n0) by RFUNCT_2:1
        .= (a^\n0).n by NAT_1:def 3;
    end;
    then
A29: f/*(h+c)-f/*c+(f/*c)=f/*(a^\n0) by A28,FUNCT_2:63
      .= (f/*a)^\n0 by A27,VALUED_0:27;
A30: for n holds (a^\n0).n in [.x0, x0 + r.]
    proof
      let n;
      a.(n + n0) in rng a by VALUED_0:28;
      then (a^\n0).n in rng a by NAT_1:def 3;
      then (a^\n0).n in right_open_halfline(x0) by A5,XBOOLE_0:def 4;
      then (a^\n0).n in {g:x0 < g} by XXREAL_1:230;
      then
A31:  ex g st g = (a^\n0).n & x0 < g;
      0 <= n & 0 + n0 = n0;
      then n0 <= n0 + n by XREAL_1:6;
      then a.(n + n0) <= x0 +r by A10;
      then (a^\n0).n <= x0 + r by NAT_1:def 3;
      then (a^\n0).n in {g: x0 <= g & g <= x0 + r} by A31;
      hence thesis by RCOMP_1:def 1;
    end;
    rng (h + c) c= [.x0,x0 + r.]
    proof
      let x be object;
      assume x in rng(h + c);
      then consider n such that
A32:  x = (h+c).n by FUNCT_2:113;
      (h+c).n=((a - b +b)^\n0).n by A12,SEQM_3:15
        .= (a - b + b) .(n + n0) by NAT_1:def 3
        .= (a - b).(n + n0) + b.(n + n0) by SEQ_1:7
        .= a.(n + n0) - b.(n + n0) + b.(n + n0) by RFUNCT_2:1
        .= (a^\n0).n by NAT_1:def 3;
      hence thesis by A30,A32;
    end;
    then rng (h + c) c= dom f by A9;
    then
A33: h"(#)(f/*(h+c) - f/*c) is convergent by A1,A25,A14;
    then
A34: lim (h(#)(h"(#)(f/*(h+c) - f/*c)))=0*lim(h"(#) (f/*(h+c) - f/*c)) by A21,
SEQ_2:15
      .=0;
    now
      let n;
A35:  h.n<>0 by A25;
      thus (h(#)(h"(#)(f/*(h+c) - f/*c))).n=h.n *(h"(#) (f/*(h+c) - f/*c)).n
      by SEQ_1:8
        .= h.n*((h").n*(f/*(h+c) - f/*c).n) by SEQ_1:8
        .= h.n*(((h.n)")*(f/*(h+c) - f/*c).n) by VALUED_1:10
        .= h.n*((h.n)")*(f/*(h+c) - f/*c).n
        .= 1*(f/*(h+c) - f/*c).n by A35,XCMPLX_0:def 7
        .= (f/*(h+c) - f/*c).n;
    end;
    then
A36: h(#)(h"(#)(f/*(h+c) - f/*c))=f/*(h+c)-f/*c by FUNCT_2:63;
    then
A37: f/*(h+c)-f/*c is convergent by A33;
    then
A38: f/*(h+c)-f/*c+f/*c is convergent by A20;
    hence f/*a is convergent by A29,SEQ_4:21;
    lim(f/*c)=f.x0 by A17,A20,SEQ_2:def 7;
    then lim(f/*(h+c)-f/*c+f/*c) = 0+f.x0 by A34,A36,A37,A20,SEQ_2:6
      .= f.x0;
    hence thesis by A38,A29,SEQ_4:22;
  end;
  x0 + 0 <= x0 +r by A2,XREAL_1:7;
  then x0 in [.x0, x0 + r.] by XXREAL_1:1;
  hence thesis by A3,A4;
end;

theorem Th8:
  f is_Rcontinuous_in x0 & f.x0 <> g2 & (ex r st r>0 & [.x0, x0+r.]
c= dom f) implies ex r1 st r1>0 & [.x0, x0+r1.] c= dom f & for g st g in [.x0,
  x0+r1.] holds f.g <> g2
proof
  assume that
A1: f is_Rcontinuous_in x0 and
A2: f.x0 <> g2;
  given r such that
A3: r>0 and
A4: [.x0, x0+r.] c= dom f;
  defpred P[Element of NAT,set] means $2 in [.x0, x0+r/($1+1).] & $2 in dom f
  & f.$2 = g2;
  assume
A5: for r1 st r1>0 & [.x0, x0+r1.] c= dom f ex g st g in [.x0, x0+r1.] &
  f.g = g2;
A6: for n ex g be Element of REAL st P[n,g]
  proof
    let n;
    x0 + 0 <= x0 +r by A3,XREAL_1:7;
    then
A7: x0 in [.x0, x0 + r.] by XXREAL_1:1;
    0 + 1 <= n + 1 by XREAL_1:7;
    then r/(n+1) <= r/1 by A3,XREAL_1:118;
    then
A8: x0 + r/(n+1) <= x0 + r by XREAL_1:7;
    x0 + 0 =x0;
    then x0 <= x0 + r/(n+1) by A3,XREAL_1:7;
    then x0 + r/(n+1) in {g1:x0 <= g1 & g1 <= x0+r} by A8;
    then x0 +r/(n+1) in [.x0,x0+r.] by RCOMP_1:def 1;
    then [.x0,x0+r/(n+1).] c= [.x0,x0+r.] by A7,XXREAL_2:def 12;
    then
A9: [.x0,x0+r/(n+1).] c= dom f by A4;
    then consider g such that
A10: g in [.x0,x0+r/(n+1).] & f.g = g2 by A3,A5,XREAL_1:139;
    take g;
    thus thesis by A9,A10;
  end;
  consider a such that
A11: for n holds P[n,a.n] from FUNCT_2:sch 3(A6);
A12: rng a c= right_open_halfline(x0) /\ dom f
  proof
    let x be object;
    assume x in rng a;
    then consider n such that
A13: x = a.n by FUNCT_2:113;
    a.n in [.x0, x0 + r/(n+1).] by A11;
    then a.n in{g1: x0<=g1 & g1<=x0+ r/(n+1)} by RCOMP_1:def 1;
    then
A14: ex g1 st g1=a.n & x0<=g1 & g1<=x0+ r/(n+1);
    x0 <> a.n by A2,A11;
    then x0 < a.n by A14,XXREAL_0:1;
    then a.n in {g1:x0 <g1};
    then
A15: a.n in right_open_halfline(x0)by XXREAL_1:230;
    a.n in dom f by A11;
    hence thesis by A13,A15,XBOOLE_0:def 4;
  end;
A16: right_open_halfline(x0) /\ dom f c= dom f by XBOOLE_1:17;
A17: for n holds (f/*a).n = g2
  proof
    let n;
    thus g2 =f.(a.n) by A11
      .=(f/*a).n by A12,A16,FUNCT_2:108,XBOOLE_1:1;
  end;
  now
    let n be Nat;
    n in NAT by ORDINAL1:def 12;
    then (f/*a).n=g2 by A17;
    hence (f/*a).n=(f/*a).(n+1) by A17;
  end;
  then
A18: lim (f/*a) = (f/*a).0 by SEQ_4:26,VALUED_0:25
    .= g2 by A17;
  deffunc F(Nat) = x0+r/($1+1);
  reconsider xx0 = x0 as Element of REAL by XREAL_0:def 1;
  set b = seq_const x0;
A19: lim b = b.0 by SEQ_4:26
    .=x0 by SEQ_1:57;
  consider d such that
A20: for n being Nat holds d.n = F(n) from SEQ_1:sch 1;
A21: now
    let n be Nat;
A22: n in NAT by ORDINAL1:def 12;
    a.n in [.x0, x0 + r/(n+1).] by A11,A22;
    then a.n in{g1: x0<=g1 & g1<=x0+ r/(n+1)} by RCOMP_1:def 1;
    then ex g1 st g1=a.n & x0<=g1 & g1<=x0+ r/(n+1);
    hence b.n <=a.n & a.n <= d.n by A20,SEQ_1:57;
  end;
  d is convergent & lim d = x0 by A20,FCONT_3:6;
  then a is convergent & lim a = x0 by A19,A21,SEQ_2:19,20;
  hence contradiction by A1,A2,A12,A18;
end;

definition
  let x0,f;
  assume
A1: f is_left_differentiable_in x0;
  func Ldiff (f,x0) -> Real means
  : Def5:
  for h,c st rng c = {x0} & rng (h + c) c= dom f &
  (for n being Nat holds h.n <0) holds it =lim (h"(#)(f/*(h+c) - f/*c));
  existence
  proof
A2: {x0} c= dom f
    proof
      let x be object;
      assume x in {x0};
      then
A3:   x = x0 by TARSKI:def 1;
      consider r such that
A4:   r > 0 and
A5:   [.x0 - r,x0.] c= dom f by A1;
      x0 - r <= x0 by A4,XREAL_1:44;
      then x0 in [.x0 - r,x0.] by XXREAL_1:1;
      hence thesis by A3,A5;
    end;
A6: for h,c st rng c = {x0} & rng (h + c) c= dom f &
    (for n being Nat holds h.n <0)
    holds h"(#)(f/*(h+c) - f/*c) is convergent by A1;
    ex r st r > 0 & [.x0 - r, x0.] c= dom f by A1;
    then consider h1,c1 such that
A7: rng c1 = {x0} and
A8: rng (h1 + c1) c= dom f & for n being Nat holds h1.n < 0 by Th1;
    take lim (h1"(#)(f/*(h1+c1) - f/*c1));
    let h,c such that
A9: rng c = {x0} and
A10: rng (h + c) c= dom f & for n being Nat holds h.n <0;
    c1 = c by A7,A9,FDIFF_2:5;
    hence thesis by A7,A8,A2,A10,A6,Th3;
  end;
  uniqueness
  proof
    ex r st r > 0 & [.x0 - r, x0.] c= dom f by A1;
    then consider h,c such that
A11: rng c = {x0} & rng (h + c) c= dom f &
   for n being Nat holds h.n < 0 by Th1;
    let g1,g2 being Real such that
A12: for h,c st rng c = {x0} & rng (h + c) c= dom f &
   (for n being Nat holds h.n
    <0) holds g1=lim (h"(#)(f/*(h+c) - f/*c)) and
A13: for h,c st rng c = {x0} & rng (h + c) c= dom f &
   (for n being Nat holds h.n
    < 0) holds g2=lim (h"(#)(f/*(h+c) - f/*c));
    g1 = lim (h"(#)(f/*(h+c) - f/*c)) by A12,A11;
    hence thesis by A13,A11;
  end;
end;

definition
  let x0,f;
  assume
A1: f is_right_differentiable_in x0;
  func Rdiff(f,x0) -> Real means
  :Def6:
  for h,c st rng c = {x0} & rng (h+c) c=
  dom f & (for n being Nat holds h.n > 0)
  holds it=lim (h"(#)(f/*(h+c) - f/*c));
  existence
  proof
A2: {x0} c= dom f
    proof
      let x be object;
      assume x in {x0};
      then
A3:   x = x0 by TARSKI:def 1;
      consider r such that
A4:   r>0 and
A5:   [.x0,x0+r.] c= dom f by A1;
      x0 + 0 <= x0 + r by A4,XREAL_1:7;
      then x0 in [.x0,x0+r.] by XXREAL_1:1;
      hence thesis by A3,A5;
    end;
A6: for h,c st rng c = {x0} & rng (h+c) c= dom f &
   (for n being Nat holds h.n>0)
    holds h"(#)(f/*(h+c) - f/*c) is convergent by A1;
    ex r st r>0 & [.x0,x0+r.] c=dom f by A1;
    then consider h,c such that
A7: rng c = {x0} and
A8: rng (h+c) c= dom f & for n being Nat holds h.n>0 by Th2;
    take lim(h"(#)(f/*(h+c) - f/*c));
    let h1,c1 such that
A9: rng c1 ={x0} and
A10: rng(h1 + c1) c=dom f & for n being Nat holds h1.n>0;
    c1 = c by A7,A9,FDIFF_2:5;
    hence thesis by A7,A8,A10,A6,A2,Th4;
  end;
  uniqueness
  proof
    ex r st r>0 & [.x0,x0 + r.] c=dom f by A1;
    then consider h,c such that
A11: rng c ={x0} & rng (h+c) c= dom f &
   for n being Nat holds h.n >0 by Th2;
    let g1,g2 being Real such that
A12: for h,c st rng c ={x0} & rng (h+c) c= dom f &
(for n being Nat holds h.n >
    0) holds g1=lim (h"(#)(f/*(h+c) - f/*c)) and
A13: for h,c st rng c ={x0} & rng (h+c) c= dom f &
(for n being Nat holds h.n >
    0) holds g2=lim (h"(#)(f/*(h+c) - f/*c));
    g1 = lim (h"(#)(f/*(h+c) - f/*c)) by A12,A11;
    hence thesis by A13,A11;
  end;
end;

theorem Th9:
 for g being Real holds
  f is_left_differentiable_in x0 & Ldiff(f,x0) = g iff (ex r st 0 <
  r & [.x0 -r,x0.] c= dom f) & for h,c st rng c = {x0} & rng (h+c) c= dom f &
  (for n being Nat holds h.n < 0)
 holds h"(#)(f/*(h+c) - f/*c) is convergent & lim(h"(#)(f/*(h+c) - f/*c)) = g
proof let g be Real;
  thus f is_left_differentiable_in x0 & Ldiff(f,x0) = g implies (ex r st 0 < r
& [.x0 -r,x0.] c= dom f) & for h,c st rng c = {x0} & rng (h+c) c= dom f &
   (for n being Nat holds h.n < 0)
  holds h"(#)(f/*(h+c) - f/*c) is convergent & lim(h"(#)(f/*(h+c
  ) - f/*c)) = g by Def5;
  thus (ex r st 0 <r & [.x0 -r,x0.] c= dom f) & (for h,c st rng c = {x0} & rng
  (h+c) c= dom f & (for n being Nat holds h.n < 0)
   holds h"(#)(f/*(h+c) - f/*c) is
  convergent & lim(h"(#)(f/*(h+c) - f/*c)) = g) implies f
  is_left_differentiable_in x0 & Ldiff(f,x0) = g
  proof
    assume that
A1: ex r st 0 < r & [.x0 -r,x0.] c= dom f and
A2: for h,c st rng c = {x0} & rng (h+c) c= dom f &
  (for n being Nat holds h.n <
0) holds h"(#)(f/*(h+c) - f/*c) is convergent & lim(h"(#) (f/*(h+c) - f/*c)) =
    g;
    for h,c holds rng c = {x0} & rng (h+c) c= dom f &
     (for n being Nat holds h.n < 0
    ) implies h"(#)(f/*(h+c) - f/*c) is convergent by A2;
    hence
A3: f is_left_differentiable_in x0 by A1;
    for h,c holds rng c = {x0} & rng (h+c) c= dom f &
    (for n being Nat holds h.n < 0
    ) implies lim(h"(#)(f/*(h+c) - f/*c)) = g by A2;
    hence thesis by A3,Def5;
  end;
end;

theorem
  f1 is_left_differentiable_in x0 & f2 is_left_differentiable_in x0
implies f1 + f2 is_left_differentiable_in x0 & Ldiff(f1+f2,x0) = Ldiff(f1,x0) +
  Ldiff(f2,x0)
proof
  assume that
A1: f1 is_left_differentiable_in x0 and
A2: f2 is_left_differentiable_in x0;
  consider r2 such that
A3: 0 < r2 and
A4: [.x0 -r2,x0.] c= dom f2 by A2;
  consider r1 such that
A5: 0 < r1 and
A6: [.x0 -r1,x0.] c= dom f1 by A1;
  set r = min(r1,r2);
A7: 0 < r by A5,A3,XXREAL_0:15;
  then
A8: x0 - r <= x0 by XREAL_1:43;
  r <= r2 by XXREAL_0:17;
  then
A9: x0 - r2 <= x0 - r by XREAL_1:13;
  then x0 - r2 <= x0 by A8,XXREAL_0:2;
  then
A10: x0 in [.x0 - r2,x0.] by XXREAL_1:1;
  x0 - r in { g: x0 - r2 <= g & g <= x0 } by A8,A9;
  then x0 - r in [.x0 - r2,x0.] by RCOMP_1:def 1;
  then [.x0 - r,x0.] c= [.x0 - r2,x0.] by A10,XXREAL_2:def 12;
  then
A11: [.x0 - r,x0.] c= dom f2 by A4;
  r <= r1 by XXREAL_0:17;
  then
A12: x0 - r1 <= x0 - r by XREAL_1:13;
  then x0 - r1 <= x0 by A8,XXREAL_0:2;
  then
A13: x0 in [.x0 - r1,x0.] by XXREAL_1:1;
  x0 - r in { g: x0 - r1 <= g & g <= x0 } by A8,A12;
  then x0 - r in [.x0 - r1,x0.] by RCOMP_1:def 1;
  then [.x0 - r,x0.] c= [.x0 - r1,x0.] by A13,XXREAL_2:def 12;
  then [.x0 - r,x0.] c= dom f1 by A6;
  then
A14: [.x0 - r,x0.] c= dom f1 /\ dom f2 by A11,XBOOLE_1:19;
A15: for h,c st rng c = {x0} & rng (h+c) c= dom (f1 + f2) &
  (for n being Nat holds h.n
< 0) holds h"(#)((f1+f2)/*(h+c) - (f1+f2)/*c) is convergent & lim(h"(#)((f1+f2)
  /*(h+c) - (f1+f2)/*c)) = Ldiff(f1,x0) + Ldiff(f2,x0)
  proof
    let h,c;
    assume that
A16: rng c = {x0} and
A17: rng (h+c) c= dom (f1 + f2) and
A18: for n being Nat holds h.n < 0;
A19: rng (h + c) c= dom f1 /\ dom f2 by A17,VALUED_1:def 1;
A20: now
      let n;
A21:  rng c c= dom f1 /\ dom f2
      proof
        let x be object;
        assume x in rng c;
        then
A22:    x = x0 by A16,TARSKI:def 1;
        x0 in [.x0 - r,x0.] by A8,XXREAL_1:1;
        hence thesis by A14,A22;
      end;
      thus (f1/*(h+c) - f1/*c + (f2/*(h+c) - f2/*c)).n =(f1/*(h+c) + (-(f1/*c)
      )).n + (f2/*(h+c) - f2/*c).n by SEQ_1:7
        .=(f1/*(h+c)).n + (-(f1/*c)).n + (f2/*(h+c) + (-(f2/*c))).n by SEQ_1:7
        .=(f1/*(h+c)).n + (-(f1/*c)).n + ((f2/*(h+c)).n + (-(f2/*c)).n) by
SEQ_1:7
        .=(f1/*(h+c)).n + (f2/*(h+c)).n+ ((-(f1/*c)).n +(-(f2/*c)).n)
        .=(f1/*(h+c)).n + (f2/*(h+c)).n + (-(f1/*c).n + (-(f2/*c)).n) by
SEQ_1:10
        .=(f1/*(h+c)).n + (f2/*(h+c)).n + (-(f1/*c).n + -(f2/*c).n) by SEQ_1:10
        .=(f1/*(h+c)).n + (f2/*(h+c)).n - ((f1/*c).n + (f2/*c).n)
        .=(f1/*(h+c) + f2/*(h+c)).n - ((f1/*c).n + (f2/*c).n) by SEQ_1:7
        .=(f1/*(h+c) + f2/*(h+c)).n - ((f1/*c + f2/*c).n) by SEQ_1:7
        .=(f1/*(h+c) + f2/*(h+c) - (f1/*c + f2/*c)).n by RFUNCT_2:1
        .=((f1+f2)/*(h+c) - (f1/*c + f2/*c)).n by A19,RFUNCT_2:8
        .=((f1+f2)/*(h+c) - (f1+f2)/*c).n by A21,RFUNCT_2:8;
    end;
    then
A23: f1/*(h+c) - f1/*c + (f2/*(h+c) - f2/*c) = (f1+f2)/*(h+c) - (f1+f2)/*c
    by FUNCT_2:63;
    dom f1 /\ dom f2 c=dom f2 by XBOOLE_1:17;
    then
A24: rng (h + c) c= dom f2 by A19;
    then
A25: lim(h"(#)(f2/*(h+c) - f2/*c)) = Ldiff(f2,x0) by A2,A16,A18,Th9;
A26: h"(#)(f2/*(h+c) - f2/*c) is convergent by A2,A16,A18,A24;
    dom f1 /\ dom f2 c= dom f1 by XBOOLE_1:17;
    then
A27: rng (h + c) c= dom f1 by A19;
A28: (h"(#)(f1/*(h+c) - f1/*c) + h"(#)(f2/*(h+c) - f2/*c)) = h"(#)(f1/*(h+
    c) - f1/*c + (f2/*(h+c) - f2/*c)) by SEQ_1:16;
A29: h"(#)(f1/*(h+c) - f1/*c) is convergent by A1,A16,A18,A27;
    then (h"(#)(f1/*(h+c) - f1/*c) + h"(#) (f2/*(h+c) - f2/*c)) is convergent
    by A26;
    hence h"(#)((f1+f2)/*(h+c) - (f1+f2)/*c) is convergent by A28,A20,
FUNCT_2:63;
    lim(h"(#)(f1/*(h+c) - f1/*c)) = Ldiff(f1,x0) by A1,A16,A18,A27,Th9;
    hence thesis by A29,A26,A25,A28,A23,SEQ_2:6;
  end;
  [.x0 - r,x0.] c= dom (f1 + f2) by A14,VALUED_1:def 1;
  hence thesis by A7,A15,Th9;
end;

theorem
  f1 is_left_differentiable_in x0 & f2 is_left_differentiable_in x0
implies f1 - f2 is_left_differentiable_in x0 & Ldiff(f1-f2,x0) = Ldiff(f1,x0) -
  Ldiff(f2,x0)
proof
  assume that
A1: f1 is_left_differentiable_in x0 and
A2: f2 is_left_differentiable_in x0;
  consider r2 such that
A3: 0 < r2 and
A4: [.x0 -r2,x0.] c= dom f2 by A2;
  consider r1 such that
A5: 0 < r1 and
A6: [.x0 -r1,x0.] c= dom f1 by A1;
  set r = min(r1,r2);
A7: 0 < r by A5,A3,XXREAL_0:15;
  then
A8: x0 - r <= x0 by XREAL_1:43;
  r <= r2 by XXREAL_0:17;
  then
A9: x0 - r2 <= x0 - r by XREAL_1:13;
  then x0 - r2 <= x0 by A8,XXREAL_0:2;
  then
A10: x0 in [.x0 - r2,x0.] by XXREAL_1:1;
  x0 - r in { g: x0 - r2 <= g & g <= x0 } by A8,A9;
  then x0 - r in [.x0 - r2,x0.] by RCOMP_1:def 1;
  then [.x0 - r,x0.] c= [.x0 - r2,x0.] by A10,XXREAL_2:def 12;
  then
A11: [.x0 - r,x0.] c= dom f2 by A4;
  r <= r1 by XXREAL_0:17;
  then
A12: x0 - r1 <= x0 - r by XREAL_1:13;
  then x0 - r1 <= x0 by A8,XXREAL_0:2;
  then
A13: x0 in [.x0 - r1,x0.] by XXREAL_1:1;
  x0 - r in { g: x0 - r1 <= g & g <= x0 } by A8,A12;
  then x0 - r in [.x0 - r1,x0.] by RCOMP_1:def 1;
  then [.x0 - r,x0.] c= [.x0 - r1,x0.] by A13,XXREAL_2:def 12;
  then [.x0 - r,x0.] c= dom f1 by A6;
  then
A14: [.x0 - r,x0.] c= dom f1 /\ dom f2 by A11,XBOOLE_1:19;
A15: for h,c st rng c = {x0} & rng (h+c) c= dom (f1 - f2) &
  (for n being Nat holds h.n
< 0) holds h"(#)((f1-f2)/*(h+c) - (f1-f2)/*c) is convergent & lim(h"(#)((f1-f2)
  /*(h+c) - (f1-f2)/*c)) = Ldiff(f1,x0) - Ldiff(f2,x0)
  proof
    let h,c;
    assume that
A16: rng c = {x0} and
A17: rng (h+c) c= dom (f1 - f2) and
A18: for n being Nat holds h.n < 0;
A19: rng (h + c) c= dom f1 /\ dom f2 by A17,VALUED_1:12;
A20: now
      let n;
A21:  rng c c= dom f1 /\ dom f2
      proof
        let x be object;
        assume x in rng c;
        then
A22:    x = x0 by A16,TARSKI:def 1;
        x0 in [.x0 - r,x0.] by A8,XXREAL_1:1;
        hence thesis by A14,A22;
      end;
      thus (f1/*(h+c) - f1/*c - (f2/*(h+c) - f2/*c)).n = (f1/*(h+c) - f1/*c).n
      - (f2/*(h+c) - f2/*c).n by RFUNCT_2:1
        .=(f1/*(h+c)).n - (f1/*c).n - (f2/*(h+c) - (f2/*c)).n by RFUNCT_2:1
        .=(f1/*(h+c)).n - (f1/*c).n - ((f2/*(h+c)).n - (f2/*c).n) by RFUNCT_2:1
        .=(f1/*(h+c)).n - (f2/*(h+c)).n - ((f1/*c).n - (f2/*c).n)
        .=(f1/*(h+c) - f2/*(h+c)).n - ((f1/*c).n - (f2/*c).n) by RFUNCT_2:1
        .=(f1/*(h+c) - f2/*(h+c)).n - ((f1/*c - f2/*c).n) by RFUNCT_2:1
        .=(f1/*(h+c) - f2/*(h+c) - (f1/*c - f2/*c)).n by RFUNCT_2:1
        .=((f1-f2)/*(h+c) - (f1/*c - f2/*c)).n by A19,RFUNCT_2:8
        .=((f1-f2)/*(h+c) - (f1-f2)/*c).n by A21,RFUNCT_2:8;
    end;
    then
A23: f1/*(h+c) - f1/*c - (f2/*(h+c) - f2/*c) = (f1-f2)/*(h+c) - (f1-f2)/*c
    by FUNCT_2:63;
    dom f1 /\ dom f2 c=dom f2 by XBOOLE_1:17;
    then
A24: rng (h + c) c= dom f2 by A19;
    then
A25: lim(h"(#)(f2/*(h+c) - f2/*c)) = Ldiff(f2,x0) by A2,A16,A18,Th9;
A26: h"(#)(f2/*(h+c) - f2/*c) is convergent by A2,A16,A18,A24;
    dom f1 /\ dom f2 c= dom f1 by XBOOLE_1:17;
    then
A27: rng (h + c) c= dom f1 by A19;
A28: (h"(#)(f1/*(h+c) - f1/*c) - h"(#)(f2/*(h+c) - f2/*c)) = h"(#)(f1/*(h+
    c) - f1/*c - (f2/*(h+c) - f2/*c)) by SEQ_1:21;
A29: h"(#)(f1/*(h+c) - f1/*c) is convergent by A1,A16,A18,A27;
    then (h"(#)(f1/*(h+c) - f1/*c) - h"(#) (f2/*(h+c) - f2/*c)) is convergent
    by A26;
    hence h"(#)((f1-f2)/*(h+c) - (f1-f2)/*c) is convergent by A28,A20,
FUNCT_2:63;
    lim(h"(#)(f1/*(h+c) - f1/*c)) = Ldiff(f1,x0) by A1,A16,A18,A27,Th9;
    hence thesis by A29,A26,A25,A28,A23,SEQ_2:12;
  end;
  [.x0 - r,x0.] c= dom (f1 - f2) by A14,VALUED_1:12;
  hence thesis by A7,A15,Th9;
end;

theorem
  f1 is_left_differentiable_in x0 & f2 is_left_differentiable_in x0
implies f1(#)f2 is_left_differentiable_in x0 & Ldiff(f1(#)f2,x0) = Ldiff(f1,x0)
  *f2.x0 + Ldiff(f2,x0)*f1.x0
proof
  assume that
A1: f1 is_left_differentiable_in x0 and
A2: f2 is_left_differentiable_in x0;
  consider r2 such that
A3: 0 < r2 and
A4: [.x0 -r2,x0.] c= dom f2 by A2;
  consider r1 such that
A5: 0 < r1 and
A6: [.x0 -r1,x0.] c= dom f1 by A1;
  set r = min(r1,r2);
A7: 0 < r by A5,A3,XXREAL_0:15;
  then
A8: x0 - r <= x0 by XREAL_1:43;
  r <= r2 by XXREAL_0:17;
  then
A9: x0 - r2 <= x0 - r by XREAL_1:13;
  then x0 - r2 <= x0 by A8,XXREAL_0:2;
  then
A10: x0 in [.x0 - r2,x0.] by XXREAL_1:1;
  x0 - r in { g: x0 - r2 <= g & g <= x0 } by A8,A9;
  then x0 - r in [.x0 - r2,x0.] by RCOMP_1:def 1;
  then [.x0 - r,x0.] c= [.x0 - r2,x0.] by A10,XXREAL_2:def 12;
  then
A11: [.x0 - r,x0.] c= dom f2 by A4;
  r <= r1 by XXREAL_0:17;
  then
A12: x0 - r1 <= x0 - r by XREAL_1:13;
  then x0 - r1 <= x0 by A8,XXREAL_0:2;
  then
A13: x0 in [.x0 - r1,x0.] by XXREAL_1:1;
  x0 - r in { g: x0 - r1 <= g & g <= x0 } by A8,A12;
  then x0 - r in [.x0 - r1,x0.] by RCOMP_1:def 1;
  then [.x0 - r,x0.] c= [.x0 - r1,x0.] by A13,XXREAL_2:def 12;
  then
A14: [.x0 - r,x0.] c= dom f1 by A6;
A15: for h,c st rng c = {x0} & rng (h+c) c= dom (f1(#)f2) &
 (for n being Nat holds h.n
< 0) holds h"(#)((f1(#)f2)/*(h+c) - (f1(#)f2)/*c) is convergent & lim(h"(#)((f1
  (#)f2)/*(h+c) - (f1(#)f2)/*c)) = Ldiff(f1,x0)*f2.x0 + Ldiff(f2,x0)*f1.x0
  proof
    let h,c;
    assume that
A16: rng c = {x0} and
A17: rng (h+c) c= dom (f1(#)f2) and
A18: for n being Nat holds h.n < 0;
A19: rng (h + c) c= dom f1 /\ dom f2 by A17,VALUED_1:def 4;
    now
      let n;
      thus (f1/*c + (f1/*(h+c) - f1/*c)).n = (f1/*c).n + (f1/*(h+c) - f1/*c).
      n by SEQ_1:7
        .= (f1/*c).n + ((f1/*(h+c)).n - (f1/*c).n) by RFUNCT_2:1
        .= (f1/*(h+c)).n;
    end;
    then
A20: f1/*c + (f1/*(h+c) - f1/*c) = f1/*(h+c) by FUNCT_2:63;
A21: for m holds c.m = x0
    proof
      let m;
      c.m in rng c by VALUED_0:28;
      hence thesis by A16,TARSKI:def 1;
    end;
    0 <= r by A5,A3,XXREAL_0:15;
    then x0 - r <= x0 by XREAL_1:43;
    then
A22: x0 in [.x0 -r,x0.] by XXREAL_1:1;
    then
A23: x0 in dom f1 by A14;
A24: rng c c= dom f1
    by A16,A23,TARSKI:def 1;
A25: for g be Real st 0 < g
   ex n being Nat st for m being Nat st n <=m
    holds |.(f1/*c).m - f1.x0.| < g
    proof
      let g be Real such that
A26:  0 < g;
      take n = 0;
      let m being Nat such that
      n <= m;
A27:    m in NAT by ORDINAL1:def 12;
      |.(f1/*c).m - f1.x0.| = |.f1.(c.m) - f1.x0.| by A24,FUNCT_2:108,A27
        .= |.f1.x0-f1.x0.| by A21,A27
        .= 0 by ABSVALUE:def 1;
      hence thesis by A26;
    end;
    then
A28: f1/*c is convergent by SEQ_2:def 6;
A29: x0 in dom f2 by A11,A22;
A30: rng c c= dom f2
    by A16,A29,TARSKI:def 1;
A31: for g be Real st 0 < g
   ex n being Nat st for m being Nat st n <=m holds |.(f2/*c
    ).m - f2.x0.| < g
    proof
      let g be Real such that
A32:  0 < g;
      take n = 0;
      let m being Nat such that
      n <= m;
A33:   m in NAT by ORDINAL1:def 12;
      |.(f2/*c).m - f2.x0.| = |.f2.(c.m) - f2.x0.| by A30,FUNCT_2:108,A33
        .= |.f2.x0 - f2.x0.| by A21,A33
        .= 0 by ABSVALUE:def 1;
      hence thesis by A32;
    end;
    then
A34: f2/*c is convergent by SEQ_2:def 6;
    dom f1 /\ dom f2 c= dom f1 by XBOOLE_1:17;
    then
A35: rng (h + c) c= dom f1 by A19;
    then
A36: lim(h"(#)(f1/*(h+c) - f1/*c)) = Ldiff(f1,x0) by A1,A16,A18,Th9;
A37: h is convergent & h"(#)(f1/*(h+c) - f1/*c) is convergent by A1,A16,A18,A35
;
    then
A38: lim (h(#)(h"(#)(f1/*(h+c) - f1/*c))) = lim h *lim (h"(#) (f1/*(h+c) -
    f1/*c)) by SEQ_2:15
      .= 0;
    dom f1 /\ dom f2 c=dom f2 by XBOOLE_1:17;
    then
A39: rng (h + c) c= dom f2 by A19;
    then
A40: lim(h"(#)(f2/*(h+c) - f2/*c)) = Ldiff(f2,x0) by A2,A16,A18,Th9;
A41: h"(#)(f1/*(h+c) - f1/*c) is convergent by A1,A16,A18,A35;
    then
A42: h"(#) (f1/*(h+c) - f1/*c)(#)(f2/*c) is convergent by A34;
A43: rng c c= dom f1 /\ dom f2 by A24,A30,XBOOLE_1:19;
A44: now
      let n;
      thus (h"(#)((f1(#)f2)/*(h+c) - (f1(#)f2)/*c)).n = ((h").n) * ((f1(#)f2)
      /*(h+c) - (f1(#)f2)/*c).n by SEQ_1:8
        .= ((h").n) * (((f1(#)f2)/*(h+c)).n - ((f1(#)f2)/*c).n) by RFUNCT_2:1
        .= h".n * (((f1/*(h+c))(#)(f2/*(h+c))).n - ((f1(#)f2)/*c).n) by A19,
RFUNCT_2:8
        .= h".n * (((f1/*(h+c))(#)(f2/*(h+c))).n - ((f1/*c)(#)(f2/*c)).n) by
A43,RFUNCT_2:8
        .= h".n * ((f1/*(h+c)).n * (f2/*(h+c)).n - ((f1/*c)(#)(f2/*c)).n) by
SEQ_1:8
        .= h".n * ((f1/*(h+c)).n * (f2/*(h+c)).n - ((f1/*c).n * (f2/*c).n))
      by SEQ_1:8
        .= h".n * ((f2/*(h+c)).n - (f2/*c).n)*(f1/*(h+c)).n + (h".n * ((f1/*
      (h+c)).n - (f1/*c).n))*(f2/*c).n
        .= h".n * (f2/*(h+c) - f2/*c).n * (f1/*(h+c)).n + (h".n * ((f1/*(h+c
      )).n - (f1/*c).n))*(f2/*c).n by RFUNCT_2:1
        .= (h"(#) (f2/*(h+c) - f2/*c)).n * (f1/*(h+c)).n + (h".n * ((f1/*(h+
      c)).n - (f1/*c).n))*(f2/*c).n by SEQ_1:8
        .= (h"(#) (f2/*(h+c) - f2/*c)).n * (f1/*(h+c)).n + (h".n * (f1/*(h+c
      ) - (f1/*c)).n)*(f2/*c).n by RFUNCT_2:1
        .= (h"(#) (f2/*(h+c) - f2/*c)).n * (f1/*(h+c)).n + (h"(#) (f1/*(h+c)
      - f1/*c)).n*(f2/*c).n by SEQ_1:8
        .= (h"(#) (f2/*(h+c) - f2/*c) (#) (f1/*(h+c))).n + (h"(#) (f1/*(h+c)
      - f1/*c)).n*(f2/*c).n by SEQ_1:8
        .= (h"(#) (f2/*(h+c) - f2/*c)(#)(f1/*(h+c))).n + (h"(#) (f1/*(h+c) -
      f1/*c)(#)(f2/*c)).n by SEQ_1:8
        .= (h"(#) (f2/*(h+c) - f2/*c)(#)(f1/*(h+c)) + h"(#) (f1/*(h+c) - f1
      /*c)(#)(f2/*c)).n by SEQ_1:7;
    end;
    then
A45: h"(#)((f1(#)f2)/*(h+c) - (f1(#)f2)/*c) = h"(#) (f2/*(h+c) - f2/*c )
    (#) (f1/*(h+c)) + h"(#) (f1/*(h+c) - f1/*c)(#)(f2/*c) by FUNCT_2:63;
    now
      let n;
A46:  h.n <> 0 by A18;
      thus (h(#)(h"(#)(f1/*(h+c) - f1/*c))).n = ((h(#)h")(#) (f1/*(h+c) - f1/*
      c)).n by SEQ_1:14
        .= (h(#)h").n *(f1/*(h+c) - f1/*c).n by SEQ_1:8
        .= h.n * (h").n *(f1/*(h+c) - f1/*c).n by SEQ_1:8
        .= h.n * (h.n)" *(f1/*(h+c) - f1/*c).n by VALUED_1:10
        .= 1*(f1/*(h+c) - f1/*c).n by A46,XCMPLX_0:def 7
        .= (f1/*(h+c) - f1/*c).n;
    end;
    then
A47: h(#)(h"(#)(f1/*(h+c) - f1/*c)) = (f1/*(h+c) - f1/*c) by FUNCT_2:63;
    h(#)(h"(#)(f1/*(h+c) - f1/*c)) is convergent by A37;
    then
A48: f1/*(h+c) is convergent by A28,A47,A20;
    lim(f1/*c) = f1.x0 by A25,A28,SEQ_2:def 7;
    then
A49: 0 = lim (f1/*(h+c)) - f1.x0 by A28,A47,A48,A38,SEQ_2:12;
A50: h"(#)(f2/*(h+c) - f2/*c) is convergent by A2,A16,A18,A39;
    then
A51: h"(#) (f2/*(h+c) - f2/*c)(#) (f1/*(h+c)) is convergent by A48;
    lim (h"(#)((f1(#)f2)/*(h+c) - (f1(#)f2)/*c)) = lim (h"(#) (f2/*(h+c)
- f2/*c)(#)(f1/*(h+c)) + h"(#) (f1/*(h+c) - f1/*c)(#) (f2/*c)) by A44,
FUNCT_2:63
      .= lim (h"(#) (f2/*(h+c) - f2/*c)(#)(f1/*(h+c))) + lim (h"(#) (f1/*(h+
    c) - f1/*c)(#)(f2/*c)) by A51,A42,SEQ_2:6
      .= lim (h"(#) (f2/*(h+c) - f2/*c))*lim(f1/*(h+c)) + lim (h"(#) (f1/*(h
    +c) - f1/*c)(#)(f2/*c)) by A50,A48,SEQ_2:15
      .= lim (h"(#) (f2/*(h+c) - f2/*c))* f1.x0 + lim (h"(#) (f1/*(h+c) - f1
    /*c))*lim(f2/*c) by A41,A49,A34,SEQ_2:15
      .= Ldiff(f1,x0) * f2.x0 + Ldiff(f2,x0) * f1.x0 by A36,A40,A31,A34,
SEQ_2:def 7;
    hence thesis by A51,A42,A45;
  end;
  [.x0 - r,x0.] c= dom f1 /\ dom f2 by A14,A11,XBOOLE_1:19;
  then [.x0 - r,x0.] c= dom (f1(#)f2) by VALUED_1:def 4;
  hence thesis by A7,A15,Th9;
end;

Lm1: f1 is_left_differentiable_in x0 & f2 is_left_differentiable_in x0 & (ex
r0 st r0 > 0 & for g st g in dom f2 & g in [.x0 - r0,x0.] holds f2.g <> 0)
implies f1/f2 is_left_differentiable_in x0 & Ldiff(f1/f2,x0) = (Ldiff(f1,x0)*f2
.x0 - Ldiff(f2,x0)*f1.x0)/(f2.x0)^2
proof
  assume that
A1: f1 is_left_differentiable_in x0 and
A2: f2 is_left_differentiable_in x0;
  consider r1 such that
A3: 0 < r1 and
A4: [.x0 -r1,x0.] c= dom f1 by A1;
  given r0 such that
A5: r0 > 0 and
A6: for g st g in dom f2 & g in [.x0 - r0,x0.] holds f2.g <> 0;
  consider r2 such that
A7: 0 < r2 and
A8: [.x0 -r2,x0.] c= dom f2 by A2;
  set r3 = min(r0,r2);
A9: 0 < r3 by A5,A7,XXREAL_0:15;
  then
A10: x0 - r3 <= x0 by XREAL_1:43;
  r3 <= r2 by XXREAL_0:17;
  then
A11: x0 - r2 <= x0 - r3 by XREAL_1:13;
  then x0 - r2 <= x0 by A10,XXREAL_0:2;
  then
A12: x0 in [.x0 - r2,x0.] by XXREAL_1:1;
  x0 - r3 in { g: x0 - r2 <= g & g <= x0 } by A10,A11;
  then x0 - r3 in [.x0 - r2,x0.] by RCOMP_1:def 1;
  then [.x0 - r3,x0.] c= [.x0 - r2,x0.] by A12,XXREAL_2:def 12;
  then
A13: [.x0 - r3,x0.] c= dom f2 by A8;
  r3 <= r0 by XXREAL_0:17;
  then
A14: x0 - r0 <= x0 - r3 by XREAL_1:13;
  then x0 - r0 <= x0 by A10,XXREAL_0:2;
  then
A15: x0 in [.x0 - r0,x0.] by XXREAL_1:1;
  x0 - r3 in { g: x0 - r0 <= g & g <= x0 } by A10,A14;
  then x0 - r3 in [.x0 - r0,x0.] by RCOMP_1:def 1;
  then
A16: [.x0 - r3,x0.] c= [.x0 - r0,x0.] by A15,XXREAL_2:def 12;
  set r = min(r1,r3);
A17: 0 < r by A3,A9,XXREAL_0:15;
  then
A18: x0 - r <= x0 by XREAL_1:43;
  r <= r3 by XXREAL_0:17;
  then
A19: x0 - r3 <= x0 - r by XREAL_1:13;
  then x0 - r3 <= x0 by A18,XXREAL_0:2;
  then
A20: x0 in [.x0 - r3,x0.] by XXREAL_1:1;
  x0 - r in { g: x0 - r3 <= g & g <= x0 } by A18,A19;
  then x0 - r in [.x0 - r3,x0.] by RCOMP_1:def 1;
  then
A21: [.x0 - r,x0.] c= [.x0 - r3,x0.] by A20,XXREAL_2:def 12;
  [.x0 - r,x0.] c= dom(f2^)
  proof
    assume not thesis;
    then consider x being object such that
A22: x in [.x0 - r,x0.] and
A23: not x in dom (f2^);
    reconsider x as Real by A22;
A24: x in [.x0 - r3,x0.] by A21,A22;
A25: not x in dom f2 \ f2"{0} by A23,RFUNCT_1:def 2;
    now
      per cases by A25,XBOOLE_0:def 5;
      suppose
        not x in dom f2;
        hence contradiction by A13,A24;
      end;
      suppose
A26:    x in f2"{0};
        then f2.x in {0} by FUNCT_1:def 7;
        then
A27:    f2.x = 0 by TARSKI:def 1;
        x in dom f2 by A26,FUNCT_1:def 7;
        hence contradiction by A6,A16,A24,A27;
      end;
    end;
    hence contradiction;
  end;
  then
A28: [.x0 - r,x0.] c= dom f2\f2"{0} by RFUNCT_1:def 2;
  r <= r1 by XXREAL_0:17;
  then
A29: x0 - r1 <= x0 - r by XREAL_1:13;
  then x0 - r1 <= x0 by A18,XXREAL_0:2;
  then
A30: x0 in [.x0 - r1,x0.] by XXREAL_1:1;
  x0 - r in { g: x0 - r1 <= g & g <= x0 } by A18,A29;
  then x0 - r in [.x0 - r1,x0.] by RCOMP_1:def 1;
  then [.x0 - r,x0.] c= [.x0 - r1,x0.] by A30,XXREAL_2:def 12;
  then
A31: [.x0 - r,x0.] c= dom f1 by A4;
A32: for h,c st rng c = {x0} & rng (h+c) c= dom (f1/f2) &
(for n being Nat holds h.n <
0) holds h"(#)((f1/f2)/*(h+c) - (f1/f2)/*c) is convergent & lim(h"(#)((f1/f2)/*
  (h+c) - (f1/f2)/*c)) = (Ldiff(f1,x0)*f2.x0 - Ldiff(f2,x0)*f1.x0)/(f2.x0)^2
  proof
    let h,c;
    assume that
A33: rng c = {x0} and
A34: rng (h+c) c= dom (f1/f2) and
A35: for n being Nat holds h.n < 0;
A36: rng (h + c) c= dom f1 /\ (dom f2\f2"{0}) by A34,RFUNCT_1:def 1;
    0 <= r by A3,A9,XXREAL_0:15;
    then x0 - r <= x0 by XREAL_1:43;
    then
A37: x0 in [.x0 -r,x0.] by XXREAL_1:1;
    then
A38: x0 in dom f1 by A31;
A39: rng c c= dom f1
    by A33,A38,TARSKI:def 1;
    dom f1 /\ (dom f2\f2"{0}) c= dom f1 by XBOOLE_1:17;
    then
A40: rng (h + c) c= dom f1 by A36;
    then
A41: lim(h"(#)(f1/*(h+c) - f1/*c)) = Ldiff(f1,x0) by A1,A33,A35,Th9;
A42: x0 in (dom f2\f2"{0}) by A28,A37;
    rng c c= dom f2\f2"{0}
    by A33,A42,TARSKI:def 1;
    then
A43: rng c c= dom (f2^) by RFUNCT_1:def 2;
    then
A44: rng c c= dom f1 /\ dom (f2^) by A39,XBOOLE_1:19;
A45: h"(#)(f1/*(h+c) - f1/*c) is convergent by A1,A33,A35,A40;
A46: f2/*c is non-zero by A43,RFUNCT_2:11;
A47: now
      let n;
      thus (h"(#)((f1/*(h+c))(#)(f2/*c) - (f1/*c)(#)(f2/*(h+c)))).n = (h").n *
      ((f1/*(h+c))(#)(f2/*c) - (f1/*c)(#)(f2/*(h+c))).n by SEQ_1:8
        .= (h").n * (((f1/*(h+c))(#)(f2/*c)).n - ((f1/*c)(#) (f2/*(h+c))).n)
      by RFUNCT_2:1
        .= (h").n * ((f1/*(h+c)).n * (f2/*c).n - ((f1/*c)(#)(f2/*(h+c))).n)
      by SEQ_1:8
        .= (h").n * (((f1/*(h+c)).n - (f1/*c).n) * (f2/*c).n + ((f1/*c).n*(
      f2/*c).n) - ((f1/*c).n * (f2/*(h+c)).n)) by SEQ_1:8
        .= (h").n * ((f1/*(h+c)).n - (f1/*c).n) * (f2/*c).n - (f1/*c).n * ((
      h").n * ((f2/*(h+c)).n - (f2/*c).n))
        .= (h").n * ((f1/*(h+c)) - (f1/*c)).n * (f2/*c).n - (f1/*c).n * ((h"
      ).n * ((f2/*(h+c)).n - (f2/*c).n)) by RFUNCT_2:1
        .= (h").n * (f1/*(h+c) - (f1/*c)).n * (f2/*c).n - (f1/*c).n * ((h").
      n * (f2/*(h+c) - (f2/*c)).n) by RFUNCT_2:1
        .= (h" (#) (f1/*(h+c) - (f1/*c))).n * (f2/*c).n - (f1/*c).n * ((h").
      n * (f2/*(h+c) - (f2/*c)).n) by SEQ_1:8
        .= (h"(#)(f1/*(h+c) - (f1/*c))).n * (f2/*c).n - (f1/*c).n * (h"(#)(
      f2/*(h+c) - (f2/*c))).n by SEQ_1:8
        .= (h"(#)(f1/*(h+c) - (f1/*c))(#)(f2/*c)).n - (f1/*c).n * (h"(#)(f2
      /*(h+c) - (f2/*c))).n by SEQ_1:8
        .= (h"(#)(f1/*(h+c) - (f1/*c))(#)(f2/*c)).n - ((f1/*c)(#)(h"(#)(f2/*
      (h+c)-(f2/*c)))).n by SEQ_1:8
        .= (h"(#)(f1/*(h+c) - (f1/*c))(#)(f2/*c) - (f1/*c)(#)(h"(#) (f2/*(h+
      c)-(f2/*c)))).n by RFUNCT_2:1;
    end;
    now
      let n;
      thus (f2/*c + (f2/*(h+c) - f2/*c)).n = (f2/*c).n + (f2/*(h+c) - f2/*c).n
      by SEQ_1:7
        .= (f2/*c).n + ((f2/*(h+c)).n - (f2/*c).n) by RFUNCT_2:1
        .= (f2/*(h+c)).n;
    end;
    then
A48: f2/*c + (f2/*(h+c) - f2/*c) = f2/*(h+c) by FUNCT_2:63;
    dom f1 /\ (dom f2\f2"{0}) c=(dom f2\f2"{0}) by XBOOLE_1:17;
    then
A49: rng (h + c) c= (dom f2\f2"{0}) by A36;
    then
A50: rng (h + c) c= dom (f2^) by RFUNCT_1:def 2;
    then
A51: rng (h + c) c= dom f1 /\ dom (f2^) by A40,XBOOLE_1:19;
A52: f2/*(h+c) is non-zero by A50,RFUNCT_2:11;
    then
A53: (f2/*(h+c)) (#) (f2/*c) is non-zero by A46,SEQ_1:35;
    h"(#) ((f1/f2)/*(h+c) - (f1/f2)/*c)=h"(#)((f1(#) (f2^))/*(h+c) - (f1
    /f2)/*c) by RFUNCT_1:31
      .=h"(#)((f1(#)(f2^))/*(h+c) - (f1(#)(f2^))/*c) by RFUNCT_1:31
      .=h"(#)((f1/*(h+c))(#)((f2^)/*(h+c)) - (f1(#) (f2^))/*c) by A51,
RFUNCT_2:8
      .=h"(#)((f1/*(h+c))/"(f2/*(h+c)) - (f1(#)(f2^))/*c) by A50,RFUNCT_2:12
      .=h"(#)((f1/*(h+c))/"(f2/*(h+c)) - (f1/*c)(#) ((f2^)/*c)) by A44,
RFUNCT_2:8
      .=h"(#)((f1/*(h+c))/"(f2/*(h+c)) - (f1/*c)/"(f2/*c)) by A43,RFUNCT_2:12
      .=h"(#)(((f1/*(h+c))(#)(f2/*c) - (f1/*c)(#)(f2/*(h+c)))/"((f2/*(h+c))
    (#) (f2/*c))) by A52,A46,SEQ_1:50
      .=(h"(#)((f1/*(h+c))(#)(f2/*c) - (f1/*c)(#)(f2/*(h+c))))/"((f2/*(h+c))
    (#) (f2/*c)) by SEQ_1:41;
    then
A54: h"(#) ((f1/f2)/*(h+c) - (f1/f2)/*c) =((h"(#)(f1/*(h+c) - (f1/*c)) )
(#) (f2/*c) - (f1/*c)(#)(h"(#)(f2/*(h+c)-(f2/*c))))/"(f2/*(h+c)(#) (f2/*c)) by
A47,FUNCT_2:63;
    dom f2 \ f2"{0} c= dom f2 by XBOOLE_1:36;
    then
A55: rng (h + c) c= dom f2 by A49;
    then
A56: lim(h"(#)(f2/*(h+c) - f2/*c)) = Ldiff(f2,x0) by A2,A33,A35,Th9;
A57: h"(#)(f2/*(h+c) - f2/*c) is convergent by A2,A33,A35,A55;
    now
      let n;
A58:  h.n <> 0 by A35;
      thus (h(#)(h"(#)(f2/*(h+c) - f2/*c))).n = ((h(#)h")(#)(f2/*(h+c) - f2/*c
      )). n by SEQ_1:14
        .= (h(#)h").n *(f2/*(h+c) - f2/*c).n by SEQ_1:8
        .= h.n * (h").n *(f2/*(h+c) - f2/*c).n by SEQ_1:8
        .= h.n * (h.n)" *(f2/*(h+c) - f2/*c).n by VALUED_1:10
        .= 1*(f2/*(h+c) - f2/*c).n by A58,XCMPLX_0:def 7
        .= (f2/*(h+c) - f2/*c).n;
    end;
    then
A59: h(#)(h"(#)(f2/*(h+c) - f2/*c)) = (f2/*(h+c) - f2/*c) by FUNCT_2:63;
A60: for m holds c.m = x0
    proof
      let m;
      c.m in rng c by VALUED_0:28;
      hence thesis by A33,TARSKI:def 1;
    end;
A61: for g be Real st 0 < g
  ex n being Nat st for m being Nat st n <=m
   holds |.(f1/*c).m - f1.x0.| < g
    proof
      let g be Real such that
A62:  0 < g;
      take n = 0;
      let m being Nat such that
      n <= m;
A63:   m in NAT by ORDINAL1:def 12;
      |.(f1/*c).m - f1.x0.| = |.f1.(c.m) - f1.x0.| by A39,FUNCT_2:108,A63
        .=|.f1.x0-f1.x0.| by A60,A63
        .= 0 by ABSVALUE:def 1;
      hence thesis by A62;
    end;
    then
A64: f1/*c is convergent by SEQ_2:def 6;
    then
A65: lim(f1/*c) = f1.x0 by A61,SEQ_2:def 7;
    dom (f2^) = dom f2 \ f2"{0} by RFUNCT_1:def 2;
    then
A66: dom (f2^) c= dom f2 by XBOOLE_1:36;
A67: for g be Real st 0 < g
ex n being Nat st for m being Nat st n <=m holds |.(f2/*
    c).m - f2.x0.| < g
    proof
      let g be Real such that
A68:  0 < g;
      take n = 0;
      let m being Nat such that
      n <= m;
A69:   m in NAT by ORDINAL1:def 12;
      |.(f2/*c).m - f2.x0.| = |.f2.(c.m) - f2.x0.| by A43,A66,FUNCT_2:108
,XBOOLE_1:1,A69
        .=|.f2.x0 - f2.x0.| by A60,A69
        .= 0 by ABSVALUE:def 1;
      hence thesis by A68;
    end;
    then
A70: f2/*c is convergent by SEQ_2:def 6;
    then
A71: lim(f2/*c) = f2.x0 by A67,SEQ_2:def 7;
    h(#)(h"(#)(f2/*(h+c) - f2/*c)) is convergent by A57;
    then
A72: f2/*(h+c) is convergent by A70,A59,A48;
    then
A73: f2/*(h+c) (#) (f2/*c) is convergent by A70;
    h"(#)(f2/*(h+c) - f2/*c) is convergent by A2,A33,A35,A55;
    then lim (h(#)(h"(#)(f2/*(h+c) - f2/*c))) = lim h *lim (h"(#)(f2/*(h+c) -
    f2/* c ) ) by SEQ_2:15
      .= 0;
    then 0 = lim (f2/*(h+c)) - f2.x0 by A70,A71,A59,A72,SEQ_2:12;
    then
A74: lim(f2/*(h+c) (#) (f2/*c)) = (f2.x0)^2 by A70,A71,A72,SEQ_2:15;
A75: lim(f2/*(h+c) (#) (f2/*c))<> 0
    proof
      assume not thesis;
      then f2.x0 = 0 by A74,XCMPLX_1:6;
      hence contradiction by A6,A8,A15,A12;
    end;
    h"(#)(f1/*(h+c) - f1/*c) is convergent by A1,A33,A35,A40;
    then
A76: h"(#) (f1/*(h+c) - f1/*c)(#)(f2/*c) is convergent by A70;
A77: (f1/*c)(#)(h"(#) (f2/*(h+c) - f2/*c)) is convergent by A57,A64;
    then
A78: ((h"(#)(f1/*(h+c) - (f1/*c)))(#)(f2/*c) - (f1/*c)(#)(h"(#) (f2/*(h+c
    )-(f2/*c)))) is convergent by A76;
    then lim(h"(#) ((f1/f2)/*(h+c) - (f1/f2)/*c)) = lim((h"(#)(f1/*(h+c) - (
f1/*c)))(#)(f2/*c) - (f1/*c)(#)(h"(#) (f2/*(h+c)-(f2/*c))))/ lim(f2/*(h+c)(#)(
    f2/*c)) by A53,A73,A75,A54,SEQ_2:24
      .=(lim((h"(#)(f1/*(h+c)-(f1/*c)))(#)(f2/*c))-lim((f1/*c)(#)(h"(#)(f2/*
    (h+c)- (f2/*c)))))/lim(f2/*(h+c)(#)(f2/*c)) by A77,A76,SEQ_2:12
      .=( lim(h"(#)(f1/*(h+c)-(f1/*c)))*lim(f2/*c) - lim((f1/*c) (#) (h"(#)(
    f2/*(h+c)-(f2/*c)))) ) / lim(f2/*(h+c)(#)(f2/*c)) by A45,A70,SEQ_2:15
      .=(Ldiff(f1,x0) * f2.x0 - Ldiff(f2,x0) * f1.x0)/(f2.x0)^2 by A41,A57,A56
,A64,A65,A71,A74,SEQ_2:15;
    hence thesis by A53,A73,A75,A78,A54,SEQ_2:23;
  end;
  [.x0 - r,x0.] c= dom f1 /\ (dom f2\f2"{0}) by A31,A28,XBOOLE_1:19;
  then [.x0 - r,x0.] c= dom (f1/f2) by RFUNCT_1:def 1;
  hence thesis by A17,A32,Th9;
end;

theorem
  f1 is_left_differentiable_in x0 & f2 is_left_differentiable_in x0 & f2
.x0 <> 0 implies f1/f2 is_left_differentiable_in x0 & Ldiff(f1/f2,x0) = (Ldiff(
  f1,x0)*f2.x0 - Ldiff(f2,x0)*f1.x0)/(f2.x0)^2
proof
  assume that
A1: f1 is_left_differentiable_in x0 and
A2: f2 is_left_differentiable_in x0 and
A3: f2.x0 <> 0;
  consider r1 such that
A4: r1 > 0 and
  [.x0-r1,x0.] c= dom f2 and
A5: for g st g in [.x0-r1,x0.] holds f2.g <> 0 by A2,A3,Th5,Th6;
  now
    take r1;
    thus r1 > 0 by A4;
    let g;
    assume that
    g in dom f2 and
A6: g in [.x0 - r1,x0.];
    thus f2.g <> 0 by A5,A6;
  end;
  hence thesis by A1,A2,Lm1;
end;

Lm2: f is_left_differentiable_in x0 & (ex r0 st r0 > 0 & for g st g in dom f &
g in [.x0 - r0,x0.] holds f.g <> 0) implies f^ is_left_differentiable_in x0 &
Ldiff(f^,x0) = - Ldiff(f,x0)/(f.x0)^2
proof
  assume
A1: f is_left_differentiable_in x0;
  then consider r2 such that
A2: 0 < r2 and
A3: [.x0 -r2,x0.] c= dom f;
  given r0 such that
A4: r0 > 0 and
A5: for g st g in dom f & g in [.x0 - r0,x0.] holds f.g <> 0;
  set r3 = min(r0,r2);
A6: 0 < r3 by A4,A2,XXREAL_0:15;
  then
A7: x0 - r3 <= x0 by XREAL_1:43;
  r3 <= r2 by XXREAL_0:17;
  then
A8: x0 - r2 <= x0 - r3 by XREAL_1:13;
  then x0 - r2 <= x0 by A7,XXREAL_0:2;
  then
A9: x0 in [.x0 - r2,x0.] by XXREAL_1:1;
  x0 - r3 in { g: x0 - r2 <= g & g <= x0 } by A7,A8;
  then x0 - r3 in [.x0 - r2,x0.] by RCOMP_1:def 1;
  then [.x0 - r3,x0.] c= [.x0 - r2,x0.] by A9,XXREAL_2:def 12;
  then
A10: [.x0 - r3,x0.] c= dom f by A3;
  r3 <= r0 by XXREAL_0:17;
  then
A11: x0 - r0 <= x0 - r3 by XREAL_1:13;
  then x0 - r0 <= x0 by A7,XXREAL_0:2;
  then
A12: x0 in [.x0 - r0,x0.] by XXREAL_1:1;
  x0 - r3 in { g: x0 - r0 <= g & g <= x0 } by A7,A11;
  then x0 - r3 in [.x0 - r0,x0.] by RCOMP_1:def 1;
  then
A13: [.x0 - r3,x0.] c= [.x0 - r0,x0.] by A12,XXREAL_2:def 12;
A14: [.x0 - r3,x0.] c= dom(f^)
  proof
    assume not thesis;
    then consider x being object such that
A15: x in [.x0 - r3,x0.] and
A16: not x in dom (f^);
    reconsider x as Real by A15;
A17: not x in dom f \ f"{0} by A16,RFUNCT_1:def 2;
    now
      per cases by A17,XBOOLE_0:def 5;
      suppose
        not x in dom f;
        hence contradiction by A10,A15;
      end;
      suppose
A18:    x in f"{0};
        then f.x in {0} by FUNCT_1:def 7;
        then
A19:    f.x = 0 by TARSKI:def 1;
        x in dom f by A18,FUNCT_1:def 7;
        hence contradiction by A5,A13,A15,A19;
      end;
    end;
    hence contradiction;
  end;
A20: x0 in [.x0 - r3,x0.] by A7,XXREAL_1:1;
  for h,c st rng c = {x0} & rng (h+c) c= dom (f^) &
 (for n being Nat holds h.n < 0)
holds h"(#)((f^)/*(h+c) - (f^)/*c) is convergent & lim(h"(#)((f^)/*(h+c) - (f^)
  /*c)) = - Ldiff(f,x0)/(f.x0)^2
  proof
    let h,c;
    assume that
A21: rng c = {x0} and
A22: rng (h+c) c= dom (f^) and
A23: for n being Nat holds h.n < 0;
A24: for m holds c.m = x0
    proof
      let m;
      c.m in rng c by VALUED_0:28;
      hence thesis by A21,TARSKI:def 1;
    end;
A25: dom f \ f"{0} c= dom f by XBOOLE_1:36;
    rng (h + c) c= dom f\f"{0} by A22,RFUNCT_1:def 2;
    then
A26: rng (h + c) c= dom f by A25;
    then
A27: lim(h"(#)(f/*(h+c) - f/*c)) = Ldiff(f,x0) by A1,A21,A23,Th9;
A28: h"(#)(f/*(h+c) - f/*c) is convergent by A1,A21,A23,A26;
    then
A29: -(h"(#)((f/*(h+c)) - (f/*c))) is convergent;
    x0 in dom (f^) by A20,A14;
    then
A30: x0 in (dom f\f"{0}) by RFUNCT_1:def 2;
    rng c c= dom f\f"{0}
    by A21,A30,TARSKI:def 1;
    then
A31: rng c c= dom (f^) by RFUNCT_1:def 2;
    then
A32: f/*c is non-zero by RFUNCT_2:11;
    now
      let n;
A33:  h.n <> 0 by A23;
      thus (h(#)(h"(#)(f/*(h+c) - f/*c))).n = ((h(#)h")(#) (f/*(h+c) - f/*c)).
      n by SEQ_1:14
        .= (h(#)h").n *(f/*(h+c) - f/*c).n by SEQ_1:8
        .= h.n * (h").n *(f/*(h+c) - f/*c).n by SEQ_1:8
        .= h.n * (h.n)" *(f/*(h+c) - f/*c).n by VALUED_1:10
        .= 1*(f/*(h+c) - f/*c).n by A33,XCMPLX_0:def 7
        .= (f/*(h+c) - f/*c).n;
    end;
    then
A34: h(#)(h"(#)(f/*(h+c) - f/*c)) = (f/*(h+c) - f/*c) by FUNCT_2:63;
A35: f/*(h+c) is non-zero by A22,RFUNCT_2:11;
    then
A36: (f/*(h+c)) (#) (f/*c) is non-zero by A32,SEQ_1:35;
    now
      let n;
      thus (f/*c + (f/*(h+c) - f/*c)).n = (f/*c).n + (f/*(h+c) - f/*c).n by
SEQ_1:7
        .= (f/*c).n + ((f/*(h+c)).n - (f/*c).n) by RFUNCT_2:1
        .= (f/*(h+c)).n;
    end;
    then
A37: f/*c + (f/*(h+c) - f/*c) = f/*(h+c) by FUNCT_2:63;
    dom (f^) = dom f \ f"{0} by RFUNCT_1:def 2;
    then
A38: dom (f^) c= dom f by XBOOLE_1:36;
A39: for g be Real st 0 < g
ex n being Nat st for m being Nat st n <=m holds |.(f/*c)
    .m - f.x0.| < g
    proof
      let g be Real such that
A40:  0 < g;
      take n = 0;
      let m being Nat such that
      n <= m;
A41:   m in NAT by ORDINAL1:def 12;
      |.(f/*c).m - f.x0.| = |.f.(c.m) - f.x0.| by A31,A38,FUNCT_2:108
,XBOOLE_1:1,A41
        .=|.f.x0 - f.x0.| by A24,A41
        .= 0 by ABSVALUE:def 1;
      hence thesis by A40;
    end;
    then
A42: f/*c is convergent by SEQ_2:def 6;
    then
A43: lim(f/*c) = f.x0 by A39,SEQ_2:def 7;
    h(#)(h"(#)(f/*(h+c) - f/*c)) is convergent by A28;
    then
A44: f/*(h+c) is convergent by A42,A34,A37;
    lim (h(#)(h"(#)(f/*(h+c) - f/*c))) = lim h *lim (h"(#)(f/*(h+c) - f/*
    c ) ) by A28,SEQ_2:15
      .= 0;
    then 0 = lim (f/*(h+c)) - f.x0 by A42,A43,A34,A44,SEQ_2:12;
    then
A45: lim(f/*(h+c) (#) (f/*c)) =(f.x0)^2 by A42,A43,A44,SEQ_2:15;
A46: lim(f/*(h+c) (#) (f/*c))<> 0
    proof
      assume not thesis;
      then f.x0 = 0 by A45,XCMPLX_1:6;
      hence contradiction by A5,A3,A12,A9;
    end;
    now
      let n;
A47:  (f/*(h+c)).n <>0 & (f/*c).n <>0 by A35,A32,SEQ_1:5;
      thus (h"(#) ((f^)/*(h+c) - ((f^)/*c))).n = (h").n* ((f^)/*(h+c) - ((f^)
      /*c)).n by SEQ_1:8
        .= (h").n* (((f^)/*(h+c)).n - ((f^)/*c).n) by RFUNCT_2:1
        .= (h").n* (((f/*(h+c))").n - ((f^)/*c).n) by A22,RFUNCT_2:12
        .= (h").n* (((f/*(h+c))").n - ((f/*c)").n) by A31,RFUNCT_2:12
        .= (h").n* (((f/*(h+c)).n)" - ((f/*c)").n) by VALUED_1:10
        .= (h").n* (((f/*(h+c)).n)" - ((f/*c).n)") by VALUED_1:10
        .= (h").n* (1/(f/*(h+c)).n - ((f/*c).n)") by XCMPLX_1:215
        .= (h").n* (1/(f/*(h+c)).n - 1/(f/*c).n) by XCMPLX_1:215
        .= (h").n* ((1*((f/*c).n) - 1*((f/*(h+c)).n))/((f/*(h+c)).n*(f/*c).n
      )) by A47,XCMPLX_1:130
        .= (h").n* ((-((f/*(h+c)).n - (f/*c).n))/((f/*(h+c))(#)(f/*c)).n) by
SEQ_1:8
        .= (h").n* ((-((f/*(h+c) - (f/*c)).n))/((f/*(h+c))(#)(f/*c)).n) by
RFUNCT_2:1
        .= (h").n*(-(((f/*(h+c) - (f/*c)).n)/((f/*(h+c))(#)(f/*c)).n)) by
XCMPLX_1:187
        .= -((h").n*(((f/*(h+c) - (f/*c)).n)/(((f/*(h+c))(#)(f/*c)).n)))
        .= -((h").n*((f/*(h+c) - (f/*c)).n))/((f/*(h+c))(#)(f/*c)).n by
XCMPLX_1:74
        .= -( ((h" (#) ((f/*(h+c)) - (f/*c))).n) )/((f/*(h+c))(#)(f/*c)).n
      by SEQ_1:8
        .= -(((h"(#)((f/*(h+c)) - (f/*c))).n))*(((f/*(h+c))(#) (f/*c)).n)"
      by XCMPLX_0:def 9
        .= -((((h"(#)((f/*(h+c)) - (f/*c))).n))*(((f/*(h+c))(#) (f/*c))").n)
      by VALUED_1:10
        .= -(((h")(#)((f/*(h+c)) - (f/*c)))/"((f/*(h+c))(#)(f/*c))).n by
SEQ_1:8
        .= (-((h"(#)((f/*(h+c)) - (f/*c)))/"((f/*(h+c))(#)(f/*c)))).n by
SEQ_1:10
        .= ((-(h"(#)((f/*(h+c)) - (f/*c))))/"((f/*(h+c))(#)(f/*c))).n by
SEQ_1:48;
    end;
    then
A48: h"(#) ((f^)/*(h+c) - (f^)/*c) = (-(h"(#)((f/*(h+c)) - (f/*c))))/"((f
    /*(h+c))(#) (f/*c)) by FUNCT_2:63;
A49: f/*(h+c) (#) (f/*c) is convergent by A42,A44;
    then
    lim(h"(#) ((f^)/*(h+c) - (f^)/*c)) = lim (-(h"(#) ((f/*(h+c)) - (f/*c
    ))))/(f.x0)^2 by A36,A45,A46,A29,A48,SEQ_2:24
      .= (-Ldiff(f,x0))/(f.x0)^2 by A28,A27,SEQ_2:10
      .= -Ldiff(f,x0)/(f.x0)^2 by XCMPLX_1:187;
    hence thesis by A36,A49,A46,A29,A48,SEQ_2:23;
  end;
  hence thesis by A6,A14,Th9;
end;

theorem
  f is_left_differentiable_in x0 & f.x0 <> 0 implies f^
  is_left_differentiable_in x0 & Ldiff(f^,x0) = - Ldiff(f,x0)/(f.x0)^2
proof
  assume that
A1: f is_left_differentiable_in x0 and
A2: f.x0 <> 0;
  consider r1 such that
A3: r1 > 0 and
  [.x0-r1,x0.] c= dom f and
A4: for g st g in [.x0-r1,x0.] holds f.g <> 0 by A1,A2,Th5,Th6;
  now
    take r1;
    thus r1 > 0 by A3;
    let g;
    assume that
    g in dom f and
A5: g in [.x0 - r1,x0.];
    thus f.g <> 0 by A4,A5;
  end;
  hence thesis by A1,Lm2;
end;

theorem Th15:
 for g1 being Real holds
  f is_right_differentiable_in x0 & Rdiff(f,x0) = g1 iff (ex r st
r>0 & [.x0,x0+r.] c= dom f) & for h,c st rng c = {x0} & rng (h+c) c= dom f & (
for n being Nat holds h.n > 0)
holds h"(#)(f/*(h+c) - f/*c) is convergent & lim (h"(#)(f
  /*(h+c) - f/*c)) = g1
proof let g1 be Real;
  thus f is_right_differentiable_in x0 & Rdiff(f,x0) = g1 implies (ex r st r>0
& [.x0,x0+r.] c= dom f) & for h,c st rng c = {x0} & rng (h+c) c= dom f &
 (for n being Nat
holds h.n > 0) holds h"(#)(f/*(h+c) - f/*c) is convergent & lim (h"(#)(f/*(h+c)
  - f/*c)) = g1 by Def6;
  assume that
A1: ex r st r>0 & [.x0,x0+r.] c= dom f and
A2: for h,c st rng c = {x0} & rng (h+c) c= dom f &
   (for n being Nat holds h.n > 0)
holds h"(#)(f/*(h+c) - f/*c) is convergent & lim (h"(#)(f/*(h+c) - f/*c)) = g1;
  for h,c holds ( rng c = {x0} & rng (h+c) c= dom f &
  for n being Nat holds h.n > 0
  ) implies h"(#)(f/*(h+c) - f/*c) is convergent by A2;
  hence
A3: f is_right_differentiable_in x0 by A1;
  for h,c holds ( rng c = {x0} & rng (h+c) c= dom f &
   for n being Nat holds h.n > 0)
  implies lim (h"(#)(f/*(h+c) - f/*c)) = g1 by A2;
  hence thesis by A3,Def6;
end;

theorem
  f1 is_right_differentiable_in x0 & f2 is_right_differentiable_in x0
  implies f1+f2 is_right_differentiable_in x0 & Rdiff(f1+f2,x0) = Rdiff(f1,x0)+
  Rdiff(f2,x0)
proof
  assume that
A1: f1 is_right_differentiable_in x0 and
A2: f2 is_right_differentiable_in x0;
  consider r2 such that
A3: r2>0 and
A4: [.x0,x0+r2.] c=dom f2 by A2;
  consider r1 such that
A5: r1>0 and
A6: [.x0,x0+r1.] c= dom f1 by A1;
A7: x0+0 = x0;
  set r = min (r1,r2);
  0 <= r by A5,A3,XXREAL_0:15;
  then
A8: x0 <= x0 + r by A7,XREAL_1:7;
  r<=r2 by XXREAL_0:17;
  then
A9: x0 + r <= x0 + r2 by XREAL_1:7;
  then x0 + r in {g: x0 <= g & g <= x0 +r2} by A8;
  then
A10: x0 + r in [.x0,x0+r2.] by RCOMP_1:def 1;
  x0 <= x0 + r2 by A8,A9,XXREAL_0:2;
  then x0 in [.x0,x0+r2.] by XXREAL_1:1;
  then [.x0,x0+r.] c= [.x0,x0+r2.] by A10,XXREAL_2:def 12;
  then
A11: [.x0,x0+r.] c= dom f2 by A4;
  r<=r1 by XXREAL_0:17;
  then
A12: x0 + r <= x0 + r1 by XREAL_1:7;
  then x0 + r in {g: x0 <= g & g <= x0 +r1} by A8;
  then
A13: x0 + r in [.x0,x0+r1.] by RCOMP_1:def 1;
  x0 <= x0 + r1 by A12,A8,XXREAL_0:2;
  then x0 in [.x0,x0+r1.] by XXREAL_1:1;
  then [.x0,x0+r.] c= [.x0,x0+r1.] by A13,XXREAL_2:def 12;
  then [.x0,x0+r.] c= dom f1 by A6;
  then
A14: [.x0,x0+r.] c= dom f1 /\ dom f2 by A11,XBOOLE_1:19;
  then
A15: [.x0,x0+r.] c= dom(f1 + f2) by VALUED_1:def 1;
A16: for h,c st rng c = {x0} & rng (h+c) c= dom (f1+f2) &
 (for n being Nat holds h.n >
0 ) holds h"(#)((f1+f2)/*(h+c) - (f1+f2)/*c) is convergent & lim (h"(#)((f1+f2)
  /*(h+c) - (f1+f2)/*c)) = Rdiff(f1,x0) + Rdiff(f2,x0)
  proof
    let h,c;
    assume that
A17: rng c = {x0} and
A18: rng (h+c) c= dom (f1+f2) and
A19: for n being Nat holds h.n > 0;
A20: rng (h+c) c= dom f1 /\ dom f2 by A18,VALUED_1:def 1;
A21: now
      let n;
A22:  rng c c= dom f1 /\ dom f2
      proof
        let x be object;
        assume x in rng c;
        then
A23:    x = x0 by A17,TARSKI:def 1;
        x0 in [.x0,x0 + r.] by A8,XXREAL_1:1;
        hence thesis by A14,A23;
      end;
      thus (f1/*(h+c) - f1/*c + (f2/*(h+c) - f2/*c)).n = (f1/*(h+c) + (-(f1/*c
      ))).n + (f2/*(h+c) - f2/*c).n by SEQ_1:7
        .= (f1/*(h+c)).n + (-(f1/*c)).n + (f2/*(h+c) + (-(f2/*c))).n by SEQ_1:7
        .= (f1/*(h+c)).n + (-(f1/*c)).n + ((f2/*(h+c)).n + (-(f2/*c)).n) by
SEQ_1:7
        .= (f1/*(h+c)).n + (f2/*(h+c)).n+ ((-(f1/*c)).n +(-(f2/*c)).n)
        .= (f1/*(h+c)).n + (f2/*(h+c)).n + (-(f1/*c).n + (-(f2/*c)).n) by
SEQ_1:10
        .= (f1/*(h+c)).n + (f2/*(h+c)).n + (-(f1/*c).n + -(f2/*c).n) by
SEQ_1:10
        .= (f1/*(h+c)).n + (f2/*(h+c)).n - ((f1/*c).n + (f2/*c).n)
        .= (f1/*(h+c) + f2/*(h+c)).n - ((f1/*c).n + (f2/*c).n) by SEQ_1:7
        .= (f1/*(h+c) + f2/*(h+c)).n - ((f1/*c + f2/*c).n) by SEQ_1:7
        .= (f1/*(h+c) + f2/*(h+c) - (f1/*c + f2/*c)).n by RFUNCT_2:1
        .= ((f1+f2)/*(h+c) - (f1/*c + f2/*c)).n by A20,RFUNCT_2:8
        .= ((f1+f2)/*(h+c) - (f1+f2)/*c).n by A22,RFUNCT_2:8;
    end;
    then
A24: f1/*(h+c)-f1/*c + (f2/*(h+c) - f2/*c)=(f1+f2)/*(h+c) - (f1+f2)/*c by
FUNCT_2:63;
    dom f1 /\dom f2 c= dom f2 by XBOOLE_1:17;
    then
A25: rng (h+c) c= dom f2 by A20;
    then
A26: lim(h"(#)(f2/*(h+c) - f2/*c)) = Rdiff(f2,x0) by A2,A17,A19,Th15;
A27: h"(#)(f2/*(h+c) - f2/*c) is convergent by A2,A17,A19,A25;
    dom f1 /\ dom f2 c= dom f1 by XBOOLE_1:17;
    then
A28: rng (h+c) c= dom f1 by A20;
A29: (h"(#)(f1/*(h+c) - f1/*c) +h"(#)(f2/*(h+c) - f2/*c)) = h"(#)(f1/*(h+c
    ) -f1/*c + (f2/*(h+c) - f2/*c)) by SEQ_1:16;
A30: h"(#)(f1/*(h+c) - f1/*c) is convergent by A1,A17,A19,A28;
    then (h"(#)(f1/*(h+c) - f1/*c) + h"(#)(f2/*(h+c) - f2/*c)) is convergent
    by A27;
    hence h"(#)((f1+f2)/*(h+c) - (f1+f2)/*c) is convergent by A29,A21,
FUNCT_2:63;
    lim(h"(#)(f1/*(h+c) - f1/*c)) = Rdiff(f1,x0) by A1,A17,A19,A28,Th15;
    hence thesis by A30,A27,A26,A29,A24,SEQ_2:6;
  end;
  0<r by A5,A3,XXREAL_0:15;
  hence thesis by A15,A16,Th15;
end;

theorem
  f1 is_right_differentiable_in x0 & f2 is_right_differentiable_in x0
implies f1 - f2 is_right_differentiable_in x0 & Rdiff(f1-f2,x0) = Rdiff(f1,x0)
  - Rdiff(f2,x0)
proof
  assume that
A1: f1 is_right_differentiable_in x0 and
A2: f2 is_right_differentiable_in x0;
  consider r2 such that
A3: r2>0 and
A4: [.x0,x0+r2.] c=dom f2 by A2;
  consider r1 such that
A5: r1>0 and
A6: [.x0,x0+r1.] c= dom f1 by A1;
  set r = min (r1,r2);
A7: 0<r by A5,A3,XXREAL_0:15;
  then
A8: x0 + 0 <= x0 + r by XREAL_1:7;
  r<=r2 by XXREAL_0:17;
  then
A9: x0 + r <= x0 + r2 by XREAL_1:7;
  then x0 + r in {g: x0 <= g & g <= x0 +r2} by A8;
  then
A10: x0 + r in [.x0,x0+r2.] by RCOMP_1:def 1;
  x0 <= x0 + r2 by A8,A9,XXREAL_0:2;
  then x0 in [.x0,x0+r2.] by XXREAL_1:1;
  then [.x0,x0+r.] c= [.x0,x0+r2.] by A10,XXREAL_2:def 12;
  then
A11: [.x0,x0+r.] c= dom f2 by A4;
  r<=r1 by XXREAL_0:17;
  then
A12: x0 + r <= x0 + r1 by XREAL_1:7;
  then x0 + r in {g: x0 <= g & g <= x0 +r1} by A8;
  then
A13: x0 + r in [.x0,x0+r1.] by RCOMP_1:def 1;
  x0 <= x0 + r1 by A12,A8,XXREAL_0:2;
  then x0 in [.x0,x0+r1.] by XXREAL_1:1;
  then [.x0,x0+r.] c= [.x0,x0+r1.] by A13,XXREAL_2:def 12;
  then [.x0,x0+r.] c= dom f1 by A6;
  then
A14: [.x0,x0+r.] c= dom f1 /\ dom f2 by A11,XBOOLE_1:19;
A15: for h,c st rng c = {x0} & rng (h+c) c= dom (f1 - f2) &
(for n being Nat holds h.n
> 0 ) holds h"(#)((f1-f2)/*(h+c) - (f1-f2)/*c) is convergent & lim(h"(#)((f1-f2
  )/*(h+c) - (f1-f2)/*c)) = Rdiff(f1,x0) - Rdiff(f2,x0)
  proof
    let h,c;
    assume that
A16: rng c ={x0} and
A17: rng (h+c) c= dom(f1-f2) and
A18: for n being Nat holds h.n > 0;
A19: rng (h+c) c= dom f1 /\ dom f2 by A17,VALUED_1:12;
A20: now
      let n;
A21:  rng c c= dom f1 /\ dom f2
      proof
        let x be object;
        assume x in rng c;
        then
A22:    x = x0 by A16,TARSKI:def 1;
        x0 in [.x0,x0+r.] by A8,XXREAL_1:1;
        hence thesis by A14,A22;
      end;
      thus (f1/*(h+c) - f1/*c - (f2/*(h+c) - f2/*c)).n = (f1/*(h+c) - f1/*c).n
      - (f2/*(h+c) - f2/*c).n by RFUNCT_2:1
        .= (f1/*(h+c)).n - (f1/*c).n - (f2/*(h+c) - (f2/*c)).n by RFUNCT_2:1
        .= (f1/*(h+c)).n - (f1/*c).n - ((f2/*(h+c)).n - (f2/*c).n) by
RFUNCT_2:1
        .= (f1/*(h+c)).n - (f2/*(h+c)).n - ((f1/*c).n - (f2/*c).n)
        .= (f1/*(h+c) - f2/*(h+c)).n - ((f1/*c).n - (f2/*c).n) by RFUNCT_2:1
        .= (f1/*(h+c) - f2/*(h+c)).n - ((f1/*c - f2/*c).n) by RFUNCT_2:1
        .= (f1/*(h+c) - f2/*(h+c) - (f1/*c - f2/*c)).n by RFUNCT_2:1
        .= ((f1-f2)/*(h+c) - (f1/*c - f2/*c)).n by A19,RFUNCT_2:8
        .= ((f1-f2)/*(h+c) - (f1-f2)/*c).n by A21,RFUNCT_2:8;
    end;
    then
A23: f1/*(h+c) - f1/*c - (f2/*(h+c) - f2/*c) = (f1-f2)/*(h+c) - (f1-f2)/*c
    by FUNCT_2:63;
    dom f1 /\ dom f2 c= dom f2 by XBOOLE_1:17;
    then
A24: rng (h+c) c= dom f2 by A19;
    then
A25: lim(h"(#)((f2/*(h+c) - f2/*c))) =Rdiff(f2,x0) by A2,A16,A18,Th15;
A26: h"(#)(f2/*(h+c) - f2/*c) is convergent by A2,A16,A18,A24;
    dom f1 /\ dom f2 c= dom f1 by XBOOLE_1:17;
    then
A27: rng (h+c) c= dom f1 by A19;
A28: (h"(#)(f1/*(h+c) - f1/*c) - h"(#)(f2/*(h+c) - f2/*c)) = h"(#)(f1/*(h+
    c) -f1/*c - (f2/*(h+c) - f2/*c)) by SEQ_1:21;
A29: h"(#)(f1/*(h+c) - f1/*c) is convergent by A1,A16,A18,A27;
    then (h"(#)(f1/*(h+c) - f1/*c) - h"(#)(f2/*(h+c) - f2/*c)) is convergent
    by A26;
    hence h"(#)((f1-f2)/*(h+c) - (f1-f2)/*c) is convergent by A28,A20,
FUNCT_2:63;
    lim(h"(#)((f1/*(h+c) - f1/*c))) =Rdiff(f1,x0) by A1,A16,A18,A27,Th15;
    hence thesis by A29,A26,A25,A28,A23,SEQ_2:12;
  end;
  [.x0,x0+r.] c= dom (f1 - f2) by A14,VALUED_1:12;
  hence thesis by A7,A15,Th15;
end;

theorem
  f1 is_right_differentiable_in x0 & f2 is_right_differentiable_in x0
implies f1(#)f2 is_right_differentiable_in x0 & Rdiff(f1(#)f2,x0) = Rdiff(f1,x0
  )*f2.x0 + Rdiff(f2,x0)*f1.x0
proof
  assume that
A1: f1 is_right_differentiable_in x0 and
A2: f2 is_right_differentiable_in x0;
A3: x0 + 0 =x0;
  consider r2 such that
A4: r2>0 and
A5: [.x0,x0+r2.] c=dom f2 by A2;
  consider r1 such that
A6: r1>0 and
A7: [.x0,x0+r1.] c= dom f1 by A1;
  set r = min (r1,r2);
  0 <= r by A6,A4,XXREAL_0:15;
  then
A8: x0 <= x0 + r by A3,XREAL_1:7;
  r<=r2 by XXREAL_0:17;
  then
A9: x0 + r <= x0 + r2 by XREAL_1:7;
  then x0 + r in {g: x0 <= g & g <= x0 +r2} by A8;
  then
A10: x0 + r in [.x0,x0+r2.] by RCOMP_1:def 1;
  x0 <= x0 + r2 by A8,A9,XXREAL_0:2;
  then x0 in [.x0,x0+r2.] by XXREAL_1:1;
  then [.x0,x0+r.] c= [.x0,x0+r2.] by A10,XXREAL_2:def 12;
  then
A11: [.x0,x0+r.] c= dom f2 by A5;
  r<=r1 by XXREAL_0:17;
  then
A12: x0 + r <= x0 + r1 by XREAL_1:7;
  then x0 + r in {g: x0 <= g & g <= x0 +r1} by A8;
  then
A13: x0 + r in [.x0,x0+r1.] by RCOMP_1:def 1;
  x0 <= x0+r1 by A12,A8,XXREAL_0:2;
  then x0 in [.x0,x0+r1.] by XXREAL_1:1;
  then [.x0,x0+r.] c= [.x0,x0+r1.] by A13,XXREAL_2:def 12;
  then
A14: [.x0,x0+r.] c= dom f1 by A7;
A15: 0<r by A6,A4,XXREAL_0:15;
A16: for h,c st rng c = {x0} & rng (h+c) c= dom (f1(#)f2) &
(for n being Nat holds h.n
> 0 ) holds h"(#)((f1(#)f2)/*(h+c) - (f1(#)f2)/*c) is convergent & lim(h"(#)((
  f1(#)f2)/*(h+c) - (f1(#) f2)/*c))=Rdiff(f1,x0)*f2.x0 + Rdiff(f2,x0)*f1.x0
  proof
    let h,c;
    assume that
A17: rng c = {x0} and
A18: rng (h+c) c= dom (f1(#)f2) and
A19: for n being Nat holds h.n > 0;
A20: rng (h + c) c= dom f1 /\ dom f2 by A18,VALUED_1:def 4;
    x0 + 0 <= x0 +r by A15,XREAL_1:7;
    then
A21: x0 in [.x0,x0+ r.] by XXREAL_1:1;
    then
A22: x0 in dom f2 by A11;
A23: rng c c=dom f2
    by A17,A22,TARSKI:def 1;
A24: for m holds c.m = x0
    proof
      let m;
      c.m in rng c by VALUED_0:28;
      hence thesis by A17,TARSKI:def 1;
    end;
A25: for g be Real st 0<g
   ex n being Nat st for m being Nat st n <= m holds |.(f2/*c)
    .m - f2.x0 .|<g
    proof
      let g be Real such that
A26:  0<g;
      take n=0;
      let m being Nat such that
      n <= m;
A27:   m in NAT by ORDINAL1:def 12;
      |.(f2/*c).m - f2.x0 .| = |.f2.(c.m) - f2.x0 .| by A23,FUNCT_2:108,A27
        .=|. f2.x0 - f2.x0 .| by A24,A27
        .= 0 by ABSVALUE:def 1;
      hence thesis by A26;
    end;
    then
A28: f2/*c is convergent by SEQ_2:def 6;
    dom f1 /\ dom f2 c=dom f2 by XBOOLE_1:17;
    then
A29: rng (h + c) c= dom f2 by A20;
    then
A30: lim(h"(#)(f2/*(h+c) - f2/*c)) = Rdiff(f2,x0) by A2,A17,A19,Th15;
    now
      let n;
A31:  h.n <> 0 by A19;
      thus (h(#)(h"(#)(f1/*(h+c) - f1/*c))).n =((h(#)h")(#)(f1/*(h+c) - f1/*c)
      ). n by SEQ_1:14
        .= (h(#)h").n*(f1/*(h+c) - f1/*c).n by SEQ_1:8
        .= h.n*(h").n*(f1/*(h+c) - f1/*c).n by SEQ_1:8
        .= h.n*(h.n)"*(f1/*(h+c) - f1/*c).n by VALUED_1:10
        .= 1*(f1/*(h+c) - f1/*c).n by A31,XCMPLX_0:def 7
        .= (f1/*(h+c) - f1/*c).n;
    end;
    then
A32: h(#)(h"(#)(f1/*(h+c) - f1/*c)) =(f1/*(h+c) - f1/*c) by FUNCT_2:63;
A33: x0 in dom f1 by A14,A21;
A34: rng c c=dom f1
    by A17,A33,TARSKI:def 1;
A35: for g be Real st 0<g
   ex n being Nat st for m being Nat st n <= m holds |.(f1/*c)
    .m - f1.x0 .|<g
    proof
      let g be Real such that
A36:  0<g;
      take n=0;
      let m being Nat such that
      n <= m;
A37:    m in NAT by ORDINAL1:def 12;
      |.(f1/*c).m - f1.x0 .| = |.f1.(c.m) - f1.x0 .| by A34,FUNCT_2:108,A37
        .=|. f1.x0 - f1.x0 .| by A24,A37
        .= 0 by ABSVALUE:def 1;
      hence thesis by A36;
    end;
    then
A38: f1/*c is convergent by SEQ_2:def 6;
    dom f1 /\ dom f2 c= dom f1 by XBOOLE_1:17;
    then
A39: rng (h + c) c= dom f1 by A20;
    then
A40: lim(h"(#)(f1/*(h+c) - f1/*c)) = Rdiff(f1,x0) by A1,A17,A19,Th15;
A41: h"(#)(f1/*(h+c) - f1/*c) is convergent by A1,A17,A19,A39;
    then
A42: h"(#) (f1/*(h+c) - f1/*c) (#) (f2/*c) is convergent by A28;
A43: rng c c= dom f1 /\ dom f2 by A34,A23,XBOOLE_1:19;
A44: now
      let n;
      thus (h"(#)((f1(#)f2)/*(h+c) - (f1(#)f2)/*c)).n = ((h").n) * ((f1(#)f2)
      /*(h+c) - (f1(#)f2)/*c).n by SEQ_1:8
        .= ((h").n) * (((f1(#)f2)/*(h+c)).n - ((f1(#)f2)/*c).n) by RFUNCT_2:1
        .= h".n * (((f1/*(h+c))(#)(f2/*(h+c))).n - ((f1(#)f2)/*c).n) by A20,
RFUNCT_2:8
        .= h".n * (((f1/*(h+c))(#)(f2/*(h+c))).n - ((f1/*c)(#)(f2/*c)).n) by
A43,RFUNCT_2:8
        .= h".n * ((f1/*(h+c)).n * (f2/*(h+c)).n - ((f1/*c)(#)(f2/*c)).n) by
SEQ_1:8
        .= h".n * ((f1/*(h+c)).n * (f2/*(h+c)).n - ((f1/*c).n * (f2/*c).n))
      by SEQ_1:8
        .= h".n * ((f2/*(h+c)).n - (f2/*c).n)*(f1/*(h+c)).n + (h".n * ((f1/*
      (h+c)).n - (f1/*c).n))*(f2/*c).n
        .= h".n * (f2/*(h+c) - f2/*c).n * (f1/*(h+c)).n + (h".n * ((f1/*(h+c
      )).n - (f1/*c).n))*(f2/*c).n by RFUNCT_2:1
        .= (h"(#) (f2/*(h+c) - f2/*c)).n * (f1/*(h+c)).n + (h".n * ((f1/*(h+
      c)).n - (f1/*c).n))*(f2/*c).n by SEQ_1:8
        .= (h"(#) (f2/*(h+c) - f2/*c)).n * (f1/*(h+c)).n + (h".n * (f1/*(h+c
      ) - (f1/*c)).n)*(f2/*c).n by RFUNCT_2:1
        .= (h"(#) (f2/*(h+c) - f2/*c)).n * (f1/*(h+c)).n + (h"(#) (f1/*(h+c)
      - f1/*c)).n*(f2/*c).n by SEQ_1:8
        .= (h"(#) (f2/*(h+c) - f2/*c) (#) (f1/*(h+c))).n + (h"(#) (f1/*(h+c)
      - f1/*c)).n*(f2/*c).n by SEQ_1:8
        .= (h"(#) (f2/*(h+c) - f2/*c)(#)(f1/*(h+c))).n + (h"(#) (f1/*(h+c) -
      f1/*c)(#)(f2/*c)).n by SEQ_1:8
        .= (h"(#) (f2/*(h+c) - f2/*c)(#)(f1/*(h+c)) + h"(#) (f1/*(h+c) - f1
      /*c)(#)(f2/*c)).n by SEQ_1:7;
    end;
    then
A45: h"(#)((f1(#)f2)/*(h+c) - (f1(#)f2)/*c) = h"(#) (f2/*(h+c) - f2/*c)(#)
    (f1/*(h+c)) + h"(#) (f1/*(h+c) - f1/*c)(#)(f2/*c) by FUNCT_2:63;
    now
      let n;
      thus (f1/*c + (f1/*(h+c) - f1/*c)).n = (f1/*c).n + (f1/*(h+c) - f1/*c).n
      by SEQ_1:7
        .= (f1/*c).n + ((f1/*(h+c)).n - (f1/*c).n) by RFUNCT_2:1
        .= (f1/*(h+c)).n;
    end;
    then
A46: f1/*c + (f1/*(h+c) - f1/*c) = f1/*(h+c) by FUNCT_2:63;
A47: h is convergent & h"(#)(f1/*(h+c) - f1/*c) is convergent by A1,A17,A19,A39
;
    then h(#)(h"(#)(f1/*(h+c) - f1/*c)) is convergent;
    then
A48: f1/*(h+c) is convergent by A38,A32,A46;
    lim(h(#)(h"(#)(f1/*(h+c) - f1/*c))) =lim h *lim(h"(#)(f1/*(h+c) - f1
    /*c) ) by A47,SEQ_2:15
      .= 0;
    then
A49: 0 = lim (f1/*(h+c)) - lim(f1/*c) by A38,A32,A48,SEQ_2:12
      .= lim (f1/*(h+c)) - f1.x0 by A35,A38,SEQ_2:def 7;
A50: h"(#)(f2/*(h+c) - f2/*c) is convergent by A2,A17,A19,A29;
    then
A51: h"(#) (f2/*(h+c)-f2/*c) (#) (f1/*(h+c)) is convergent by A48;
    lim (h"(#)((f1(#)f2)/*(h+c) - (f1(#)f2)/*c)) = lim (h"(#) (f2/*(h+c)
- f2/*c)(#)(f1/*(h+c)) + h"(#) (f1/*(h+c) - f1/*c)(#) (f2/*c)) by A44,
FUNCT_2:63
      .= lim (h"(#) (f2/*(h+c) - f2/*c)(#)(f1/*(h+c))) + lim (h"(#) (f1/*(h+
    c) - f1/*c)(#)(f2/*c)) by A51,A42,SEQ_2:6
      .= lim (h"(#) (f2/*(h+c) - f2/*c))*lim(f1/*(h+c)) + lim (h"(#) (f1/*(h
    +c) - f1/*c)(#)(f2/*c)) by A50,A48,SEQ_2:15
      .= lim (h"(#) (f2/*(h+c) - f2/*c))* f1.x0 + lim (h"(#) (f1/*(h+c) - f1
    /*c))*lim(f2/*c) by A41,A49,A28,SEQ_2:15
      .= Rdiff(f1,x0)*f2.x0 + Rdiff(f2,x0)*f1.x0 by A40,A30,A25,A28,SEQ_2:def 7
;
    hence thesis by A51,A42,A45;
  end;
  [.x0,x0+r.] c= dom f1 /\ dom f2 by A14,A11,XBOOLE_1:19;
  then [.x0,x0+r.] c= dom (f1 (#) f2) by VALUED_1:def 4;
  hence thesis by A15,A16,Th15;
end;

Lm3: f1 is_right_differentiable_in x0 & f2 is_right_differentiable_in x0 & (
ex r0 st r0 > 0 & for g st g in dom f2 & g in [.x0, x0 + r0.] holds f2.g <> 0 )
implies f1/f2 is_right_differentiable_in x0 & Rdiff(f1/f2,x0) =(Rdiff(f1,x0)*f2
.x0 - Rdiff(f2,x0)*f1.x0)/(f2.x0)^2
proof
  assume that
A1: f1 is_right_differentiable_in x0 and
A2: f2 is_right_differentiable_in x0;
  consider r2 such that
A3: 0 < r2 and
A4: [.x0,x0 + r2.] c= dom f2 by A2;
  consider r1 such that
A5: 0 < r1 and
A6: [.x0,x0 + r1.] c= dom f1 by A1;
  given r0 such that
A7: r0 > 0 and
A8: for g st g in dom f2 & g in [.x0,x0 + r0.] holds f2.g <> 0;
A9: 0 + x0 =x0;
  set r3 = min(r0,r2);
  0 <= r3 by A7,A3,XXREAL_0:15;
  then
A10: x0 <= x0 +r3 by A9,XREAL_1:6;
  r3 <= r2 by XXREAL_0:17;
  then
A11: x0 + r3 <= x0 + r2 by XREAL_1:7;
  then x0 <= x0 + r2 by A10,XXREAL_0:2;
  then
A12: x0 in [.x0,x0 + r2.] by XXREAL_1:1;
  x0 + r3 in { g:x0 <= g & g <= x0 + r2 } by A10,A11;
  then x0 + r3 in [.x0,x0 +r2.] by RCOMP_1:def 1;
  then [.x0,x0 + r3.] c= [.x0,x0 + r2.] by A12,XXREAL_2:def 12;
  then
A13: [.x0,x0 + r3.] c= dom f2 by A4;
  r3 <= r0 by XXREAL_0:17;
  then
A14: x0 + r3 <= x0 + r0 by XREAL_1:7;
  then x0 <= x0 +r0 by A10,XXREAL_0:2;
  then
A15: x0 in [.x0,x0 + r0.] by XXREAL_1:1;
A16: x0 +0 = x0;
  set r = min(r1,r3);
A17: 0 < r3 by A7,A3,XXREAL_0:15;
  then 0 <= r by A5,XXREAL_0:15;
  then
A18: x0 <= x0 + r by A16,XREAL_1:7;
  r <= r3 by XXREAL_0:17;
  then
A19: x0 + r <= x0 + r3 by XREAL_1:7;
  then x0 <= x0 + r3 by A18,XXREAL_0:2;
  then
A20: x0 in [.x0,x0 + r3.] by XXREAL_1:1;
  x0 + r3 in { g: x0 <= g & g<= x0 + r0 } by A10,A14;
  then x0 + r3 in [.x0,x0 + r0.] by RCOMP_1:def 1;
  then
A21: [.x0,x0 +r3.] c= [.x0,x0 +r0.] by A15,XXREAL_2:def 12;
  x0 + r in {g:x0 <= g & g <= x0 + r3} by A18,A19;
  then x0 + r in [.x0,x0 +r3.] by RCOMP_1:def 1;
  then
A22: [.x0,x0 + r.] c= [.x0,x0 +r3.] by A20,XXREAL_2:def 12;
  [.x0,x0 + r.] c= dom(f2^)
  proof
    assume not thesis;
    then consider x being object such that
A23: x in [.x0,x0 + r.] and
A24: not x in dom (f2^);
    reconsider x as Real by A23;
A25: x in [.x0,x0 + r3.] by A22,A23;
A26: not x in dom f2 \ f2"{0} by A24,RFUNCT_1:def 2;
    now
      per cases by A26,XBOOLE_0:def 5;
      suppose
        not x in dom f2;
        hence contradiction by A13,A25;
      end;
      suppose
A27:    x in f2"{0};
        then f2.x in {0} by FUNCT_1:def 7;
        then
A28:    f2.x = 0 by TARSKI:def 1;
        x in dom f2 by A27,FUNCT_1:def 7;
        hence contradiction by A8,A21,A25,A28;
      end;
    end;
    hence contradiction;
  end;
  then
A29: [.x0,x0 + r.] c= dom f2\f2"{0} by RFUNCT_1:def 2;
  r <= r1 by XXREAL_0:17;
  then
A30: x0 + r <= x0 + r1 by XREAL_1:7;
  then x0 <= x0 + r1 by A18,XXREAL_0:2;
  then
A31: x0 in [.x0,x0 +r1.] by XXREAL_1:1;
  x0 + r in { g:x0 <= g & g <= x0 + r1 } by A18,A30;
  then x0 + r in [.x0,x0 + r1.] by RCOMP_1:def 1;
  then [.x0,x0 +r.] c= [.x0,x0 + r1.] by A31,XXREAL_2:def 12;
  then
A32: [.x0,x0 + r.] c= dom f1 by A6;
  then [.x0,x0 + r.] c= dom f1 /\ (dom f2\f2"{0}) by A29,XBOOLE_1:19;
  then
A33: [.x0,x0 + r.] c= dom (f1/f2) by RFUNCT_1:def 1;
A34: for h,c st rng c = {x0} & rng (h+c) c= dom (f1/f2) &
(for n being Nat holds h.n >
0) holds h"(#)((f1/f2)/*(h+c) - (f1/f2)/*c) is convergent & lim(h"(#)((f1/f2)/*
  (h+c) - (f1/f2)/*c)) = (Rdiff(f1,x0)*f2.x0 - Rdiff(f2,x0)*f1.x0)/(f2.x0)^2
  proof
    let h,c;
    assume that
A35: rng c = {x0} and
A36: rng (h+c) c= dom (f1/f2) and
A37: for n being Nat holds h.n > 0;
A38: rng (h + c) c= dom f1 /\ (dom f2\f2"{0}) by A36,RFUNCT_1:def 1;
    0 <= r & x0 + 0 = x0 by A5,A17,XXREAL_0:15;
    then x0 <= x0 + r by XREAL_1:7;
    then
A39: x0 in [.x0,x0 + r.] by XXREAL_1:1;
    then
A40: x0 in dom f1 by A32;
A41: rng c c= dom f1
    by A35,A40,TARSKI:def 1;
    dom f1 /\ (dom f2\f2"{0}) c= dom f1 by XBOOLE_1:17;
    then
A42: rng (h + c) c= dom f1 by A38;
    then
A43: lim(h"(#)(f1/*(h+c) - f1/*c)) = Rdiff(f1,x0) by A1,A35,A37,Th15;
A44: x0 in (dom f2\f2"{0}) by A29,A39;
    rng c c= (dom f2\f2"{0})
    by A35,A44,TARSKI:def 1;
    then
A45: rng c c= dom (f2^) by RFUNCT_1:def 2;
    then
A46: rng c c= dom f1 /\ dom (f2^) by A41,XBOOLE_1:19;
A47: h"(#)(f1/*(h+c) - f1/*c) is convergent by A1,A35,A37,A42;
A48: f2/*c is non-zero by A45,RFUNCT_2:11;
A49: now
      let n;
      thus (h"(#)((f1/*(h+c))(#)(f2/*c) - (f1/*c)(#)(f2/*(h+c)))).n = (h").n *
      ((f1/*(h+c))(#)(f2/*c) - (f1/*c)(#)(f2/*(h+c))).n by SEQ_1:8
        .= (h").n * (((f1/*(h+c))(#)(f2/*c)).n - ((f1/*c)(#) (f2/*(h+c))).n)
      by RFUNCT_2:1
        .= (h").n * ((f1/*(h+c)).n * (f2/*c).n - ((f1/*c)(#)(f2/*(h+c))).n)
      by SEQ_1:8
        .= (h").n * (((f1/*(h+c)).n - (f1/*c).n) * (f2/*c).n + ((f1/*c).n*(
      f2/*c).n) - ((f1/*c).n * (f2/*(h+c)).n)) by SEQ_1:8
        .= (h").n * ((f1/*(h+c)).n - (f1/*c).n) * (f2/*c).n - (f1/*c).n * ((
      h").n * ((f2/*(h+c)).n - (f2/*c).n))
        .= (h").n * ((f1/*(h+c)) - (f1/*c)).n * (f2/*c).n - (f1/*c).n * ((h"
      ).n * ((f2/*(h+c)).n - (f2/*c).n)) by RFUNCT_2:1
        .= (h").n * (f1/*(h+c) - (f1/*c)).n * (f2/*c).n - (f1/*c).n * ((h").
      n * (f2/*(h+c) - (f2/*c)).n) by RFUNCT_2:1
        .= (h" (#) (f1/*(h+c) - (f1/*c))).n * (f2/*c).n - (f1/*c).n * ((h").
      n * (f2/*(h+c) - (f2/*c)).n) by SEQ_1:8
        .= (h"(#)(f1/*(h+c) - (f1/*c))).n * (f2/*c).n - (f1/*c).n * (h"(#)(
      f2/*(h+c) - (f2/*c))).n by SEQ_1:8
        .= (h"(#)(f1/*(h+c) - (f1/*c))(#)(f2/*c)).n - (f1/*c).n * (h"(#)(f2
      /*(h+c) - (f2/*c))).n by SEQ_1:8
        .= (h"(#)(f1/*(h+c) - (f1/*c))(#)(f2/*c)).n - ((f1/*c)(#)(h"(#)(f2/*
      (h+c)-(f2/*c)))).n by SEQ_1:8
        .= (h"(#)(f1/*(h+c) - (f1/*c))(#)(f2/*c) - (f1/*c)(#)(h"(#) (f2/*(h+
      c)-(f2/*c)))).n by RFUNCT_2:1;
    end;
    now
      let n;
      thus (f2/*c + (f2/*(h+c) - f2/*c)).n = (f2/*c).n + (f2/*(h+c) - f2/*c).n
      by SEQ_1:7
        .= (f2/*c).n + ((f2/*(h+c)).n - (f2/*c).n) by RFUNCT_2:1
        .= (f2/*(h+c)).n;
    end;
    then
A50: f2/*c + (f2/*(h+c) - f2/*c) = f2/*(h+c) by FUNCT_2:63;
    dom f1 /\ (dom f2\f2"{0}) c=(dom f2\f2"{0}) by XBOOLE_1:17;
    then
A51: rng (h + c) c= (dom f2\f2"{0}) by A38;
    then
A52: rng (h + c) c= dom (f2^) by RFUNCT_1:def 2;
    then
A53: rng (h + c) c= dom f1 /\ dom (f2^) by A42,XBOOLE_1:19;
A54: f2/*(h+c) is non-zero by A52,RFUNCT_2:11;
    then
A55: (f2/*(h+c)) (#) (f2/*c) is non-zero by A48,SEQ_1:35;
    h"(#) ((f1/f2)/*(h+c) - (f1/f2)/*c)=h"(#)((f1(#) (f2^))/*(h+c) - (f1
    /f2)/*c) by RFUNCT_1:31
      .=h"(#)((f1(#)(f2^))/*(h+c) - (f1(#)(f2^))/*c) by RFUNCT_1:31
      .=h"(#)((f1/*(h+c))(#)((f2^)/*(h+c)) - (f1(#) (f2^))/*c) by A53,
RFUNCT_2:8
      .=h"(#)((f1/*(h+c))/"(f2/*(h+c)) - (f1(#)(f2^))/*c) by A52,RFUNCT_2:12
      .=h"(#)((f1/*(h+c))/"(f2/*(h+c)) - (f1/*c)(#) ((f2^)/*c)) by A46,
RFUNCT_2:8
      .=h"(#)((f1/*(h+c))/"(f2/*(h+c)) - (f1/*c)/"(f2/*c)) by A45,RFUNCT_2:12
      .=h"(#)(((f1/*(h+c))(#)(f2/*c) - (f1/*c)(#)(f2/*(h+c)))/"((f2/*(h+c))
    (#) (f2/*c))) by A54,A48,SEQ_1:50
      .=(h"(#)((f1/*(h+c))(#)(f2/*c) - (f1/*c)(#)(f2/*(h+c))))/"((f2/*(h+c))
    (#) (f2/*c)) by SEQ_1:41;
    then
A56: h"(#) ((f1/f2)/*(h+c) - (f1/f2)/*c) =((h"(#)(f1/*(h+c) - (f1/*c)) )
(#) (f2/*c) - (f1/*c)(#)(h"(#)(f2/*(h+c)-(f2/*c))))/"(f2/*(h+c)(#) (f2/*c)) by
A49,FUNCT_2:63;
    dom f2 \ f2"{0} c= dom f2 by XBOOLE_1:36;
    then
A57: rng (h + c) c= dom f2 by A51;
    then
A58: lim(h"(#)(f2/*(h+c) - f2/*c)) = Rdiff(f2,x0) by A2,A35,A37,Th15;
A59: h"(#)(f2/*(h+c) - f2/*c) is convergent by A2,A35,A37,A57;
    now
      let n;
A60:  h.n <> 0 by A37;
      thus (h(#)(h"(#)(f2/*(h+c) - f2/*c))).n = ((h(#)h")(#)(f2/*(h+c) - f2/*c
      )). n by SEQ_1:14
        .= (h(#)h").n *(f2/*(h+c) - f2/*c).n by SEQ_1:8
        .= h.n * (h").n *(f2/*(h+c) - f2/*c).n by SEQ_1:8
        .= h.n * (h.n)" *(f2/*(h+c) - f2/*c).n by VALUED_1:10
        .= 1*(f2/*(h+c) - f2/*c).n by A60,XCMPLX_0:def 7
        .= (f2/*(h+c) - f2/*c).n;
    end;
    then
A61: h(#)(h"(#)(f2/*(h+c) - f2/*c)) = (f2/*(h+c) - f2/*c) by FUNCT_2:63;
A62: for m holds c.m = x0
    proof
      let m;
      c.m in rng c by VALUED_0:28;
      hence thesis by A35,TARSKI:def 1;
    end;
A63: for g be Real st 0 < g
 ex n being Nat st for m being Nat st n <=m holds |.(f1/*c
    ).m - f1.x0.| < g
    proof
      let g be Real such that
A64:  0 < g;
      take n = 0;
      let m being Nat such that
      n <= m;
A65:   m in NAT by ORDINAL1: def 12;
      |.(f1/*c).m - f1.x0.| = |.f1.(c.m) - f1.x0.| by A41,FUNCT_2:108,A65
        .=|.f1.x0-f1.x0.| by A62,A65
        .= 0 by ABSVALUE:def 1;
      hence thesis by A64;
    end;
    then
A66: f1/*c is convergent by SEQ_2:def 6;
    then
A67: lim(f1/*c) = f1.x0 by A63,SEQ_2:def 7;
    dom (f2^) = dom f2 \ f2"{0} by RFUNCT_1:def 2;
    then
A68: dom (f2^) c= dom f2 by XBOOLE_1:36;
A69: for g be Real st 0 < g
ex n being Nat st for m being Nat st n <=m holds |.(f2/*
    c).m - f2.x0.| < g
    proof
      let g be Real such that
A70:  0 < g;
      take n = 0;
      let m being Nat such that
      n <= m;
A71:   m in NAT by ORDINAL1: def 12;
      |.(f2/*c).m - f2.x0.| = |.f2.(c.m) - f2.x0.| by A45,A68,FUNCT_2:108
,XBOOLE_1:1,A71
        .=|.f2.x0 - f2.x0.| by A62,A71
        .= 0 by ABSVALUE:def 1;
      hence thesis by A70;
    end;
    then
A72: f2/*c is convergent by SEQ_2:def 6;
    then
A73: lim(f2/*c) = f2.x0 by A69,SEQ_2:def 7;
    h(#)(h"(#)(f2/*(h+c) - f2/*c)) is convergent by A59;
    then
A74: f2/*(h+c) is convergent by A72,A61,A50;
    then
A75: f2/*(h+c) (#) (f2/*c) is convergent by A72;
    h"(#)(f2/*(h+c) - f2/*c) is convergent by A2,A35,A37,A57;
    then lim (h(#)(h"(#)(f2/*(h+c) - f2/*c))) = lim h *lim (h"(#)(f2/*(h+c) -
    f2/* c ) ) by SEQ_2:15
      .= 0;
    then 0 = lim (f2/*(h+c)) - f2.x0 by A72,A73,A61,A74,SEQ_2:12;
    then
A76: lim(f2/*(h+c) (#) (f2/*c)) = (f2.x0)^2 by A72,A73,A74,SEQ_2:15;
A77: lim(f2/*(h+c) (#) (f2/*c))<> 0
    proof
      assume not thesis;
      then f2.x0 = 0 by A76,XCMPLX_1:6;
      hence contradiction by A8,A4,A15,A12;
    end;
    h"(#)(f1/*(h+c) - f1/*c) is convergent by A1,A35,A37,A42;
    then
A78: h"(#) (f1/*(h+c) - f1/*c)(#)(f2/*c) is convergent by A72;
A79: (f1/*c)(#)(h"(#) (f2/*(h+c) - f2/*c)) is convergent by A59,A66;
    then
A80: ((h"(#)(f1/*(h+c) - (f1/*c)))(#)(f2/*c) - (f1/*c)(#)(h"(#) (f2/*(h+c
    )-(f2/*c)))) is convergent by A78;
    then lim(h"(#) ((f1/f2)/*(h+c) - (f1/f2)/*c)) = lim((h"(#)(f1/*(h+c) - (
f1/*c)))(#)(f2/*c) - (f1/*c)(#)(h"(#) (f2/*(h+c)-(f2/*c))))/ lim(f2/*(h+c)(#)(
    f2/*c)) by A55,A75,A77,A56,SEQ_2:24
      .=(lim((h"(#)(f1/*(h+c)-(f1/*c)))(#)(f2/*c))-lim((f1/*c)(#)(h"(#)(f2/*
    (h+c)- (f2/*c)))))/lim(f2/*(h+c)(#)(f2/*c)) by A79,A78,SEQ_2:12
      .=( lim(h"(#)(f1/*(h+c)-(f1/*c)))*lim(f2/*c) - lim((f1/*c) (#) (h"(#)(
    f2/*(h+c)-(f2/*c)))) ) / lim(f2/*(h+c)(#)(f2/*c)) by A47,A72,SEQ_2:15
      .=(Rdiff(f1,x0) * f2.x0 - Rdiff(f2,x0) * f1.x0)/(f2.x0)^2 by A43,A59,A58
,A66,A67,A73,A76,SEQ_2:15;
    hence thesis by A55,A75,A77,A80,A56,SEQ_2:23;
  end;
  0 < r by A5,A17,XXREAL_0:15;
  hence thesis by A33,A34,Th15;
end;

theorem
  f1 is_right_differentiable_in x0 & f2 is_right_differentiable_in x0 &
  f2.x0 <> 0 implies f1/f2 is_right_differentiable_in x0 & Rdiff(f1/f2,x0) = (
  Rdiff(f1,x0)*f2.x0 - Rdiff(f2,x0)*f1.x0)/(f2.x0)^2
proof
  assume that
A1: f1 is_right_differentiable_in x0 and
A2: f2 is_right_differentiable_in x0 and
A3: f2.x0 <> 0;
  consider r1 such that
A4: r1 > 0 and
  [.x0,x0 + r1.] c= dom f2 and
A5: for g st g in [.x0,x0 + r1.] holds f2.g <> 0 by A2,A3,Th7,Th8;
  now
    take r1;
    thus r1 > 0 by A4;
    let g;
    assume that
    g in dom f2 and
A6: g in [.x0,x0+r1.];
    thus f2.g <> 0 by A5,A6;
  end;
  hence thesis by A1,A2,Lm3;
end;

Lm4: f is_right_differentiable_in x0 & (ex r0 st r0 > 0 & for g st g in dom f
& g in [.x0, x0 + r0.] holds f.g <> 0) implies f^ is_right_differentiable_in x0
& Rdiff(f^,x0) = - Rdiff(f,x0)/(f.x0)^2
proof
A1: 0 + x0 =x0;
  assume
A2: f is_right_differentiable_in x0;
  then consider r2 such that
A3: 0 < r2 and
A4: [.x0,x0 + r2.] c= dom f;
  given r0 such that
A5: r0 > 0 and
A6: for g st g in dom f & g in [.x0,x0 + r0.] holds f.g <> 0;
  set r3 = min(r0,r2);
  0 <= r3 by A5,A3,XXREAL_0:15;
  then
A7: x0 <= x0 +r3 by A1,XREAL_1:6;
  r3 <= r2 by XXREAL_0:17;
  then
A8: x0 + r3 <= x0 + r2 by XREAL_1:7;
  then x0 <= x0 + r2 by A7,XXREAL_0:2;
  then
A9: x0 in [.x0,x0 + r2.] by XXREAL_1:1;
  x0 + r3 in { g:x0 <= g & g <= x0 + r2 } by A7,A8;
  then x0 + r3 in [.x0,x0 +r2.] by RCOMP_1:def 1;
  then [.x0,x0 + r3.] c= [.x0,x0 + r2.] by A9,XXREAL_2:def 12;
  then
A10: [.x0,x0 + r3.] c= dom f by A4;
  r3 <= r0 by XXREAL_0:17;
  then
A11: x0 + r3 <= x0 + r0 by XREAL_1:7;
  then x0 <= x0 +r0 by A7,XXREAL_0:2;
  then
A12: x0 in [.x0,x0 + r0.] by XXREAL_1:1;
  x0 + r3 in { g: x0 <= g & g<= x0 + r0 } by A7,A11;
  then x0 + r3 in [.x0,x0 + r0.] by RCOMP_1:def 1;
  then
A13: [.x0,x0 +r3.] c= [.x0,x0 +r0.] by A12,XXREAL_2:def 12;
A14: [.x0,x0 + r3.] c= dom(f^)
  proof
    assume not thesis;
    then consider x being object such that
A15: x in [.x0,x0 + r3.] and
A16: not x in dom (f^);
    reconsider x as Real by A15;
A17: not x in dom f \ f"{0} by A16,RFUNCT_1:def 2;
    now
      per cases by A17,XBOOLE_0:def 5;
      suppose
        not x in dom f;
        hence contradiction by A10,A15;
      end;
      suppose
A18:    x in f"{0};
        then f.x in {0} by FUNCT_1:def 7;
        then
A19:    f.x = 0 by TARSKI:def 1;
        x in dom f by A18,FUNCT_1:def 7;
        hence contradiction by A6,A13,A15,A19;
      end;
    end;
    hence contradiction;
  end;
A20: x0 in [. x0, x0 + r3 .] by A7,XXREAL_1:1;
A21: for h,c st rng c = {x0} & rng (h+c) c= dom (f^) &
 (for n being Nat holds h.n > 0)
holds h"(#)((f^)/*(h+c) - (f^)/*c) is convergent & lim(h"(#)((f^)/*(h+c) - (f^)
  /*c)) = - Rdiff(f,x0)/(f.x0)^2
  proof
    let h,c;
    assume that
A22: rng c = {x0} and
A23: rng (h+c) c= dom (f^) and
A24: for n being Nat holds h.n > 0;
A25: for m holds c.m = x0
    proof
      let m;
      c.m in rng c by VALUED_0:28;
      hence thesis by A22,TARSKI:def 1;
    end;
A26: dom f \ f"{0} c= dom f by XBOOLE_1:36;
    rng (h + c) c= dom f\f"{0} by A23,RFUNCT_1:def 2;
    then
A27: rng (h + c) c= dom f by A26;
    then
A28: lim(h"(#)(f/*(h+c) - f/*c)) = Rdiff(f,x0) by A2,A22,A24,Th15;
A29: h"(#)(f/*(h+c) - f/*c) is convergent by A2,A22,A24,A27;
    then
A30: -(h"(#)((f/*(h+c)) - (f/*c))) is convergent;
    x0 in dom (f^) by A20,A14;
    then
A31: x0 in (dom f\f"{0}) by RFUNCT_1:def 2;
    rng c c= (dom f\f"{0})
    by A22,A31,TARSKI:def 1;
    then
A32: rng c c= dom (f^) by RFUNCT_1:def 2;
    then
A33: f/*c is non-zero by RFUNCT_2:11;
    now
      let n;
A34:  h.n <> 0 by A24;
      thus (h(#)(h"(#)(f/*(h+c) - f/*c))).n = ((h(#)h")(#)(f/*(h+c) - f/*c)).n
      by SEQ_1:14
        .= (h(#)h").n *(f/*(h+c) - f/*c).n by SEQ_1:8
        .= h.n * (h").n *(f/*(h+c) - f/*c).n by SEQ_1:8
        .= h.n * (h.n)" *(f/*(h+c) - f/*c).n by VALUED_1:10
        .= 1*(f/*(h+c) - f/*c).n by A34,XCMPLX_0:def 7
        .= (f/*(h+c) - f/*c).n;
    end;
    then
A35: h(#)(h"(#)(f/*(h+c) - f/*c)) = (f/*(h+c) - f/*c) by FUNCT_2:63;
A36: f/*(h+c) is non-zero by A23,RFUNCT_2:11;
    then
A37: (f/*(h+c)) (#) (f/*c) is non-zero by A33,SEQ_1:35;
    now
      let n;
      thus (f/*c + (f/*(h+c) - f/*c)).n = (f/*c).n + (f/*(h+c) - f/*c).n by
SEQ_1:7
        .= (f/*c).n + ((f/*(h+c)).n - (f/*c).n) by RFUNCT_2:1
        .= (f/*(h+c)).n;
    end;
    then
A38: f/*c + (f/*(h+c) - f/*c) = f/*(h+c) by FUNCT_2:63;
    dom (f^) = dom f \ f"{0} by RFUNCT_1:def 2;
    then
A39: dom (f^) c= dom f by XBOOLE_1:36;
A40: for g be Real st 0 < g
  ex n being Nat st for m being Nat st n <=m holds |.(f/*c)
    .m - f.x0.| < g
    proof
      let g be Real such that
A41:  0 < g;
      take n = 0;
      let m being Nat such that
      n <= m;
A42:   m in NAT by ORDINAL1:def 12;
      |.(f/*c).m - f.x0.| = |.f.(c.m) - f.x0.| by A32,A39,FUNCT_2:108
,XBOOLE_1:1,A42
        .=|.f.x0 - f.x0.| by A25,A42
        .= 0 by ABSVALUE:def 1;
      hence thesis by A41;
    end;
    then
A43: f/*c is convergent by SEQ_2:def 6;
    then
A44: lim(f/*c) = f.x0 by A40,SEQ_2:def 7;
    h(#)(h"(#)(f/*(h+c) - f/*c)) is convergent by A29;
    then
A45: f/*(h+c) is convergent by A43,A35,A38;
    lim (h(#)(h"(#)(f/*(h+c) - f/*c))) = lim h *lim (h"(#)(f/*(h+c) - f/*
    c)) by A29,SEQ_2:15
      .= 0;
    then 0 = lim (f/*(h+c)) - f.x0 by A43,A44,A35,A45,SEQ_2:12;
    then
A46: lim(f/*(h+c) (#) (f/*c)) = (f.x0)^2 by A43,A44,A45,SEQ_2:15;
A47: lim(f/*(h+c) (#) (f/*c))<> 0
    proof
      assume not thesis;
      then f.x0 = 0 by A46,XCMPLX_1:6;
      hence contradiction by A6,A4,A12,A9;
    end;
    now
      let n;
A48:  (f/*(h+c)).n <>0 & (f/*c).n <>0 by A36,A33,SEQ_1:5;
      thus (h"(#) ((f^)/*(h+c) - (f^)/*c)).n = (h").n* ((f^)/*(h+c) - (f^)/*c)
      .n by SEQ_1:8
        .= (h").n* (((f^)/*(h+c)).n - ((f^)/*c).n) by RFUNCT_2:1
        .= (h").n* (((f/*(h+c))").n - ((f^)/*c).n) by A23,RFUNCT_2:12
        .= (h").n* (((f/*(h+c))").n - ((f/*c)").n) by A32,RFUNCT_2:12
        .= (h").n* (((f/*(h+c)).n)" - ((f/*c)").n) by VALUED_1:10
        .= (h").n* (((f/*(h+c)).n)" - ((f/*c).n)") by VALUED_1:10
        .= (h").n* (1/(f/*(h+c)).n - ((f/*c).n)") by XCMPLX_1:215
        .= (h").n* (1/(f/*(h+c)).n - 1/(f/*c).n) by XCMPLX_1:215
        .= (h").n* ((1*((f/*c).n) - 1*((f/*(h+c)).n))/((f/*(h+c)).n*(f/*c).n
      )) by A48,XCMPLX_1:130
        .= (h").n* ((-((f/*(h+c)).n - (f/*c).n))/((f/*(h+c))(#)(f/*c)).n) by
SEQ_1:8
        .= (h").n* ((-((f/*(h+c) - (f/*c)).n))/((f/*(h+c))(#)(f/*c)).n) by
RFUNCT_2:1
        .= (h").n*(-(((f/*(h+c) - (f/*c)).n)/((f/*(h+c))(#)(f/*c)).n)) by
XCMPLX_1:187
        .= -((h").n*(((f/*(h+c) - (f/*c)).n)/(((f/*(h+c))(#)(f/*c)).n)))
        .= -((h").n*((f/*(h+c) - (f/*c)).n))/((f/*(h+c))(#)(f/*c)).n by
XCMPLX_1:74
        .= -( ((h" (#) ((f/*(h+c)) - (f/*c))).n) )/((f/*(h+c))(#)(f/*c)).n
      by SEQ_1:8
        .= -(((h"(#)((f/*(h+c)) - (f/*c))).n))*(((f/*(h+c))(#) (f/*c)).n)"
      by XCMPLX_0:def 9
        .= -((((h"(#)((f/*(h+c)) - (f/*c))).n))*(((f/*(h+c))(#) (f/*c))").n)
      by VALUED_1:10
        .= -(((h")(#)((f/*(h+c)) - (f/*c)))/"((f/*(h+c))(#)(f/*c))).n by
SEQ_1:8
        .= (-((h"(#)((f/*(h+c)) - (f/*c)))/"((f/*(h+c))(#)(f/*c)))).n by
SEQ_1:10
        .= ((-(h"(#)((f/*(h+c)) - (f/*c))))/"((f/*(h+c))(#)(f/*c))).n by
SEQ_1:48;
    end;
    then
A49: h"(#) ((f^)/*(h+c) - (f^)/*c) = (-(h"(#)((f/*(h+c)) - (f/*c))))/"((f
    /*(h+c ))(#) (f/*c)) by FUNCT_2:63;
A50: f/*(h+c) (#) (f/*c) is convergent by A43,A45;
    then
    lim(h"(#) ((f^)/*(h+c) - (f^)/*c)) = lim(-(h"(#) ((f/*(h+c))- (f/*c))
    ))/(f.x0)^2 by A37,A46,A47,A30,A49,SEQ_2:24
      .=(- Rdiff(f,x0)) /(f.x0)^2 by A29,A28,SEQ_2:10
      .=- Rdiff(f,x0) /(f.x0)^2 by XCMPLX_1:187;
    hence thesis by A37,A50,A47,A30,A49,SEQ_2:23;
  end;
  0 < r3 by A5,A3,XXREAL_0:15;
  hence thesis by A14,A21,Th15;
end;

theorem
  f is_right_differentiable_in x0 & f.x0 <> 0 implies f^
  is_right_differentiable_in x0 & Rdiff(f^,x0) = - Rdiff(f,x0)/(f.x0)^2
proof
  assume that
A1: f is_right_differentiable_in x0 and
A2: f.x0 <> 0;
  consider r1 such that
A3: r1 > 0 and
  [.x0,x0 + r1.] c= dom f and
A4: for g st g in [.x0,x0 + r1.] holds f.g <> 0 by A1,A2,Th7,Th8;
  now
    take r1;
    thus r1 > 0 by A3;
    let g;
    assume that
    g in dom f and
A5: g in [.x0,x0+r1.];
    thus f.g <> 0 by A4,A5;
  end;
  hence thesis by A1,Lm4;
end;

theorem
  f is_right_differentiable_in x0 & f is_left_differentiable_in x0 &
Rdiff(f,x0) = Ldiff(f,x0) implies f is_differentiable_in x0 & diff(f,x0)=Rdiff(
  f,x0) & diff(f,x0)=Ldiff(f,x0)
proof
  assume that
A1: f is_right_differentiable_in x0 and
A2: f is_left_differentiable_in x0 and
A3: Rdiff(f,x0) = Ldiff(f,x0);
A4: ex N being Neighbourhood of x0 st N c= dom f
  proof
    consider r2 such that
A5: r2>0 and
A6: [.x0,x0+r2.] c= dom f by A1;
    consider r1 such that
A7: r1>0 and
A8: [.x0-r1,x0.] c= dom f by A2;
    set r = min(r1,r2);
    r > 0 by A7,A5,XXREAL_0:15;
    then reconsider N = ].x0 -r,x0+r.[ as Neighbourhood of x0 by RCOMP_1:def 6;
    take N;
    let x be object;
    assume x in N;
    then x in { g: x0 - r < g & g < x0 + r} by RCOMP_1:def 2;
    then consider g such that
A9: g = x and
A10: x0 - r < g and
A11: g < x0 + r;
    now
      per cases;
      suppose
A12:    g <= x0;
        r <= r1 by XXREAL_0:17;
        then x0 - r1 <= x0 - r by XREAL_1:13;
        then x0 - r1 <= g by A10,XXREAL_0:2;
        then g in {g1: x0 - r1 <= g1 & g1 <= x0} by A12;
        then g in [.x0-r1,x0.] by RCOMP_1:def 1;
        hence thesis by A8,A9;
      end;
      suppose
A13:    g > x0;
        r <= r2 by XXREAL_0:17;
        then x0 + r <= x0 + r2 by XREAL_1:7;
        then g <= x0 + r2 by A11,XXREAL_0:2;
        then g in {g1: x0 <= g1 & g1 <= x0+r2} by A13;
        then g in [.x0,x0+r2.] by RCOMP_1:def 1;
        hence thesis by A6,A9;
      end;
    end;
    hence thesis;
  end;
  for h,c st rng c = {x0} & rng (h + c) c= dom f holds h"(#)(f/*(h+c) - f
  /*c) is convergent & lim (h"(#) (f/*(h+c) - f/*c)) = Ldiff(f,x0)
  proof
    let h,c;
    assume that
A14: rng c = {x0} and
A15: rng (h + c) c= dom f;
A16: rng c c= dom f
    proof
      consider S being Neighbourhood of x0 such that
A17:  S c= dom f by A4;
      x0 in S by RCOMP_1:16;
      hence thesis by A14,A17,ZFMISC_1:31;
    end;
    now
      per cases;
      suppose
        ex N be Element of NAT st for n st n >= N holds h.n > 0;
        then consider N be Element of NAT such that
A18:    for n st n >= N holds h.n > 0;
        set h1 = h ^\N;
A19:    for n being Nat holds h1.n > 0
        proof
          let n be Nat;
          h1.n = h.(n+N) & N + 0 <= n + N by NAT_1:def 3,XREAL_1:7;
          hence thesis by A18;
        end;
        set c1 = c ^\N;
A20:    rng c1 = {x0}
        proof
          thus rng c1 c= {x0} by A14,VALUED_0:21;
          let x be object;
A21:      c.N in rng c by VALUED_0:28;
          assume x in {x0};
          then
A22:      x = x0 by TARSKI:def 1;
          c1.0 = c.(0+N) by NAT_1:def 3
            .= c.N;
          then c1.0 = x by A14,A22,A21,TARSKI:def 1;
          hence thesis by VALUED_0:28;
        end;
A23:    h1 + c1 = (h + c)^\N by SEQM_3:15;
        then
A24:    h1"(#)(f/*(h1+c1) - f/*c1) = h1"(#)((f/*(h+c))^\N - f/*c1) by A15,
VALUED_0:27
          .= h1"(#)((f/*(h+c))^\N - (f/*c)^\N) by A16,VALUED_0:27
          .= h1"(#)((f/*(h+c) - f/*c)^\N) by SEQM_3:17
          .= ((h")^\N) (#)((f/*(h+c) - f/*c)^\N) by SEQM_3:18
          .= (h"(#)(f/*(h+c) - f/*c))^\N by SEQM_3:19;
        rng (h1 + c1) c= rng (h + c) by A23,VALUED_0:21;
        then
A25:    rng (h1 + c1) c= dom f by A15;
        then
A26:    h1"(#)(f/*(h1+c1) - f/*c1) is convergent by A1,A20,A19;
        hence h"(#)(f/*(h+c) - f/*c) is convergent by A24,SEQ_4:21;
        lim (h1"(#)(f/*(h1+c1) - f/*c1)) = Rdiff(f,x0) by A1,A20,A25,A19,Th15;
        hence lim (h"(#)(f/*(h+c) - f/*c)) =Ldiff(f,x0) by A3,A26,A24,SEQ_4:22;
      end;
      suppose
A27:    for N be Element of NAT ex n st n >= N & h.n <= 0;
        now
          per cases;
          suppose
            ex M be Element of NAT st for m st m >= M holds h.m < 0;
            then consider M be Element of NAT such that
A28:        for n st n >= M holds h.n < 0;
            set h1 = h ^\M;
A29:        for n being Nat holds h1.n < 0
            proof
              let n be Nat;
              h1.n = h.(n+M) & M + 0 <= n + M by NAT_1:def 3,XREAL_1:7;
              hence thesis by A28;
            end;
            set c1 = c ^\M;
A30:        rng c1 = {x0}
            proof
              thus rng c1 c= {x0} by A14,VALUED_0:21;
              let x be object;
A31:          c.M in rng c by VALUED_0:28;
              assume x in {x0};
              then
A32:          x = x0 by TARSKI:def 1;
              c1.0 = c.(0+M) by NAT_1:def 3
                .= c.M;
              then c1.0 = x by A14,A32,A31,TARSKI:def 1;
              hence thesis by VALUED_0:28;
            end;
A33:        h1 + c1 = (h + c)^\M by SEQM_3:15;
            then
A34:        h1"(#)(f/*(h1+c1) - f/*c1) = h1"(#)((f/*(h+c))^\M - f/*c1) by A15,
VALUED_0:27
              .= h1"(#)((f/*(h+c))^\M - (f/*c)^\M) by A16,VALUED_0:27
              .= h1"(#)((f/*(h+c) - f/*c)^\M) by SEQM_3:17
              .= ((h")^\M) (#)((f/*(h+c) - f/*c)^\M) by SEQM_3:18
              .= (h"(#)(f/*(h+c) - f/*c))^\M by SEQM_3:19;
            rng (h1 + c1) c= rng (h + c) by A33,VALUED_0:21;
            then
A35:        rng (h1 + c1) c= dom f by A15;
            then
A36:        h1"(#)(f/*(h1+c1) - f/*c1) is convergent by A2,A30,A29;
            hence h"(#)(f/*(h+c) - f/*c) is convergent by A34,SEQ_4:21;
            lim (h1"(#)(f/*(h1+c1) - f/*c1)) = Ldiff(f,x0) by A2,A30,A35,A29
,Th9;
            hence lim (h"(#)(f/*(h+c) - f/*c)) =Ldiff(f,x0) by A36,A34,SEQ_4:22
;
          end;
          suppose
A37:        for M be Element of NAT ex m st m >= M & h.m >= 0;
            set s = (h")(#)(f/*(h+c)-f/*c);
            defpred R[Real] means $1 > 0;
            defpred P[Real] means $1 < 0;
A38:        for N be Element of NAT ex n st n >= N & P[h.n]
            proof
              let m;
              consider n such that
A39:          n >= m and
A40:          h.n <= 0 by A27;
              take n;
              thus n >= m by A39;
              h.n <> 0 by SEQ_1:5;
              hence thesis by A40;
            end;
            consider q1 being increasing sequence of NAT such that
A41:        (for n being Nat holds P[(h*q1).n]) &
             for n st (for r st r = h.n
            holds P[r]) ex m st n = q1.m from FDIFF_2:sch 1(A38);
A42:        for N be Element of NAT ex n st n >= N & R[h.n]
            proof
              let m;
              consider n such that
A43:          n >= m and
A44:          h.n >= 0 by A37;
              take n;
              thus n >= m by A43;
              h.n <> 0 by SEQ_1:5;
              hence thesis by A44;
            end;
            consider q2 being increasing sequence of NAT such that
A45:        (for n being Nat holds R[(h*q2).n]) &
            for n st (for r st r = h.n
            holds R[r]) ex m st n = q2.m from FDIFF_2:sch 1(A42);
            set h1 = h*q1;
            reconsider h1 as subsequence of h;
A46:        h1 is convergent by SEQ_4:16;
A47:        lim h = 0;
            then
A48:        lim h1 = 0 by SEQ_4:17;
            set h2 = h*q2;
A49:        h2 is convergent by SEQ_4:16;
            lim h2 = 0 by A47,SEQ_4:17;
            then reconsider h2 as 0-convergent non-zero Real_Sequence
              by A49,FDIFF_1:def 1;
            set c2 = c*q2;
A50:        rng c2 = {x0} by A14,VALUED_0:26;
            reconsider c2 as constant Real_Sequence;
            rng ((h+c)*q2) c= rng (h+c) by VALUED_0:21;
            then rng ((h+c)*q2) c= dom f by A15;
            then rng (h2+c2) c= dom f by RFUNCT_2:2;
            then
A51:        h2"(#)(f/*(h2+c2)-f/*c2) is convergent & lim(h2"(#)(f/*(h2+
            c2)-f/*c2))=Ldiff (f,x0) by A1,A3,A45,A50,Th15;
A52:        h2"(#)(f/*(h2+c2)-f/*c2) = h2"(#)(f/*((h+c)*q2)-f/*c2) by
RFUNCT_2:2
              .= h2"(#)(f/*(h+c)*q2-f/*c2) by A15,FUNCT_2:110
              .= ((h")*q2)(#)(f/*(h+c)*q2-f/*c2) by RFUNCT_2:5
              .= ((h")*q2)(#)(f/*(h+c)*q2-f/*c*q2) by A16,FUNCT_2:110
              .= ((h")*q2)(#)((f/*(h+c)-f/*c)*q2) by RFUNCT_2:2
              .= ((h")(#)(f/*(h+c)-f/*c))*q2 by RFUNCT_2:2;
            reconsider h1 as 0-convergent non-zero Real_Sequence
              by A46,A48,FDIFF_1:def 1;
            set c1 = c*q1;
A53:        rng c1 = {x0} by A14,VALUED_0:26;
            reconsider c1 as constant Real_Sequence;
            rng ((h+c)*q1) c= rng (h+c) by VALUED_0:21;
            then rng ((h+c)*q1) c= dom f by A15;
            then rng (h1+c1) c= dom f by RFUNCT_2:2;
            then
A54:        h1"(#)(f/*(h1+c1)-f/*c1) is convergent & lim(h1"(#)(f/*(h1+
            c1)-f/*c1))=Ldiff (f,x0) by A2,A41,A53,Th9;
A55:        h1"(#)(f/*(h1+c1)-f/*c1) = h1"(#)(f/*((h+c)*q1)-f/*c1) by
RFUNCT_2:2
              .= h1"(#)(f/*(h+c)*q1-f/*c1) by A15,FUNCT_2:110
              .= ((h")*q1)(#)(f/*(h+c)*q1-f/*c1) by RFUNCT_2:5
              .= ((h")*q1)(#)(f/*(h+c)*q1-f/*c*q1) by A16,FUNCT_2:110
              .= ((h")*q1)(#)((f/*(h+c)-f/*c)*q1) by RFUNCT_2:2
              .= ((h")(#)(f/*(h+c)-f/*c))*q1 by RFUNCT_2:2;
A56:        for g1 be Real st 0<g1
       ex n being Nat st for m being Nat st n<=m holds
            |.s.m - Ldiff(f,x0).|<g1
            proof
              let g1 be Real;
              assume
A57:          0 < g1;
              then consider n1 be Nat such that
A58:          for m being Nat st n1 <= m
holds |.(s*q1).m - Ldiff(f,x0).|<g1
              by A54,A55,SEQ_2:def 7;
              consider n2 be Nat such that
A59:          for m being Nat st n2 <= m
holds |.(s*q2).m - Ldiff(f,x0).|<g1
              by A51,A52,A57,SEQ_2:def 7;
              take n = max(q1.n1,q2.n2);
              let m being Nat such that
A60:          n <= m;
A61:           m in NAT by ORDINAL1:def 12;
A62:          n >= q2.n2 by XXREAL_0:25;
A63:          n >= q1.n1 by XXREAL_0:25;
                per cases;
                suppose
                  h.m > 0;
                  then for r st r = h.m holds r > 0;
                  then consider k such that
A64:              m = q2.k by A45,A61;
A65:         n2 in NAT by ORDINAL1:def 12;
                  dom q2 = NAT & q2.k >= q2.n2 by A60,A62,A64,FUNCT_2:def 1
,XXREAL_0:2;
                  then not k < n2 by VALUED_0:def 13,A65;
                  then |.(s*q2).k - Ldiff(f,x0).|<g1 by A59;
                  hence thesis by A64,FUNCT_2:15;
                end;
                suppose
A66:              h.m <= 0;
                  h.m <> 0 by SEQ_1:5;
                  then for r st r = h.m holds r < 0 by A66;
                  then consider k such that
A67:              m = q1.k by A41,A61;
A68:         n1 in NAT by ORDINAL1:def 12;
                  dom q1 = NAT & q1.k >= q1.n1 by A60,A63,A67,FUNCT_2:def 1
,XXREAL_0:2;
                  then not k < n1 by VALUED_0:def 13,A68;
                  then |.(s*q1).k - Ldiff(f,x0).|<g1 by A58;
                  hence thesis by A67,FUNCT_2:15;
                end;
              end;
            hence s is convergent by SEQ_2:def 6;
            hence lim s = Ldiff(f,x0) by A56,SEQ_2:def 7;
          end;
        end;
        hence thesis;
      end;
    end;
    hence thesis;
  end;
  hence thesis by A3,A4,FDIFF_2:12;
end;

theorem
  f is_differentiable_in x0 implies f is_right_differentiable_in x0 & f
is_left_differentiable_in x0 & diff(f,x0) = Rdiff(f,x0) & diff(f,x0) = Ldiff(f,
  x0)
proof
  assume
A1: f is_differentiable_in x0;
  then consider N be Neighbourhood of x0 such that
A2: N c= dom f by FDIFF_2:11;
  consider g1 be Real such that
A3: g1 > 0 and
A4: N = ].x0 - g1,x0 + g1.[ by RCOMP_1:def 6;
A5: g1 > g1/2 by A3,XREAL_1:216;
A6: ex r st r>0 & [.x0,x0+r.] c= dom f
  proof
    take r = g1/2;
    thus r > 0 by A3,XREAL_1:215;
    |.(x0 + g1/2) -x0 .| = g1/2 by A3,ABSVALUE:def 1;
    then
A7: x0 + r in ].x0 -g1,x0 +g1.[ by A5,RCOMP_1:1;
    x0 in ].x0 - g1, x0 + g1 .[ by A4,RCOMP_1:16;
    then [.x0,x0 +r.] c= ].x0 -g1,x0 +g1.[ by A7,XXREAL_2:def 12;
    hence thesis by A2,A4;
  end;
A8: ex r st 0 < r & [.x0 -r,x0.] c= dom f
  proof
    take r = g1/2;
    thus r > 0 by A3,XREAL_1:215;
    |.(x0 - g1/2) -x0 .| =|.-g1/2 + 0 .| .=|.g1/2 .|by COMPLEX1:52
      .=g1/2 by A3,ABSVALUE:def 1;
    then
A9: x0 - r in ].x0 -g1,x0 +g1.[ by A5,RCOMP_1:1;
    x0 in ].x0 - g1, x0 + g1 .[ by A4,RCOMP_1:16;
    then [.x0 -r,x0 .] c= ].x0 -g1,x0 +g1.[ by A9,XXREAL_2:def 12;
    hence thesis by A2,A4;
  end;
  diff(f,x0) = diff(f,x0);
  then ( for h,c st rng c = {x0} & rng (h+c) c= dom f &
  (for n being Nat holds h.n>0)
  holds h" (#)(f/*(h+c) - f/*c) is convergent & lim (h"(#) (f/*(h+c) - f/*c)) =
diff(f,x0) )& for h,c st rng c = {x0} & rng (h+c) c= dom f &
 (for n being Nat holds h.n <
  0) holds h"(#)(f/*(h+c) - f/*c) is convergent & lim(h"(#)(f/*(h+c) - f/*c)) =
  diff(f,x0) by A1,FDIFF_2:12;
  hence thesis by A6,A8,Th9,Th15;
end;