:: Inverse Trigonometric Functions Arctan and Arccot
::  by Xiquan Liang and Bing Xie
::
:: Received March 18, 2008
:: Copyright (c) 2008 Association of Mizar Users

environ

 vocabularies FUNCT_1, RELAT_1, PRE_TOPC, ARYTM_1, ARYTM_3, PARTFUN1, SIN_COS,
      FDIFF_1, SQUARE_1, FINSEQ_1, SIN_COS4, ARYTM, BOOLE, SEQ_1, RCOMP_1,
      INT_1, FCONT_1, RFUNCT_2, SIN_COS9, TAYLOR_1, PREPOWER, LIMFUNC1;
 notations TARSKI, SUBSET_1, ORDINAL1, XXREAL_0, XCMPLX_0, FUNCT_1, RELSET_1,
      PARTFUN1, RCOMP_1, SIN_COS, RFUNCT_1, SQUARE_1, VALUED_1, NUMBERS,
      REAL_1, SEQ_1, FDIFF_1, XREAL_0, INT_1, SIN_COS4, PARTFUN2, RFUNCT_2,
      FCONT_1, XBOOLE_0, TAYLOR_1, PREPOWER, LIMFUNC1;
 constructors REAL_1, SQUARE_1, RCOMP_1, RFUNCT_1, FDIFF_1, RFUNCT_2, FCONT_1,
      SIN_COS, PARTFUN2, SIN_COS4, TOPALG_2, TAYLOR_1, PREPOWER, LIMFUNC1,
      SEQ_1;
 registrations XCMPLX_0, XXREAL_0, XREAL_0, MEMBERED, RCOMP_1, RELSET_1,
      SIN_COS, FUNCT_1, SIN_COS6, RFUNCT_2, NUMBERS, INT_1, VALUED_0;
 requirements SUBSET, BOOLE, NUMERALS, ARITHM, REAL;
 definitions TARSKI, XCMPLX_0, LIMFUNC1, SIN_COS, VALUED_1, SQUARE_1;
 theorems FDIFF_2, XCMPLX_1, FDIFF_1, RELAT_1, SIN_COS, COMPTRIG, RFUNCT_2,
      FCONT_1, SIN_COS4, FUNCT_1, RCOMP_1, REAL_1, XBOOLE_0, SQUARE_1, FCONT_3,
      XREAL_1, TARSKI, XBOOLE_1, FDIFF_7, ROLLE, RFUNCT_1, REAL_2, FCONT_2,
      TAYLOR_1, PREPOWER, VALUED_1, FDIFF_4, FDIFF_5, LIMFUNC1, XXREAL_1;

begin :: arctan,arccot

reserve x, r, s, h for Real,
        a, b, p, q, th for real number,
        i for integer number,
        n for Element of NAT,
        rr, y for set,
        Z for open Subset of REAL,
        X, Y for Subset of REAL,
        f, f1, f2, g for PartFunc of REAL,REAL;

theorem Th1:
  ].-PI/2,PI/2.[ c= dom tan
proof
  ].-PI/2,PI/2.[ c= dom cos \ cos"{0}
  proof
  A1: ].-PI/2,PI/2.[ \ cos"{0} c= dom cos \ cos"{0} by SIN_COS:27,XBOOLE_1:33;
      ].-PI/2,PI/2.[ /\ cos"{0}={}
      proof
        assume ].-PI/2,PI/2.[ /\ cos"{0}<>{};
        then consider rr such that
    A2: rr in ].-PI/2,PI/2.[ /\ cos"{0} by XBOOLE_0:def 1;
    A3: rr in ].-PI/2,PI/2.[ & rr in cos"{0} by A2,XBOOLE_0:def 3;
    A4: cos.rr <>0 by A3,COMPTRIG:27;
        cos.rr in {0} by A3,FUNCT_1:def 13;
        hence contradiction by A4,TARSKI:def 1;
      end;
      then ].-PI/2,PI/2.[ misses cos"{0} by XBOOLE_0:def 7;
      hence thesis by A1,XBOOLE_1:83;
  end;
  then ].-PI/2,PI/2.[ c= dom sin /\ (dom cos \ cos"{0})
  by SIN_COS:27,XBOOLE_1:19;
  hence thesis by RFUNCT_1:def 4;
end;

theorem Th2:
  ].0,PI.[ c= dom cot
proof
  ].0,PI.[ c= dom sin \ sin"{0}
  proof
  A1: ].0,PI.[ \ sin"{0} c= dom sin \ sin"{0} by SIN_COS:27,XBOOLE_1:33;
      ].0,PI.[ /\ sin"{0}={}
      proof
        assume ].0,PI.[ /\ sin"{0}<>{};
        then consider rr such that
    A2: rr in ].0,PI.[ /\ sin"{0} by XBOOLE_0:def 1;
    A3: rr in ].0,PI.[ & rr in sin"{0} by A2,XBOOLE_0:def 3;
    A4: sin.rr <>0 by A3,COMPTRIG:23;
        sin.rr in {0} by A3,FUNCT_1:def 13;
        hence contradiction by A4,TARSKI:def 1;
      end;
      then ].0,PI.[ misses sin"{0} by XBOOLE_0:def 7;
      hence thesis by A1,XBOOLE_1:83;
   end;
   then ].0,PI.[ c= dom cos /\ (dom sin \ sin"{0})
   by SIN_COS:27,XBOOLE_1:19;
   hence thesis by RFUNCT_1:def 4;
end;

Lm1:
  tan is_differentiable_on ].-PI/2,PI/2.[
proof
    for x st x in ].-PI/2,PI/2.[ holds tan is_differentiable_in x
    proof
      let x;
      assume x in ].-PI/2,PI/2.[;
      then cos.x <> 0 by COMPTRIG:27;
      hence thesis by FDIFF_7:46;
    end;
    hence thesis by Th1,FDIFF_1:16;
end;

Lm2:
  cot is_differentiable_on ].0,PI.[
proof
    for x st x in ].0,PI.[ holds cot is_differentiable_in x
    proof
      let x;
      assume x in ].0,PI.[;
      then sin.x <> 0 by COMPTRIG:23;
      hence thesis by FDIFF_7:47;
    end;
    hence thesis by Th2,FDIFF_1:16;
end;

Lm3:
  for x st x in ].-PI/2,PI/2.[ holds diff(tan,x) = 1/(cos.x)^2
proof
  let x;
  assume x in ].-PI/2,PI/2.[;
  then cos.x <>0 by COMPTRIG:27;
  hence thesis by FDIFF_7:46;
end;

Lm4:
  for x st x in ].0,PI.[ holds diff(cot,x) = -1/(sin.x)^2
proof
  let x;
  assume x in ].0,PI.[;
  then sin.x <>0 by COMPTRIG:23;
  hence thesis by FDIFF_7:47;
end;

theorem
  tan is_differentiable_on ].-PI/2,PI/2.[ &
  for x st x in ].-PI/2,PI/2.[ holds diff(tan,x) = 1/(cos.x)^2 by Lm1,Lm3;

theorem
  cot is_differentiable_on ].0,PI.[ &
  for x st x in ].0,PI.[ holds diff(cot,x) = -1/(sin.x)^2 by Lm2,Lm4;

theorem
  tan is_continuous_on ].-PI/2,PI/2.[ by Lm1,FDIFF_1:33;

theorem
  cot is_continuous_on ].0,PI.[ by Lm2,FDIFF_1:33;

theorem Th7:
  tan is_increasing_on ].-PI/2,PI/2.[
proof
    for x be Real st x in ].-PI/2,PI/2.[ holds diff(tan,x) > 0
    proof
      let x be Real;
      assume
  A3: x in ].-PI/2,PI/2.[;
      then 0 < cos.x by COMPTRIG:27;then
      (cos.x)^2 > 0 by SQUARE_1:74;
      then 1/(cos.x)^2 > 0 /(cos.x)^2 by REAL_1:73;
      hence thesis by A3,Lm3;
    end;
    hence thesis by Lm1,ROLLE:9;
end;

theorem Th8:
  cot is_decreasing_on ].0,PI.[
proof
    PI in ].0, 4.[ by SIN_COS:def 32;then
A1: PI > 0 by XXREAL_1:4;
    for x be Real st x in ].0,PI.[ holds diff(cot,x) < 0
    proof
      let x be Real;
      assume
  A3: x in ].0,PI.[;
      then 0 < sin.x by COMPTRIG:23;then
      (sin.x)^2 > 0 by SQUARE_1:74;
      then 1/(sin.x)^2 > 0 /(sin.x)^2 by REAL_1:73;
      then -1/(sin.x)^2 < -0 by XREAL_1:26;
      hence thesis by A3,Lm4;
    end;
    hence thesis by A1,Lm2,ROLLE:10;
end;

theorem
  tan | ].-PI/2,PI/2.[ is one-to-one by Th7,FCONT_3:16;

theorem
  cot | ].0,PI.[ is one-to-one by Th8,FCONT_3:16;

registration
  cluster tan | ].-PI/2,PI/2.[ -> one-to-one;
  coherence by Th7,FCONT_3:16;
  cluster cot | ].0,PI.[ -> one-to-one;
  coherence by Th8,FCONT_3:16;
end;

definition
  func arctan -> PartFunc of REAL,REAL equals
  (tan | ].-PI/2,PI/2.[)";
  coherence;
  func arccot -> PartFunc of REAL, REAL equals
  (cot | ].0,PI.[)";
  coherence;
end;

definition let r be Real;
  func arctan r equals
  arctan.r;
  coherence;
  func arccot r equals
  arccot.r;
  coherence;
end;

definition let r be Real;
  redefine func arctan r -> Real;
  coherence;
  redefine func arccot r -> Real;
  coherence;
end;

Lm5:
  (arctan qua Function)" = tan | ].-PI/2,PI/2.[ by FUNCT_1:65;

Lm6:
  (arccot qua Function)" = cot | ].0,PI.[ by FUNCT_1:65;

theorem Th11:
  rng arctan = ].-PI/2,PI/2.[
proof
  dom (tan|].-PI/2,PI/2.[) = ].-PI/2,PI/2.[ by Th1,RELAT_1:91;
  hence thesis by FUNCT_1:55;
end;

theorem Th12:
  rng arccot = ].0,PI.[
proof
  dom (cot|].0,PI.[) = ].0,PI.[ by Th2,RELAT_1:91;
  hence thesis by FUNCT_1:55;
end;

registration
  cluster arctan -> one-to-one;
  coherence;
  cluster arccot -> one-to-one;
  coherence;
end;

definition let th be Real;
  redefine func tan th -> Real;
  coherence;
  redefine func cot th -> Real;
  coherence;
end;

Lm7:
  -PI/4 in ].-PI/2,PI/2.[
proof
    PI in ].0,4.[ by SIN_COS:def 32;then
A1: PI > 0 by XXREAL_1:4;
A3: PI/(-4) > PI/(-2) by A1,REAL_2:200;
    -PI/4 in { s where s is Real: -PI/2 < s & s < PI/2 } by A3;
    hence thesis by RCOMP_1:def 2;
end;

Lm8:
  PI/4 in ].-PI/2,PI/2.[
proof
    PI in ].0,4.[ by SIN_COS:def 32;
    then PI > 0 by XXREAL_1:4;then
A1: PI/4 < PI/2 by REAL_2:200;
    PI/4 in { s where s is Real: -PI/2 < s & s < PI/2 } by A1;
    hence thesis by RCOMP_1:def 2;
end;

Lm9:
  PI/4 in ].0,PI.[
proof
    PI in ].0,4.[ by SIN_COS:def 32;then
A1: PI > 0 by XXREAL_1:4;then
A2: PI/4 > 0/4 by XREAL_1:76;
    PI/4 < PI/1 by A1,REAL_2:200;
    hence PI/4 in ].0,PI.[ by A2,XXREAL_1:4;
end;

Lm10:
  3/4*PI in ].0,PI.[
proof
    PI in ].0,4.[ by SIN_COS:def 32;then
A1: PI > 0 by XXREAL_1:4;then
A2: (3/4)*PI > (3/4)*0 by XREAL_1:70;
    3/4*PI < PI by A1,REAL_2:145;
    hence 3/4*PI in ].0,PI.[ by A2,XXREAL_1:4;
end;

Lm11:
  dom (tan | [.-PI/4,PI/4.]) = [.-PI/4,PI/4.]
proof
  [.-PI/4,PI/4.] c= ].-PI/2,PI/2.[ by Lm7,Lm8,RCOMP_1:17;
  hence thesis by Th1,XBOOLE_1:1,RELAT_1:91;
end;

Lm12:
  dom (cot | [.PI/4,3/4*PI.]) = [.PI/4,3/4*PI.]
proof
  [.PI/4,3/4*PI.] c= ].0,PI.[ by Lm9,Lm10,RCOMP_1:17;
  hence thesis by Th2,XBOOLE_1:1,RELAT_1:91;
end;

theorem Th13:
  for x be real number st x in ].-PI/2,PI/2.[ holds tan.x = tan x
proof
    let x be real number;
    assume
A1: x in ].-PI/2,PI/2.[;
    tan.x = (sin x)/(cos x) by A1,Th1,RFUNCT_1:def 4
         .= tan x by SIN_COS4:def 1;
    hence thesis;
end;

theorem Th14:
  for x be real number st x in ].0,PI.[ holds cot.x = cot x
proof
    let x be real number;
    assume x in ].0,PI.[; then
    cot.x = (cos x)/(sin x) by Th2,RFUNCT_1:def 4
         .= cot x by SIN_COS4:def 2;
    hence thesis;
end;

theorem
  for x be Real st cos.x <> 0 holds tan.x = tan x
proof
    let x be Real;
    assume
A1: cos.x <> 0;
A2: x in dom (sin/cos)
    proof
      not x in cos"{0}
      proof
        assume x in cos"{0};
        then cos.x in {0} by FUNCT_1:def 13;
        hence contradiction by A1,TARSKI:def 1;
      end;
      then x in dom cos \ cos"{0} by SIN_COS:27,XBOOLE_0:def 4;
      then x in dom sin /\ (dom cos \ cos"{0}) by SIN_COS:27,XBOOLE_0:def 3;
      hence thesis by RFUNCT_1:def 4;
    end;
    tan.x = (sin x)/(cos x) by A2,RFUNCT_1:def 4
         .= tan x by SIN_COS4:def 1;
    hence thesis;
end;

theorem
  for x be Real st sin.x <> 0 holds cot.x = cot x
proof
    let x be Real;
    assume
A1: sin.x <> 0;
A2: x in dom (cos/sin)
    proof
      not x in sin"{0}
      proof
        assume x in sin"{0};
        then sin.x in {0} by FUNCT_1:def 13;
        hence contradiction by A1,TARSKI:def 1;
      end;
      then x in dom sin \ sin"{0} by SIN_COS:27,XBOOLE_0:def 4;
      then x in dom cos /\ (dom sin \ sin"{0}) by SIN_COS:27,XBOOLE_0:def 3;
      hence thesis by RFUNCT_1:def 4;
    end;
    cot.x = (cos x)/(sin x) by A2,RFUNCT_1:def 4
         .= cot x by SIN_COS4:def 2;
    hence thesis;
end;

theorem Th15:
  tan.(-PI/4) = -1 & tan(-PI/4) = -1
proof
A4: cos.(PI/4) <> 0 by Lm8,COMPTRIG:27;
A5: sin.(PI/4)/cos.(PI/4) = 1 by A4,SIN_COS:78,XCMPLX_1:60;
    tan.(-PI/4) = sin.(-PI/4)/(cos.(-PI/4)) by Lm7,Th1,RFUNCT_1:def 4
               .= (-sin.(PI/4))/cos.(-PI/4) by SIN_COS:33
               .= (-sin.(PI/4))/cos.(PI/4)  by SIN_COS:33
               .= -1 by A5;
    hence thesis by Lm7,Th13;
end;

theorem Th16:
  cot.(PI/4) = 1 & cot(PI/4) = 1 &
  cot.(3/4*PI) = -1 & cot(3/4*PI) = -1
proof
A4:  sin.(PI/4) <> 0 by Lm9,COMPTRIG:23;
A5:  cot.(PI/4) = cos.(PI/4)/(sin.(PI/4)) by Lm9,Th2,RFUNCT_1:def 4
               .= 1 by A4,SIN_COS:78,XCMPLX_1:60;
     cot.(3/4*PI) = cos.(3/4*PI)*(sin.(3/4*PI))"
                  by Lm10,Th2,RFUNCT_1:def 4
                 .= (-sin.(PI/4))/sin.(PI/2 + PI/4) by SIN_COS:83
                 .= (-sin.(PI/4))/cos.(PI/4) by SIN_COS:83
                 .= -sin.(PI/4)/cos.(PI/4)
                 .= -1 by A4,XCMPLX_1:60,SIN_COS:78;
     hence thesis by A5,Lm9,Lm10,Th14;
end;

theorem Th17:
  for x be set st x in [.-PI/4,PI/4.] holds
  tan.x in [.-1,1.]
proof
    let x be set;
    assume
A1: x in [.-PI/4,PI/4.];
    x in ].-PI/4,PI/4.[ \/ {-PI/4,PI/4} by A1,XXREAL_1:128;then
A3: x in ].-PI/4,PI/4.[ or x in {-PI/4,PI/4} by XBOOLE_0:def 2;
    per cases by A3,TARSKI:def 2;
      suppose
   A4:  x in ].-PI/4,PI/4.[;
   A6:  [.-PI/4,PI/4.] c= ].-PI/2,PI/2.[ by Lm7,Lm8,RCOMP_1:17;
   A7:  tan is_increasing_on [.-PI/4,PI/4.]
        by Lm7,Lm8,Th7,RCOMP_1:17,RFUNCT_2:60;
        -PI/4 in {s where s is Real: -PI/4 <= s & s <= PI/4};then
   A8:  -PI/4 in [.-PI/4,PI/4.] by RCOMP_1:def 1;
   A9:  [.-PI/4,PI/4.] /\ dom tan = [.-PI/4,PI/4.]
        by A6,Th1,XBOOLE_1:1,XBOOLE_1:28;
   A11: ].-PI/4,PI/4.[ c= [.-PI/4,PI/4.] by XXREAL_1:25;
        x in { s where s is Real: -PI/4 < s & s < PI/4 }
        by A4,RCOMP_1:def 2;
        then ex s be Real st s=x & -PI/4 < s & s < PI/4;then
   A12: -1 < tan.x by A4,A7,A8,A9,A11,Th15,RFUNCT_2:def 2;
        PI/4 in {s where s is Real: -PI/4 <= s & s <= PI/4};then
   A13: PI/4 in [.-PI/4,PI/4.] /\ dom tan by A9,RCOMP_1:def 1;
        x in { s where s is Real: -PI/4 < s & s < PI/4 }
        by A4,RCOMP_1:def 2;
        then ex s be Real st s=x & -PI/4 < s & s < PI/4;
        then tan.x < tan.(PI/4) by A4,A7,A9,A11,A13,RFUNCT_2:def 2;then
        tan.x < 1 by SIN_COS:def 32;
        then tan.x in { s where s is Real: -1 < s & s < 1 } by A12;then
   A14: tan.x in ].-1,1.[ by RCOMP_1:def 2;
        ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
        hence tan.x in [.-1,1.] by A14;
      end;
      suppose x = -PI/4;
        then tan.x in { s where s is Real: -1 <= s & s <= 1 } by Th15;
        hence tan.x in [.-1,1.] by RCOMP_1:def 1;
      end;
      suppose x = PI/4;
        then tan.x = 1 by SIN_COS:def 32;
        then tan.x in { s where s is Real: -1 <= s & s <= 1 };
        hence tan.x in [.-1,1.] by RCOMP_1:def 1;
      end;
end;

theorem Th18:
  for x be set st x in [.PI/4,3/4*PI.] holds
  cot.x in [.-1,1.]
proof
    let x be set;
    assume
A1: x in [.PI/4,3/4*PI.];
A2: PI/4 <= 3/4*PI
    proof
      PI in ].0,4.[ by SIN_COS:def 32;
      then PI > 0 by XXREAL_1:4;
      then PI/4 > 0/4 by XREAL_1:76;
      then (PI/4)*3 > PI/4 by REAL_2:144;
      hence PI/4 <= 3/4*PI;
    end;
    x in ].PI/4,3/4*PI.[ \/ {PI/4,3/4*PI} by A1,A2,XXREAL_1:128;then
A3: x in ].PI/4,3/4*PI.[ or x in {PI/4,3/4*PI} by XBOOLE_0:def 2;
    per cases by A3,TARSKI:def 2;
      suppose
   A4:  x in ].PI/4,3/4*PI.[;
   A6:  [.PI/4,3/4*PI.] c= ].0,PI.[ by Lm9,Lm10,RCOMP_1:17;
   A7:  cot is_decreasing_on [.PI/4,3/4*PI.]
        by Lm9,Lm10,Th8,RCOMP_1:17,RFUNCT_2:61;
   A8:  PI/4 in {s where s is Real: PI/4 <= s & s <= 3/4*PI} by A2;
   A9:  [.PI/4,3/4*PI.] /\ dom cot = [.PI/4,3/4*PI.]
        by A6,Th2,XBOOLE_1:1,XBOOLE_1:28;then
   A10: PI/4 in [.PI/4,3/4*PI.] /\ dom cot by A8,RCOMP_1:def 1;
   A11: ].PI/4,3/4*PI.[ c= [.PI/4,3/4*PI.] by XXREAL_1:25;
        x in { s where s is Real: PI/4 < s & s < 3/4*PI }
        by A4,RCOMP_1:def 2;
        then ex s be Real st s=x & PI/4 < s & s < 3/4*PI;then
   A12: cot.x < 1 by A4,A7,A9,A10,A11,Th16,RFUNCT_2:def 3;
        3/4*PI in {s where s is Real: PI/4 <= s & s <= 3/4*PI} by A2;then
   A13: 3/4*PI in [.PI/4,3/4*PI.] /\ dom cot by A9,RCOMP_1:def 1;
        x in { s where s is Real: PI/4 < s & s < 3/4*PI }
        by A4,RCOMP_1:def 2;
        then ex s be Real st s=x & PI/4 < s & s < 3/4*PI;
        then -1 < cot.x by A4,A7,A9,A11,A13,Th16,RFUNCT_2:def 3;
        then cot.x in { s where s is Real: -1 < s & s < 1 } by A12;then
   A14: cot.x in ].-1,1.[ by RCOMP_1:def 2;
        ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
        hence cot.x in [.-1,1.] by A14;
      end;
      suppose x = PI/4;
        then cot.x in { s where s is Real: -1 <= s & s <= 1 } by Th16;
        hence cot.x in [.-1,1.] by RCOMP_1:def 1;
      end;
      suppose x = 3/4*PI;
        then cot.x in { s where s is Real: -1 <= s & s <= 1 } by Th16;
        hence cot.x in [.-1,1.] by RCOMP_1:def 1;
      end;
end;

theorem Th19:
  rng (tan | [.-PI/4,PI/4.]) = [.-1,1.]
proof
  now let y be set;
    thus y in [.-1,1.] implies ex x be set st x in dom (tan | [.-PI/4,PI/4.])
    & y = (tan | [.-PI/4,PI/4.]).x
    proof
      assume
  A1: y in [.-1,1.];
      then reconsider y1=y as Real;
  A2: tan is_continuous_on ].-PI/2,PI/2.[ by Lm1,FDIFF_1:33;
  A4: tan is_continuous_on [.-PI/4,PI/4.]
      by A2,Lm7,Lm8,RCOMP_1:17,FCONT_1:17;
      y1 in [.tan.(-PI/4),tan.(PI/4).] by A1,SIN_COS:def 32,Th15;
      then y1 in [.tan.(-PI/4),tan.(PI/4).] \/ [.tan.(PI/4),tan.(-PI/4).]
      by XBOOLE_0:def 2;
      then consider x be Real such that
  A5: x in [.-PI/4,PI/4.] and
  A6: y1 = tan.x by A4,FCONT_2:16;
      take x;
      thus x in dom (tan | [.-PI/4,PI/4.]) & y = (tan | [.-PI/4,PI/4.]).x
      by A5,A6,Lm11,FUNCT_1:72;
    end;
    thus (ex x be set st x in dom (tan | [.-PI/4,PI/4.]) &
    y = (tan | [.-PI/4,PI/4.]).x) implies y in [.-1,1.]
    proof
        given x be set such that
    A7: x in dom (tan | [.-PI/4,PI/4.]) and
    A8: y = (tan | [.-PI/4,PI/4.]).x;
        reconsider x1=x as Real by A7;
        y = tan.x1 by A7,A8,Lm11,FUNCT_1:72;
        hence y in [.-1,1.] by A7,Lm11,Th17;
    end;
  end;
  hence thesis by FUNCT_1:def 5;
end;

theorem Th20:
  rng (cot | [.PI/4,3/4*PI.]) = [.-1,1.]
proof
  now let y be set;
    thus y in [.-1,1.] implies ex x be set st x in dom (cot | [.PI/4,3/4*PI.])
    & y = (cot | [.PI/4,3/4*PI.]).x
    proof
      assume
  A1: y in [.-1,1.];
      then reconsider y1=y as Real;
  A2: PI/4 <= 3/4*PI
      proof
        PI in ].0,4.[ by SIN_COS:def 32;
        then PI > 0 by XXREAL_1:4;
        then PI/4 > 0/4 by XREAL_1:76;
        then (PI/4)*3 > PI/4 by REAL_2:144;
        hence PI/4 <= 3/4*PI;
      end;
  A3: cot is_continuous_on ].0,PI.[ by Lm2,FDIFF_1:33;
  A5: cot is_continuous_on [.PI/4,3/4*PI.]
      by A3,Lm9,Lm10,RCOMP_1:17,FCONT_1:17;
      y1 in [.cot.(3/4*PI),cot.(PI/4).] \/ [.cot.(PI/4),cot.(3/4*PI).]
      by A1,Th16,XBOOLE_0:def 2;
      then consider x be Real such that
  A6: x in [.PI/4,3/4*PI.] and
  A7: y1 = cot.x by A2,A5,FCONT_2:16;
      take x;
      thus x in dom (cot | [.PI/4,3/4*PI.]) & y = (cot | [.PI/4,3/4*PI.]).x
      by A6,A7,Lm12,FUNCT_1:72;
    end;
    thus (ex x be set st x in dom (cot | [.PI/4,3/4*PI.]) &
    y = (cot | [.PI/4,3/4*PI.]).x) implies y in [.-1,1.]
    proof
      given x be set such that
 A8:  x in dom (cot | [.PI/4,3/4*PI.]) and
 A9:  y = (cot | [.PI/4,3/4*PI.]).x;
      reconsider x1=x as Real by A8;
      y = cot.x1 by A8,A9,Lm12,FUNCT_1:72;
      hence y in [.-1,1.] by A8,Lm12,Th18;
    end;
  end;
  hence thesis by FUNCT_1:def 5;
end;

theorem Th21:
  [.-1,1.] c= dom arctan
proof
A1: [.-PI/4,PI/4.] c= ].-PI/2,PI/2.[ by Lm7,Lm8,RCOMP_1:17;
    rng (tan | [.-PI/4,PI/4.]) c= rng (tan | ].-PI/2,PI/2.[)
    proof
      let y be set;
      assume y in rng (tan | [.-PI/4,PI/4.]);
      then y in tan.:[.-PI/4,PI/4.] by RELAT_1:148;
      then consider x be set such that
  A3: x in dom tan and
  A4: x in [.-PI/4,PI/4.] and
  A5: y = tan.x by FUNCT_1:def 12;
      y in tan.:].-PI/2,PI/2.[ by A1,A3,A4,A5,FUNCT_1:def 12;
      hence thesis by RELAT_1:148;
    end;
    hence [.-1,1.] c= dom arctan by Th19,FUNCT_1:55;
end;

theorem Th22:
  [.-1,1.] c= dom arccot
proof
A1: [.PI/4,3/4*PI.] c= ].0,PI.[ by Lm9,Lm10,RCOMP_1:17;
    rng (cot | [.PI/4,3/4*PI.]) c= rng (cot | ].0,PI.[)
    proof
      let y be set;
      assume y in rng (cot | [.PI/4,3/4*PI.]);
      then y in cot.:[.PI/4,3/4*PI.] by RELAT_1:148;
      then consider x be set such that
  A3: x in dom cot and
  A4: x in [.PI/4,3/4*PI.] and
  A5: y = cot.x by FUNCT_1:def 12;
      y in cot.:].0,PI.[ by A1,A3,A4,A5,FUNCT_1:def 12;
      hence thesis by RELAT_1:148;
    end;
    hence [.-1,1.] c= dom arccot by Th20,FUNCT_1:55;
end;

Lm13:
  tan | [.-PI/4,PI/4.] is_increasing_on [.-PI/4,PI/4.]
proof
    tan is_increasing_on [.-PI/4,PI/4.]
    by Lm7,Lm8,Th7,RCOMP_1:17,RFUNCT_2:60;
    hence thesis by RFUNCT_2:50;
end;

Lm14:
  cot | [.PI/4,3/4*PI.] is_decreasing_on [.PI/4,3/4*PI.]
proof
    cot is_decreasing_on [.PI/4,3/4*PI.]
    by Lm9,Lm10,Th8,RCOMP_1:17,RFUNCT_2:61;
    hence thesis by RFUNCT_2:51;
end;

Lm15:
  tan | [.-PI/4,PI/4.] is one-to-one
proof
    (tan | ].-PI/2,PI/2.[) | [.-PI/4,PI/4.]
    = tan | [.-PI/4,PI/4.] by Lm7,Lm8,RCOMP_1:17,RELAT_1:103;
    hence tan | [.-PI/4,PI/4.] is one-to-one;
end;

Lm16:
  cot | [.PI/4,3/4*PI.] is one-to-one
proof
    (cot | ].0,PI.[) | [.PI/4,3/4*PI.] = cot | [.PI/4,3/4*PI.]
    by Lm9,Lm10,RCOMP_1:17,RELAT_1:103;
    hence cot | [.PI/4,3/4*PI.] is one-to-one;
end;

registration
  cluster tan | [.-PI/4,PI/4.] -> one-to-one;
  coherence by Lm15;
  cluster cot | [.PI/4,3/4*PI.] -> one-to-one;
  coherence by Lm16;
end;

theorem Th23:
  arctan | [.-1,1.] = (tan | [.-PI/4,PI/4.])"
proof
    set h = tan | ].-PI/2,PI/2.[;
    (tan | [.-PI/4,PI/4.])" = (h | [.-PI/4,PI/4.])"
                            by Lm7,Lm8,RCOMP_1:17,RELAT_1:103
                           .= h" | (h.:[.-PI/4,PI/4.]) by RFUNCT_2:40
                           .= h" | rng (h | [.-PI/4,PI/4.]) by RELAT_1:148
                           .= h" | ([.-1,1.])
                            by Lm7,Lm8,Th19,RCOMP_1:17,RELAT_1:103;
    hence (tan | [.-PI/4,PI/4.])" = arctan | [.-1,1.];
end;

theorem Th24:
  arccot | [.-1,1.] = (cot | [.PI/4,3/4*PI.])"
proof
    set h = cot | ].0,PI.[;
    (cot | [.PI/4,3/4*PI.])" = (h | [.PI/4,3/4*PI.])"
                             by Lm9,Lm10,RCOMP_1:17,RELAT_1:103
                            .= h" | (h.:[.PI/4,3/4*PI.]) by RFUNCT_2:40
                            .= h" | rng (h | [.PI/4,3/4*PI.]) by RELAT_1:148
                            .= h" | ([.-1,1.])
                             by Lm9,Lm10,Th20,RCOMP_1:17,RELAT_1:103;
    hence (cot | [.PI/4,3/4*PI.])" = arccot | [.-1,1.];
end;

theorem
  (tan | [.-PI/4,PI/4.]) qua Function * (arctan | [.-1,1.]) = id [.-1,1.]
  by Th19,Th23,FUNCT_1:61;

theorem
  (cot | [.PI/4,3/4*PI.]) qua Function * (arccot | [.-1,1.]) = id [.-1,1.]
  by Th20,Th24,FUNCT_1:61;

theorem
  (tan | [.-PI/4,PI/4.]) * (arctan | [.-1,1.]) = id [.-1,1.]
  by Th19,Th23,FUNCT_1:61;

theorem
  (cot | [.PI/4,3/4*PI.]) * (arccot | [.-1,1.]) = id [.-1,1.]
  by Th20,Th24,FUNCT_1:61;

theorem Th29:
  (arctan qua Function) * (tan | ].-PI/2,PI/2.[) = id ].-PI/2,PI/2.[
  by Lm5,Th11,FUNCT_1:61;

theorem Th30:
  arccot * (cot | ].0,PI.[) = id ].0,PI.[ by Lm6,Th12,FUNCT_1:61;

theorem
  arctan qua Function * (tan | ].-PI/2,PI/2.[) = id ].-PI/2,PI/2.[
  by Lm5,Th11,FUNCT_1:61;

theorem
  arccot qua Function * (cot | ].0,PI.[) = id ].0,PI.[
  by Lm6,Th12,FUNCT_1:61;

theorem Th33:
  -PI/2 < r & r < PI/2 implies arctan tan.r = r & arctan tan r = r
proof
    assume -PI/2 < r & r < PI/2;then
A1: r in ].-PI/2,PI/2.[ by XXREAL_1:4;
A2: dom (tan|].-PI/2,PI/2.[) = ].-PI/2,PI/2.[ by Th1,RELAT_1:91;
    arctan tan.r = arctan.((tan|].-PI/2,PI/2.[).r) by A1,FUNCT_1:72
                .= (id ].-PI/2,PI/2.[).r by A1,A2,Th29,FUNCT_1:23
                .= r by A1,FUNCT_1:35;
    hence thesis by A1,Th13;
end;

theorem Th34:
  0 < r & r < PI implies arccot cot.r = r & arccot cot r = r
proof
    assume 0 < r & r < PI;then
A1: r in ].0,PI.[ by XXREAL_1:4;
A2: dom (cot|].0,PI.[) = ].0,PI.[ by Th2,RELAT_1:91;
A3: arccot cot.r = arccot.((cot|].0,PI.[).r) by A1,FUNCT_1:72
                .= (id ].0,PI.[).r by A1,A2,Th30,FUNCT_1:23
                .= r by A1,FUNCT_1:35;
    thus thesis by A1,A3,Th14;
end;

theorem Th35:
  arctan (-1) = -PI/4 & arctan.(-1) = -PI/4
proof
    -PI/2 < -PI/4 & -PI/4 < PI/2 by Lm7,XXREAL_1:4;then
    arctan (-1) = -PI/4 by Th15,Th33;
    hence thesis;
end;

theorem Th36:
  arccot (-1) = 3/4*PI & arccot.(-1) = 3/4*PI
proof
    0 < 3/4*PI & 3/4*PI < PI by Lm10,XXREAL_1:4;then
    arccot (-1) = 3/4*PI by Th16,Th34;
    hence thesis;
end;

theorem Th37:
  arctan 1 = PI/4 & arctan.1 = PI/4
proof
A1: arctan 1 = arctan tan.(PI/4) by SIN_COS:def 32;
    -PI/2 < PI/4 & PI/4 < PI/2 by Lm8,XXREAL_1:4;
    hence thesis by A1,Th33;
end;

theorem Th38:
  arccot 1 = PI/4 & arccot.1 = PI/4
proof
    0 < PI/4 & PI/4 < PI by Lm9,XXREAL_1:4;then
    arccot 1 = PI/4 by Th16,Th34;
    hence thesis;
end;

theorem Th39:
  tan.0 = 0 & tan 0 =0
proof
    PI in ].0,4.[ by SIN_COS:def 32;then
    PI > 0 by XXREAL_1:4;then
A2: PI/2 > 0/2 by XREAL_1:76;
    0-PI/2 < 0 by XREAL_1:51;then
A4: 0 in ].-PI/2,PI/2.[ by A2,XXREAL_1:4;
    tan.0 = 0/cos.0 by A4,Th1,SIN_COS:33,RFUNCT_1:def 4
         .= 0;
    hence thesis by A4,Th13;
end;

theorem Th40:
  cot.(PI/2) = 0 & cot (PI/2) = 0
proof
    PI in ].0,4.[ by SIN_COS:def 32;then
A1: PI > 0 by XXREAL_1:4;then
A2: PI/2 > 0/2 by XREAL_1:76;
    PI/2 < PI/1 by A1,REAL_2:200;then
A4: PI/2 in ].0,PI.[ by A2,XXREAL_1:4;
    cot.(PI/2) = 0/sin.(PI/2) by A4,Th2,SIN_COS:81,RFUNCT_1:def 4
              .= 0;
    hence thesis by A4,Th14;
end;

theorem
  arctan 0 = 0 & arctan.0 = 0
proof
    PI in ].0,4.[ by SIN_COS:def 32;
    then PI > 0 by XXREAL_1:4;then
A2: PI/2 > 0/2 by XREAL_1:76;
    0 - PI/2 < 0 by XREAL_1:51;
    then arctan 0 = 0 by A2,Th33,Th39;
    hence thesis;
end;

theorem
  arccot 0 = PI/2 & arccot.0 = PI/2
proof
    PI in ].0,4.[ by SIN_COS:def 32;then
A1: PI > 0 by XXREAL_1:4;then
A2: PI/2 > 0/2 by XREAL_1:76;
    PI/2 < PI/1 by A1,REAL_2:200;
    then arccot 0 = PI/2 by A2,Th34,Th40;
    hence thesis;
end;

theorem Th43:
  arctan is_increasing_on tan.:].-PI/2,PI/2.[
proof
    set f = tan | ].-PI/2,PI/2.[;
A4: f|].-PI/2,PI/2.[ = f by RELAT_1:102;
A5: f is_increasing_on ].-PI/2,PI/2.[ by Th7,RFUNCT_2:50;
    f.:].-PI/2,PI/2.[ = rng(f|].-PI/2,PI/2.[) by RELAT_1:148
                     .= rng(tan|].-PI/2,PI/2.[) by RELAT_1:102
                     .= tan.:].-PI/2,PI/2.[ by RELAT_1:148;
    hence arctan is_increasing_on tan.:].-PI/2,PI/2.[ by A4,A5,FCONT_3:17;
end;

theorem Th44:
  arccot is_decreasing_on cot.:].0,PI.[
proof
    set f = cot | ].0,PI.[;
A4: f|].0,PI.[ = f by RELAT_1:102;
A5: f is_decreasing_on ].0,PI.[ by Th8,RFUNCT_2:51;
    f.:].0,PI.[ = rng(f|].0,PI.[) by RELAT_1:148
               .= rng(cot|].0,PI.[) by RELAT_1:102
               .= cot.:].0,PI.[ by RELAT_1:148;
    hence arccot is_decreasing_on cot.:].0,PI.[ by A4,A5,FCONT_3:18;
end;

theorem Th45:
  arctan is_increasing_on [.-1,1.]
proof
A2: [.-1,1.] = tan.:[.-PI/4,PI/4.] by Th19,RELAT_1:148;
    [.-1,1.] c= tan.:].-PI/2,PI/2.[
    by A2,Lm7,Lm8,RCOMP_1:17,RELAT_1:156;
    hence arctan is_increasing_on [.-1,1.] by Th43,RFUNCT_2:60;
end;

theorem Th46:
  arccot is_decreasing_on [.-1,1.]
proof
A2: [.-1,1.] = cot.:[.PI/4,3/4*PI.] by Th20,RELAT_1:148;
    [.-1,1.] c= cot.:].0,PI.[
    by A2,Lm9,Lm10,RCOMP_1:17,RELAT_1:156;
    hence arccot is_decreasing_on [.-1,1.] by Th44,RFUNCT_2:61;
end;

theorem Th47:
  for x be set st x in [.-1,1.] holds arctan.x in [.-PI/4,PI/4.]
proof
    let x be set;
    assume x in [.-1,1.];
    then x in ].-1,1.[ \/ {-1,1} by XXREAL_1:128;then
A1: x in ].-1,1.[ or x in {-1,1} by XBOOLE_0:def 2;
    per cases by A1,TARSKI:def 2;
      suppose
    A2: x in ].-1,1.[;
    A4: -1 in [.-1,1.] by XXREAL_1:1;
    A5: [.-1,1.] /\ dom arctan = [.-1,1.] by Th21,XBOOLE_1:28;
    A7: ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
        x in { s where s is Real: -1 < s & s < 1 } by A2,RCOMP_1:def 2;then
    A8: ex s be Real st s=x & -1 < s & s < 1;then
    A9: -PI/4 < arctan.x by A2,A4,A5,A7,Th35,Th45,RFUNCT_2:def 2;
        1 in [.-1,1.] /\ dom arctan by A5,XXREAL_1:1;
        then arctan.x < PI/4 by A2,A5,A7,A8,Th37,Th45,RFUNCT_2:def 2;
        hence arctan.x in [.-PI/4,PI/4.] by A9,XXREAL_1:1;
      end;
      suppose x = -1;
        hence arctan.x in [.-PI/4,PI/4.] by Th35,XXREAL_1:1;
      end;
      suppose x = 1;
        hence arctan.x in [.-PI/4,PI/4.] by Th37,XXREAL_1:1;
      end;
end;

theorem Th48:
  for x be set st x in [.-1,1.] holds arccot.x in [.PI/4,3/4*PI.]
proof
    let x be set;
    assume x in [.-1,1.];
    then x in ].-1,1.[ \/ {-1,1} by XXREAL_1:128;then
A1: x in ].-1,1.[ or x in {-1,1} by XBOOLE_0:def 2;
    per cases by A1,TARSKI:def 2;
      suppose
   A2:  x in ].-1,1.[;
   A4:  -1 in [.-1,1.] by XXREAL_1:1;
   A5:  [.-1,1.] /\ dom arccot = [.-1,1.] by Th22,XBOOLE_1:28;
   A7:  ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
        x in { s where s is Real: -1 < s & s < 1 } by A2,RCOMP_1:def 2;then
   A8:  ex s be Real st s=x & -1 < s & s < 1;then
   A9:  3/4*PI > arccot.x by A2,A4,A5,A7,Th36,Th46,RFUNCT_2:def 3;
        1 in [.-1,1.] /\ dom arccot by A5,XXREAL_1:1;
        then arccot.x > PI/4 by A2,A5,A7,A8,Th38,Th46,RFUNCT_2:def 3;
        hence arccot.x in [.PI/4,3/4*PI.] by A9,XXREAL_1:1;
      end;
      suppose
   A10: x = -1;
        PI in ].0,4.[ by SIN_COS:def 32;
        then PI > 0 by XXREAL_1:4;
        then PI/4 > 0/4 by XREAL_1:76;
        then PI/4 < (PI/4)*3 by REAL_2:144;
        hence arccot.x in [.PI/4,3/4*PI.] by A10,Th36,XXREAL_1:1;
      end;
      suppose
   A11: x = 1;
        PI in ].0,4.[ by SIN_COS:def 32;
        then PI > 0 by XXREAL_1:4;
        then PI/4 > 0/4 by XREAL_1:76;
        then PI/4 < (PI/4)*3 by REAL_2:144;
        hence arccot.x in [.PI/4,3/4*PI.] by A11,Th38,XXREAL_1:1;
      end;
end;

theorem Th49:
  -1 <= r & r <= 1 implies tan arctan r = r
proof
    assume -1 <= r & r <= 1;then
A1: r in [.-1,1.] by XXREAL_1:1;then
A2: r in dom (arctan | [.-1,1.]) by Th21,RELAT_1:91;
A3: arctan.r in [.-PI/4,PI/4.] by A1,Th47;
A4: [.-PI/4,PI/4.] c= ].-PI/2,PI/2.[ by Lm7,Lm8,RCOMP_1:17;
    thus tan (arctan r) = tan.(arctan.r) by A3,A4,Th13
    .= ((tan|[.-PI/4,PI/4.]) qua Function).(arctan.r)
       by A1,Th47,FUNCT_1:72
    .= ((tan|[.-PI/4,PI/4.]) qua Function).((arctan | [.-1,1.]).r)
       by A1,FUNCT_1:72
    .= ((tan | [.-PI/4,PI/4.]) qua Function * (arctan | [.-1,1.])).r
        by A2,FUNCT_1:23
    .= (id [.-1,1.]).r by Th19,Th23,FUNCT_1:61
    .= r by A1,FUNCT_1:35;
end;

theorem Th50:
  -1 <= r & r <= 1 implies cot arccot r = r
proof
    assume -1 <= r & r <= 1;then
A1: r in [.-1,1.] by XXREAL_1:1;then
A2: r in dom (arccot | [.-1,1.]) by Th22,RELAT_1:91;
A3: arccot.r in [.PI/4,3/4*PI.] by A1,Th48;
A4: [.PI/4,3/4*PI.] c= ].0,PI.[ by Lm9,Lm10,RCOMP_1:17;
    thus cot (arccot r) = cot.(arccot.r) by A3,A4,Th14
    .= ((cot|[.PI/4,3/4*PI.]) qua Function).(arccot.r)
       by A1,Th48,FUNCT_1:72
    .= ((cot|[.PI/4,3/4*PI.]) qua Function).((arccot | [.-1,1.]).r)
       by A1,FUNCT_1:72
    .= ((cot|[.PI/4,3/4*PI.]) qua Function * (arccot | [.-1,1.])).r
        by A2,FUNCT_1:23
    .= (id [.-1,1.]).r by Th20,Th24,FUNCT_1:61
    .= r by A1,FUNCT_1:35;
end;

theorem Th51:
  arctan is_continuous_on [.-1,1.]
proof
    set f = tan | [.-PI/4,PI/4.];
A3: f|[.-PI/4,PI/4.] = f by RELAT_1:101;
    (f|[.-PI/4,PI/4.])" is_continuous_on f.:[.-PI/4,PI/4.]
    by Lm11,Lm13,FCONT_1:54;
    then arctan | [.-1,1.] is_continuous_on [.-1,1.]
    by A3,Th19,Th23,RELAT_1:148;
    hence arctan is_continuous_on [.-1,1.] by FCONT_1:16;
end;

theorem Th52:
  arccot is_continuous_on [.-1,1.]
proof
    set f = cot | [.PI/4,3/4*PI.];
    PI in ].0,4.[ by SIN_COS:def 32;
    then PI > 0 by XXREAL_1:4;
    then PI/4 > 0/4 by XREAL_1:76;then
A1: PI/4 < (PI/4)*3 by REAL_2:144;
A3: f|[.PI/4,3/4*PI.] = f by RELAT_1:101;
    (f|[.PI/4,3/4*PI.])" is_continuous_on f.:[.PI/4,3/4*PI.]
    by A1,Lm12,Lm14,FCONT_1:54;
    then arccot | [.-1,1.] is_continuous_on [.-1,1.]
    by A3,Th20,Th24,RELAT_1:148;
    hence arccot is_continuous_on [.-1,1.] by FCONT_1:16;
end;

theorem Th53:
  rng(arctan | [.-1,1.]) = [.-PI/4,PI/4.]
proof
  now let y be set;
    thus y in [.-PI/4,PI/4.] implies
    ex x be set st x in dom (arctan | [.-1,1.])
    & y = (arctan | [.-1,1.]).x
    proof
      assume
  A1: y in [.-PI/4,PI/4.];
      then reconsider y1=y as Real;
      y1 in [.arctan.(-1),arctan.1.] \/ [.arctan.1,arctan.(-1).]
      by A1,Th35,Th37,XBOOLE_0:def 2;
      then consider x be Real such that
  A3: x in [.-1,1.] and
  A4: y1 = arctan.x by Th51,FCONT_2:16;
      take x;
      thus x in dom (arctan | [.-1,1.]) & y = (arctan | [.-1,1.]).x
      by A3,A4,Th21,RELAT_1:91,FUNCT_1:72;
    end;
    thus (ex x be set st x in dom (arctan | [.-1,1.]) &
    y = (arctan | [.-1,1.]).x) implies y in [.-PI/4,PI/4.]
    proof
      given x be set such that
  A6: x in dom (arctan | [.-1,1.]) and
  A7: y = (arctan | [.-1,1.]).x;
  A8: dom (arctan | [.-1,1.]) = [.-1,1.] by Th21,RELAT_1:91;
      reconsider x1=x as Real by A6;
      y = arctan.x by A6,A7,A8,FUNCT_1:72;
      hence y in [.-PI/4,PI/4.] by A6,A8,Th47;
    end;
  end;
  hence thesis by FUNCT_1:def 5;
end;

theorem Th54:
  rng(arccot | [.-1,1.]) = [.PI/4,3/4*PI.]
proof
  now let y be set;
    thus y in [.PI/4,3/4*PI.] implies
    ex x be set st x in dom (arccot | [.-1,1.])
    & y = (arccot | [.-1,1.]).x
    proof
      assume
  A1: y in [.PI/4,3/4*PI.];
      then reconsider y1=y as Real;
      y1 in [.arccot.1,arccot.(-1).] \/ [.arccot.(-1),arccot.1.]
      by A1,Th36,Th38,XBOOLE_0:def 2;
      then consider x be Real such that
  A3: x in [.-1,1.] and
  A4: y1 = arccot.x by Th52,FCONT_2:16;
      take x;
      thus x in dom (arccot | [.-1,1.]) & y = (arccot | [.-1,1.]).x
      by A3,A4,Th22,RELAT_1:91,FUNCT_1:72;
    end;
    thus (ex x be set st x in dom (arccot | [.-1,1.]) &
    y = (arccot | [.-1,1.]).x) implies y in [.PI/4,3/4*PI.]
    proof
      given x be set such that
  A6: x in dom (arccot | [.-1,1.]) and
  A7: y = (arccot | [.-1,1.]).x;
  A8: dom (arccot | [.-1,1.]) = [.-1,1.] by Th22,RELAT_1:91;
      reconsider x1=x as Real by A6;
      y = arccot.x by A6,A7,A8,FUNCT_1:72;
      hence y in [.PI/4,3/4*PI.] by A6,A8,Th48;
    end;
  end;
  hence thesis by FUNCT_1:def 5;
end;

theorem
  -1 <= r & r <= 1 & arctan r = -PI/4 implies r = -1 by Th49,Th15;

theorem
  -1 <= r & r <= 1 & arccot r = 3/4*PI implies r = -1 by Th50,Th16;

theorem
  -1 <= r & r <= 1 & arctan r = 0 implies r = 0 by Th49,Th39;

theorem
  -1 <= r & r <= 1 & arccot r = PI/2 implies r = 0 by Th40,Th50;

theorem
  -1 <= r & r <= 1 & arctan r = PI/4 implies r = 1
proof
    assume -1 <= r & r <= 1 & arctan r = PI/4;
    hence r = tan(PI/4) by Th49
           .= tan.(PI/4) by Lm8,Th13
           .= 1 by SIN_COS:def 32;
end;

theorem
  -1 <= r & r <= 1 & arccot r = PI/4 implies r = 1 by Th16,Th50;

theorem Th61:
  -1 <= r & r <= 1 implies -PI/4 <= arctan r & arctan r <= PI/4
proof
    assume -1 <= r & r <= 1;then
A1: r in [.-1,1.] by XXREAL_1:1;
    then r in dom (arctan | [.-1,1.]) by Th21,RELAT_1:91;
    then (arctan | [.-1,1.]).r in rng (arctan | [.-1,1.])
    by FUNCT_1:def 5;
    then arctan r in rng (arctan | [.-1,1.]) by A1,FUNCT_1:72;
    hence thesis by Th53,XXREAL_1:1;
end;

theorem Th62:
  -1 <= r & r <= 1 implies PI/4 <= arccot r & arccot r <= 3/4*PI
proof
    assume -1 <= r & r <= 1;then
A1: r in [.-1,1.] by XXREAL_1:1;
    then r in dom (arccot | [.-1,1.]) by Th22,RELAT_1:91;
    then (arccot | [.-1,1.]).r in rng (arccot | [.-1,1.])
    by FUNCT_1:def 5;
    then arccot r in rng (arccot | [.-1,1.]) by A1,FUNCT_1:72;
    hence thesis by Th54,XXREAL_1:1;
end;

theorem
  -1 < r & r < 1 implies -PI/4 < arctan r & arctan r < PI/4
proof
    assume
A1: -1 < r & r < 1;
    then -PI/4 <= arctan r & arctan r <= PI/4 by Th61;then
A2: -PI/4 < arctan r & arctan r < PI/4 or
    -PI/4 = arctan r or arctan r = PI/4 by REAL_1:def 5;
    tan (PI/4) = tan.(PI/4) by Lm8,Th13
               .= 1 by SIN_COS:def 32;
    hence thesis by A1,A2,Th15,Th49;
end;

theorem
  -1 < r & r < 1 implies PI/4 < arccot r & arccot r < 3/4*PI
proof
    assume
A1: -1 < r & r < 1;
    then PI/4 <= arccot r & arccot r <= 3/4*PI by Th62;then
A2: PI/4 < arccot r & arccot r < 3/4*PI or
    PI/4 = arccot r or arccot r = 3/4*PI by REAL_1:def 5;
    thus thesis by A1,A2,Th16,Th50;
end;

theorem
  -1 <= r & r <= 1 implies arctan r = -arctan(-r)
proof
    assume -1 <= r & r <= 1;then
A1: --1 >= -r & -r >= -1 by XREAL_1:26;then
A2: tan arctan(-r) = -r by Th49;
    -PI/4 <= arctan(-r) & arctan(-r) <= PI/4 by A1,Th61;then
A4: arctan(-r) in [.-PI/4,PI/4.] by XXREAL_1:1;
    [.-PI/4,PI/4.] c= ].-PI/2,PI/2.[ by Lm7,Lm8,RCOMP_1:17; then
A5: cos arctan(-r) <> 0 by A4,COMPTRIG:27;
A6: r = (tan 0 - tan arctan(-r))/(1 + (tan 0) * tan arctan(-r))
      by A2,Th39
     .= tan(0 - arctan(-r)) by A5,SIN_COS:34,SIN_COS4:12;
    arctan(-r) <= PI/4 by A1,Th61;then
A7: -PI/4 <= -arctan(-r) by XREAL_1:26;
    -PI/4 <= arctan(-r) by A1,Th61;
    then -arctan(-r) <= --PI/4 by XREAL_1:26;then
A8: -arctan(-r) in [.-PI/4,PI/4.] by A7,XXREAL_1:1;
    [.-PI/4,PI/4.] c= ].-PI/2,PI/2.[ by Lm7,Lm8,RCOMP_1:17;
    then -PI/2 < -arctan(-r) & -arctan(-r) < PI/2 by A8,XXREAL_1:4;
    hence arctan r = -arctan(-r) by A6,Th33;
end;

theorem
  -1 <= r & r <= 1 implies arccot r = PI - arccot(-r)
proof
    set x = arccot(-r);
    assume
A1: -1 <= r & r <= 1;
A2: --1 >= -r & -r >= -1 by A1,XREAL_1:26;
    then -r in [.-1,1.] by XXREAL_1:1;then
A3: x in [.PI/4,3/4*PI.] by Th48;
    -r = cot x by A2,Th50;then
A6: r = -cot x
     .= -(cos x/sin x) by SIN_COS4:def 2
     .= cos x/(-(sin x)) by XCMPLX_1:189
     .= cos x/sin(-x) by SIN_COS:34
     .= cos(-x)/sin(-x) by SIN_COS:34
     .= cot(-x) by SIN_COS4:def 2;
A7: 0 < PI+(-x) & PI+(-x) < PI
    proof
      PI/4 <= x & x <= 3/4*PI by A3,XXREAL_1:1;
      then -PI/4 >= -x & -x >= -3/4*PI by XREAL_1:26;
      then PI+(-PI/4) >= PI+(-x) & PI+(-x) >= PI+(-3/4*PI) by XREAL_1:8;then
  A8: PI+(-x) in [.PI/4,3/4*PI.] by XXREAL_1:1;
      [.PI/4,3/4*PI.] c= ].0,PI.[ by Lm9,Lm10,RCOMP_1:17;
      hence 0 < PI+(-x) & PI+(-x) < PI by A8,XXREAL_1:4;
    end;
    cot(PI+(-x)) = cos(PI+(-x))/sin(PI+(-x)) by SIN_COS4:def 2
                .= (-cos(-x))/sin(PI+(-x)) by SIN_COS:84
                .= (-cos(-x))/(-sin(-x)) by SIN_COS:84
                .= cos(-x)/sin(-x) by XCMPLX_1:192
                .= cot(-x)by SIN_COS4:def 2;
    hence arccot r = PI - arccot(-r) by A6,A7,Th34;
end;

theorem
  -1 <= r & r <= 1 implies cot arctan r = 1/r
proof
    set x = arctan r;
    assume that
A1: -1 <= r & r <= 1;
A4: sin x /cos x = tan x by SIN_COS4:def 1
                .= r by A1,Th49;
    cot x = cos x/sin x by SIN_COS4:def 2
         .= 1/r by A4,XCMPLX_1:57;
    hence thesis;
end;

theorem
  -1 <= r & r <= 1 implies tan arccot r = 1/r
proof
    set x = arccot r;
    assume that
A1: -1 <= r & r <= 1;
A4: cos x /sin x = cot x by SIN_COS4:def 2
                .= r by A1,Th50;
    tan x = sin x/cos x by SIN_COS4:def 1
         .= 1/r by A4,XCMPLX_1:57;
    hence thesis;
end;

theorem Th69:
  arctan is_differentiable_on tan.:].-PI/2,PI/2.[
proof
    set f = tan|].-PI/2,PI/2.[;
    set g = arctan;
A1: f|].-PI/2,PI/2.[ = f by RELAT_1:101;
A3: dom(f") = rng (tan|].-PI/2,PI/2.[) by FUNCT_1:55
           .= tan.:].-PI/2,PI/2.[ by RELAT_1:148;
A5: f is_differentiable_on ].-PI/2,PI/2.[ by Lm1,FDIFF_2:16;
    now
      let x0 be Real such that
  A7: x0 in ].-PI/2,PI/2.[;
  A8: diff(f,x0) = (f`|].-PI/2,PI/2.[).x0 by A5,A7,FDIFF_1:def 8
                .= (tan`|].-PI/2,PI/2.[).x0 by Lm1,FDIFF_2:16
                .= diff(tan,x0) by A7,Lm1,FDIFF_1:def 8
                .= 1/(cos.x0)^2 by A7,Lm3;
      for x0 be Real st x0 in ].-PI/2,PI/2.[ holds 1/(cos.x0)^2 > 0
      proof
        let x0 be Real;
        assume x0 in ].-PI/2,PI/2.[;
        then 0 < cos.x0 by COMPTRIG:27;then
    A9: (cos.x0)^2 > 0 by SQUARE_1:74;
        1/(cos.x0)^2 > 0 /(cos.x0)^2 by A9,REAL_1:73;
        hence 1/(cos.x0)^2 > 0;
      end;
      hence 0 < diff(f,x0) by A7,A8;
    end;
    hence g is_differentiable_on tan.:].-PI/2,PI/2.[ by A1,A3,A5,FDIFF_2:48;
end;

theorem Th70:
  arccot is_differentiable_on cot.:].0,PI.[
proof
    set f = cot|].0,PI.[;
    set g = arccot;
A1: f|].0,PI.[ = f by RELAT_1:101;
A3: dom(f") = rng (cot|].0,PI.[) by FUNCT_1:55
           .= cot.:].0,PI.[ by RELAT_1:148;
A5: f is_differentiable_on ].0,PI.[ by Lm2,FDIFF_2:16;
    now
      let x0 be Real such that
  A7: x0 in ].0,PI.[;
  A8: diff(f,x0) = (f`|].0,PI.[).x0 by A5,A7,FDIFF_1:def 8
                .= (cot`|].0,PI.[).x0 by Lm2,FDIFF_2:16
                .= diff(cot,x0) by A7,Lm2,FDIFF_1:def 8
                .= -1/(sin.x0)^2 by A7,Lm4;
      for x0 be Real st x0 in ].0,PI.[ holds -1/(sin.x0)^2 < 0
      proof
        let x0 be Real;
        assume x0 in ].0,PI.[;
        then 0 < sin.x0 by COMPTRIG:23;then
    A9: (sin.x0)^2 > 0 by SQUARE_1:74;
        1/(sin.x0)^2 > 0 /(sin.x0)^2 by A9,REAL_1:73;
        then -1/(sin.x0)^2 < -0 by XREAL_1:26;
        hence -1/(sin.x0)^2 < 0;
      end;
      hence diff(f,x0) < 0 by A7,A8;
    end;
    hence g is_differentiable_on cot.:].0,PI.[ by A1,A3,A5,FDIFF_2:48;
end;

theorem Th71:
  arctan is_differentiable_on ].-1,1.[
proof
    ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;then
A1: ].-1,1.[ c= dom arctan by Th21,XBOOLE_1:1;
    for x be Real st x in ].-1,1.[ holds arctan is_differentiable_in x
    proof
      let x be Real;
      assume
  A2: x in ].-1,1.[;
  A3: dom arctan = rng (tan | ].-PI/2,PI/2.[) by FUNCT_1:55
                .= tan.:].-PI/2,PI/2.[ by RELAT_1:148;
      arctan|dom arctan is_differentiable_in x
      by A1,A2,A3,Th69,FDIFF_1:def 7;
      hence arctan is_differentiable_in x by RELAT_1:98;
    end;
    hence arctan is_differentiable_on ].-1,1.[ by A1,FDIFF_1:16;
end;

theorem Th72:
  arccot is_differentiable_on ].-1,1.[
proof
    ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;then
A1: ].-1,1.[ c= dom arccot by Th22,XBOOLE_1:1;
    for x be Real st x in ].-1,1.[ holds arccot is_differentiable_in x
    proof
      let x be Real;
      assume
  A2: x in ].-1,1.[;
  A3: dom arccot = rng (cot | ].0,PI.[) by FUNCT_1:55
                .= cot.:].0,PI.[ by RELAT_1:148;
      arccot|dom arccot is_differentiable_in x
      by A1,A2,A3,Th70,FDIFF_1:def 7;
      hence arccot is_differentiable_in x by RELAT_1:98;
    end;
    hence arccot is_differentiable_on ].-1,1.[ by A1,FDIFF_1:16;
end;

theorem Th73:
  -1 <= r & r <= 1 implies diff(arctan,r) = 1/(1+r^2)
proof
     set f = tan|].-PI/2,PI/2.[;
     set g = arctan;
     set x = arctan.r;
     set X = tan.:].-PI/2,PI/2.[;
     assume
A1:  -1 <= r & r <= 1;then
A2:  r in [.-1,1.] by XXREAL_1:1;then
A3:  x in [.-PI/4,PI/4.] by Th47;
A4:  [.-PI/4,PI/4.] c= ].-PI/2,PI/2.[ by Lm7,Lm8,RCOMP_1:17;
A5:  f is_differentiable_on ].-PI/2,PI/2.[ by Lm1,FDIFF_2:16;
A6:  diff(f,x) = (f`|].-PI/2,PI/2.[).x by A3,A4,A5,FDIFF_1:def 8
              .= (tan`|].-PI/2,PI/2.[).x by Lm1,FDIFF_2:16
              .= diff(tan,x) by A3,A4,Lm1,FDIFF_1:def 8
              .= 1/(cos x)^2 by A3,A4,Lm3;
A7:  cos x <> 0 by A3,A4,COMPTRIG:27;
B8:  (sin.x)^2 + (cos.x)^2 = 1 by SIN_COS:31;
     x = arctan r;
     then r = tan x by A1,Th49
           .= sin x/cos x by SIN_COS4:def 1;
     then r * cos x = sin x by A7,XCMPLX_1:88; then
A9:  1 = (cos x)^2 * ( r^2 + 1 ) by B8;
A13: f is_differentiable_on ].-PI/2,PI/2.[ by Lm1,FDIFF_2:16;
A14: now
       let x0 be Real such that
  A15: x0 in ].-PI/2,PI/2.[;
  A16: diff(f,x0) = (f`|].-PI/2,PI/2.[).x0 by A13,A15,FDIFF_1:def 8
                 .= (tan`|].-PI/2,PI/2.[).x0 by Lm1,FDIFF_2:16
                 .= diff(tan,x0) by A15,Lm1,FDIFF_1:def 8
                 .= 1/(cos.x0)^2 by A15,Lm3;
       for x0 be Real st x0 in ].-PI/2,PI/2.[ holds 1/(cos.x0)^2 > 0
       proof
         let x0 be Real;
         assume x0 in ].-PI/2,PI/2.[;
         then 0 < cos.x0 by COMPTRIG:27;then
    A17: (cos.x0)^2 > 0 by SQUARE_1:74;
         1/(cos.x0)^2 > 0 /(cos.x0)^2 by A17,REAL_1:73;
         hence 1/(cos.x0)^2 > 0;
       end;
       hence 0 < diff(f,x0) by A15,A16;
     end;
A18: f|].-PI/2,PI/2.[ = f by RELAT_1:101;
     diff(g,r) = 1/(1/(cos x)^2)
               by A2,A6,A13,A14,A18,Th21,FDIFF_2:48
              .= 1/(r^2+1) by A9,XCMPLX_1:74;
     hence diff(arctan,r) = 1/(1+r^2);
end;

theorem Th74:
  -1 <= r & r <= 1 implies diff(arccot,r) = -1/(1+r^2)
proof
     set f = cot|].0,PI.[;
     set g = arccot;
     set x = arccot.r;
     set X = cot.:].0,PI.[;
     assume
A1:  -1 <= r & r <= 1;then
A2:  r in [.-1,1.] by XXREAL_1:1;then
A3:  x in [.PI/4,3/4*PI.] by Th48;
A4:  [.PI/4,3/4*PI.] c= ].0,PI.[ by Lm9,Lm10,RCOMP_1:17;
A5:  f is_differentiable_on ].0,PI.[ by Lm2,FDIFF_2:16;
A6:  diff(f,x) = (f`|].0,PI.[).x by A3,A4,A5,FDIFF_1:def 8
              .= (cot`|].0,PI.[).x by Lm2,FDIFF_2:16
              .= diff(cot,x) by A3,A4,Lm2,FDIFF_1:def 8
              .= -1/(sin x)^2 by A3,A4,Lm4;
A7:  sin x <> 0 by A3,A4,COMPTRIG:23;
B8:  (sin.x)^2 + (cos.x)^2 = 1 by SIN_COS:31;
     x = arccot r;
     then r = cot x by A1,Th50
           .= cos x/sin x by SIN_COS4:def 2;
     then r * sin x = cos x by A7,XCMPLX_1:88;
     then
A9:  1 = (sin x)^2 * ( r^2 + 1 ) by B8;
A13: f is_differentiable_on ].0,PI.[ by Lm2,FDIFF_2:16;
A14: now
       let x0 be Real such that
  A15: x0 in ].0,PI.[;
  A16: diff(f,x0) = (f`|].0,PI.[).x0 by A13,A15,FDIFF_1:def 8
                 .= (cot`|].0,PI.[).x0 by Lm2,FDIFF_2:16
                 .= diff(cot,x0) by A15,Lm2,FDIFF_1:def 8
                 .= -1/(sin.x0)^2 by A15,Lm4;
       for x0 be Real st x0 in ].0,PI.[ holds -1/(sin.x0)^2 < 0
       proof
         let x0 be Real;
         assume x0 in ].0,PI.[;
         then 0 < sin.x0 by COMPTRIG:23;then
    A17: (sin.x0)^2 > 0 by SQUARE_1:74;
         1/(sin.x0)^2 > 0 /(sin.x0)^2 by A17,REAL_1:73;
         then -1/(sin.x0)^2 < -0 by XREAL_1:26;
         hence -1/(sin.x0)^2 < 0;
       end;
       hence diff(f,x0) < 0 by A15,A16;
     end;
A18: f|].0,PI.[ = f by RELAT_1:101;
     diff(g,r) = 1/(-(1/(sin x)^2)) by A2,A6,A13,A14,A18,Th22,FDIFF_2:48
              .= -1/(1/(sin x)^2) by XCMPLX_1:189
              .= -1/(r^2+1) by A9,XCMPLX_1:74;
     hence diff(arccot,r) = -1/(1+r^2);
end;

theorem
  arctan is_continuous_on tan.:].-PI/2,PI/2.[ by Th69,FDIFF_1:33;

theorem
  arccot is_continuous_on cot.:].0,PI.[ by Th70,FDIFF_1:33;

theorem
  dom arctan is open
proof
    for x0 be Real st x0 in ].-PI/2,PI/2.[ holds 0 < diff(tan,x0)
    proof
      let x0 be Real;
      assume
  A2: x0 in ].-PI/2,PI/2.[;
      0 < cos.x0 by A2,COMPTRIG:27;then
  A4: (cos.x0)^2 > 0 by SQUARE_1:74;
      1/(cos.x0)^2 > 0 /(cos.x0)^2 by A4,REAL_1:73;
      hence 0 < diff(tan,x0) by A2,Lm3;
    end;
    then rng (tan|].-PI/2,PI/2.[) is open by Lm1,FDIFF_2:41;
    hence dom arctan is open by FUNCT_1:55;
end;

theorem
  dom arccot is open
proof
    for x0 be Real st x0 in ].0,PI.[ holds diff(cot,x0) < 0
    proof
      let x0 be Real;
      assume
  A2: x0 in ].0,PI.[;
      0 < sin.x0 by A2,COMPTRIG:23;then
  A4: (sin.x0)^2 > 0 by SQUARE_1:74;
      1/(sin.x0)^2 > 0 /(sin.x0)^2 by A4,REAL_1:73;
      then -1/(sin.x0)^2 < -0 by XREAL_1:26;
      hence diff(cot,x0) < 0 by A2,Lm4;
    end;
    then rng (cot|].0,PI.[) is open by Lm2,FDIFF_2:41;
    hence dom arccot is open by FUNCT_1:55;
end;

begin ::  Differentiation Formulas of arctan,arccot

:: f.x=arctan.x
theorem Th79:
  Z c= ].-1,1.[ implies arctan is_differentiable_on Z &
  for x st x in Z holds ((arctan)`|Z).x = 1/(1+x^2)
proof
    assume
A1: Z c= ].-1,1.[;then
A2: arctan is_differentiable_on Z by Th71,FDIFF_1:34;
    for x st x in Z holds ((arctan)`|Z).x = 1/(1+x^2)
    proof
      let x be Real;
      assume
  A4: x in Z;then
  A5: -1 <= x & x <= 1 by A1,XXREAL_1:4;
      thus ((arctan)`|Z).x = diff(arctan,x) by A2,A4,FDIFF_1:def 8
                          .= 1/(1+x^2) by A5,Th73;
    end;
    hence thesis by A1,Th71,FDIFF_1:34;
end;

:: f.x=arccot.x
theorem Th80:
  Z c= ].-1,1.[ implies arccot is_differentiable_on Z &
  for x st x in Z holds ((arccot)`|Z).x = -1/(1+x^2)
proof
    assume
A1: Z c= ].-1,1.[;then
A2: arccot is_differentiable_on Z by Th72,FDIFF_1:34;
    for x st x in Z holds ((arccot)`|Z).x = -1/(1+x^2)
    proof
      let x be Real;
      assume
  A4: x in Z;then
  A5: -1 <= x & x <= 1 by A1,XXREAL_1:4;
      thus ((arccot)`|Z).x = diff(arccot,x) by A2,A4,FDIFF_1:def 8
                          .= -1/(1+x^2) by A5,Th74;
    end;
    hence thesis by A1,Th72,FDIFF_1:34;
end;

::f.x=r*arctanx
theorem
  Z c= ].-1,1.[ implies r(#)arctan is_differentiable_on Z &
  for x st x in Z holds ((r(#)arctan)`|Z).x = r/(1+x^2)
proof
    assume
A1: Z c= ].-1,1.[;
    ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
    then ].-1,1.[ c= dom arctan by Th21,XBOOLE_1:1;
    then Z c= dom arctan by A1,XBOOLE_1:1;then
A2: Z c= dom (r(#)arctan) by VALUED_1:def 5;
A3: arctan is_differentiable_on Z by A1,Th79;
    for x st x in Z holds ((r(#)arctan)`|Z).x = r/(1+x^2)
    proof
      let x;
      assume
  A4: x in Z;then
  A5: -1 < x & x < 1 by A1,XXREAL_1:4;
      ((r(#)arctan)`|Z).x = r*diff(arctan,x) by A2,A3,A4,FDIFF_1:28
                         .= r*(1/(1+x^2)) by A5,Th73
                         .= r/(1+x^2);
      hence thesis;
    end;
    hence thesis by A2,A3,FDIFF_1:28;
end;

::f.x=r*arccotx
theorem
  Z c= ].-1,1.[ implies r(#)arccot is_differentiable_on Z &
  for x st x in Z holds ((r(#)arccot)`|Z).x = -r/(1+x^2)
proof
    assume
A1: Z c= ].-1,1.[;
    ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
    then ].-1,1.[ c= dom arccot by Th22,XBOOLE_1:1;
    then Z c= dom arccot by A1,XBOOLE_1:1;then
A2: Z c= dom (r(#)arccot) by VALUED_1:def 5;
A3: arccot is_differentiable_on Z by A1,Th80;
    for x st x in Z holds ((r(#)arccot)`|Z).x = -r/(1+x^2)
    proof
      let x;
      assume
  A4: x in Z;then
  A5: -1 < x & x < 1 by A1,XXREAL_1:4;
      ((r(#)arccot)`|Z).x = r*diff(arccot,x) by A2,A3,A4,FDIFF_1:28
                         .= r*(-1/(1+x^2)) by A5,Th74
                         .= -r/(1+x^2);
      hence thesis;
    end;
    hence thesis by A2,A3,FDIFF_1:28;
end;

theorem Th83:
  f is_differentiable_in x & f.x > -1 & f.x < 1 implies
  (arctan)*f is_differentiable_in x &
  diff((arctan)*f,x) = diff(f,x)/(1+(f.x)^2)
proof
    assume that
A1: f is_differentiable_in x and
A2: f.x > -1 & f.x < 1;
    f.x in ].-1,1.[ by A2,XXREAL_1:4;then
A3: arctan is_differentiable_in f.x by Th71,FDIFF_1:16;
    then diff(arctan*f,x) = diff(arctan,f.x)*diff(f,x) by A1,FDIFF_2:13
                         .= diff(f,x)*(1/(1+(f.x)^2)) by A2,Th73
                         .= diff(f,x)/(1+(f.x)^2);
    hence thesis by A1,A3,FDIFF_2:13;
end;

theorem Th84:
  f is_differentiable_in x & f.x > -1 & f.x < 1 implies
  (arccot)*f is_differentiable_in x &
  diff((arccot)*f,x) = -diff(f,x)/(1+(f.x)^2)
proof
    assume that
A1: f is_differentiable_in x and
A2: f.x > -1 & f.x < 1;
    f.x in ]. -1,1 .[ by A2,XXREAL_1:4;then
A3: arccot is_differentiable_in f.x by Th72,FDIFF_1:16;
    then diff(arccot*f,x) = diff(arccot,f.x)*diff(f,x) by A1,FDIFF_2:13
                         .= diff(f,x)*(-1/(1+(f.x)^2)) by A2,Th74
                         .= -diff(f,x)/(1+(f.x)^2);
    hence thesis by A1,A3,FDIFF_2:13;
end;

::f.x=arctan.(r*x+s)
theorem Th85:
 Z c= dom ((arctan)*f) &
 (for x st x in Z holds f.x=r*x+s & f.x > -1 & f.x < 1)
 implies (arctan)*f is_differentiable_on Z &
 for x st x in Z holds (((arctan)*f)`|Z).x = r/(1+(r*x+s)^2)
proof
    assume that
A1: Z c= dom ((arctan)*f) and
A2: for x st x in Z holds f.x=r*x+s & f.x > -1 & f.x < 1;
A3: for x st x in Z holds f.x=r*x+s by A2;
    for y st y in Z holds y in dom f by A1,FUNCT_1:21;then
A4: Z c= dom f by TARSKI:def 3;then
A5: f is_differentiable_on Z & for x st x in Z holds (f`|Z).x = r
    by A3,FDIFF_1:31;
A6: for x st x in Z holds (arctan)*f is_differentiable_in x
    proof
      let x;
      assume
  A7: x in Z;then
  A8: f is_differentiable_in x by A5,FDIFF_1:16;
      f.x > -1 & f.x < 1 by A2,A7;
      hence (arctan)*f is_differentiable_in x by A8,Th83;
    end;
    then
A9: (arctan)*f is_differentiable_on Z by A1,FDIFF_1:16;
    for x st x in Z holds (((arctan)*f)`|Z).x = r/(1+(r*x+s)^2)
    proof
      let x;
      assume
 A10: x in Z;then
 A11: f is_differentiable_in x by A5,FDIFF_1:16;
      f.x > -1 & f.x < 1 by A2,A10;then
      diff((arctan)*f,x) = diff(f,x)/(1+(f.x)^2) by A11,Th83
                        .= (f`|Z).x/(1+(f.x)^2) by A5,A10,FDIFF_1:def 8
                        .= r/(1+(f.x)^2) by A3,A4,A10,FDIFF_1:31
                        .= r/(1+(r*x+s)^2) by A2,A10;
      hence thesis by A9,A10,FDIFF_1:def 8;
    end;
    hence thesis by A1,A6,FDIFF_1:16;
end;

::f.x=arccot.(r*x+s)
theorem Th86:
 Z c= dom ((arccot)*f) &
 (for x st x in Z holds f.x=r*x+s & f.x > -1 & f.x < 1)
 implies (arccot)*f is_differentiable_on Z &
 for x st x in Z holds (((arccot)*f)`|Z).x = -r/(1+(r*x+s)^2)
proof
    assume that
A1: Z c= dom ((arccot)*f) and
A2: for x st x in Z holds f.x=r*x+s & f.x > -1 & f.x < 1;
A3: for x st x in Z holds f.x=r*x+s by A2;
    for y st y in Z holds y in dom f by A1,FUNCT_1:21;then
A4: Z c= dom f by TARSKI:def 3;then
A5: f is_differentiable_on Z & for x st x in Z holds (f`|Z).x = r
    by A3,FDIFF_1:31;
A6: for x st x in Z holds (arccot)*f is_differentiable_in x
    proof
      let x;
      assume
  A7: x in Z;then
  A8: f is_differentiable_in x by A5,FDIFF_1:16;
      f.x > -1 & f.x < 1 by A2,A7;
      hence (arccot)*f is_differentiable_in x by A8,Th84;
    end;
    then
A9: (arccot)*f is_differentiable_on Z by A1,FDIFF_1:16;
    for x st x in Z holds (((arccot)*f)`|Z).x = -r/(1+(r*x+s)^2)
    proof
      let x;
      assume
 A10: x in Z;then
 A11: f is_differentiable_in x by A5,FDIFF_1:16;
      f.x > -1 & f.x < 1 by A2,A10;then
      diff((arccot)*f,x) = -diff(f,x)/(1+(f.x)^2) by A11,Th84
                        .= -(f`|Z).x/(1+(f.x)^2) by A5,A10,FDIFF_1:def 8
                        .= -r/(1+(f.x)^2) by A3,A4,A10,FDIFF_1:31
                        .= -r/(1+(r*x+s)^2) by A2,A10;
      hence thesis by A9,A10,FDIFF_1:def 8;
    end;
    hence thesis by A1,A6,FDIFF_1:16;
end;

::f.x=ln(arctan.x)
theorem
  Z c= dom (ln*(arctan)) & Z c= ].-1,1.[ &
  (for x st x in Z holds arctan.x>0) implies
  ln*(arctan) is_differentiable_on Z & for x st x in Z holds
  ((ln*(arctan))`|Z).x = 1/((1+x^2)*arctan.x)
proof
    assume that
A1: Z c= dom (ln*arctan) and
A2: Z c= ].-1,1.[ and
A3: for x st x in Z holds arctan.x > 0;
A4: for x st x in Z holds ln*arctan is_differentiable_in x
    proof
      let x;
      assume
  A5: x in Z;
      arctan is_differentiable_on Z by A2,Th79;then
  A6: arctan is_differentiable_in x by A5,FDIFF_1:16;
      arctan.x >0 by A3,A5;
      hence ln*arctan is_differentiable_in x by A6,TAYLOR_1:20;
    end;
    then
A7: ln*arctan is_differentiable_on Z by A1,FDIFF_1:16;
    for x st x in Z holds
    ((ln*(arctan))`|Z).x = 1/((1+x^2)*arctan.x)
    proof
      let x;
      assume
 A8:  x in Z;then
 A9:  -1 < x & x < 1 by A2,XXREAL_1:4;
      arctan is_differentiable_on Z by A2,Th79;then
 A10: arctan is_differentiable_in x by A8,FDIFF_1:16;
      arctan.x >0 by A3,A8;
      then diff(ln*arctan,x) = diff(arctan,x)/arctan.x by A10,TAYLOR_1:20
                            .= (1/(1+x^2))/arctan.x by A9,Th73
                            .= 1/((1+x^2)*arctan.x) by XCMPLX_1:79;
      hence thesis by A7,A8,FDIFF_1:def 8;
    end;
    hence thesis by A1,A4,FDIFF_1:16;
end;

::f.x=ln(arccot.x)
theorem
  Z c= dom (ln*(arccot)) & Z c= ].-1,1.[ &
  (for x st x in Z holds arccot.x>0) implies
  ln*(arccot) is_differentiable_on Z & for x st x in Z holds
  ((ln*(arccot))`|Z).x = -1/((1+x^2)*arccot.x)
proof
    assume that
A1: Z c= dom (ln*arccot) and
A2: Z c= ].-1,1.[ and
A3: for x st x in Z holds arccot.x > 0;
A4: for x st x in Z holds ln*arccot is_differentiable_in x
    proof
      let x;
      assume
  A5: x in Z;
      arccot is_differentiable_on Z by A2,Th80;then
  A6: arccot is_differentiable_in x by A5,FDIFF_1:16;
      arccot.x >0 by A3,A5;
      hence ln*arccot is_differentiable_in x by A6,TAYLOR_1:20;
    end;
    then
A7: ln*arccot is_differentiable_on Z by A1,FDIFF_1:16;
    for x st x in Z holds
    ((ln*(arccot))`|Z).x = -1/((1+x^2)*arccot.x)
    proof
      let x;
      assume
 A8:  x in Z;then
 A9:  -1 < x & x < 1 by A2,XXREAL_1:4;
      arccot is_differentiable_on Z by A2,Th80;then
 A10: arccot is_differentiable_in x by A8,FDIFF_1:16;
      arccot.x >0 by A3,A8;
      then diff(ln*arccot,x) = diff(arccot,x)/arccot.x by A10,TAYLOR_1:20
                            .= (-1/(1+x^2))/arccot.x by A9,Th74
                            .= -(1/(1+x^2))/arccot.x
                            .= -1/((1+x^2)*arccot.x) by XCMPLX_1:79;
      hence thesis by A7,A8,FDIFF_1:def 8;
    end;
    hence thesis by A1,A4,FDIFF_1:16;
end;

::f.x=(arctan)|^n
theorem Th89:
  Z c= dom (( #Z n)*(arctan)) & Z c=].-1,1.[ implies
  ( #Z n)*(arctan) is_differentiable_on Z & for x st x in Z holds
  ((( #Z n)*arctan)`|Z).x = n*(arctan.x) #Z (n-1) / (1+x^2)
proof
    assume that
A1: Z c= dom (( #Z n)*arctan) and
A2: Z c= ].-1,1.[;
A3: for x st x in Z holds ( #Z n)*arctan is_differentiable_in x
    proof
      let x;
      assume
  A4: x in Z;
      arctan is_differentiable_on Z by A2,Th79;
      then arctan is_differentiable_in x by A4,FDIFF_1:16;
      hence thesis by TAYLOR_1:3;
    end;
    then
A5: ( #Z n)*(arctan) is_differentiable_on Z by A1,FDIFF_1:16;
    for x st x in Z holds
    ((( #Z n)*(arctan))`|Z).x = n*(arctan.x) #Z (n-1) / (1+x^2)
    proof
      let x;
      assume
  A6: x in Z;then
  A7: -1 < x & x < 1 by A2,XXREAL_1:4;
      arctan is_differentiable_on Z by A2,Th79;then
  A8: arctan is_differentiable_in x by A6,FDIFF_1:16;
      ((( #Z n)*arctan)`|Z).x = diff(( #Z n)*arctan,x) by A5,A6,FDIFF_1:def 8
                             .= (n*((arctan.x) #Z (n-1))) * diff(arctan,x)
                                by A8,TAYLOR_1:3
                             .= (n*((arctan.x) #Z (n-1))) *(1/(1+x^2))
                                by A7,Th73
                             .= n*(arctan.x) #Z (n-1) / (1+x^2);
      hence thesis;
    end;
    hence thesis by A1,A3,FDIFF_1:16;
end;

::f.x=(arccot)|^n
theorem Th90:
  Z c= dom (( #Z n)*(arccot)) & Z c=].-1,1.[ implies
  ( #Z n)*(arccot) is_differentiable_on Z & for x st x in Z holds
  ((( #Z n)*arccot)`|Z).x = -n*(arccot.x) #Z (n-1) / (1+x^2)
proof
    assume that
A1: Z c= dom (( #Z n)*arccot) and
A2: Z c= ].-1,1.[;
A3: for x st x in Z holds ( #Z n)*arccot is_differentiable_in x
    proof
      let x;
      assume
  A4: x in Z;
      arccot is_differentiable_on Z by A2,Th80;
      then arccot is_differentiable_in x by A4,FDIFF_1:16;
      hence thesis by TAYLOR_1:3;
    end;
    then
A5: ( #Z n)*(arccot) is_differentiable_on Z by A1,FDIFF_1:16;
    for x st x in Z holds
    ((( #Z n)*(arccot))`|Z).x = -n*(arccot.x) #Z (n-1) / (1+x^2)
    proof
      let x;
      assume
  A6: x in Z;then
  A7: -1 < x & x < 1 by A2,XXREAL_1:4;
      arccot is_differentiable_on Z by A2,Th80;then
  A8: arccot is_differentiable_in x by A6,FDIFF_1:16;
      ((( #Z n)*arccot)`|Z).x = diff(( #Z n)*arccot,x) by A5,A6,FDIFF_1:def 8
                             .= (n*((arccot.x) #Z (n-1))) * diff(arccot,x)
                                by A8,TAYLOR_1:3
                             .= (n*((arccot.x) #Z (n-1))) * (-1/(1+x^2))
                                by A7,Th74
                             .= -n*(arccot.x) #Z (n-1) / (1+x^2);
      hence thesis;
    end;
    hence thesis by A1,A3,FDIFF_1:16;
end;

::f.x=(1/2)*(arctan)|^2
theorem
  Z c= dom ((1/2)(#)(( #Z 2)*(arctan))) & Z c=].-1,1.[ implies
  (1/2)(#)(( #Z 2)*(arctan)) is_differentiable_on Z & for x st x in Z holds
  (((1/2)(#)(( #Z 2)*(arctan)))`|Z).x = arctan.x / (1+x^2)
proof
    assume that
A1: Z c= dom ((1/2)(#)(( #Z 2)*(arctan))) and
A2: Z c=].-1,1.[;
A3: Z c= dom (( #Z 2)*(arctan)) by A1,VALUED_1:def 5;then
A4: ( #Z 2)*(arctan) is_differentiable_on Z & for x st x in Z holds
    ((( #Z 2)*(arctan))`|Z).x =2*(arctan.x) #Z (2-1) / (1+x^2)  by A2,Th89;
    for x st x in Z holds
    (((1/2)(#)(( #Z 2)*(arctan)))`|Z).x = arctan.x / (1+x^2)
    proof
      let x;
      assume
  A5: x in Z;then
      (((1/2)(#)(( #Z 2)*(arctan)))`|Z).x
      = (1/2)*diff((( #Z 2)*arctan),x) by A1,A4,FDIFF_1:28
     .= (1/2)*((( #Z 2)*(arctan))`|Z).x by A4,A5,FDIFF_1:def 8
     .= (1/2)*((2*(arctan.x) #Z (2-1)) / (1+x^2)) by A2,A3,A5,Th89
     .= (1/2)*(2*arctan.x / (1+x^2)) by PREPOWER:45
     .= arctan.x / (1+x^2);
      hence thesis;
    end;
    hence thesis by A1,A4,FDIFF_1:28;
end;

::f.x=(1/2)*(arccot)|^2
theorem
  Z c= dom ((1/2)(#)(( #Z 2)*(arccot))) & Z c=].-1,1.[ implies
  (1/2)(#)(( #Z 2)*(arccot)) is_differentiable_on Z & for x st x in Z holds
  (((1/2)(#)(( #Z 2)*(arccot)))`|Z).x = -arccot.x / (1+x^2)
proof
    assume that
A1: Z c= dom ((1/2)(#)(( #Z 2)*(arccot))) and
A2: Z c=].-1,1.[;
A3: Z c= dom (( #Z 2)*(arccot)) by A1,VALUED_1:def 5;then
A4: ( #Z 2)*(arccot) is_differentiable_on Z & for x st x in Z holds
    ((( #Z 2)*(arccot))`|Z).x = -2*(arccot.x) #Z (2-1) / (1+x^2)  by A2,Th90;
    for x st x in Z holds
    (((1/2)(#)(( #Z 2)*(arccot)))`|Z).x = -arccot.x / (1+x^2)
    proof
      let x;
      assume
  A5: x in Z;then
      (((1/2)(#)(( #Z 2)*(arccot)))`|Z).x
      = (1/2)*diff((( #Z 2)*arccot),x) by A1,A4,FDIFF_1:28
     .= (1/2)*((( #Z 2)*(arccot))`|Z).x by A4,A5,FDIFF_1:def 8
     .= (1/2)*(-2*(arccot.x) #Z (2-1) / (1+x^2)) by A2,A3,A5,Th90
     .= -(1/2)*(2*(arccot.x) #Z 1 / (1+x^2))
     .= -(1/2)*(2*arccot.x / (1+x^2)) by PREPOWER:45
     .= -arccot.x / (1+x^2);
      hence thesis;
    end;
    hence thesis by A1,A4,FDIFF_1:28;
end;

::f.x=x*arctan.x
theorem Th93:
  Z c= ].-1,1.[ implies (id Z)(#)(arctan) is_differentiable_on Z &
  for x st x in Z holds (((id Z)(#)(arctan))`|Z).x = arctan.x + x/(1+x^2)
proof
    assume
A1: Z c= ].-1,1.[;
A2: Z c= dom (id Z) by FUNCT_1:34;
    ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
    then ].-1,1.[ c= dom arctan by Th21,XBOOLE_1:1;
    then Z c= dom arctan by A1,XBOOLE_1:1;
    then Z c= dom (id Z) /\ dom arctan by A2,XBOOLE_1:19;then
A3: Z c= dom ((id Z)(#)(arctan)) by VALUED_1:def 4;
A4: for x st x in Z holds (id Z).x = 1*x+0 by FUNCT_1:35;then
A5: id Z is_differentiable_on Z & for x st x in Z
    holds ((id Z)`|Z).x = 1 by A2,FDIFF_1:31;
A6: arctan is_differentiable_on Z by A1,Th79;
    for x st x in Z holds (((id Z)(#)(arctan))`|Z).x = arctan.x + x/(1+x^2)
    proof
      let x;
      assume
  A7: x in Z;then
  A8: -1 < x & x < 1 by A1,XXREAL_1:4;
      (((id Z)(#)(arctan))`|Z).x
      = (arctan.x)*diff((id Z),x) + ((id Z).x)*diff(arctan,x)
        by A3,A5,A6,A7,FDIFF_1:29
     .= (arctan.x)*((id Z)`|Z).x + ((id Z).x)*diff(arctan,x)
        by A5,A7,FDIFF_1:def 8
     .= (arctan.x)*1 + ((id Z).x)*diff(arctan,x) by A2,A4,A7,FDIFF_1:31
     .= arctan.x + x*diff(arctan,x) by A7,FUNCT_1:35
     .= arctan.x + x*(1/(1+x^2)) by A8,Th73
     .= arctan.x + x/(1+x^2);
     hence thesis;
    end;
    hence thesis by A3,A5,A6,FDIFF_1:29;
end;

::f.x=x*arccot.x
theorem Th94:
  Z c= ].-1,1.[ implies (id Z)(#)(arccot) is_differentiable_on Z &
  for x st x in Z holds (((id Z)(#)(arccot))`|Z).x = arccot.x - x/(1+x^2)
proof
    assume
A1: Z c= ].-1,1.[;
A2: Z c= dom (id Z) by FUNCT_1:34;
    ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
    then ].-1,1.[ c= dom arccot by Th22,XBOOLE_1:1;
    then Z c= dom arccot by A1,XBOOLE_1:1;
    then Z c= dom (id Z) /\ dom arccot by A2,XBOOLE_1:19;then
A3: Z c= dom ((id Z)(#)(arccot)) by VALUED_1:def 4;
A4: for x st x in Z holds (id Z).x = 1*x+0 by FUNCT_1:35;then
A5: id Z is_differentiable_on Z & for x st x in Z
    holds ((id Z)`|Z).x = 1 by A2,FDIFF_1:31;
A6: arccot is_differentiable_on Z by A1,Th80;
    for x st x in Z holds (((id Z)(#)(arccot))`|Z).x = arccot.x - x/(1+x^2)
    proof
      let x;
      assume
  A7: x in Z;then
  A8: -1 < x & x < 1 by A1,XXREAL_1:4;
      (((id Z)(#)(arccot))`|Z).x
      = (arccot.x)*diff((id Z),x) + ((id Z).x)*diff(arccot,x)
        by A3,A5,A6,A7,FDIFF_1:29
     .= (arccot.x)*((id Z)`|Z).x + ((id Z).x)*diff(arccot,x)
        by A5,A7,FDIFF_1:def 8
     .= (arccot.x)*1 + ((id Z).x)*diff(arccot,x) by A2,A4,A7,FDIFF_1:31
     .= arccot.x + x*diff(arccot,x) by A7,FUNCT_1:35
     .= arccot.x + x*(-1/(1+x^2)) by A8,Th74
     .= arccot.x - x/(1+x^2);
     hence thesis;
    end;
    hence thesis by A3,A5,A6,FDIFF_1:29;
end;

::f.x=(r*x+s)*arctan.x
theorem
  Z c= dom (f(#)(arctan)) & Z c= ].-1,1.[ &
  (for x st x in Z holds f.x=r*x+s) implies
  f(#)(arctan) is_differentiable_on Z & for x st x in Z holds
  ((f(#)(arctan))`|Z).x = r*arctan.x + (r*x+s)/(1+x^2)
proof
    assume that
A1: Z c= dom (f(#)(arctan)) and
A2: Z c= ].-1,1.[ and
A3: (for x st x in Z holds f.x=r*x+s);
    Z c= dom f /\ dom arctan by A1,VALUED_1:def 4;then
A4: Z c= dom f by XBOOLE_1:18;then
A5: f is_differentiable_on Z & for x st x in Z holds (f`|Z).x = r
    by A3,FDIFF_1:31;
A6: arctan is_differentiable_on Z by A2,Th79;
    for x st x in Z holds
    ((f(#)(arctan))`|Z).x = r*arctan.x + (r*x+s)/(1+x^2)
    proof
      let x;
      assume
  A7: x in Z;then
  A8: -1 < x & x < 1 by A2,XXREAL_1:4;
      ((f(#)(arctan))`|Z).x
      = (arctan.x)*diff(f,x) + (f.x)*diff(arctan,x) by A1,A5,A6,A7,FDIFF_1:29
     .= (arctan.x)*(f`|Z).x + (f.x)*diff(arctan,x) by A5,A7,FDIFF_1:def 8
     .= (arctan.x)*r + (f.x)*diff(arctan,x) by A3,A4,A7,FDIFF_1:31
     .= (arctan.x)*r + (f.x)*(1/(1+x^2)) by A8,Th73
     .= r*arctan.x + (r*x+s)/(1+x^2) by A3,A7;
      hence thesis;
    end;
    hence thesis by A1,A5,A6,FDIFF_1:29;
end;

::f.x=(r*x+s)*arccot.x
theorem
  Z c= dom (f(#)(arccot)) & Z c= ].-1,1.[ &
  (for x st x in Z holds f.x=r*x+s) implies
  f(#)(arccot) is_differentiable_on Z & for x st x in Z holds
  ((f(#)(arccot))`|Z).x = r*arccot.x - (r*x+s)/(1+x^2)
proof
    assume that
A1: Z c= dom (f(#)(arccot)) and
A2: Z c= ].-1,1.[ and
A3: (for x st x in Z holds f.x=r*x+s);
    Z c= dom f /\ dom arccot by A1,VALUED_1:def 4;then
A4: Z c= dom f by XBOOLE_1:18;then
A5: f is_differentiable_on Z & for x st x in Z holds (f`|Z).x = r
    by A3,FDIFF_1:31;
A6: arccot is_differentiable_on Z by A2,Th80;
    for x st x in Z holds
    ((f(#)(arccot))`|Z).x = r*arccot.x - (r*x+s)/(1+x^2)
    proof
      let x;
      assume
  A7: x in Z;then
  A8: -1 < x & x < 1 by A2,XXREAL_1:4;
      ((f(#)(arccot))`|Z).x
      = (arccot.x)*diff(f,x) + (f.x)*diff(arccot,x) by A1,A5,A6,A7,FDIFF_1:29
     .= (arccot.x)*(f`|Z).x + (f.x)*diff(arccot,x) by A5,A7,FDIFF_1:def 8
     .= (arccot.x)*r + (f.x)*diff(arccot,x) by A3,A4,A7,FDIFF_1:31
     .= (arccot.x)*r + (f.x)*(-1/(1+x^2)) by A8,Th74
     .= (arccot.x)*r - (f.x)*(1/(1+x^2))
     .= r*arccot.x - (r*x+s)/(1+x^2) by A3,A7;
     hence thesis;
    end;
    hence thesis by A1,A5,A6,FDIFF_1:29;
end;

::f.x=(1/2)*arctan(2*x)
theorem
  Z c= dom ((1/2)(#)((arctan)*f)) & (for x st x in Z holds f.x=2*x &
  f.x > -1 & f.x < 1) implies (1/2)(#)((arctan)*f) is_differentiable_on Z
  & for x st x in Z holds (((1/2)(#)((arctan)*f))`|Z).x = 1/(1+(2*x)^2)
proof
    assume that
A1: Z c= dom ((1/2)(#)((arctan)*f)) and
A2: for x st x in Z holds f.x=2*x & f.x > -1 & f.x < 1;
A3: Z c= dom ((arctan)*f) by A1,VALUED_1:def 5;
A4: for x st x in Z holds f.x=2*x+0 & f.x > -1 & f.x < 1 by A2;then
A5: (arctan)*f is_differentiable_on Z & for x st x in Z holds
    (((arctan)*f)`|Z).x = 2/(1+(2*x+0)^2) by A3,Th85;
    for x st x in Z holds (((1/2)(#)((arctan)*f))`|Z).x = 1/(1+(2*x)^2)
    proof
        let x;
        assume
    A6: x in Z;then
        (((1/2)(#)((arctan)*f))`|Z).x
        = (1/2)*diff(((arctan)*f),x) by A1,A5,FDIFF_1:28
       .= (1/2)*(((arctan)*f)`|Z).x by A5,A6,FDIFF_1:def 8
       .= (1/2)*(2/(1+(2*x+0)^2)) by A3,A4,A6,Th85
       .= 1/(1+(2*x)^2);
        hence thesis;
    end;
    hence thesis by A1,A5,FDIFF_1:28;
end;

::f.x=(1/2)*arccot(2*x)
theorem
  Z c= dom ((1/2)(#)((arccot)*f)) & (for x st x in Z holds f.x=2*x &
  f.x > -1 & f.x < 1) implies (1/2)(#)((arccot)*f) is_differentiable_on Z
  & for x st x in Z holds (((1/2)(#)((arccot)*f))`|Z).x = -1/(1+(2*x)^2)
proof
    assume that
A1: Z c= dom ((1/2)(#)((arccot)*f)) and
A2: for x st x in Z holds f.x=2*x & f.x > -1 & f.x < 1;
A3: Z c= dom ((arccot)*f) by A1,VALUED_1:def 5;
A4: for x st x in Z holds f.x=2*x+0 & f.x > -1 & f.x < 1 by A2;then
A5: (arccot)*f is_differentiable_on Z & for x st x in Z holds
    (((arccot)*f)`|Z).x = -2/(1+(2*x+0)^2) by A3,Th86;
    for x st x in Z holds (((1/2)(#)((arccot)*f))`|Z).x = -1/(1+(2*x)^2)
    proof
      let x;
      assume
  A6: x in Z;then
      (((1/2)(#)((arccot)*f))`|Z).x
      = (1/2)*diff(((arccot)*f),x) by A1,A5,FDIFF_1:28
     .= (1/2)*(((arccot)*f)`|Z).x by A5,A6,FDIFF_1:def 8
     .= (1/2)*(-2/(1+(2*x+0)^2)) by A3,A4,A6,Th86
     .= -1/(1+(2*x)^2);
      hence thesis;
    end;
    hence thesis by A1,A5,FDIFF_1:28;
end;

::f.x=1+x|^2
theorem Th99:
  Z c= dom (f1+f2) & (for x st x in Z holds f1.x=1) & f2=#Z 2
  implies f1+f2 is_differentiable_on Z &
  for x st x in Z holds ((f1+f2)`|Z).x = 2*x
proof
    assume
A1: Z c= dom (f1+f2) & (for x st x in Z holds f1.x=1) & f2=#Z 2;
    then Z c= dom f1 /\ dom f2 by VALUED_1:def 1;then
A2: Z c= dom f1 & Z c= dom f2 by XBOOLE_1:18;
AA: for x st x in Z holds f1.x=0*x+1 by A1;then
A4: f1 is_differentiable_on Z & for x st x in Z
    holds (f1`|Z).x = 0 by A2,FDIFF_1:31;
A5: f2 is_differentiable_on Z
    proof
      for x st x in Z holds f2 is_differentiable_in x by A1,TAYLOR_1:2;
      hence f2 is_differentiable_on Z by A2,FDIFF_1:16;
    end;
A6: for x st x in Z holds (f2`|Z).x=2*x
    proof
      let x;
      assume
  A7: x in Z;
      2*(x #Z (2-1)) = 2*x by PREPOWER:45;
      then diff(f2,x) = 2*x by A1,TAYLOR_1:2;
      hence (f2`|Z).x = 2*x by A5,A7,FDIFF_1:def 8;
    end;
    for x st x in Z holds ((f1+f2)`|Z).x = 2*x
    proof
      let x;
      assume
  A8: x in Z;
      then ((f1+f2)`|Z).x = diff(f1,x) + diff(f2,x) by FDIFF_1:26,A1,A4,A5
      .= (f1`|Z).x + diff(f2,x) by A4,A8,FDIFF_1:def 8
      .= (f1`|Z).x + (f2`|Z).x  by A5,A8,FDIFF_1:def 8
      .= 0 + (f2`|Z).x by A2,AA,A8,FDIFF_1:31
      .= 2*x by A6,A8;
      hence thesis;
    end;
    hence thesis by A1,A4,A5,FDIFF_1:26;
end;

::f.x=(1/2)ln(1+x|^2)
theorem Th100:
  Z c= dom ((1/2)(#)(ln*(f1+f2))) & f2=#Z 2 &
  (for x st x in Z holds f1.x=1 ) implies
  ((1/2)(#)(ln*(f1+f2))) is_differentiable_on Z & for x st x in Z holds
  (((1/2)(#)(ln*(f1+f2)))`|Z).x = x/(1+x^2)
proof
     assume that
A1:  Z c= dom ((1/2)(#)(ln*(f1+f2))) and
A2:  f2=#Z 2 and
A3:  (for x st x in Z holds f1.x=1);
A4:  Z c= dom (ln*(f1+f2)) by A1,VALUED_1:def 5;
     then for y st y in Z holds y in dom (f1+f2)
     by FUNCT_1:21;then
A5:  Z c= dom (f1+f2) by TARSKI:def 3;
A6:  f1+f2 is_differentiable_on Z &
     for x st x in Z holds ((f1+f2)`|Z).x = 2*x by A2,A3,A5,Th99;
     for x st x in Z holds ln*(f1+f2) is_differentiable_in x
     proof
       let x;
       assume
  A8:  x in Z;then
  A9:  (f1+f2) is_differentiable_in x by A6,FDIFF_1:16;
  A10: (f1+f2).x = f1.x+f2.x by A5,A8,VALUED_1:def 1
       .= 1+f2.x by A3,A8
       .= 1+(x #Z (1+1)) by A2,TAYLOR_1:def 1
       .= 1+(x #Z 1)*(x #Z 1) by TAYLOR_1:1
       .= 1+x*(x #Z 1) by PREPOWER:45
       .= 1+x*x by PREPOWER:45;
       (f1+f2).x > 0 by A10,XREAL_1:36,XREAL_1:65;
       hence ln*(f1+f2) is_differentiable_in x by A9,TAYLOR_1:20;
     end;
     then
A11: ln*(f1+f2) is_differentiable_on Z by A4,FDIFF_1:16;
     for x st x in Z holds (((1/2)(#)(ln*(f1+f2)))`|Z).x = x/(1+x^2)
     proof
       let x;
       assume
  A12: x in Z;
  A13: (f1+f2) is_differentiable_in x by A6,A12,FDIFF_1:16;
  A14: (f1+f2).x = f1.x+f2.x by A5,A12,VALUED_1:def 1
       .= 1+f2.x by A3,A12
       .= 1+(x #Z (1+1)) by A2,TAYLOR_1:def 1
       .= 1+(x #Z 1)*(x #Z 1) by TAYLOR_1:1
       .= 1+x*(x #Z 1) by PREPOWER:45
       .= 1+x*x by PREPOWER:45;
  A15: (f1+f2).x > 0 by A14,XREAL_1:36,XREAL_1:65;
  A16: diff(ln*(f1+f2),x) = diff((f1+f2),x)/((f1+f2).x)
       by A13,A15,TAYLOR_1:20
       .= ((f1+f2)`|Z).x/((f1+f2).x) by A6,A12,FDIFF_1:def 8
       .= (2*x)/(1+x^2) by A2,A3,A5,A12,A14,Th99;
       thus (((1/2)(#)(ln*(f1+f2)))`|Z).x
       = (1/2)*((2*x)/(1+x^2)) by A1,A11,A12,A16,FDIFF_1:28
      .= x/(1+x^2);
     end;
     hence thesis by A1,A11,FDIFF_1:28;
end;

::f.x=x*arctan.x-(1/2)ln(1+x|^2)
theorem
  Z c= dom ((id Z)(#)(arctan)-(1/2)(#)(ln*(f1+f2))) & Z c= ].-1,1.[ &
  f2=#Z 2 & (for x st x in Z holds f1.x=1 ) implies
  (id Z)(#)(arctan)-(1/2)(#)(ln*(f1+f2)) is_differentiable_on Z &
  for x st x in Z holds
  (((id Z)(#)(arctan)-(1/2)(#)(ln*(f1+f2)))`|Z).x = arctan.x
proof
    assume that
A1: Z c= dom ((id Z)(#)(arctan)-(1/2)(#)(ln*(f1+f2))) and
A2: Z c= ].-1,1.[ and
A3: f2=#Z 2 & (for x st x in Z holds f1.x=1);
A4: Z c= dom ((id Z)(#)(arctan)) /\ dom ((1/2)(#)(ln*(f1+f2)))
    by A1,VALUED_1:12;
A6: Z c= dom ((1/2)(#)(ln*(f1+f2))) by A4,XBOOLE_1:18;
A7: (id Z)(#)(arctan) is_differentiable_on Z & for x st x in Z holds
    (((id Z)(#)(arctan))`|Z).x = arctan.x+x/(1+x^2) by A2,Th93;
A8: ((1/2)(#)(ln*(f1+f2))) is_differentiable_on Z & for x st x in Z holds
    (((1/2)(#)(ln*(f1+f2)))`|Z).x = x/(1+x^2) by A3,A6,Th100;
    for x st x in Z holds
    (((id Z)(#)(arctan)-(1/2)(#)(ln*(f1+f2)))`|Z).x = arctan.x
    proof
      let x;
      assume
  A9: x in Z;
      hence (((id Z)(#)(arctan)-(1/2)(#)(ln*(f1+f2)))`|Z).x
      = diff((id Z)(#)(arctan),x)-diff((1/2)(#)(ln*(f1+f2)),x)
      by A1,A7,A8,FDIFF_1:27
      .= (((id Z)(#)(arctan))`|Z).x-diff((1/2)(#)(ln*(f1+f2)),x)
      by A7,A9,FDIFF_1:def 8
      .= (((id Z)(#)(arctan))`|Z).x-(((1/2)(#)(ln*(f1+f2)))`|Z).x
      by A8,A9,FDIFF_1:def 8
      .= arctan.x+x/(1+x^2)-(((1/2)(#)(ln*(f1+f2)))`|Z).x
      by A2,A9,Th93
      .= arctan.x+x/(1+x^2)-x/(1+x^2) by A3,A6,A9,Th100
      .= arctan.x;
    end;
    hence thesis by A1,A7,A8,FDIFF_1:27;
end;

::f.x=x*arccot.x+(1/2)ln(1+x|^2)
theorem
  Z c= dom ((id Z)(#)(arccot)+(1/2)(#)(ln*(f1+f2))) & Z c= ].-1,1.[ &
  f2=#Z 2 & (for x st x in Z holds f1.x=1 ) implies
  (id Z)(#)(arccot)+(1/2)(#)(ln*(f1+f2)) is_differentiable_on Z &
  for x st x in Z holds
  (((id Z)(#)(arccot)+(1/2)(#)(ln*(f1+f2)))`|Z).x = arccot.x
proof
    assume that
A1: Z c= dom ((id Z)(#)(arccot)+(1/2)(#)(ln*(f1+f2))) and
A2: Z c= ].-1,1.[ and
A3: f2=#Z 2 & (for x st x in Z holds f1.x=1);
A4: Z c= dom ((id Z)(#)(arccot)) /\ dom ((1/2)(#)(ln*(f1+f2)))
    by A1,VALUED_1:def 1;
A6: Z c= dom ((1/2)(#)(ln*(f1+f2))) by A4,XBOOLE_1:18;
A7: (id Z)(#)(arccot) is_differentiable_on Z & for x st x in Z holds
    (((id Z)(#)(arccot))`|Z).x = arccot.x-x/(1+x^2) by A2,Th94;
A8: ((1/2)(#)(ln*(f1+f2))) is_differentiable_on Z & for x st x in Z holds
    (((1/2)(#)(ln*(f1+f2)))`|Z).x = x/(1+x^2) by A3,A6,Th100;
    for x st x in Z holds
    (((id Z)(#)(arccot)+(1/2)(#)(ln*(f1+f2)))`|Z).x = arccot.x
    proof
      let x;
      assume
  A9: x in Z;
      hence (((id Z)(#)(arccot)+(1/2)(#)(ln*(f1+f2)))`|Z).x
      = diff((id Z)(#)(arccot),x)+diff((1/2)(#)(ln*(f1+f2)),x)
      by A1,A7,A8,FDIFF_1:26
      .= (((id Z)(#)(arccot))`|Z).x+diff((1/2)(#)(ln*(f1+f2)),x)
      by A7,A9,FDIFF_1:def 8
      .= (((id Z)(#)(arccot))`|Z).x+(((1/2)(#)(ln*(f1+f2)))`|Z).x
      by A8,A9,FDIFF_1:def 8
      .= arccot.x-x/(1+x^2)+(((1/2)(#)(ln*(f1+f2)))`|Z).x by A2,A9,Th94
      .= arccot.x-x/(1+x^2)+x/(1+x^2) by A3,A6,A9,Th100
      .= arccot.x;
    end;
    hence thesis by A1,A7,A8,FDIFF_1:26;
end;

::f.x=x*arctan(x/r)
theorem Th103:
  Z c= dom ((id Z)(#)((arctan)*f)) &
  (for x st x in Z holds f.x=x/r & f.x > -1 & f.x < 1) implies
  (id Z)(#)((arctan)*f) is_differentiable_on Z & for x st x in Z holds
  (((id Z)(#)((arctan)*f))`|Z).x = arctan.(x/r)+x/(r*(1+(x/r)^2))
proof
     assume that
A1:  Z c= dom ((id Z)(#)((arctan)*f)) and
A2:  for x st x in Z holds f.x=x/r & f.x > -1 & f.x < 1;
     for x st x in Z holds f.x=(1/r)*x+0
     proof
       let x;
       assume x in Z;
       then f.x=x/r by A2;
       hence f.x=(1/r)*x+0;
     end;
     then
A3:  for x st x in Z holds f.x=(1/r)*x+0 & f.x > -1 & f.x < 1 by A2;
A4:  Z c= dom (id Z) /\ dom ((arctan)*f) by A1,VALUED_1:def 4;then
A5:  Z c= dom (id Z) by XBOOLE_1:18;
A6:  Z c= dom ((arctan)*f) by A4,XBOOLE_1:18;
A7:  for x st x in Z holds (id Z).x = 1*x+0 by FUNCT_1:35;then
A8:  id Z is_differentiable_on Z & for x st x in Z
     holds ((id Z)`|Z).x = 1 by A5,FDIFF_1:31;
A9:  (arctan)*f is_differentiable_on Z & for x st x in Z holds
     (((arctan)*f)`|Z).x = (1/r)/(1+((1/r)*x+0)^2) by A3,A6,Th85;
A10: for x st x in Z holds (((arctan)*f)`|Z).x = 1/(r*(1+(x/r)^2))
     proof
       let x;
       assume x in Z;
       then (((arctan)*f)`|Z).x = (1/r)/(1+((1/r)*x+0)^2) by A3,A6,Th85
       .= 1/(r*(1+(x/r)^2)) by XCMPLX_1:79;
       hence thesis;
     end;
     for x st x in Z holds
     (((id Z)(#)((arctan)*f))`|Z).x = arctan.(x/r)+x/(r*(1+(x/r)^2))
     proof
        let x;
        assume
   A11: x in Z;then
   A12: ((arctan)*f).x = arctan.(f.x) by A6,FUNCT_1:22
        .= arctan.(x/r) by A2,A11;
        (((id Z)(#)((arctan)*f))`|Z).x
        = ((arctan)*f).x*diff((id Z),x) + ((id Z).x)*diff((arctan)*f,x)
        by A1,A8,A9,A11,FDIFF_1:29
        .= ((arctan)*f).x*((id Z)`|Z).x + ((id Z).x)*diff((arctan)*f,x)
        by A8,A11,FDIFF_1:def 8
        .= ((arctan)*f).x*1 + ((id Z).x)*diff((arctan)*f,x)
        by A5,A7,A11,FDIFF_1:31
        .= ((arctan)*f).x*1 + ((id Z).x)*(((arctan)*f)`|Z).x
        by A9,A11,FDIFF_1:def 8
        .= ((arctan)*f).x + x*(((arctan)*f)`|Z).x by A11,FUNCT_1:35
        .= arctan.(x/r) + x*(1/(r*(1+(x/r)^2))) by A10,A11,A12
        .= arctan.(x/r) + x/(r*(1+(x/r)^2));
        hence thesis;
      end;
      hence thesis by A1,A8,A9,FDIFF_1:29;
end;

::f.x=x*arccot(x/r)
theorem Th104:
  Z c= dom ((id Z)(#)((arccot)*f)) &
  (for x st x in Z holds f.x=x/r & f.x > -1 & f.x < 1) implies
  (id Z)(#)((arccot)*f) is_differentiable_on Z & for x st x in Z holds
  (((id Z)(#)((arccot)*f))`|Z).x = arccot.(x/r)-x/(r*(1+(x/r)^2))
proof
     assume that
A1:  Z c= dom ((id Z)(#)((arccot)*f)) and
A2:  for x st x in Z holds f.x=x/r & f.x > -1 & f.x < 1;
     for x st x in Z holds f.x=(1/r)*x+0
     proof
       let x;
       assume x in Z;
       then f.x=x/r by A2;
       hence f.x=(1/r)*x+0;
     end;
     then
A3:  for x st x in Z holds f.x=(1/r)*x+0 & f.x > -1 & f.x < 1 by A2;
A4:  Z c= dom (id Z) /\ dom ((arccot)*f) by A1,VALUED_1:def 4;then
A5:  Z c= dom (id Z) by XBOOLE_1:18;
A6:  Z c= dom ((arccot)*f) by A4,XBOOLE_1:18;
A7:  for x st x in Z holds (id Z).x = 1*x+0 by FUNCT_1:35;then
A8:  id Z is_differentiable_on Z & for x st x in Z
     holds ((id Z)`|Z).x = 1 by A5,FDIFF_1:31;
A9:  (arccot)*f is_differentiable_on Z & for x st x in Z holds
     (((arccot)*f)`|Z).x = -(1/r)/(1+((1/r)*x+0)^2) by A3,A6,Th86;
A10: for x st x in Z holds (((arccot)*f)`|Z).x = -1/(r*(1+(x/r)^2))
     proof
       let x;
       assume x in Z;
       then (((arccot)*f)`|Z).x = -(1/r)/(1+((1/r)*x+0)^2) by A3,A6,Th86
       .= -1/(r*(1+(x/r)^2)) by XCMPLX_1:79;
       hence thesis;
     end;
     for x st x in Z holds
     (((id Z)(#)((arccot)*f))`|Z).x = arccot.(x/r)-x/(r*(1+(x/r)^2))
     proof
        let x;
        assume
   A11: x in Z;then
   A12: ((arccot)*f).x = arccot.(f.x) by A6,FUNCT_1:22
        .= arccot.(x/r) by A2,A11;
        (((id Z)(#)((arccot)*f))`|Z).x
        = ((arccot)*f).x*diff((id Z),x) + ((id Z).x)*diff((arccot)*f,x)
        by A1,A8,A9,A11,FDIFF_1:29
        .= ((arccot)*f).x*((id Z)`|Z).x + ((id Z).x)*diff((arccot)*f,x)
        by A8,A11,FDIFF_1:def 8
        .= ((arccot)*f).x*1 + ((id Z).x)*diff((arccot)*f,x)
        by A5,A7,A11,FDIFF_1:31
        .= ((arccot)*f).x*1 + ((id Z).x)*(((arccot)*f)`|Z).x
        by A9,A11,FDIFF_1:def 8
        .= ((arccot)*f).x + x*(((arccot)*f)`|Z).x by A11,FUNCT_1:35
        .= arccot.(x/r) + x*(-1/(r*(1+(x/r)^2))) by A10,A11,A12
        .= arccot.(x/r) - x/(r*(1+(x/r)^2));
        hence thesis;
      end;
      hence thesis by A1,A8,A9,FDIFF_1:29;
end;

::f.x=1+(x/r)^2
theorem Th105:
  Z c= dom (f1+f2) & (for x st x in Z holds f1.x=1) & f2=( #Z 2)*f &
  (for x st x in Z holds f.x=x/r)
  implies f1+f2 is_differentiable_on Z &
  for x st x in Z holds ((f1+f2)`|Z).x = (2*x)/(r^2)
proof
     assume that
A1:  Z c= dom (f1+f2) and
A2:  (for x st x in Z holds f1.x=1) and
A3:  f2=( #Z 2)*f & (for x st x in Z holds f.x=x/r);
A4:  for x st x in Z holds f.x=(1/r)*x+0
     proof
        let x;
        assume x in Z;
        hence f.x = x/r by A3.= (1/r)*x+0;
     end;
AA:  Z c= dom f1 /\ dom f2 by A1,VALUED_1:def 1;then
A5:  Z c= dom f1 & Z c= dom f2 by XBOOLE_1:18;
A6:  for x st x in Z holds f1.x=0*x+1 by A2;then
A7:  f1 is_differentiable_on Z & for x st x in Z
     holds (f1`|Z).x = 0 by A5,FDIFF_1:31;
     for x st x in Z holds f2 is_differentiable_in x
     proof
       let x;
       assume
   A8: x in Z;
       Z c= dom (( #Z 2)*f) by A3,AA,XBOOLE_1:18;
       then for y st y in Z holds y in dom f
       by FUNCT_1:21;then
       Z c= dom f by TARSKI:def 3;
       then f is_differentiable_on Z by A4,FDIFF_1:31;
       then f is_differentiable_in x by A8,FDIFF_1:16;
       hence thesis by A3,TAYLOR_1:3;
     end;
     then
A9:  f2 is_differentiable_on Z by A5,FDIFF_1:16;
A10: for x st x in Z holds (f2`|Z).x = (2*x)/(r^2)
     proof
       let x;
       assume
  A11: x in Z;
       Z c= dom (( #Z 2)*f) by A3,AA,XBOOLE_1:18;
       then for y st y in Z holds y in dom f
       by FUNCT_1:21;then
  A12: Z c= dom f by TARSKI:def 3;then
  A13: f is_differentiable_on Z by A4,FDIFF_1:31;then
  A14: f is_differentiable_in x by A11,FDIFF_1:16;
       (f2`|Z).x = diff(( #Z 2)*f,x) by A3,A9,A11,FDIFF_1:def 8
       .= 2 * (f.x) #Z (2-1) *diff(f,x) by A14,TAYLOR_1:3
       .= 2*(f.x)*diff(f,x) by PREPOWER:45
       .= 2*(x/r)*diff(f,x) by A3,A11
       .= 2*(x/r)*(f`|Z).x by A11,A13,FDIFF_1:def 8
       .= 2*(x/r)*(1/r) by A4,A11,A12,FDIFF_1:31
       .= 2*((x/r)*(1/r))
       .= 2*((x*1)/(r*r)) by XCMPLX_1:77
       .= (2*x)/(r^2);
       hence thesis;
     end;
     for x st x in Z holds ((f1+f2)`|Z).x = (2*x)/(r^2)
     proof
       let x;
       assume
  A15: x in Z;
       then ((f1+f2)`|Z).x = diff(f1,x) + diff(f2,x) by A1,A7,A9,FDIFF_1:26
       .= (f1`|Z).x + diff(f2,x) by A7,A15,FDIFF_1:def 8
       .= (f1`|Z).x + (f2`|Z).x  by A9,A15,FDIFF_1:def 8
       .= 0 + (f2`|Z).x by A5,A6,A15,FDIFF_1:31
       .= (2*x)/(r^2) by A10,A15;
       hence thesis;
     end;
     hence thesis by A1,A7,A9,FDIFF_1:26;
end;

::f.x=(r/2)ln(1+(x/r)^2)
theorem Th106:
  Z c= dom ((r/2)(#)(ln*(f1+f2))) & (for x st x in Z holds f1.x=1) & r <> 0 &
  f2=( #Z 2)*f & (for x st x in Z holds f.x=x/r) implies
  ((r/2)(#)(ln*(f1+f2))) is_differentiable_on Z & for x st x in Z holds
  (((r/2)(#)(ln*(f1+f2)))`|Z).x = x/(r*(1+(x/r)^2))
proof
     assume that
A1:  Z c= dom ((r/2)(#)(ln*(f1+f2))) and
A2:  (for x st x in Z holds f1.x=1) and
A3:  r <> 0  and
A4:  f2=( #Z 2)*f & (for x st x in Z holds f.x=x/r);
A5:  Z c= dom (ln*(f1+f2)) by A1,VALUED_1:def 5;
     then for y st y in Z holds y in dom (f1+f2)
     by FUNCT_1:21;then
A6:  Z c= dom (f1+f2) by TARSKI:def 3;
     dom (f1+f2) = dom f1 /\ dom f2 by VALUED_1:def 1;then
A7:  Z c= dom f1 & Z c= dom f2 by A6,XBOOLE_1:18;
A8:  f1+f2 is_differentiable_on Z &
     for x st x in Z holds ((f1+f2)`|Z).x = (2*x)/(r^2) by A2,A4,A6,Th105;
     for x st x in Z holds ln*(f1+f2) is_differentiable_in x
     proof
       set g = #Z 2;
       let x;
       assume
  A10: x in Z;then
  A11: (f1+f2) is_differentiable_in x by A8,FDIFF_1:16;
  A13: (f1+f2).x = f1.x+f2.x by A6,A10,VALUED_1:def 1
       .= 1+(g*f).x by A2,A4,A10
       .= 1+g.(f.x) by A4,A7,A10,FUNCT_1:22
       .= 1+g.(x/r) by A4,A10
       .= 1+((x/r) #Z (1+1)) by TAYLOR_1:def 1
       .= 1+((x/r) #Z 1)*((x/r) #Z 1) by TAYLOR_1:1
       .= 1+(x/r)*((x/r) #Z 1) by PREPOWER:45
       .= 1+(x/r)*(x/r) by PREPOWER:45;
       (f1+f2).x > 0 by A13,XREAL_1:36,XREAL_1:65;
       hence ln*(f1+f2) is_differentiable_in x by A11,TAYLOR_1:20;
     end;
     then
A14: ln*(f1+f2) is_differentiable_on Z by A5,FDIFF_1:16;
     for x st x in Z holds (((r/2)(#)(ln*(f1+f2)))`|Z).x = x/(r*(1+(x/r)^2))
     proof
       set g = #Z 2;
       let x;
       assume
  A15: x in Z;
  A16: (f1+f2) is_differentiable_in x by A8,A15,FDIFF_1:16;
  A17: (f1+f2).x = f1.x+f2.x by A6,A15,VALUED_1:def 1
       .= 1+(g*f).x by A2,A4,A15
       .= 1+g.(f.x) by A4,A7,A15,FUNCT_1:22
       .= 1+g.(x/r) by A4,A15
       .= 1+((x/r) #Z (1+1)) by TAYLOR_1:def 1
       .= 1+((x/r) #Z 1)*((x/r) #Z 1) by TAYLOR_1:1
       .= 1+(x/r)*((x/r) #Z 1) by PREPOWER:45
       .= 1+(x/r)*(x/r) by PREPOWER:45;
  A18: (f1+f2).x > 0 by A17,XREAL_1:36,XREAL_1:65;
  A19: diff(ln*(f1+f2),x) = diff((f1+f2),x)/((f1+f2).x)
       by A16,A18,TAYLOR_1:20
       .= ((f1+f2)`|Z).x/((f1+f2).x) by A8,A15,FDIFF_1:def 8
       .= ((2*x)/(r^2))/(1+(x/r)^2) by A2,A4,A6,A15,A17,Th105;
       thus (((r/2)(#)(ln*(f1+f2)))`|Z).x = (r/2)*diff((ln*(f1+f2)),x)
       by A1,A14,A15,FDIFF_1:28
       .= (r*x)/(r^2)/(1+(x/r)^2) by A19
       .= ((r/r)*(x/r))/(1+(x/r)^2) by XCMPLX_1:77
       .= (1*(x/r))/(1+(x/r)^2) by A3,XCMPLX_1:60
       .= x/(r*(1+(x/r)^2)) by XCMPLX_1:79;
     end;
     hence thesis by A1,A14,FDIFF_1:28;
end;

::f.x=x*arctan.(x/r)-(r/2)ln(1+(x/r)^2)
theorem
  Z c= dom ((id Z)(#)((arctan)*f)-(r/2)(#)(ln*(f1+f2))) & r <> 0 &
  (for x st x in Z holds f.x=x/r & f.x > -1 & f.x < 1) &
  (for x st x in Z holds f1.x=1) &
  f2=( #Z 2)*f & (for x st x in Z holds f.x=x/r)
  implies (id Z)(#)((arctan)*f)-(r/2)(#)(ln*(f1+f2)) is_differentiable_on Z &
  for x st x in Z holds
  (((id Z)(#)((arctan)*f)-(r/2)(#)(ln*(f1+f2)))`|Z).x = arctan.(x/r)
proof
     assume that
A1:  Z c= dom ((id Z)(#)((arctan)*f)-(r/2)(#)(ln*(f1+f2))) and
A2:  r <> 0 and
A3:  (for x st x in Z holds f.x=x/r & f.x > -1 & f.x < 1) and
A4:  (for x st x in Z holds f1.x=1) and
A5:  f2=( #Z 2)*f & (for x st x in Z holds f.x=x/r);
A6:  Z c= dom ((id Z)(#)((arctan)*f)) /\ dom ((r/2)(#)(ln*(f1+f2)))
     by A1,VALUED_1:12;then
A7:  Z c= dom ((id Z)(#)((arctan)*f)) by XBOOLE_1:18;
A8:  Z c= dom ((r/2)(#)(ln*(f1+f2))) by A6,XBOOLE_1:18;
A9:  (id Z)(#)((arctan)*f) is_differentiable_on Z & for x st x in Z holds
     (((id Z)(#)((arctan)*f))`|Z).x = arctan.(x/r)+x/(r*(1+(x/r)^2))
     by A3,A7,Th103;
A10: (r/2)(#)(ln*(f1+f2)) is_differentiable_on Z & for x st x in Z holds
     (((r/2)(#)(ln*(f1+f2)))`|Z).x = x/(r*(1+(x/r)^2)) by A2,A4,A5,A8,Th106;
     for x st x in Z holds
     (((id Z)(#)((arctan)*f)-(r/2)(#)(ln*(f1+f2)))`|Z).x = arctan.(x/r)
     proof
       let x;
       assume
  A11: x in Z;
       hence (((id Z)(#)((arctan)*f)-(r/2)(#)(ln*(f1+f2)))`|Z).x
       = diff((id Z)(#)((arctan)*f),x)-diff((r/2)(#)(ln*(f1+f2)),x)
       by A1,A9,A10,FDIFF_1:27
       .= (((id Z)(#)((arctan)*f))`|Z).x-diff((r/2)(#)(ln*(f1+f2)),x)
       by A9,A11,FDIFF_1:def 8
       .= (((id Z)(#)((arctan)*f))`|Z).x-(((r/2)(#)(ln*(f1+f2)))`|Z).x
       by A10,A11,FDIFF_1:def 8
       .= arctan.(x/r)+x/(r*(1+(x/r)^2))-(((r/2)(#)(ln*(f1+f2)))`|Z).x
       by A3,A7,A11,Th103
       .= arctan.(x/r)+x/(r*(1+(x/r)^2))-x/(r*(1+(x/r)^2))
       by A2,A4,A5,A8,A11,Th106
      .= arctan.(x/r);
     end;
     hence thesis by A1,A9,A10,FDIFF_1:27;
end;

::f.x=x*arccot.(x/r)+(r/2)ln(1+(x/r)^2)
theorem
  Z c= dom ((id Z)(#)((arccot)*f)+(r/2)(#)(ln*(f1+f2))) & r <> 0 &
  (for x st x in Z holds f.x=x/r & f.x > -1 & f.x < 1) &
  (for x st x in Z holds f1.x=1) &
  f2=( #Z 2)*f & (for x st x in Z holds f.x=x/r)
  implies (id Z)(#)((arccot)*f)+(r/2)(#)(ln*(f1+f2)) is_differentiable_on Z &
  for x st x in Z holds
  (((id Z)(#)((arccot)*f)+(r/2)(#)(ln*(f1+f2)))`|Z).x = arccot.(x/r)
proof
     assume that
A1:  Z c= dom ((id Z)(#)((arccot)*f)+(r/2)(#)(ln*(f1+f2))) and
A2:  r <> 0 and
A3:  (for x st x in Z holds f.x=x/r & f.x > -1 & f.x < 1) and
A4:  (for x st x in Z holds f1.x=1) and
A5:  f2=( #Z 2)*f & (for x st x in Z holds f.x=x/r);
A6:  Z c= dom ((id Z)(#)((arccot)*f)) /\ dom ((r/2)(#)(ln*(f1+f2)))
     by A1,VALUED_1:def 1;then
A7:  Z c= dom ((id Z)(#)((arccot)*f)) by XBOOLE_1:18;
A8:  Z c= dom ((r/2)(#)(ln*(f1+f2))) by A6,XBOOLE_1:18;
A9:  (id Z)(#)((arccot)*f) is_differentiable_on Z & for x st x in Z holds
     (((id Z)(#)((arccot)*f))`|Z).x = arccot.(x/r)-x/(r*(1+(x/r)^2))
     by A3,A7,Th104;
A10: (r/2)(#)(ln*(f1+f2)) is_differentiable_on Z & for x st x in Z holds
     (((r/2)(#)(ln*(f1+f2)))`|Z).x = x/(r*(1+(x/r)^2)) by A2,A4,A5,A8,Th106;
     for x st x in Z holds
     (((id Z)(#)((arccot)*f)+(r/2)(#)(ln*(f1+f2)))`|Z).x = arccot.(x/r)
     proof
       let x;
       assume
  A11: x in Z;
       hence (((id Z)(#)((arccot)*f)+(r/2)(#)(ln*(f1+f2)))`|Z).x
       = diff((id Z)(#)((arccot)*f),x)+diff((r/2)(#)(ln*(f1+f2)),x)
       by A1,A9,A10,FDIFF_1:26
       .= (((id Z)(#)((arccot)*f))`|Z).x+diff((r/2)(#)(ln*(f1+f2)),x)
       by A9,A11,FDIFF_1:def 8
       .= (((id Z)(#)((arccot)*f))`|Z).x+(((r/2)(#)(ln*(f1+f2)))`|Z).x
       by A10,A11,FDIFF_1:def 8
       .= arccot.(x/r)-x/(r*(1+(x/r)^2))+(((r/2)(#)(ln*(f1+f2)))`|Z).x
       by A3,A7,A11,Th104
       .= arccot.(x/r)-x/(r*(1+(x/r)^2))+x/(r*(1+(x/r)^2))
       by A2,A4,A5,A8,A11,Th106
      .= arccot.(x/r);
     end;
     hence thesis by A1,A9,A10,FDIFF_1:26;
end;

::f.x=arctan.(1/x)
theorem
  Z c= dom (arctan*(f^)) &
  (for x st x in Z holds f.x = x & (f^).x > -1 & (f^).x < 1)
  implies (arctan*(f^)) is_differentiable_on Z &
  for x st x in Z holds ((arctan*(f^))`|Z).x = -1/(1+x^2)
proof
     assume that
A1:  Z c= dom (arctan*(f^)) and
A2:  for x st x in Z holds f.x = x & (f^).x > -1 & (f^).x < 1;
     dom (arctan*(f^)) c= dom (f^) by RELAT_1:44;then
A3:  Z c= dom(f^) by A1,XBOOLE_1:1;
     dom (f^) c= dom f by RFUNCT_1:11;then
A4:  Z c= dom f by A3,XBOOLE_1:1;
A5:  for x st x in Z holds f.x = x & f.x <> 0 by A2,A3,RFUNCT_1:13;then
A6:  f^ is_differentiable_on Z &
     for x st x in Z holds ((f^)`|Z).x = -1/x^2 by A4,FDIFF_5:4;
A7:  for x st x in Z holds arctan*(f^) is_differentiable_in x
     proof
       let x;
       assume
  A8:  x in Z;then
  A9:  f^ is_differentiable_in x by A6,FDIFF_1:16;
       (f^).x > -1 & (f^).x < 1 by A2,A8;
       hence arctan*(f^) is_differentiable_in x by A9,Th83;
     end;
     then
A11: arctan*(f^) is_differentiable_on Z by A1,FDIFF_1:16;
     for x st x in Z holds ((arctan*(f^))`|Z).x = -1/(1+x^2)
     proof
       let x;
       assume
  A12: x in Z;then
  A13: f^ is_differentiable_in x by A6,FDIFF_1:16;
  A14: (f^).x > -1 & (f^).x < 1 by A2,A12;
       f.x = x by A2,A12;
       then x <> 0 by A3,A12,RFUNCT_1:13;then
  A15: x^2 <> 0 by SQUARE_1:74;
       ((arctan*(f^))`|Z).x = diff((arctan)*(f^),x) by A11,A12,FDIFF_1:def 8
       .= diff((f^),x)/(1+((f^).x)^2) by A13,A14,Th83
       .= ((f^)`|Z).x/(1+((f^).x)^2) by A6,A12,FDIFF_1:def 8
       .= (-1/x^2)/(1+((f^).x)^2) by A4,A5,A12,FDIFF_5:4
       .= (-1/x^2)/(1+((f.x)")^2) by A3,A12,RFUNCT_1:def 8
       .= (-1/x^2)/(1+(1/x)^2) by A2,A12
       .= -(1/x^2)/(1+(1/x)^2)
       .= -1/((x^2)*(1+(1/x)^2)) by XCMPLX_1:79
       .= -1/((x^2)*1+(x^2)*(1/x)^2)
       .= -1/((x^2)+(x^2)*(1/(x*x))) by XCMPLX_1:103
       .= -1/((x^2)+((x^2)*1)/(x^2))
       .= -1/(1+x^2) by A15,XCMPLX_1:60;
       hence thesis;
     end;
     hence thesis by A1,A7,FDIFF_1:16;
end;

::f.x=arccot.(1/x)
theorem
  Z c= dom (arccot*(f^)) &
  (for x st x in Z holds f.x = x & (f^).x > -1 & (f^).x < 1)
  implies (arccot*(f^)) is_differentiable_on Z &
  for x st x in Z holds ((arccot*(f^))`|Z).x = 1/(1+x^2)
proof
     assume that
A1:  Z c= dom (arccot*(f^)) and
A2:  for x st x in Z holds f.x = x & (f^).x > -1 & (f^).x < 1;
     dom (arccot*(f^)) c= dom (f^) by RELAT_1:44;then
A3:  Z c= dom(f^) by A1,XBOOLE_1:1;
     dom (f^) c= dom f by RFUNCT_1:11;then
A4:  Z c= dom f by A3,XBOOLE_1:1;
A5:  for x st x in Z holds f.x = x & f.x <> 0 by A2,A3,RFUNCT_1:13;then
A6:  f^ is_differentiable_on Z &
     for x st x in Z holds ((f^)`|Z).x = -1/x^2 by A4,FDIFF_5:4;
A7:  for x st x in Z holds arccot*(f^) is_differentiable_in x
     proof
       let x;
       assume
  A8:  x in Z;then
  A9:  f^ is_differentiable_in x by A6,FDIFF_1:16;
       (f^).x > -1 & (f^).x < 1 by A2,A8;
       hence arccot*(f^) is_differentiable_in x by A9,Th84;
     end;
     then
A11: arccot*(f^) is_differentiable_on Z by A1,FDIFF_1:16;
     for x st x in Z holds ((arccot*(f^))`|Z).x = 1/(1+x^2)
     proof
       let x;
       assume
  A12: x in Z;then
  A13: f^ is_differentiable_in x by A6,FDIFF_1:16;
  A14: (f^).x > -1 & (f^).x < 1 by A2,A12;
       f.x = x by A2,A12;
       then x <> 0 by A3,A12,RFUNCT_1:13;then
  A15: x^2 <> 0 by SQUARE_1:74;
       ((arccot*(f^))`|Z).x = diff((arccot)*(f^),x)
       by A11,A12,FDIFF_1:def 8
       .= -diff((f^),x)/(1+((f^).x)^2) by A13,A14,Th84
       .= -((f^)`|Z).x/(1+((f^).x)^2) by A6,A12,FDIFF_1:def 8
       .= -(-1/x^2)/(1+((f^).x)^2) by A4,A5,A12,FDIFF_5:4
       .= -(-1/x^2)/(1+((f.x)")^2) by A3,A12,RFUNCT_1:def 8
       .= -(-1/x^2)/(1+(1/x)^2) by A2,A12
       .= (1/x^2)/(1+(1/x)^2)
       .= 1/((x^2)*(1+(1/x)^2)) by XCMPLX_1:79
       .= 1/((x^2)*1+(x^2)*(1/x)^2)
       .= 1/((x^2)+(x^2)*(1/(x*x))) by XCMPLX_1:103
       .= 1/((x^2)+((x^2)*1)/(x^2))
       .= 1/(1+x^2) by A15,XCMPLX_1:60;
       hence thesis;
     end;
     hence thesis by A1,A7,FDIFF_1:16;
end;

::f.x=arctan.(r+s*x+h*x^2)
theorem
  Z c= dom (arctan*f) & f=f1+h(#)f2 &
  (for x st x in Z holds f.x > -1 & f.x < 1) &
  (for x st x in Z holds f1.x = r+s*x) & f2=#Z 2
  implies arctan*(f1+h(#)f2) is_differentiable_on Z &
  for x st x in Z holds ((arctan*(f1+h(#)f2))`|Z).x
  = (s+2*h*x)/(1+(r+s*x+h*x^2)^2)
proof
     assume that
A1:  Z c= dom (arctan*f) & f=f1+h(#)f2 and
A2:  (for x st x in Z holds f.x > -1 & f.x < 1) and
A3:  (for x st x in Z holds f1.x = r+s*x) & f2=#Z 2;
     dom (arctan*f) c= dom f by RELAT_1:44;then
A4:  Z c= dom (f1+h(#)f2) by A1,XBOOLE_1:1;
     then Z c= dom f1 /\ dom (h(#)f2) by VALUED_1:def 1;then
A5:  Z c= dom f1 & Z c= dom (h(#)f2) by XBOOLE_1:18;
A6:  (f1+h(#)f2) is_differentiable_on Z &
     for x st x in Z holds ((f1+h(#)f2)`|Z).x = s+2*h*x
     by A3,A4,FDIFF_4:12;
A7:  for x st x in Z holds arctan*(f1+h(#)f2) is_differentiable_in x
     proof
       let x;
       assume
   A8: x in Z;then
   A9: f.x > -1 & f.x < 1 by A2;
       f is_differentiable_in x by A1,A6,A8,FDIFF_1:16;
       hence arctan*(f1+h(#)f2) is_differentiable_in x
       by A1,A9,Th83;
     end;
     then
A10: arctan*(f1+h(#)f2) is_differentiable_on Z by A1,FDIFF_1:16;
     for x st x in Z holds ((arctan*(f1+h(#)f2))`|Z).x
     = (s+2*h*x)/(1+(r+s*x+h*x^2)^2)
     proof
       let x;
       assume
  A11: x in Z;then
  A12: f is_differentiable_in x by A1,A6,FDIFF_1:16;
  A13: f.x > -1 & f.x < 1 by A2,A11;
  A14: (f1+h(#)f2).x = f1.x+(h(#)f2).x by A4,A11,VALUED_1:def 1
       .= f1.x+h*f2.x by A5,A11,VALUED_1:def 5
       .= r+s*x+h*(f2.x) by A3,A11
       .= r+s*x+h*(x #Z (1+1)) by A3,TAYLOR_1:def 1
       .= r+s*x+h*((x #Z 1)*(x #Z 1)) by TAYLOR_1:1
       .= r+s*x+h*(x*(x #Z 1)) by PREPOWER:45
       .= r+s*x+h*x^2 by PREPOWER:45;
       ((arctan*(f1+h(#)f2))`|Z).x = diff((arctan)*f,x)
       by A1,A10,A11,FDIFF_1:def 8
       .= diff(f,x)/(1+(f.x)^2) by A12,A13,Th83
       .= ((f1+h(#)f2)`|Z).x/(1+(f.x)^2) by A1,A6,A11,FDIFF_1:def 8
       .= (s+2*h*x)/(1+(r+s*x+h*x^2)^2) by A1,A3,A4,A11,A14,FDIFF_4:12;
       hence thesis;
     end;
     hence thesis by A1,A7,FDIFF_1:16;
end;

::f.x=arccot.(r+s*x+h*x^2)
theorem
  Z c= dom (arccot*f) & f=f1+h(#)f2 &
  (for x st x in Z holds f.x > -1 & f.x < 1) &
  (for x st x in Z holds f1.x = r+s*x) & f2=#Z 2
  implies arccot*(f1+h(#)f2) is_differentiable_on Z &
  for x st x in Z holds ((arccot*(f1+h(#)f2))`|Z).x
  = -(s+2*h*x)/(1+(r+s*x+h*x^2)^2)
proof
     assume that
A1:  Z c= dom (arccot*f) & f=f1+h(#)f2 and
A2:  (for x st x in Z holds f.x > -1 & f.x < 1) and
A3:  (for x st x in Z holds f1.x = r+s*x) & f2=#Z 2;
     dom (arccot*f) c= dom f by RELAT_1:44;then
A4:  Z c= dom (f1+h(#)f2) by A1,XBOOLE_1:1;
     then Z c= dom f1 /\ dom (h(#)f2) by VALUED_1:def 1;then
A5:  Z c= dom f1 & Z c= dom (h(#)f2) by XBOOLE_1:18;
A6:  (f1+h(#)f2) is_differentiable_on Z &
     for x st x in Z holds ((f1+h(#)f2)`|Z).x = s+2*h*x
     by A3,A4,FDIFF_4:12;
A7:  for x st x in Z holds arccot*(f1+h(#)f2) is_differentiable_in x
     proof
       let x;
       assume
   A8: x in Z;then
   A9: f.x > -1 & f.x < 1 by A2;
       f is_differentiable_in x by A1,A6,A8,FDIFF_1:16;
       hence arccot*(f1+h(#)f2) is_differentiable_in x by A1,A9,Th84;
     end;
     then
A10: arccot*(f1+h(#)f2) is_differentiable_on Z by A1,FDIFF_1:16;
     for x st x in Z holds ((arccot*(f1+h(#)f2))`|Z).x
     = -(s+2*h*x)/(1+(r+s*x+h*x^2)^2)
     proof
       let x;
       assume
  A11: x in Z;then
  A12: f is_differentiable_in x by A1,A6,FDIFF_1:16;
  A13: f.x > -1 & f.x < 1 by A2,A11;
  A14: (f1+h(#)f2).x = f1.x+(h(#)f2).x by A4,A11,VALUED_1:def 1
       .= f1.x+h*f2.x by A5,A11,VALUED_1:def 5
       .= r+s*x+h*(f2.x) by A3,A11
       .= r+s*x+h*(x #Z (1+1)) by A3,TAYLOR_1:def 1
       .= r+s*x+h*((x #Z 1)*(x #Z 1)) by TAYLOR_1:1
       .= r+s*x+h*(x*(x #Z 1)) by PREPOWER:45
       .= r+s*x+h*x^2 by PREPOWER:45;
       ((arccot*(f1+h(#)f2))`|Z).x = diff((arccot)*f,x)
       by A1,A10,A11,FDIFF_1:def 8
       .= -diff(f,x)/(1+(f.x)^2) by A12,A13,Th84
       .= -((f1+h(#)f2)`|Z).x/(1+(f.x)^2) by A1,A6,A11,FDIFF_1:def 8
       .= -(s+2*h*x)/(1+(r+s*x+h*x^2)^2) by A1,A3,A4,A11,A14,FDIFF_4:12;
       hence thesis;
     end;
     hence thesis by A1,A7,FDIFF_1:16;
end;

::f.x=arctan.(exp_R.x)
theorem
  Z c= dom (arctan*exp_R) & (for x st x in Z holds exp_R.x < 1)
  implies arctan*exp_R is_differentiable_on Z & for x st x in Z
  holds ((arctan*exp_R)`|Z).x = exp_R.x/(1+(exp_R.x)^2)
proof
    assume that
A1: Z c= dom (arctan*exp_R) and
A2: for x st x in Z holds exp_R.x < 1;
A3: for x st x in Z holds arctan*exp_R is_differentiable_in x
    proof
      let x;
      assume
  A4: x in Z;
      exp_R.x + 0 > 0 + (-1) by SIN_COS:59,XREAL_1:10;then
  A5: exp_R.x > -1 & exp_R.x < 1 by A2,A4;
      exp_R is_differentiable_in x by SIN_COS:70;
      hence arctan*exp_R is_differentiable_in x by A5,Th83;
    end;
    then
A6: arctan*exp_R is_differentiable_on Z by A1,FDIFF_1:16;
    for x st x in Z holds ((arctan*exp_R)`|Z).x
    = exp_R.x/(1+(exp_R.x)^2)
    proof
      let x;
      assume
  A7: x in Z;
      exp_R.x + 0 > 0 + (-1) by SIN_COS:59,XREAL_1:10;then
  A8: exp_R.x > -1 & exp_R.x < 1 by A2,A7;
  A9: exp_R is_differentiable_in x by SIN_COS:70;
      ((arctan*exp_R)`|Z).x = diff(arctan*exp_R,x)
      by A6,A7,FDIFF_1:def 8
      .= diff(exp_R,x)/(1+(exp_R.x)^2) by A8,A9,Th83
      .= (exp_R.x)/(1+(exp_R.x)^2) by SIN_COS:70;
      hence thesis;
    end;
    hence thesis by A1,A3,FDIFF_1:16;
end;

::f.x=arccot.(exp_R.x)
theorem
  Z c= dom (arccot*exp_R) & (for x st x in Z holds exp_R.x < 1)
  implies arccot*exp_R is_differentiable_on Z & for x st x in Z
  holds ((arccot*exp_R)`|Z).x = -exp_R.x/(1+(exp_R.x)^2)
proof
    assume that
A1: Z c= dom (arccot*exp_R) and
A2: for x st x in Z holds exp_R.x < 1;
A3: for x st x in Z holds arccot*exp_R is_differentiable_in x
    proof
        let x;
        assume
    A4: x in Z;
        exp_R.x + 0 > 0 + (-1) by SIN_COS:59,XREAL_1:10;then
    A5: exp_R.x > -1 & exp_R.x < 1 by A2,A4;
        exp_R is_differentiable_in x by SIN_COS:70;
        hence arccot*exp_R is_differentiable_in x by A5,Th84;
    end;
    then
A6: arccot*exp_R is_differentiable_on Z by A1,FDIFF_1:16;
    for x st x in Z holds ((arccot*exp_R)`|Z).x
    = -exp_R.x/(1+(exp_R.x)^2)
    proof
        let x;
        assume
    A7: x in Z;
        exp_R.x + 0 > 0 + (-1) by SIN_COS:59,XREAL_1:10;then
    A8: exp_R.x > -1 & exp_R.x < 1 by A2,A7;
    A9: exp_R is_differentiable_in x by SIN_COS:70;
        ((arccot*exp_R)`|Z).x = diff(arccot*exp_R,x)
        by A6,A7,FDIFF_1:def 8
        .= -diff(exp_R,x)/(1+(exp_R.x)^2) by A8,A9,Th84
        .= -(exp_R.x)/(1+(exp_R.x)^2) by SIN_COS:70;
        hence thesis;
    end;
    hence thesis by A1,A3,FDIFF_1:16;
end;

::f.x=arctan.(ln.x)
theorem
  Z c= dom (arctan*ln) & (for x st x in Z holds ln.x > -1 & ln.x < 1)
  implies arctan*ln is_differentiable_on Z & for x st x in Z holds
  ((arctan*ln)`|Z).x = 1/(x*(1+(ln.x)^2))
proof
    assume that
A1: Z c= dom (arctan*ln) and
A2: for x st x in Z holds ln.x > -1 & ln.x < 1;
A3: right_open_halfline 0 = {g where g is Real: 0 < g} by XXREAL_1:230;
    dom (arctan*ln) c= dom ln by RELAT_1:44;then
A4: Z c= dom ln by A1,XBOOLE_1:1;
A5: for x st x in Z holds x > 0
    proof
      let x;
      assume x in Z;
      then x in right_open_halfline(0) by A4,TAYLOR_1:18;
      then ex g being Real st x = g & 0 < g by A3;
      hence thesis;
    end;
A6: for x st x in Z holds arctan*ln is_differentiable_in x
    proof
        let x;
        assume
    A7: x in Z;
        then x > 0 by A5;then
    A8: ln is_differentiable_in x by TAYLOR_1:18;
        ln.x > -1 & ln.x < 1 by A2,A7;
        hence (arctan)*ln is_differentiable_in x by A8,Th83;
    end;
    then
A8: arctan*ln is_differentiable_on Z by A1,FDIFF_1:16;
    for x st x in Z holds
    ((arctan*ln)`|Z).x = 1/(x*(1+(ln.x)^2))
    proof
         let x;
         assume
    A9:  x in Z;
    A10: x > 0 by A5,A9;then
    A11: x in right_open_halfline(0) by A3;
    A12: ln is_differentiable_in x by A10,TAYLOR_1:18;
    A13: ln.x > -1 & ln.x < 1 by A2,A9;
         ((arctan*ln)`|Z).x = diff(arctan*ln,x)
         by A8,A9,FDIFF_1:def 8
         .= diff(ln,x)/(1+(ln.x)^2) by A12,A13,Th83
         .= (1/x)/(1+(ln.x)^2) by A11,TAYLOR_1:18
         .= 1/(x*(1+(ln.x)^2)) by XCMPLX_1:79;
         hence thesis;
    end;
    hence thesis by A1,A6,FDIFF_1:16;
end;

::f.x=arccot.(ln.x)
theorem
  Z c= dom (arccot*ln) & (for x st x in Z holds ln.x > -1 & ln.x < 1)
  implies arccot*ln is_differentiable_on Z & for x st x in Z holds
  ((arccot*ln)`|Z).x = -1/(x*(1+(ln.x)^2))
proof
    assume that
A1: Z c= dom (arccot*ln) and
A2: for x st x in Z holds ln.x > -1 & ln.x < 1;
A3: right_open_halfline 0 = {g where g is Real: 0 < g} by XXREAL_1:230;
    dom (arccot*ln) c= dom ln by RELAT_1:44;then
A4: Z c= dom ln by A1,XBOOLE_1:1;
A5: for x st x in Z holds x > 0
    proof
      let x;
      assume x in Z;
      then x in right_open_halfline(0) by A4,TAYLOR_1:18;
      then ex g being Real st x = g & 0 < g by A3;
      hence thesis;
    end;
A6: for x st x in Z holds arccot*ln is_differentiable_in x
    proof
        let x;
        assume
    A7: x in Z;
        then x > 0 by A5;then
    A8: ln is_differentiable_in x by TAYLOR_1:18;
        ln.x > -1 & ln.x < 1 by A2,A7;
        hence (arccot)*ln is_differentiable_in x by A8,Th84;
    end;
    then
A8: arccot*ln is_differentiable_on Z by A1,FDIFF_1:16;
    for x st x in Z holds
    ((arccot*ln)`|Z).x = -1/(x*(1+(ln.x)^2))
    proof
         let x;
         assume
    A9:  x in Z;
    A10: x > 0 by A5,A9;then
    A11: x in right_open_halfline(0) by A3;
    A12: ln is_differentiable_in x by A10,TAYLOR_1:18;
    A13: ln.x > -1 & ln.x < 1 by A2,A9;
         ((arccot*ln)`|Z).x = diff(arccot*ln,x)
         by A8,A9,FDIFF_1:def 8
         .= -diff(ln,x)/(1+(ln.x)^2) by A12,A13,Th84
         .= -(1/x)/(1+(ln.x)^2) by A11,TAYLOR_1:18
         .= -1/(x*(1+(ln.x)^2)) by XCMPLX_1:79;
         hence thesis;
    end;
    hence thesis by A1,A6,FDIFF_1:16;
end;

::f.x=exp_R.(arctan.x)
theorem
  Z c= dom (exp_R*arctan) & Z c= ].-1,1.[ implies
  exp_R*arctan is_differentiable_on Z & for x st x in Z holds
  ((exp_R*arctan)`|Z).x = exp_R.(arctan.x)/(1+x^2)
proof
    assume that
A1: Z c= dom (exp_R*arctan) and
A2: Z c= ].-1,1.[;
A3: for x st x in Z holds exp_R*arctan is_differentiable_in x
    proof
        let x;
        assume
    A4: x in Z;
        arctan is_differentiable_on Z by A2,Th79;then
    A5: arctan is_differentiable_in x by A4,FDIFF_1:16;
        exp_R is_differentiable_in arctan.x by SIN_COS:70;
        hence exp_R*arctan is_differentiable_in x by A5,FDIFF_2:13;
    end;
    then
A6: exp_R*arctan is_differentiable_on Z by A1,FDIFF_1:16;
    for x st x in Z holds
    ((exp_R*arctan)`|Z).x = exp_R.(arctan.x)/(1+x^2)
    proof
        let x;
        assume
    A7: x in Z;
    A8: arctan is_differentiable_on Z by A2,Th79;then
    A9: arctan is_differentiable_in x by A7,FDIFF_1:16;
        exp_R is_differentiable_in arctan.x by SIN_COS:70;
        then diff(exp_R*arctan,x) = diff(exp_R,arctan.x)*diff(arctan,x)
        by A9,FDIFF_2:13
        .= diff(exp_R,arctan.x)*((arctan)`|Z).x by A7,A8,FDIFF_1:def 8
        .= diff(exp_R,arctan.x)*(1/(1+x^2)) by A2,A7,Th79
        .= exp_R.(arctan.x)/(1+x^2) by SIN_COS:70;
        hence thesis by A6,A7,FDIFF_1:def 8;
    end;
    hence thesis by A1,A3,FDIFF_1:16;
end;

::f.x=exp_R.(arccot.x)
theorem
  Z c= dom (exp_R*arccot) & Z c= ].-1,1.[ implies
  exp_R*arccot is_differentiable_on Z & for x st x in Z holds
  ((exp_R*arccot)`|Z).x = -exp_R.(arccot.x)/(1+x^2)
proof
    assume that
A1: Z c= dom (exp_R*arccot) and
A2: Z c= ].-1,1.[;
A3: for x st x in Z holds exp_R*arccot is_differentiable_in x
    proof
        let x;
        assume
    A4: x in Z;
        arccot is_differentiable_on Z by A2,Th80;then
    A5: arccot is_differentiable_in x by A4,FDIFF_1:16;
        exp_R is_differentiable_in arccot.x by SIN_COS:70;
        hence exp_R*arccot is_differentiable_in x by A5,FDIFF_2:13;
    end;
    then
A6: exp_R*arccot is_differentiable_on Z by A1,FDIFF_1:16;
    for x st x in Z holds
    ((exp_R*arccot)`|Z).x = -exp_R.(arccot.x)/(1+x^2)
    proof
        let x;
        assume
    A7: x in Z;
    A8: arccot is_differentiable_on Z by A2,Th80;then
    A9: arccot is_differentiable_in x by A7,FDIFF_1:16;
        exp_R is_differentiable_in arccot.x by SIN_COS:70;
        then diff(exp_R*arccot,x) = diff(exp_R,arccot.x)*diff(arccot,x)
        by A9,FDIFF_2:13
        .= diff(exp_R,arccot.x)*((arccot)`|Z).x by A7,A8,FDIFF_1:def 8
        .= diff(exp_R,arccot.x)*(-1/(1+x^2)) by A2,A7,Th80
        .= -diff(exp_R,arccot.x)*(1/(1+x^2))
        .= -exp_R.(arccot.x)/(1+x^2) by SIN_COS:70;
        hence thesis by A6,A7,FDIFF_1:def 8;
    end;
    hence thesis by A1,A3,FDIFF_1:16;
end;

::f.x=arctan.x-x
theorem
  Z c= dom (arctan-id Z) & Z c= ].-1,1.[
  implies arctan-id Z is_differentiable_on Z & for x st x in Z holds
  ((arctan-id Z)`|Z).x = -x^2/(1+x^2)
proof
    assume that
A1: Z c= dom (arctan-id Z) and
A2: Z c= ].-1,1.[;
    Z c= dom arctan /\ dom (id Z) by A1,VALUED_1:12;then
A3: Z c= dom arctan & Z c= dom (id Z) by XBOOLE_1:18;
A4: for x st x in Z holds (id Z).x = 1*x+0 by FUNCT_1:35;then
A5: id Z is_differentiable_on Z & for x st x in Z holds
    ((id Z)`|Z).x = 1 by A3,FDIFF_1:31;
A6: arctan is_differentiable_on Z by A2,Th79;
    for x st x in Z holds ((arctan-id Z)`|Z).x = -x^2/(1+x^2)
    proof
        let x;
        assume
    A7: x in Z;
    A8: 1+x^2 > 0 by XREAL_1:36,XREAL_1:65;
        ((arctan-id Z)`|Z).x = diff(arctan,x)-diff(id Z,x)
        by A1,A5,A6,A7,FDIFF_1:27
        .= ((arctan)`|Z).x-diff(id Z,x) by A6,A7,FDIFF_1:def 8
        .= 1/(1+x^2)-diff(id Z,x) by A2,A7,Th79
        .= 1/(1+x^2)-((id Z)`|Z).x by A5,A7,FDIFF_1:def 8
        .= 1/(1+x^2)-1 by A3,A4,A7,FDIFF_1:31
        .= 1/(1+x^2)-(1+x^2)/(1+x^2) by A8,XCMPLX_1:60
        .= -x^2/(1+x^2);
        hence thesis;
    end;
    hence thesis by A1,A5,A6,FDIFF_1:27;
end;

::f.x=-arccot.x-x
theorem
  Z c= dom (-arccot-id Z) & Z c= ].-1,1.[
  implies -arccot-id Z is_differentiable_on Z & for x st x in Z holds
  ((-arccot-id Z)`|Z).x = -x^2/(1+x^2)
proof
    assume that
A1: Z c= dom (-arccot-id Z) and
A2: Z c= ].-1,1.[;
B3: Z c= dom (-arccot) /\ dom (id Z) by A1,VALUED_1:12;then
A3: Z c= dom (-arccot) & Z c= dom (id Z) by XBOOLE_1:18;
A4: Z c= dom ((-1)(#)arccot) by B3,XBOOLE_1:18;
A6: for x st x in Z holds (id Z).x = 1*x+0 by FUNCT_1:35;then
A7: id Z is_differentiable_on Z & for x st x in Z holds
    ((id Z)`|Z).x = 1 by A3,FDIFF_1:31;
A8: arccot is_differentiable_on Z by A2,Th80; then
A9: -arccot is_differentiable_on Z by A4,FDIFF_1:28;
    for x st x in Z holds ((-arccot-id Z)`|Z).x = -x^2/(1+x^2)
    proof
      let x;
      assume
 A10: x in Z;
 A11: 1+x^2 > 0 by XREAL_1:36,XREAL_1:65;
      ((-arccot-id Z)`|Z).x = diff(-arccot,x)-diff(id Z,x)
      by A1,A7,A9,A10,FDIFF_1:27
      .= ((-arccot)`|Z).x-diff(id Z,x) by A9,A10,FDIFF_1:def 8
      .= (-1)*diff(arccot,x)-diff(id Z,x) by A4,A8,A10,FDIFF_1:28
      .= (-1)*((arccot)`|Z).x-diff(id Z,x) by A8,A10,FDIFF_1:def 8
      .= (-1)*(-1/(1+x^2))-diff(id Z,x) by A2,A10,Th80
      .= 1/(1+x^2)-((id Z)`|Z).x by A7,A10,FDIFF_1:def 8
      .= 1/(1+x^2)-1 by A3,A6,A10,FDIFF_1:31
      .= 1/(1+x^2)-(1+x^2)/(1+x^2) by A11,XCMPLX_1:60
      .= -x^2/(1+x^2);
      hence thesis;
    end;
    hence thesis by A1,A7,A9,FDIFF_1:27;
end;

::f.x=exp_R.x*arctan.x
theorem
  Z c= ].-1,1.[ implies (exp_R(#)arctan) is_differentiable_on Z &
  for x st x in Z holds
  ((exp_R(#)arctan)`|Z).x = exp_R.x*arctan.x+exp_R.x/(1+x^2)
proof
    assume
A1: Z c= ].-1,1.[;
    ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
    then ].-1,1.[ c= dom arctan by Th21,XBOOLE_1:1;
    then Z c= dom arctan by A1,XBOOLE_1:1;
    then Z c= dom (exp_R) /\ dom arctan by SIN_COS:51,XBOOLE_1:19;then
A3: Z c= dom (exp_R(#)arctan) by VALUED_1:def 4;
    for x st x in Z holds exp_R is_differentiable_in x by SIN_COS:70;then
A4: exp_R is_differentiable_on Z by SIN_COS:51,FDIFF_1:16;
A5: arctan is_differentiable_on Z by A1,Th79;
    for x st x in Z holds
    ((exp_R(#)arctan)`|Z).x = exp_R.x*arctan.x+exp_R.x/(1+x^2)
    proof
      let x;
      assume
  A6: x in Z;
      then ((exp_R(#)arctan)`|Z).x
      = (arctan.x)*diff(exp_R,x)+(exp_R.x)*diff(arctan,x)
      by A3,A4,A5,FDIFF_1:29
      .= (arctan.x)*exp_R.x+(exp_R.x)*diff(arctan,x) by SIN_COS:70
      .= exp_R.x*arctan.x+(exp_R.x)*((arctan)`|Z).x by A5,A6,FDIFF_1:def 8
      .= exp_R.x*arctan.x+(exp_R.x)*(1/(1+x^2)) by A1,A6,Th79
      .= exp_R.x*arctan.x+exp_R.x/(1+x^2);
      hence thesis;
    end;
    hence thesis by A3,A4,A5,FDIFF_1:29;
end;

::f.x=exp_R.x*arccot.x
theorem
  Z c= ].-1,1.[ implies (exp_R(#)arccot) is_differentiable_on Z &
  for x st x in Z holds
  ((exp_R(#)arccot)`|Z).x = exp_R.x*arccot.x-exp_R.x/(1+x^2)
proof
    assume
A1: Z c= ].-1,1.[;
    ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
    then ].-1,1.[ c= dom arccot by Th22,XBOOLE_1:1;
    then Z c= dom arccot by A1,XBOOLE_1:1;
    then Z c= dom (exp_R) /\ dom arccot by SIN_COS:51,XBOOLE_1:19;then
A3: Z c= dom (exp_R(#)arccot) by VALUED_1:def 4;
    for x st x in Z holds exp_R is_differentiable_in x by SIN_COS:70;then
A4: exp_R is_differentiable_on Z by SIN_COS:51,FDIFF_1:16;
A5: arccot is_differentiable_on Z by A1,Th80;
    for x st x in Z holds
    ((exp_R(#)arccot)`|Z).x = exp_R.x*arccot.x-exp_R.x/(1+x^2)
    proof
      let x;
      assume
  A6: x in Z;
      then ((exp_R(#)arccot)`|Z).x
      = (arccot.x)*diff(exp_R,x)+(exp_R.x)*diff(arccot,x)
      by A3,A4,A5,FDIFF_1:29
      .= (arccot.x)*exp_R.x+(exp_R.x)*diff(arccot,x) by SIN_COS:70
      .= exp_R.x*arccot.x+(exp_R.x)*((arccot)`|Z).x by A5,A6,FDIFF_1:def 8
      .= exp_R.x*arccot.x+(exp_R.x)*(-1/(1+x^2)) by A1,A6,Th80
      .= exp_R.x*arccot.x-exp_R.x/(1+x^2);
      hence thesis;
    end;
    hence thesis by A3,A4,A5,FDIFF_1:29;
end;

::f.x=(1/r)*arctan.(r*x)-x
theorem
  Z c= dom ((1/r)(#)(arctan*f)-id Z) & (for x st x in Z holds
  f.x=r*x & r<>0 & f.x > -1 & f.x < 1) implies
  (1/r)(#)(arctan*f)-id Z is_differentiable_on Z & for x st x in Z holds
  (((1/r)(#)(arctan*f)-id Z)`|Z).x = -(r*x)^2/(1+(r*x)^2)
proof
    assume that
A1: Z c= dom ((1/r)(#)(arctan*f)-id Z) and
A2: for x st x in Z holds f.x=r*x & r<>0 & f.x > -1 & f.x < 1;
A3: for x st x in Z holds f.x=r*x+0 & f.x > -1 & f.x < 1 by A2;
    Z c= dom ((1/r)(#)(arctan*f)) /\ dom (id Z) by A1,VALUED_1:12;then
A4: Z c= dom ((1/r)(#)(arctan*f)) & Z c= dom (id Z) by XBOOLE_1:18;then
AA: Z c= dom (arctan*f) by VALUED_1:def 5;then
A5: arctan*f is_differentiable_on Z & for x st x in Z holds
    ((arctan*f)`|Z).x = r/(1+(r*x+0)^2) by A3,Th85;then
A6: (1/r)(#)(arctan*f) is_differentiable_on Z & for x st x in Z holds
    ((1/r)(#)(arctan*f)`|Z).x = (1/r)*diff(arctan*f,x) by A4,FDIFF_1:28;
AB: for x st x in Z holds (id Z).x = 1*x+0 by FUNCT_1:35;then
A7: id Z is_differentiable_on Z & for x st x in Z holds
    ((id Z)`|Z).x = 1 by A4,FDIFF_1:31;
    set g = (1/r)(#)(arctan*f);
    for x st x in Z holds
    (((1/r)(#)(arctan*f)-id Z)`|Z).x= -(r*x)^2/(1+(r*x)^2)
    proof
      let x;
      assume
 A8:  x in Z;
 A9:  1+(r*x)^2 > 0 by XREAL_1:36,XREAL_1:65;
 A10: r <> 0 by A2,A8;
      ((g-id Z)`|Z).x = diff(g,x)-diff(id Z,x) by A1,A6,A7,A8,FDIFF_1:27
      .= (g`|Z).x-diff(id Z,x) by A6,A8,FDIFF_1:def 8
      .= (1/r)*diff(arctan*f,x)-diff(id Z,x) by A4,A5,A8,FDIFF_1:28
      .= (1/r)*((arctan*f)`|Z).x-diff(id Z,x) by A5,A8,FDIFF_1:def 8
      .= (1/r)*((arctan*f)`|Z).x-((id Z)`|Z).x by A7,A8,FDIFF_1:def 8
      .= (1/r)*(r/(1+(r*x+0)^2))-((id Z)`|Z).x by A3,AA,A8,Th85
      .= (1/r)*(r/(1+(r*x)^2))-1 by A4,AB,A8,FDIFF_1:31
      .= (1*r)/(r*(1+(r*x)^2))-1 by XCMPLX_1:77
      .= 1/(1+(r*x)^2)-1 by A10,XCMPLX_1:92
      .= 1/(1+(r*x)^2)-(1+(r*x)^2)/(1+(r*x)^2) by A9,XCMPLX_1:60
      .= -(r*x)^2/(1+(r*x)^2);
      hence thesis;
    end;
    hence thesis by A1,A6,A7,FDIFF_1:27;
end;

::f.x=(-1/r)*arccot.(r*x)-x
theorem
  Z c= dom ((-1/r)(#)(arccot*f)-id Z) & (for x st x in Z holds
  f.x=r*x & r<>0 & f.x > -1 & f.x < 1) implies
  (-1/r)(#)(arccot*f)-id Z is_differentiable_on Z & for x st x in Z holds
  (((-1/r)(#)(arccot*f)-id Z)`|Z).x = -(r*x)^2/(1+(r*x)^2)
proof
    assume that
A1: Z c= dom ((-1/r)(#)(arccot*f)-id Z) and
A2: for x st x in Z holds f.x=r*x & r<>0 & f.x > -1 & f.x < 1;
A3: for x st x in Z holds f.x=r*x+0 & f.x > -1 & f.x < 1 by A2;
    Z c= dom ((-1/r)(#)(arccot*f)) /\ dom (id Z) by A1,VALUED_1:12;then
A4: Z c= dom ((-1/r)(#)(arccot*f)) & Z c= dom (id Z) by XBOOLE_1:18;then
AA: Z c= dom (arccot*f) by VALUED_1:def 5;then
A5: arccot*f is_differentiable_on Z & for x st x in Z holds
    ((arccot*f)`|Z).x = -r/(1+(r*x+0)^2) by A3,Th86;then
A6: (-1/r)(#)(arccot*f) is_differentiable_on Z & for x st x in Z holds
    ((-1/r)(#)(arccot*f)`|Z).x = (-1/r)*diff(arccot*f,x) by A4,FDIFF_1:28;
AB: for x st x in Z holds (id Z).x = 1*x+0 by FUNCT_1:35;then
A7: id Z is_differentiable_on Z & for x st x in Z holds
    ((id Z)`|Z).x = 1 by A4,FDIFF_1:31;
    set g = (-1/r)(#)(arccot*f);
    for x st x in Z holds
    (((-1/r)(#)(arccot*f)-id Z)`|Z).x = -(r*x)^2/(1+(r*x)^2)
    proof
      let x;
      assume
 A8:  x in Z;
 A9:  1+(r*x)^2 > 0 by XREAL_1:36,XREAL_1:65;
 A10: r <> 0 by A2,A8;
      ((g-id Z)`|Z).x = diff(g,x)-diff(id Z,x) by A1,A6,A7,A8,FDIFF_1:27
      .= (g`|Z).x-diff(id Z,x) by A6,A8,FDIFF_1:def 8
      .= (-1/r)*diff(arccot*f,x)-diff(id Z,x) by A4,A5,A8,FDIFF_1:28
      .= (-1/r)*((arccot*f)`|Z).x-diff(id Z,x) by A5,A8,FDIFF_1:def 8
      .= (-1/r)*((arccot*f)`|Z).x-((id Z)`|Z).x by A7,A8,FDIFF_1:def 8
      .= (-1/r)*(-r/(1+(r*x+0)^2))-((id Z)`|Z).x by A3,AA,A8,Th86
      .= ((-1)/r)*((-r)/(1+(r*x)^2))-1 by A4,AB,A8,FDIFF_1:31
      .= ((-1)*(-r))/(r*(1+(r*x)^2))-1 by XCMPLX_1:77
      .= (1*r)/(r*(1+(r*x)^2))-1
      .= 1/(1+(r*x)^2)-1 by A10,XCMPLX_1:92
      .= 1/(1+(r*x)^2)-(1+(r*x)^2)/(1+(r*x)^2) by A9,XCMPLX_1:60
      .= -(r*x)^2/(1+(r*x)^2);
      hence thesis;
    end;
    hence thesis by A1,A6,A7,FDIFF_1:27;
end;

::f.x=ln.x*arctan.x
theorem
  Z c= dom (ln(#)arctan) & Z c= ].-1,1.[ implies
  (ln(#)arctan) is_differentiable_on Z & for x st x in Z holds
  ((ln(#)arctan)`|Z).x = arctan.x/x+ln.x/(1+x^2)
proof
    assume that
A1: Z c= dom (ln(#)arctan) and
A2: Z c= ].-1,1.[;
    Z c= dom ln /\ dom arctan by A1,VALUED_1:def 4;then
A3: Z c= dom ln by XBOOLE_1:18;
A4: right_open_halfline 0 = {g where g is Real : 0 < g} by XXREAL_1:230;
A5: for x st x in Z holds x > 0
    proof
      let x;
      assume x in Z;
      then x in right_open_halfline(0) by A3,TAYLOR_1:18;
      then ex g being Real st x = g & 0 < g by A4;
      hence thesis;
    end;
    for x st x in Z holds ln is_differentiable_in x by A5,TAYLOR_1:18;
    then
A6: ln is_differentiable_on Z by A3,FDIFF_1:16;
A7: arctan is_differentiable_on Z by A2,Th79;
A8: for x st x in Z holds diff(ln,x) = 1/x
    proof
      let x;
      assume x in Z;
      then x > 0 by A5;
      then x in right_open_halfline(0) by A4;
      hence thesis by TAYLOR_1:18;
    end;
    for x st x in Z holds
    ((ln(#)arctan)`|Z).x = arctan.x/x+ln.x/(1+x^2)
    proof
      let x;
      assume
  A9: x in Z;
      then ((ln(#)arctan)`|Z).x = (arctan.x)*diff(ln,x)+(ln.x)*diff(arctan,x)
      by A1,A6,A7,FDIFF_1:29
      .= (arctan.x)*(1/x)+(ln.x)*diff(arctan,x) by A8,A9
      .= (arctan.x)*(1/x)+(ln.x)*((arctan)`|Z).x
      by A7,A9,FDIFF_1:def 8
      .= ((arctan.x)*1)/x+(ln.x)*(1/(1+x^2)) by A2,A9,Th79
      .= arctan.x/x+ln.x/(1+x^2);
      hence thesis;
    end;
    hence thesis by A1,A6,A7,FDIFF_1:29;
end;

::f.x=ln.x*arccot.x
theorem
  Z c= dom (ln(#)arccot) & Z c= ].-1,1.[ implies
  (ln(#)arccot) is_differentiable_on Z & for x st x in Z holds
  ((ln(#)arccot)`|Z).x = arccot.x/x-ln.x/(1+x^2)
proof
    assume that
A1: Z c= dom (ln(#)arccot) and
A2: Z c= ].-1,1.[;
    Z c= dom ln /\ dom arccot by A1,VALUED_1:def 4;then
A3: Z c= dom ln by XBOOLE_1:18;
A4: right_open_halfline 0 = {g where g is Real : 0 < g}
    by XXREAL_1:230;
A5: for x st x in Z holds x > 0
    proof
      let x;
      assume x in Z;
      then x in right_open_halfline(0) by A3,TAYLOR_1:18;
      then ex g being Real st x = g & 0 < g by A4;
      hence thesis;
    end;
    for x st x in Z holds ln is_differentiable_in x by A5,TAYLOR_1:18;
    then
A6: ln is_differentiable_on Z by A3,FDIFF_1:16;
A7: arccot is_differentiable_on Z by A2,Th80;
A8: for x st x in Z holds diff(ln,x) = 1/x
    proof
      let x;
      assume x in Z;
      then x > 0 by A5;
      then x in right_open_halfline(0) by A4;
      hence thesis by TAYLOR_1:18;
    end;
    for x st x in Z holds
    ((ln(#)arccot)`|Z).x = arccot.x/x-ln.x/(1+x^2)
    proof
      let x;
      assume
  A9: x in Z;
      then ((ln(#)arccot)`|Z).x
      = (arccot.x)*diff(ln,x)+(ln.x)*diff(arccot,x) by A1,A6,A7,FDIFF_1:29
      .= (arccot.x)*(1/x)+(ln.x)*diff(arccot,x) by A8,A9
      .= (arccot.x)*(1/x)+(ln.x)*((arccot)`|Z).x by A7,A9,FDIFF_1:def 8
      .= (arccot.x)*(1/x)+(ln.x)*(-1/(1+x^2)) by A2,A9,Th80
      .= arccot.x/x-ln.x/(1+x^2);
      hence thesis;
    end;
    hence thesis by A1,A6,A7,FDIFF_1:29;
end;

::f.x=1/x*arctan.x
theorem
  Z c= dom (f^(#)arctan) & Z c= ].-1,1.[ & (for x st x in Z
  holds f.x=x) implies (f^(#)arctan) is_differentiable_on Z &
  for x st x in Z holds
  ((f^(#)arctan)`|Z).x = -arctan.x/(x^2)+1/(x*(1+x^2))
proof
    assume that
A1: Z c= dom (f^(#)arctan) and
A2: Z c= ].-1,1.[ and
A3: for x st x in Z holds f.x=x;
    Z c= dom (f^) /\ dom arctan by A1,VALUED_1:def 4;then
A4: Z c= dom (f^) by XBOOLE_1:18;
    dom (f^) c= dom f by RFUNCT_1:11;then
A5: Z c= dom f by A4,XBOOLE_1:1;
A6: for x st x in Z holds f.x = x & f.x<>0 by A3,A4,RFUNCT_1:13;then
A7: f^ is_differentiable_on Z & for x st x in Z holds
    ((f^)`|Z).x = -1/x^2 by A5,FDIFF_5:4;
A8: arctan is_differentiable_on Z by A2,Th79;
    for x st x in Z holds
    ((f^(#)arctan)`|Z).x = -arctan.x/(x^2)+1/(x*(1+x^2))
    proof
      let x;
      assume
  A9: x in Z;
      then ((f^(#)arctan)`|Z).x
      = (arctan.x)*diff(f^,x)+((f^).x)*diff(arctan,x)
      by A1,A7,A8,FDIFF_1:29
      .= (arctan.x)*((f^)`|Z).x+((f^).x)*diff(arctan,x)
      by A7,A9,FDIFF_1:def 8
      .= (arctan.x)*(-1/x^2)+((f^).x)*diff(arctan,x)
      by A5,A6,A9,FDIFF_5:4
      .= -(arctan.x)*(1/x^2)+((f^).x)*((arctan)`|Z).x by A8,A9,FDIFF_1:def 8
      .= -((arctan.x)*1)/(x^2)+((f^).x)*(1/(1+x^2)) by A2,A9,Th79
      .= -arctan.x/(x^2)+(f.x)"*(1/(1+x^2)) by A4,A9,RFUNCT_1:def 8
      .= -arctan.x/(x^2)+(1/x)*(1/(1+x^2)) by A3,A9
      .= -arctan.x/(x^2)+(1*1)/(x*(1+x^2)) by XCMPLX_1:77
      .= -arctan.x/(x^2)+1/(x*(1+x^2));
      hence thesis;
    end;
    hence thesis by A1,A7,A8,FDIFF_1:29;
end;

::f.x=1/x*arccot.x
theorem
  Z c= dom (f^(#)arccot) & Z c= ].-1,1.[ & (for x st x in Z
  holds f.x=x) implies (f^(#)arccot) is_differentiable_on Z &
  for x st x in Z holds
  ((f^(#)arccot)`|Z).x = -arccot.x/(x^2)-1/(x*(1+x^2))
proof
    assume that
A1: Z c= dom (f^(#)arccot) and
A2: Z c= ].-1,1.[ and
A3: for x st x in Z holds f.x=x;
    Z c= dom (f^) /\ dom arccot by A1,VALUED_1:def 4;then
A4: Z c= dom (f^) by XBOOLE_1:18;
    dom (f^) c= dom f by RFUNCT_1:11;then
A5: Z c= dom f by A4,XBOOLE_1:1;
A6: for x st x in Z holds f.x = x & f.x<>0 by A3,A4,RFUNCT_1:13;then
A7: f^ is_differentiable_on Z & for x st x in Z holds
    ((f^)`|Z).x = -1/x^2 by A5,FDIFF_5:4;
A8: arccot is_differentiable_on Z by A2,Th80;
    for x st x in Z holds
    ((f^(#)arccot)`|Z).x = -arccot.x/(x^2)-1/(x*(1+x^2))
    proof
      let x;
      assume
  A9: x in Z;
      then ((f^(#)arccot)`|Z).x
      = (arccot.x)*diff(f^,x)+((f^).x)*diff(arccot,x) by A1,A7,A8,FDIFF_1:29
      .= (arccot.x)*((f^)`|Z).x+((f^).x)*diff(arccot,x)
      by A7,A9,FDIFF_1:def 8
      .= (arccot.x)*(-1/x^2)+((f^).x)*diff(arccot,x) by A5,A6,A9,FDIFF_5:4
      .= -(arccot.x)*(1/x^2)+((f^).x)*((arccot)`|Z).x
      by A8,A9,FDIFF_1:def 8
      .= -(arccot.x)*(1/x^2)+((f^).x)*(-1/(1+x^2)) by A2,A9,Th80
      .= -((arccot.x)*1)/(x^2)-((f^).x)*(1/(1+x^2))
      .= -arccot.x/(x^2)-(f.x)"*(1/(1+x^2)) by A4,A9,RFUNCT_1:def 8
      .= -arccot.x/(x^2)-(1/x)*(1/(1+x^2)) by A3,A9
      .= -arccot.x/(x^2)-(1*1)/(x*(1+x^2)) by XCMPLX_1:77
      .= -arccot.x/(x^2)-1/(x*(1+x^2));
      hence thesis;
    end;
    hence thesis by A1,A7,A8,FDIFF_1:29;
end;