SIN_COS9

:: Inverse Trigonometric Functions Arctan and Arccot
::  by Xiquan Liang and Bing Xie
::
:: Received March 18, 2008
:: Copyright (c) 2008-2026 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, REAL_1, XREAL_0, SUBSET_1, RCOMP_1, PARTFUN1, XXREAL_1,
      ARYTM_1, SIN_COS, ARYTM_3, TARSKI, RELAT_1, XBOOLE_0, CARD_1, FUNCT_1,
      FDIFF_1, SQUARE_1, ORDINAL2, XXREAL_0, VALUED_0, VALUED_1, TAYLOR_1,
      PREPOWER, ORDINAL4, LIMFUNC1, SIN_COS9, ORDINAL1;
 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, FDIFF_1, XREAL_0, INT_1, SIN_COS4, PARTFUN2, FCONT_1, XBOOLE_0,
      TAYLOR_1, PREPOWER, LIMFUNC1, RFUNCT_2;
 constructors REAL_1, SQUARE_1, RCOMP_1, RFUNCT_1, FDIFF_1, RFUNCT_2, FCONT_1,
      SIN_COS, PARTFUN2, SIN_COS4, TAYLOR_1, PREPOWER, LIMFUNC1, VALUED_1,
      XXREAL_2, PARTFUN1, SIN_COS6, RELSET_1, COMPLEX1;
 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, XXREAL_2,
      ORDINAL1, SQUARE_1, PREPOWER;
 requirements SUBSET, NUMERALS, ARITHM, REAL;
 definitions TARSKI;
 equalities XCMPLX_0, LIMFUNC1, SIN_COS, VALUED_1, SQUARE_1;
 expansions TARSKI;
 theorems FDIFF_2, XCMPLX_1, FDIFF_1, RELAT_1, SIN_COS, COMPTRIG, RFUNCT_2,
      FCONT_1, SIN_COS4, FUNCT_1, RCOMP_1, XBOOLE_0, FCONT_3, XREAL_1, TARSKI,
      XBOOLE_1, FDIFF_7, ROLLE, RFUNCT_1, FCONT_2, TAYLOR_1, PREPOWER,
      VALUED_1, FDIFF_4, FDIFF_5, XXREAL_1, XXREAL_0, XXREAL_2, XREAL_0;

begin :: arctan,arccot

reserve x,x0, r, s, h for Real,

  n for Element of NAT,
  rr, y for set,
  Z for open Subset of REAL,

  f, f1, f2 for PartFunc of REAL,REAL;

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

theorem Th2:
  ].0,PI.[ c= dom cot
proof
  ].0,PI.[ /\ sin"{0}={}
  proof
    assume ].0,PI.[ /\ sin"{0}<>{};
    then consider rr being object such that
A1: rr in ].0,PI.[ /\ sin"{0} by XBOOLE_0:7;
    rr in sin"{0} by A1,XBOOLE_0:def 4;
    then
A2: sin.rr in {0} by FUNCT_1:def 7;
    rr in ].0,PI.[ by A1,XBOOLE_0:def 4;
    then sin.rr <>0 by COMPTRIG:7;
    hence contradiction by A2,TARSKI:def 1;
  end;
  then
A3: ].0,PI.[ misses sin"{0} by XBOOLE_0:def 7;
  ].0,PI.[ \ sin"{0} c= dom sin \ sin"{0} by SIN_COS:24,XBOOLE_1:33;
  then ].0,PI.[ c= dom sin \ sin"{0} by A3,XBOOLE_1:83;
  then ].0,PI.[ c= dom cos /\ (dom sin \ sin"{0}) by SIN_COS:24,XBOOLE_1:19;
  hence thesis by RFUNCT_1:def 1;
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:11;
    hence thesis by FDIFF_7:46;
  end;
  hence thesis by Th1,FDIFF_1:9;
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:7;
    hence thesis by FDIFF_7:47;
  end;
  hence thesis by Th2,FDIFF_1:9;
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:11;
  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:7;
  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|].-PI/2,PI/2.[ is continuous by Lm1,FDIFF_1:25;

theorem
  cot|].0,PI.[ is continuous by Lm2,FDIFF_1:25;

theorem Th7:
  tan|].-PI/2,PI/2.[ is increasing
proof
A1: for x st x in ].-PI/2,PI/2.[ holds diff(tan,x) > 0
  proof
    let x;
    assume
A2: x in ].-PI/2,PI/2.[;
    then 0 < cos.x by COMPTRIG:11;
    then (cos.x)^2 > 0;
    then 1/(cos.x)^2 > 0 /(cos.x)^2;
    hence thesis by A2,Lm3;
  end;
  ].-PI/2,PI/2.[ c= dom tan by Lm1,FDIFF_1:def 6;
  hence thesis by A1,Lm1,ROLLE:9;
end;

theorem Th8:
  cot|].0,PI.[ is decreasing
proof
A1: for x st x in ].0,PI.[ holds diff(cot,x) < 0
  proof
    let x;
    assume
A2: x in ].0,PI.[;
    then 0 < sin.x by COMPTRIG:7;
    then (sin.x)^2 > 0;
    then 1/(sin.x)^2 > 0 /(sin.x)^2;
    then -1/(sin.x)^2 < -0;
    hence thesis by A2,Lm4;
  end;
  ].0,PI.[ c= dom cot by Lm2,FDIFF_1:def 6;
  hence thesis by A1,Lm2,ROLLE:10;
end;

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

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

registration
  cluster tan | ].-PI/2,PI/2.[ -> one-to-one;
  coherence by Th7,FCONT_3:8;
  cluster cot | ].0,PI.[ -> one-to-one;
  coherence by Th8,FCONT_3:8;
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 -> number equals
  arctan.r;
  coherence;
  func arccot r -> number equals
  arccot.r;
  coherence;
end;

registration
  let r be Real;
  cluster arctan r -> real;
  coherence;
  cluster arccot r -> real;
  coherence;
end;

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

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

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

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

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

Lm7: -PI/4 in ].-PI/2,PI/2.[
proof
  PI/(-4) > PI/(-2) by XREAL_1:99;
  then -PI/4 in { s where s is Real: -PI/2 < s & s < PI/2 };
  hence thesis by RCOMP_1:def 2;
end;

Lm8: PI/4 in ].-PI/2,PI/2.[
proof
  PI/4 < PI/2 by XREAL_1:76;
  then PI/4 in { s where s is Real: -PI/2 < s & s < PI/2 };
  hence thesis by RCOMP_1:def 2;
end;

Lm9: PI/4 in ].0,PI.[
proof
A1: PI/4 < PI/1 by XREAL_1:76;
  thus thesis by A1,XXREAL_1:4;
end;

Lm10: 3/4*PI in ].0,PI.[
proof
A1: 3/4*PI < PI by XREAL_1:157;
  thus thesis by A1,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,XXREAL_2:def 12;
  hence thesis by Th1,RELAT_1:62,XBOOLE_1:1;
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,XXREAL_2:def 12;
  hence thesis by Th2,RELAT_1:62,XBOOLE_1:1;
end;

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

theorem Th14:
  for x be Real st x in ].0,PI.[ holds cot.x = cot x
proof
  let x be Real;
  assume x in ].0,PI.[;
  then cot.x = (cos x)/(sin x) by Th2,RFUNCT_1:def 1
    .= 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 REAL by XREAL_0:def 1;
  not x in cos"{0}
  proof
    assume x in cos"{0};
    then cos.x in {0} by FUNCT_1:def 7;
    hence contradiction by A1,TARSKI:def 1;
  end;
  then x in dom cos \ cos"{0} by SIN_COS:24,XBOOLE_0:def 5,A2;
  then x in dom sin /\ (dom cos \ cos"{0}) by SIN_COS:24,XBOOLE_0:def 4,A2;
  then x in dom (sin/cos) by RFUNCT_1:def 1;
  then tan.x = (sin x)/(cos x) by RFUNCT_1:def 1
    .= 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 REAL by XREAL_0:def 1;
  not x in sin"{0}
  proof
    assume x in sin"{0};
    then sin.x in {0} by FUNCT_1:def 7;
    hence contradiction by A1,TARSKI:def 1;
  end;
  then x in dom sin \ sin"{0} by SIN_COS:24,XBOOLE_0:def 5,A2;
  then x in dom cos /\ (dom sin \ sin"{0}) by SIN_COS:24,XBOOLE_0:def 4,A2;
  then x in dom (cos/sin) by RFUNCT_1:def 1;
  then cot.x = (cos x)/(sin x) by RFUNCT_1:def 1
    .= cot x by SIN_COS4:def 2;
  hence thesis;
end;

theorem Th17:
  tan.(-PI/4) = -1 & tan(-PI/4) = -1
proof
  cos.(PI/4) <> 0 by Lm8,COMPTRIG:11;
  then
A1: sin.(PI/4)/cos.(PI/4) = 1 by SIN_COS:73,XCMPLX_1:60;
  tan.(-PI/4) = sin.(-PI/4)/(cos.(-PI/4)) by Lm7,Th1,RFUNCT_1:def 1
    .= (-sin.(PI/4))/cos.(-PI/4) by SIN_COS:30
    .= (-sin.(PI/4))/cos.(PI/4) by SIN_COS:30
    .= -1 by A1;
  hence thesis by Lm7,Th13;
end;

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

theorem Th19:
  for x be set st x in [.-PI/4,PI/4.] holds tan.x in [.-1,1.]
proof
  let x be set;
  assume x in [.-PI/4,PI/4.];
  then x in ].-PI/4,PI/4.[ \/ {-PI/4,PI/4} by XXREAL_1:128;
  then
A1: x in ].-PI/4,PI/4.[ or x in {-PI/4,PI/4} by XBOOLE_0:def 3;
  per cases by A1,TARSKI:def 2;
  suppose
A2: x in ].-PI/4,PI/4.[;
    then x in { s where s is Real: -PI/4 < s & s < PI/4 }
         by RCOMP_1:def 2;
    then
A3: ex s be Real st s=x & -PI/4 < s & s < PI/4;
A4: ].-PI/4,PI/4.[ c= [.-PI/4,PI/4.] by XXREAL_1:25;
    -PI/4 in {s where s is Real: -PI/4 <= s & s <= PI/4};
    then
A5: -PI/4 in [.-PI/4,PI/4.] by RCOMP_1:def 1;
A6: [.-PI/4,PI/4.] c= ].-PI/2,PI/2.[ by Lm7,Lm8,XXREAL_2:def 12;
    then
A7: tan|[.-PI/4,PI/4.] is increasing by Th7,RFUNCT_2:28;
A8: [.-PI/4,PI/4.] /\ dom tan = [.-PI/4,PI/4.] by A6,Th1,XBOOLE_1:1,28;
    PI/4 in {s where s is Real: -PI/4 <= s & s <= PI/4};
    then PI/4 in [.-PI/4,PI/4.] /\ dom tan by A8,RCOMP_1:def 1;
    then tan.x < tan.(PI/4) by A2,A7,A8,A4,A3,RFUNCT_2:20;
    then
A9: tan.x < 1 by SIN_COS:def 28;
    x in { s where s is Real: -PI/4 < s & s < PI/4 }
     by A2,RCOMP_1:def 2;
    then ex s be Real st s=x & -PI/4 < s & s < PI/4;
    then -1 < tan.x by A2,A7,A5,A8,A4,Th17,RFUNCT_2:20;
    then tan.x in { s where s is Real: -1 < s & s < 1 } by A9;
    then
A10: tan.x in ].-1,1.[ by RCOMP_1:def 2;
    ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
    hence thesis by A10;
  end;
  suppose
    x = -PI/4;
    then tan.x in { s where s is Real: -1 <= s & s <= 1 } by Th17;
    hence thesis by RCOMP_1:def 1;
  end;
  suppose
    x = PI/4;
    then tan.x = 1 by SIN_COS:def 28;
    then tan.x in { s where s is Real: -1 <= s & s <= 1 };
    hence thesis by RCOMP_1:def 1;
  end;
end;

theorem Th20:
  for x be set st x in [.PI/4,3/4*PI.] holds cot.x in [.-1,1.]
proof
  let x be set;
A1: (PI/4)*3 > PI/4 by XREAL_1:155;
  assume x in [.PI/4,3/4*PI.];
  then x in ].PI/4,3/4*PI.[ \/ {PI/4,3/4*PI} by A1,XXREAL_1:128;
  then
A2: x in ].PI/4,3/4*PI.[ or x in {PI/4,3/4*PI} by XBOOLE_0:def 3;
  per cases by A2,TARSKI:def 2;
  suppose
A3: x in ].PI/4,3/4*PI.[;
    then x in { s where s is Real: PI/4 < s & s < 3/4*PI }
              by RCOMP_1:def 2;
    then
A4: ex s be Real st s=x & PI/4 < s & s < 3/4*PI;
A5: [.PI/4,3/4*PI.] c= ].0,PI.[ by Lm9,Lm10,XXREAL_2:def 12;
    then
A6: cot|[.PI/4,3/4*PI.] is decreasing by Th8,RFUNCT_2:29;
    x in { s where s is Real: PI/4 < s & s < 3/4*PI }
     by A3,RCOMP_1:def 2;
    then
A7: ex s be Real st s=x & PI/4 < s & s < 3/4*PI;
A8: ].PI/4,3/4*PI.[ c= [.PI/4,3/4*PI.] by XXREAL_1:25;
A9: [.PI/4,3/4*PI.] /\ dom cot = [.PI/4,3/4*PI.] by A5,Th2,XBOOLE_1:1,28;
    3/4*PI in {s where s is Real: PI/4 <= s & s <= 3/4*PI} by A1;
    then 3/4*PI in [.PI/4,3/4*PI.] /\ dom cot by A9,RCOMP_1:def 1;
    then
A10: -1 < cot.x by A3,A6,A9,A8,A7,Th18,RFUNCT_2:21;
    PI/4 in {s where s is Real: PI/4 <= s & s <= 3/4*PI} by A1;
    then PI/4 in [.PI/4,3/4*PI.] /\ dom cot by A9,RCOMP_1:def 1;
    then cot.x < 1 by A3,A6,A9,A8,A4,Th18,RFUNCT_2:21;
    then cot.x in { s where s is Real: -1 < s & s < 1 } by A10;
    then
A11: cot.x in ].-1,1.[ by RCOMP_1:def 2;
    ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
    hence thesis by A11;
  end;
  suppose
    x = PI/4;
    then cot.x in { s where s is Real: -1 <= s & s <= 1 } by Th18;
    hence thesis 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 Th18;
    hence thesis by RCOMP_1:def 1;
  end;
end;

theorem Th21:
  rng (tan | [.-PI/4,PI/4.]) = [.-1,1.]
proof
  now
    let y be object;
    thus y in [.-1,1.] implies
   ex x be object 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;
      y1 in [.tan.(-PI/4),tan.(PI/4).] by A1,Th17,SIN_COS:def 28;
      then
A2:   y1 in [.tan.(-PI/4),tan.(PI/4).] \/ [.tan.(PI/4),tan.(-PI/4).] by
XBOOLE_0:def 3;
A3:   [.-PI/4,PI/4.] c= ].-PI/2,PI/2.[ by Lm7,Lm8,XXREAL_2:def 12;
      tan|].-PI/2,PI/2.[ is continuous by Lm1,FDIFF_1:25;
      then tan|[.-PI/4,PI/4.] is continuous by A3,FCONT_1:16;
      then consider x be Real such that
A4:   x in [.-PI/4,PI/4.] and
A5:   y1 = tan.x by A3,A2,Th1,FCONT_2:15,XBOOLE_1:1;
      take x;
      thus thesis by A4,A5,Lm11,FUNCT_1:49;
    end;
    thus (ex x be object
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 object such that
A6:   x in dom (tan | [.-PI/4,PI/4.]) and
A7:   y = (tan | [.-PI/4,PI/4.]).x;
      reconsider x1=x as Real by A6;
      y = tan.x1 by A6,A7,Lm11,FUNCT_1:49;
      hence thesis by A6,Lm11,Th19;
    end;
  end;
  hence thesis by FUNCT_1:def 3;
end;

theorem Th22:
  rng (cot | [.PI/4,3/4*PI.]) = [.-1,1.]
proof
  now
    let y be object;
    thus y in [.-1,1.] implies
ex x be object st x in dom (cot | [.PI/4,3/4*PI.])
    & y = (cot | [.PI/4,3/4*PI.]).x
    proof
A1:   (PI/4)*3 > PI/4 by XREAL_1:155;
      assume
A2:   y in [.-1,1.];
      then reconsider y1=y as Real;
A3:   y1 in [.cot.(3/4*PI),cot.(PI/4).] \/ [.cot.(PI/4),cot.(3/4*PI).] by A2
,Th18,XBOOLE_0:def 3;
A4:   [.PI/4,3/4*PI.] c= ].0,PI.[ by Lm9,Lm10,XXREAL_2:def 12;
      cot|].0,PI.[ is continuous by Lm2,FDIFF_1:25;
      then cot|[.PI/4,3/4*PI.] is continuous by A4,FCONT_1:16;
      then consider x be Real such that
A5:   x in [.PI/4,3/4*PI.] and
A6:   y1 = cot.x by A1,A4,A3,Th2,FCONT_2:15,XBOOLE_1:1;
      take x;
      thus thesis by A5,A6,Lm12,FUNCT_1:49;
    end;
    thus (ex x be object
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 object such that
A7:   x in dom (cot | [.PI/4,3/4*PI.]) and
A8:   y = (cot | [.PI/4,3/4*PI.]).x;
      reconsider x1=x as Real by A7;
      y = cot.x1 by A7,A8,Lm12,FUNCT_1:49;
      hence thesis by A7,Lm12,Th20;
    end;
  end;
  hence thesis by FUNCT_1:def 3;
end;

theorem Th23:
  [.-1,1.] c= dom arctan
proof
A1: [.-PI/4,PI/4.] c= ].-PI/2,PI/2.[ by Lm7,Lm8,XXREAL_2:def 12;
  rng (tan | [.-PI/4,PI/4.]) c= rng (tan | ].-PI/2,PI/2.[)
  proof
    let y be object;
    assume y in rng (tan | [.-PI/4,PI/4.]);
    then y in tan.:[.-PI/4,PI/4.] by RELAT_1:115;
    then ex x be object st x in dom tan & x in [.-PI/4,PI/4.] & y = tan.x by
FUNCT_1:def 6;
    then y in tan.:].-PI/2,PI/2.[ by A1,FUNCT_1:def 6;
    hence thesis by RELAT_1:115;
  end;
  hence thesis by Th21,FUNCT_1:33;
end;

theorem Th24:
  [.-1,1.] c= dom arccot
proof
A1: [.PI/4,3/4*PI.] c= ].0,PI.[ by Lm9,Lm10,XXREAL_2:def 12;
  rng (cot | [.PI/4,3/4*PI.]) c= rng (cot | ].0,PI.[)
  proof
    let y be object;
    assume y in rng (cot | [.PI/4,3/4*PI.]);
    then y in cot.:[.PI/4,3/4*PI.] by RELAT_1:115;
    then
    ex x be object st x in dom cot & x in [.PI/4,3/4*PI.] & y = cot.x by
FUNCT_1:def 6;
    then y in cot.:].0,PI.[ by A1,FUNCT_1:def 6;
    hence thesis by RELAT_1:115;
  end;
  hence thesis by Th22,FUNCT_1:33;
end;

Lm13: tan | [.-PI/4,PI/4.]|[.-PI/4,PI/4.] is increasing
proof
  [.-PI/4,PI/4.] c= ].-PI/2,PI/2.[ by Lm7,Lm8,XXREAL_2:def 12;
  then tan|[.-PI/4,PI/4.] is increasing by Th7,RFUNCT_2:28;
  hence thesis;
end;

Lm14: cot | [.PI/4,3/4*PI.] |[.PI/4,3/4*PI.] is decreasing
proof
  [.PI/4,3/4*PI.] c= ].0,PI.[ by Lm9,Lm10,XXREAL_2:def 12;
  then cot|[.PI/4,3/4*PI.] is decreasing by Th8,RFUNCT_2:29;
  hence thesis;
end;

Lm15: tan | [.-PI/4,PI/4.] is one-to-one
proof
  [.-PI/4,PI/4.] c= ].-PI/2,PI/2.[ by Lm7,Lm8,XXREAL_2:def 12;
  then (tan | ].-PI/2,PI/2.[) | [.-PI/4,PI/4.] = tan | [.-PI/4,PI/4.] by
RELAT_1:74;
  hence thesis;
end;

Lm16: cot | [.PI/4,3/4*PI.] is one-to-one
proof
  [.PI/4,3/4*PI.] c= ].0,PI.[ by Lm9,Lm10,XXREAL_2:def 12;
  then (cot | ].0,PI.[) | [.PI/4,3/4*PI.] = cot | [.PI/4,3/4*PI.] by RELAT_1:74
;
  hence thesis;
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 Th25:
  arctan | [.-1,1.] = (tan | [.-PI/4,PI/4.])"
proof
  set h = tan | ].-PI/2,PI/2.[;
A1: [.-PI/4,PI/4.] c= ].-PI/2,PI/2.[ by Lm7,Lm8,XXREAL_2:def 12;
  then (tan | [.-PI/4,PI/4.])" = (h | [.-PI/4,PI/4.])" by RELAT_1:74
    .= h" | (h.:[.-PI/4,PI/4.]) by RFUNCT_2:17
    .= h" | rng (h | [.-PI/4,PI/4.]) by RELAT_1:115
    .= h" | ([.-1,1.]) by A1,Th21,RELAT_1:74;
  hence thesis;
end;

theorem Th26:
  arccot | [.-1,1.] = (cot | [.PI/4,3/4*PI.])"
proof
  set h = cot | ].0,PI.[;
A1: [.PI/4,3/4*PI.] c= ].0,PI.[ by Lm9,Lm10,XXREAL_2:def 12;
  then (cot | [.PI/4,3/4*PI.])" = (h | [.PI/4,3/4*PI.])" by RELAT_1:74
    .= h" | (h.:[.PI/4,3/4*PI.]) by RFUNCT_2:17
    .= h" | rng (h | [.PI/4,3/4*PI.]) by RELAT_1:115
    .= h" | ([.-1,1.]) by A1,Th22,RELAT_1:74;
  hence thesis;
end;

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

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

theorem
  (tan | [.-PI/4,PI/4.]) * (arctan | [.-1,1.]) = id [.-1,1.] by Th21,Th25,
FUNCT_1:39;

theorem
  (cot | [.PI/4,3/4*PI.]) * (arccot | [.-1,1.]) = id [.-1,1.] by Th22,Th26,
FUNCT_1:39;

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

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

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

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

theorem Th35:
  -PI/2 < r & r < PI/2 implies arctan tan.r = r & arctan tan r = r
proof
  assume that
A1: -PI/2 < r and
A2: r < PI/2;
A3: dom (tan|].-PI/2,PI/2.[) = ].-PI/2,PI/2.[ by Th1,RELAT_1:62;
A4: r in ].-PI/2,PI/2.[ by A1,A2,XXREAL_1:4;
  then arctan tan.r = arctan.((tan|].-PI/2,PI/2.[).r) by FUNCT_1:49
    .= (id ].-PI/2,PI/2.[).r by A4,A3,Th31,FUNCT_1:13
    .= r by A4,FUNCT_1:18;
  hence thesis by A4,Th13;
end;

theorem Th36:
  0 < r & r < PI implies arccot cot.r = r & arccot cot r = r
proof
  assume that
A1: 0 < r and
A2: r < PI;
A3: dom (cot|].0,PI.[) = ].0,PI.[ by Th2,RELAT_1:62;
A4: r in ].0,PI.[ by A1,A2,XXREAL_1:4;
  then arccot cot.r = arccot.((cot|].0,PI.[).r) by FUNCT_1:49
    .= (id ].0,PI.[).r by A4,A3,Th32,FUNCT_1:13
    .= r by A4,FUNCT_1:18;
  hence thesis by A4,Th14;
end;

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

theorem Th38:
  arccot (-1) = 3/4*PI & arccot.(-1) = 3/4*PI
proof
A1: 3/4*PI < PI by Lm10,XXREAL_1:4;
  arccot (-1) = 3/4*PI by A1,Th18,Th36;
  hence thesis;
end;

theorem Th39:
  arctan 1 = PI/4 & arctan.1 = PI/4
proof
A1: arctan 1 = arctan tan.(PI/4) by SIN_COS:def 28;
  PI/4 < PI/2 by Lm8,XXREAL_1:4;
  hence thesis by A1,Th35;
end;

theorem Th40:
  arccot 1 = PI/4 & arccot.1 = PI/4
proof
A1: PI/4 < PI by Lm9,XXREAL_1:4;
  arccot 1 = PI/4 by A1,Th18,Th36;
  hence thesis;
end;

theorem Th41:
  tan.0 = 0 & tan 0 =0
proof
A1: 0 in ].-PI/2,PI/2.[ by XXREAL_1:4;
  then tan.0 = 0/cos.0 by Th1,RFUNCT_1:def 1,SIN_COS:30
    .= 0;
  hence thesis by A1,Th13;
end;

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

theorem
  arctan 0 = 0 & arctan.0 = 0
proof
  arctan 0 = 0 by Th35,Th41;
  hence thesis;
end;

theorem
  arccot 0 = PI/2 & arccot.0 = PI/2
proof
A1: PI/2 < PI/1 by XREAL_1:76;
  arccot 0 = PI/2 by A1,Th36,Th42;
  hence thesis;
end;

theorem Th45:
  arctan|(tan.:].-PI/2,PI/2.[) is increasing
proof
  set f = tan | ].-PI/2,PI/2.[;
A1: f.:].-PI/2,PI/2.[ = rng(f|].-PI/2,PI/2.[) by RELAT_1:115
    .= rng(tan|].-PI/2,PI/2.[) by RELAT_1:73
    .= tan.:].-PI/2,PI/2.[ by RELAT_1:115;
  f|].-PI/2,PI/2.[ = f by RELAT_1:73;
  hence thesis by A1,Th7,FCONT_3:9;
end;

theorem Th46:
  arccot|(cot.:].0,PI.[) is decreasing
proof
  set f = cot | ].0,PI.[;
A1: f.:].0,PI.[ = rng(f|].0,PI.[) by RELAT_1:115
    .= rng(cot|].0,PI.[) by RELAT_1:73
    .= cot.:].0,PI.[ by RELAT_1:115;
  f|].0,PI.[ = f by RELAT_1:73;
  hence thesis by A1,Th8,FCONT_3:10;
end;

theorem Th47:
  arctan|[.-1,1.] is increasing
proof
A1: [.-1,1.] = tan.:[.-PI/4,PI/4.] by Th21,RELAT_1:115;
  [.-PI/4,PI/4.] c= ].-PI/2,PI/2.[ by Lm7,Lm8,XXREAL_2:def 12;
  hence thesis by A1,Th45,RELAT_1:123,RFUNCT_2:28;
end;

theorem Th48:
  arccot|[.-1,1.] is decreasing
proof
A1: [.-1,1.] = cot.:[.PI/4,3/4*PI.] by Th22,RELAT_1:115;
  [.PI/4,3/4*PI.] c= ].0,PI.[ by Lm9,Lm10,XXREAL_2:def 12;
  hence thesis by A1,Th46,RELAT_1:123,RFUNCT_2:29;
end;

theorem Th49:
  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 3;
  per cases by A1,TARSKI:def 2;
  suppose
A2: x in ].-1,1.[;
    then x in { s where s is Real: -1 < s & s < 1 } by RCOMP_1:def 2;
    then
A3: ex s be Real st s=x & -1 < s & s < 1;
A4: ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
A5: [.-1,1.] /\ dom arctan = [.-1,1.] by Th23,XBOOLE_1:28;
    then 1 in [.-1,1.] /\ dom arctan by XXREAL_1:1;
    then
A6: arctan.x < PI/4 by A2,A5,A4,A3,Th39,Th47,RFUNCT_2:20;
    -1 in [.-1,1.] by XXREAL_1:1;
    then -PI/4 < arctan.x by A2,A5,A4,A3,Th37,Th47,RFUNCT_2:20;
    hence thesis by A6,XXREAL_1:1;
  end;
  suppose
    x = -1;
    hence thesis by Th37,XXREAL_1:1;
  end;
  suppose
    x = 1;
    hence thesis by Th39,XXREAL_1:1;
  end;
end;

theorem Th50:
  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 3;
  per cases by A1,TARSKI:def 2;
  suppose
A2: x in ].-1,1.[;
    then x in { s where s is Real: -1 < s & s < 1 } by RCOMP_1:def 2;
    then
A3: ex s be Real st s=x & -1 < s & s < 1;
A4: ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
A5: [.-1,1.] /\ dom arccot = [.-1,1.] by Th24,XBOOLE_1:28;
    then 1 in [.-1,1.] /\ dom arccot by XXREAL_1:1;
    then
A6: arccot.x > PI/4 by A2,A5,A4,A3,Th40,Th48,RFUNCT_2:21;
    -1 in [.-1,1.] by XXREAL_1:1;
    then 3/4*PI > arccot.x by A2,A5,A4,A3,Th38,Th48,RFUNCT_2:21;
    hence thesis by A6,XXREAL_1:1;
  end;
  suppose
A7: x = -1;
    PI/4 < (PI/4)*3 by XREAL_1:155;
    hence thesis by A7,Th38,XXREAL_1:1;
  end;
  suppose
A8: x = 1;
    PI/4 < (PI/4)*3 by XREAL_1:155;
    hence thesis by A8,Th40,XXREAL_1:1;
  end;
end;

theorem Th51:
  -1 <= r & r <= 1 implies tan arctan r = r
proof
A1: [.-PI/4,PI/4.] c= ].-PI/2,PI/2.[ by Lm7,Lm8,XXREAL_2:def 12;
  assume that
A2: -1 <= r and
A3: r <= 1;
A4: r in [.-1,1.] by A2,A3,XXREAL_1:1;
  then
A5: r in dom (arctan | [.-1,1.]) by Th23,RELAT_1:62;
  arctan.r in [.-PI/4,PI/4.] by A4,Th49;
  hence tan (arctan r) = tan.(arctan.r) by A1,Th13
    .= ((tan|[.-PI/4,PI/4.]) qua Function).(arctan.r) by A4,Th49,FUNCT_1:49
    .= ((tan|[.-PI/4,PI/4.]) qua Function).((arctan | [.-1,1.]).r) by A4,
FUNCT_1:49
    .= ((tan | [.-PI/4,PI/4.]) qua Function * (arctan | [.-1,1.])).r by A5,
FUNCT_1:13
    .= (id [.-1,1.]).r by Th21,Th25,FUNCT_1:39
    .= r by A4,FUNCT_1:18;
end;

theorem Th52:
  -1 <= r & r <= 1 implies cot arccot r = r
proof
A1: [.PI/4,3/4*PI.] c= ].0,PI.[ by Lm9,Lm10,XXREAL_2:def 12;
  assume that
A2: -1 <= r and
A3: r <= 1;
A4: r in [.-1,1.] by A2,A3,XXREAL_1:1;
  then
A5: r in dom (arccot | [.-1,1.]) by Th24,RELAT_1:62;
  arccot.r in [.PI/4,3/4*PI.] by A4,Th50;
  hence cot (arccot r) = cot.(arccot.r) by A1,Th14
    .= ((cot|[.PI/4,3/4*PI.]) qua Function).(arccot.r) by A4,Th50,FUNCT_1:49
    .= ((cot|[.PI/4,3/4*PI.]) qua Function).((arccot | [.-1,1.]).r) by A4,
FUNCT_1:49
    .= ((cot|[.PI/4,3/4*PI.]) qua Function * (arccot | [.-1,1.])).r by A5,
FUNCT_1:13
    .= (id [.-1,1.]).r by Th22,Th26,FUNCT_1:39
    .= r by A4,FUNCT_1:18;
end;

theorem Th53:
  arctan|[.-1,1.] is continuous
proof
  set f = tan | [.-PI/4,PI/4.];
A1: f|[.-PI/4,PI/4.] = f by RELAT_1:72;
  (f|[.-PI/4,PI/4.])"|(f.:[.-PI/4,PI/4.]) is continuous by Lm11,Lm13,FCONT_1:47
;
  then arctan | [.-1,1.]|[.-1,1.] is continuous by A1,Th21,Th25,RELAT_1:115;
  hence thesis by FCONT_1:15;
end;

theorem Th54:
  arccot|[.-1,1.] is continuous
proof
  set f = cot | [.PI/4,3/4*PI.];
  PI/4 < (PI/4)*3 by XREAL_1:155;
  then
A1: (f|[.PI/4,3/4*PI.])"|(f.:[.PI/4,3/4*PI.]) is continuous by Lm12,Lm14,
FCONT_1:47;
  f|[.PI/4,3/4*PI.] = f by RELAT_1:72;
  then arccot | [.-1,1.]|[.-1,1.] is continuous by A1,Th22,Th26,RELAT_1:115;
  hence thesis by FCONT_1:15;
end;

theorem Th55:
  rng(arctan | [.-1,1.]) = [.-PI/4,PI/4.]
proof
  now
    let y be object;
    thus y in [.-PI/4,PI/4.] implies
ex x be object 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,Th37
,Th39,XBOOLE_0:def 3;
      then consider x be Real such that
A2:   x in [.-1,1.] and
A3:   y1 = arctan.x by Th23,Th53,FCONT_2:15;
      take x;
      thus thesis by A2,A3,Th23,FUNCT_1:49,RELAT_1:62;
    end;
    thus (ex x be object
st x in dom (arctan | [.-1,1.]) & y = (arctan | [.-1,1.]
    ).x) implies y in [.-PI/4,PI/4.]
    proof
      given x be object such that
A4:   x in dom (arctan | [.-1,1.]) and
A5:   y = (arctan | [.-1,1.]).x;
A6:   dom (arctan | [.-1,1.]) = [.-1,1.] by Th23,RELAT_1:62;
      then y = arctan.x by A4,A5,FUNCT_1:49;
      hence thesis by A4,A6,Th49;
    end;
  end;
  hence thesis by FUNCT_1:def 3;
end;

theorem Th56:
  rng(arccot | [.-1,1.]) = [.PI/4,3/4*PI.]
proof
  now
    let y be object;
    thus y in [.PI/4,3/4*PI.] implies
ex x be object 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,Th38
,Th40,XBOOLE_0:def 3;
      then consider x be Real such that
A2:   x in [.-1,1.] and
A3:   y1 = arccot.x by Th24,Th54,FCONT_2:15;
      take x;
      thus thesis by A2,A3,Th24,FUNCT_1:49,RELAT_1:62;
    end;
    thus (ex x be object
st x in dom (arccot | [.-1,1.]) & y = (arccot | [.-1,1.]
    ).x) implies y in [.PI/4,3/4*PI.]
    proof
      given x be object such that
A4:   x in dom (arccot | [.-1,1.]) and
A5:   y = (arccot | [.-1,1.]).x;
A6:   dom (arccot | [.-1,1.]) = [.-1,1.] by Th24,RELAT_1:62;
      then y = arccot.x by A4,A5,FUNCT_1:49;
      hence thesis by A4,A6,Th50;
    end;
  end;
  hence thesis by FUNCT_1:def 3;
end;

theorem
  -1 <= r & r <= 1 & arctan r = -PI/4 implies r = -1 by Th17,Th51;

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

theorem
  -1 <= r & r <= 1 & arctan r = 0 implies r = 0 by Th41,Th51;

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

theorem
  -1 <= r & r <= 1 & arctan r = PI/4 implies r = 1
proof
  assume that
A1: -1 <= r and
A2: r <= 1 and
A3: arctan r = PI/4;
  thus r = tan(PI/4) by A1,A2,A3,Th51
    .= tan.(PI/4) by Lm8,Th13
    .= 1 by SIN_COS:def 28;
end;

theorem
  -1 <= r & r <= 1 & arccot r = PI/4 implies r = 1 by Th18,Th52;

theorem Th63:
  -1 <= r & r <= 1 implies -PI/4 <= arctan r & arctan r <= PI/4
proof
  assume that
A1: -1 <= r and
A2: r <= 1;
A3: r in [.-1,1.] by A1,A2,XXREAL_1:1;
  then r in dom (arctan | [.-1,1.]) by Th23,RELAT_1:62;
  then (arctan | [.-1,1.]).r in rng (arctan | [.-1,1.]) by FUNCT_1:def 3;
  then arctan r in rng (arctan | [.-1,1.]) by A3,FUNCT_1:49;
  hence thesis by Th55,XXREAL_1:1;
end;

theorem Th64:
  -1 <= r & r <= 1 implies PI/4 <= arccot r & arccot r <= 3/4*PI
proof
  assume that
A1: -1 <= r and
A2: r <= 1;
A3: r in [.-1,1.] by A1,A2,XXREAL_1:1;
  then r in dom (arccot | [.-1,1.]) by Th24,RELAT_1:62;
  then (arccot | [.-1,1.]).r in rng (arccot | [.-1,1.]) by FUNCT_1:def 3;
  then arccot r in rng (arccot | [.-1,1.]) by A3,FUNCT_1:49;
  hence thesis by Th56,XXREAL_1:1;
end;

theorem
  -1 < r & r < 1 implies -PI/4 < arctan r & arctan r < PI/4
proof
A1: tan (PI/4) = tan.(PI/4) by Lm8,Th13
    .= 1 by SIN_COS:def 28;
  assume that
A2: -1 < r and
A3: r < 1;
A4: arctan r <= PI/4 by A2,A3,Th63;
  -PI/4 <= arctan r by A2,A3,Th63;
  then
  -PI/4 < arctan r & arctan r < PI/4 or -PI/4 = arctan r or arctan r = PI/
  4 by A4,XXREAL_0:1;
  hence thesis by A2,A3,A1,Th17,Th51;
end;

theorem
  -1 < r & r < 1 implies PI/4 < arccot r & arccot r < 3/4*PI
proof
  assume that
A1: -1 < r and
A2: r < 1;
A3: arccot r <= 3/4*PI by A1,A2,Th64;
  PI/4 <= arccot r by A1,A2,Th64;
  then
  PI/4 < arccot r & arccot r < 3/4*PI or PI/4 = arccot r or arccot r = 3/4
  *PI by A3,XXREAL_0:1;
  hence thesis by A1,A2,Th18,Th52;
end;

theorem
  -1 <= r & r <= 1 implies arctan r = -arctan(-r)
proof
A1: [.-PI/4,PI/4.] c= ].-PI/2,PI/2.[ by Lm7,Lm8,XXREAL_2:def 12;
  assume that
A2: -1 <= r and
A3: r <= 1;
A4: -r >= -1 by A3,XREAL_1:24;
A5: --1 >= -r by A2,XREAL_1:24;
  then
A6: arctan(-r) <= PI/4 by A4,Th63;
  -PI/4 <= arctan(-r) by A5,A4,Th63;
  then
A7: -arctan(-r) <= --PI/4 by XREAL_1:24;
  arctan(-r) <= PI/4 by A5,A4,Th63;
  then -PI/4 <= -arctan(-r) by XREAL_1:24;
  then
A8: -arctan(-r) in [.-PI/4,PI/4.] by A7,XXREAL_1:1;
  -PI/4 <= arctan(-r) by A5,A4,Th63;
  then arctan(-r) in [.-PI/4,PI/4.] by A6,XXREAL_1:1;
  then
A9: cos arctan(-r) <> 0 by A1,COMPTRIG:11;
  tan arctan(-r) = -r by A5,A4,Th51;
  then
A10: r = (tan 0 - tan arctan(-r))/(1 + (tan 0) * tan arctan(-r)) by Th41
    .= tan(0 - arctan(-r)) by A9,SIN_COS:31,SIN_COS4:8;
A11: [.-PI/4,PI/4.] c= ].-PI/2,PI/2.[ by Lm7,Lm8,XXREAL_2:def 12;
  then
A12: -arctan(-r) < PI/2 by A8,XXREAL_1:4;
  -PI/2 < -arctan(-r) by A8,A11,XXREAL_1:4;
  hence thesis by A10,A12,Th35;
end;

theorem
  -1 <= r & r <= 1 implies arccot r = PI - arccot(-r)
proof
  set x = arccot(-r);
  assume that
A1: -1 <= r and
A2: r <= 1;
A3: -r >= -1 by A2,XREAL_1:24;
A4: --1 >= -r by A1,XREAL_1:24;
  then -r = cot x by A3,Th52;
  then
A5: r = -cot x .= -(cos x/sin x) by SIN_COS4:def 2
    .= cos x/(-(sin x)) by XCMPLX_1:188
    .= cos x/sin(-x) by SIN_COS:31
    .= cos(-x)/sin(-x) by SIN_COS:31
    .= cot(-x) by SIN_COS4:def 2;
  -r in [.-1,1.] by A4,A3,XXREAL_1:1;
  then
A6: x in [.PI/4,3/4*PI.] by Th50;
  then x <= 3/4*PI by XXREAL_1:1;
  then -x >= -3/4*PI by XREAL_1:24;
  then
A7: PI+(-x) >= PI+(-3/4*PI) by XREAL_1:6;
  PI/4 <= x by A6,XXREAL_1:1;
  then -PI/4 >= -x by XREAL_1:24;
  then PI+(-PI/4) >= PI+(-x) by XREAL_1:6;
  then
A8: PI+(-x) in [.PI/4,3/4*PI.] by A7,XXREAL_1:1;
A9: [.PI/4,3/4*PI.] c= ].0,PI.[ by Lm9,Lm10,XXREAL_2:def 12;
  then
A10: PI+(-x) < PI by A8,XXREAL_1:4;
A11: cot(PI+(-x)) = cos(PI+(-x))/sin(PI+(-x)) by SIN_COS4:def 2
    .= (-cos(-x))/sin(PI+(-x)) by SIN_COS:79
    .= (-cos(-x))/(-sin(-x)) by SIN_COS:79
    .= cos(-x)/sin(-x) by XCMPLX_1:191
    .= cot(-x)by SIN_COS4:def 2;
  0 < PI+(-x) by A8,A9,XXREAL_1:4;
  hence thesis by A5,A10,A11,Th36;
end;

theorem
  -1 <= r & r <= 1 implies cot arctan r = 1/r
proof
  set x = arctan r;
  assume that
A1: -1 <= r and
A2: r <= 1;
A3: sin x /cos x = tan x by SIN_COS4:def 1
    .= r by A1,A2,Th51;
  cot x = cos x/sin x by SIN_COS4:def 2
    .= 1/r by A3,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 and
A2: r <= 1;
A3: cos x /sin x = cot x by SIN_COS4:def 2
    .= r by A1,A2,Th52;
  tan x = sin x/cos x by SIN_COS4:def 1
    .= 1/r by A3,XCMPLX_1:57;
  hence thesis;
end;

theorem Th71:
  arctan is_differentiable_on tan.:].-PI/2,PI/2.[
proof
  set f = tan|].-PI/2,PI/2.[;
A1: dom(f") = rng (tan|].-PI/2,PI/2.[) by FUNCT_1:33
    .= tan.:].-PI/2,PI/2.[ by RELAT_1:115;
  dom f = dom tan /\ ].-PI/2,PI/2.[ by RELAT_1:61;
  then
A2: ].-PI/2,PI/2.[ c= dom f by Th1,XBOOLE_1:19;
A3: f is_differentiable_on ].-PI/2,PI/2.[ by Lm1,FDIFF_2:16;
A4: now
A5: for x0 st x0 in ].-PI/2,PI/2.[ holds 1/(cos.x0)^2 > 0
    proof
      let x0;
      assume x0 in ].-PI/2,PI/2.[;
      then 0 < cos.x0 by COMPTRIG:11;
      then (cos.x0)^2 > 0;
      then 1/(cos.x0)^2 > 0 /(cos.x0)^2;
      hence thesis;
    end;
    let x0 such that
A6: x0 in ].-PI/2,PI/2.[;
    diff(f,x0) = (f`|].-PI/2,PI/2.[).x0 by A3,A6,FDIFF_1:def 7
      .= (tan`|].-PI/2,PI/2.[).x0 by Lm1,FDIFF_2:16
      .= diff(tan,x0) by A6,Lm1,FDIFF_1:def 7
      .= 1/(cos.x0)^2 by A6,Lm3;
    hence 0 < diff(f,x0) by A6,A5;
  end;
  f|].-PI/2,PI/2.[ = f by RELAT_1:72;
  hence thesis by A1,A3,A2,A4,FDIFF_2:48;
end;

theorem Th72:
  arccot is_differentiable_on cot.:].0,PI.[
proof
  set f = cot|].0,PI.[;
A1: dom(f") = rng (cot|].0,PI.[) by FUNCT_1:33
    .= cot.:].0,PI.[ by RELAT_1:115;
  dom f = dom cot /\ ].0,PI.[ by RELAT_1:61;
  then
A2: ].0,PI.[ c= dom f by Th2,XBOOLE_1:19;
A3: f is_differentiable_on ].0,PI.[ by Lm2,FDIFF_2:16;
A4: now
A5: for x0 st x0 in ].0,PI.[ holds -1/(sin.x0)^2 < 0
    proof
      let x0;
      assume x0 in ].0,PI.[;
      then 0 < sin.x0 by COMPTRIG:7;
      then (sin.x0)^2 > 0;
      then 1/(sin.x0)^2 > 0 /(sin.x0)^2;
      then -1/(sin.x0)^2 < -0;
      hence thesis;
    end;
    let x0 such that
A6: x0 in ].0,PI.[;
    diff(f,x0) = (f`|].0,PI.[).x0 by A3,A6,FDIFF_1:def 7
      .= (cot`|].0,PI.[).x0 by Lm2,FDIFF_2:16
      .= diff(cot,x0) by A6,Lm2,FDIFF_1:def 7
      .= -1/(sin.x0)^2 by A6,Lm4;
    hence diff(f,x0) < 0 by A6,A5;
  end;
  f|].0,PI.[ = f by RELAT_1:72;
  hence thesis by A1,A2,A3,A4,FDIFF_2:48;
end;

theorem Th73:
  arctan is_differentiable_on ].-1,1.[
proof
  ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
  then
A1: ].-1,1.[ c= dom arctan by Th23;
  for x st x in ].-1,1.[ holds arctan is_differentiable_in x
  proof
    let x;
A2: dom arctan = rng (tan | ].-PI/2,PI/2.[) by FUNCT_1:33
      .= tan.:].-PI/2,PI/2.[ by RELAT_1:115;
    assume x in ].-1,1.[;
    then arctan|dom arctan is_differentiable_in x by A1,A2,Th71,FDIFF_1:def 6;
    hence thesis by RELAT_1:69;
  end;
  hence thesis by A1,FDIFF_1:9;
end;

theorem Th74:
  arccot is_differentiable_on ].-1,1.[
proof
  ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
  then
A1: ].-1,1.[ c= dom arccot by Th24;
  for x st x in ].-1,1.[ holds arccot is_differentiable_in x
  proof
    let x;
A2: dom arccot = rng (cot | ].0,PI.[) by FUNCT_1:33
      .= cot.:].0,PI.[ by RELAT_1:115;
    assume x in ].-1,1.[;
    then arccot|dom arccot is_differentiable_in x by A1,A2,Th72,FDIFF_1:def 6;
    hence thesis by RELAT_1:69;
  end;
  hence thesis by A1,FDIFF_1:9;
end;

theorem Th75:
  -1 <= r & r <= 1 implies diff(arctan,r) = 1/(1+r^2)
proof
  set g = arctan;
  set f = tan|].-PI/2,PI/2.[;
  set x = arctan.r;
  assume that
A1: -1 <= r and
A2: r <= 1;
A3: (sin.x)^2 + (cos.x)^2 = 1 by SIN_COS:28;
A4: f is_differentiable_on ].-PI/2,PI/2.[ by Lm1,FDIFF_2:16;
A5: now
A6: for x0 st x0 in ].-PI/2,PI/2.[ holds 1/(cos.x0)^2 > 0
    proof
      let x0;
      assume x0 in ].-PI/2,PI/2.[;
      then 0 < cos.x0 by COMPTRIG:11;
      then (cos.x0)^2 > 0;
      then 1/(cos.x0)^2 > 0 /(cos.x0)^2;
      hence thesis;
    end;
    let x0 such that
A7: x0 in ].-PI/2,PI/2.[;
    diff(f,x0) = (f`|].-PI/2,PI/2.[).x0 by A4,A7,FDIFF_1:def 7
      .= (tan`|].-PI/2,PI/2.[).x0 by Lm1,FDIFF_2:16
      .= diff(tan,x0) by A7,Lm1,FDIFF_1:def 7
      .= 1/(cos.x0)^2 by A7,Lm3;
    hence 0 < diff(f,x0) by A7,A6;
  end;
A8: r in [.-1,1.] by A1,A2,XXREAL_1:1;
  then
A9: x in [.-PI/4,PI/4.] by Th49;
  x = arctan r;
  then
A10: r = tan x by A1,A2,Th51
    .= sin x/cos x by SIN_COS4:def 1;
  dom f = dom tan /\ ].-PI/2,PI/2.[ by RELAT_1:61;
  then
A11: ].-PI/2,PI/2.[ c= dom f by Th1,XBOOLE_1:19;
A12: f|].-PI/2,PI/2.[ = f by RELAT_1:72;
A13: [.-PI/4,PI/4.] c= ].-PI/2,PI/2.[ by Lm7,Lm8,XXREAL_2:def 12;
  then cos x <> 0 by A9,COMPTRIG:11;
  then r * cos x = sin x by A10,XCMPLX_1:87;
  then
A14: 1 = (cos x)^2 * ( r^2 + 1 ) by A3;
  f is_differentiable_on ].-PI/2,PI/2.[ by Lm1,FDIFF_2:16;
  then diff(f,x) = (f`|].-PI/2,PI/2.[).x by A9,A13,FDIFF_1:def 7
    .= (tan`|].-PI/2,PI/2.[).x by Lm1,FDIFF_2:16
    .= diff(tan,x) by A9,A13,Lm1,FDIFF_1:def 7
    .= 1/(cos x)^2 by A9,A13,Lm3;
  then diff(g,r) = 1/(1/(cos x)^2) by A8,A4,A5,A12,A11,Th23,FDIFF_2:48
    .= 1/(r^2+1) by A14,XCMPLX_1:73;
  hence thesis;
end;

theorem Th76:
  -1 <= r & r <= 1 implies diff(arccot,r) = -1/(1+r^2)
proof
  set g = arccot;
  set f = cot|].0,PI.[;
  set x = arccot.r;
  assume that
A1: -1 <= r and
A2: r <= 1;
A3: (sin.x)^2 + (cos.x)^2 = 1 by SIN_COS:28;
A4: f is_differentiable_on ].0,PI.[ by Lm2,FDIFF_2:16;
A5: now
A6: for x0 st x0 in ].0,PI.[ holds -1/(sin.x0)^2 < 0
    proof
      let x0;
      assume x0 in ].0,PI.[;
      then 0 < sin.x0 by COMPTRIG:7;
      then (sin.x0)^2 > 0;
      then 1/(sin.x0)^2 > 0 /(sin.x0)^2;
      then -1/(sin.x0)^2 < -0;
      hence thesis;
    end;
    let x0 such that
A7: x0 in ].0,PI.[;
    diff(f,x0) = (f`|].0,PI.[).x0 by A4,A7,FDIFF_1:def 7
      .= (cot`|].0,PI.[).x0 by Lm2,FDIFF_2:16
      .= diff(cot,x0) by A7,Lm2,FDIFF_1:def 7
      .= -1/(sin.x0)^2 by A7,Lm4;
    hence diff(f,x0) < 0 by A7,A6;
  end;
A8: r in [.-1,1.] by A1,A2,XXREAL_1:1;
  then
A9: x in [.PI/4,3/4*PI.] by Th50;
  x = arccot r;
  then
A10: r = cot x by A1,A2,Th52
    .= cos x/sin x by SIN_COS4:def 2;
  dom f = dom cot /\ ].0,PI.[ by RELAT_1:61;
  then
A11: ].0,PI.[ c= dom f by Th2,XBOOLE_1:19;
A12: f|].0,PI.[ = f by RELAT_1:72;
A13: [.PI/4,3/4*PI.] c= ].0,PI.[ by Lm9,Lm10,XXREAL_2:def 12;
  then sin x <> 0 by A9,COMPTRIG:7;
  then r * sin x = cos x by A10,XCMPLX_1:87;
  then
A14: 1 = (sin x)^2 * ( r^2 + 1 ) by A3;
  f is_differentiable_on ].0,PI.[ by Lm2,FDIFF_2:16;
  then diff(f,x) = (f`|].0,PI.[).x by A9,A13,FDIFF_1:def 7
    .= (cot`|].0,PI.[).x by Lm2,FDIFF_2:16
    .= diff(cot,x) by A9,A13,Lm2,FDIFF_1:def 7
    .= -1/(sin x)^2 by A9,A13,Lm4;
  then diff(g,r) = 1/(-(1/(sin x)^2)) by A8,A4,A5,A12,A11,Th24,FDIFF_2:48
    .= -1/(1/(sin x)^2) by XCMPLX_1:188
    .= -1/(r^2+1) by A14,XCMPLX_1:73;
  hence thesis;
end;

theorem
  arctan|(tan.:].-PI/2,PI/2.[) is continuous by Th71,FDIFF_1:25;

theorem
  arccot|(cot.:].0,PI.[) is continuous by Th72,FDIFF_1:25;

theorem
  dom arctan is open
proof
  for x0 st x0 in ].-PI/2,PI/2.[ holds 0 < diff(tan,x0)
  proof
    let x0;
    assume
A1: x0 in ].-PI/2,PI/2.[;
    then 0 < cos.x0 by COMPTRIG:11;
    then (cos.x0)^2 > 0;
    then 1/(cos.x0)^2 > 0 /(cos.x0)^2;
    hence thesis by A1,Lm3;
  end;
  then rng (tan|].-PI/2,PI/2.[) is open by Lm1,Th1,FDIFF_2:41;
  hence thesis by FUNCT_1:33;
end;

theorem
  dom arccot is open
proof
  for x0 st x0 in ].0,PI.[ holds diff(cot,x0) < 0
  proof
    let x0;
    assume
A1: x0 in ].0,PI.[;
    then 0 < sin.x0 by COMPTRIG:7;
    then (sin.x0)^2 > 0;
    then 1/(sin.x0)^2 > 0 /(sin.x0)^2;
    then -1/(sin.x0)^2 < -0;
    hence thesis by A1,Lm4;
  end;
  then rng (cot|].0,PI.[) is open by Lm2,Th2,FDIFF_2:41;
  hence thesis by FUNCT_1:33;
end;

begin ::  Differentiation Formulas of arctan,arccot
:: f.x=arctan.x

theorem Th81:
  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 Th73,FDIFF_1:26;
  for x st x in Z holds ((arctan)`|Z).x = 1/(1+x^2)
  proof
    let x;
    assume
A3: x in Z;
    then
A4: -1 <= x by A1,XXREAL_1:4;
A5: x <= 1 by A1,A3,XXREAL_1:4;
    thus ((arctan)`|Z).x = diff(arctan,x) by A2,A3,FDIFF_1:def 7
      .= 1/(1+x^2) by A4,A5,Th75;
  end;
  hence thesis by A1,Th73,FDIFF_1:26;
end;

:: f.x=arccot.x

theorem Th82:
  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 Th74,FDIFF_1:26;
  for x st x in Z holds ((arccot)`|Z).x = -1/(1+x^2)
  proof
    let x;
    assume
A3: x in Z;
    then
A4: -1 <= x by A1,XXREAL_1:4;
A5: x <= 1 by A1,A3,XXREAL_1:4;
    thus ((arccot)`|Z).x = diff(arccot,x) by A2,A3,FDIFF_1:def 7
      .= -1/(1+x^2) by A4,A5,Th76;
  end;
  hence thesis by A1,Th74,FDIFF_1:26;
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 Th23;
  then Z c= dom arctan by A1;
  then
A2: Z c= dom (r(#)arctan) by VALUED_1:def 5;
A3: arctan is_differentiable_on Z by A1,Th81;
  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 by A1,XXREAL_1:4;
A6: x < 1 by A1,A4,XXREAL_1:4;
    ((r(#)arctan)`|Z).x = r*diff(arctan,x) by A2,A3,A4,FDIFF_1:20
      .= r*(1/(1+x^2)) by A5,A6,Th75
      .= r/(1+x^2);
    hence thesis;
  end;
  hence thesis by A2,A3,FDIFF_1:20;
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 Th24;
  then Z c= dom arccot by A1;
  then
A2: Z c= dom (r(#)arccot) by VALUED_1:def 5;
A3: arccot is_differentiable_on Z by A1,Th82;
  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 by A1,XXREAL_1:4;
A6: x < 1 by A1,A4,XXREAL_1:4;
    ((r(#)arccot)`|Z).x = r*diff(arccot,x) by A2,A3,A4,FDIFF_1:20
      .= r*(-1/(1+x^2)) by A5,A6,Th76
      .= -r/(1+x^2);
    hence thesis;
  end;
  hence thesis by A2,A3,FDIFF_1:20;
end;

theorem Th85:
  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 and
A3: f.x < 1;
  f.x in ].-1,1.[ by A2,A3,XXREAL_1:4;
  then
A4: arctan is_differentiable_in f.x by Th73,FDIFF_1:9;
  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,A3,Th75
    .= diff(f,x)/(1+(f.x)^2);
  hence thesis by A1,A4,FDIFF_2:13;
end;

theorem Th86:
  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 and
A3: f.x < 1;
  f.x in ]. -1,1 .[ by A2,A3,XXREAL_1:4;
  then
A4: arccot is_differentiable_in f.x by Th74,FDIFF_1:9;
  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,A3,Th76
    .= -diff(f,x)/(1+(f.x)^2);
  hence thesis by A1,A4,FDIFF_2:13;
end;

::f.x=arctan.(r*x+s)

theorem Th87:
  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;
  for y being object st y in Z holds y in dom f by A1,FUNCT_1:11;
  then
A3: Z c= dom f;
A4: for x st x in Z holds f.x=r*x+s by A2;
  then
A5: f is_differentiable_on Z by A3,FDIFF_1:23;
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.x > -1 by A2;
A9: f.x < 1 by A2,A7;
    f is_differentiable_in x by A5,A7,FDIFF_1:9;
    hence thesis by A8,A9,Th85;
  end;
  then
A10: (arctan)*f is_differentiable_on Z by A1,FDIFF_1:9;
  for x st x in Z holds (((arctan)*f)`|Z).x = r/(1+(r*x+s)^2)
  proof
    let x;
    assume
A11: x in Z;
    then
A12: f.x > -1 by A2;
A13: f.x < 1 by A2,A11;
    f is_differentiable_in x by A5,A11,FDIFF_1:9;
    then diff((arctan)*f,x) = diff(f,x)/(1+(f.x)^2) by A12,A13,Th85
      .= (f`|Z).x/(1+(f.x)^2) by A5,A11,FDIFF_1:def 7
      .= r/(1+(f.x)^2) by A4,A3,A11,FDIFF_1:23
      .= r/(1+(r*x+s)^2) by A2,A11;
    hence thesis by A10,A11,FDIFF_1:def 7;
  end;
  hence thesis by A1,A6,FDIFF_1:9;
end;

::f.x=arccot.(r*x+s)

theorem Th88:
  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;
  for y being object st y in Z holds y in dom f by A1,FUNCT_1:11;
  then
A3: Z c= dom f;
A4: for x st x in Z holds f.x=r*x+s by A2;
  then
A5: f is_differentiable_on Z by A3,FDIFF_1:23;
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.x > -1 by A2;
A9: f.x < 1 by A2,A7;
    f is_differentiable_in x by A5,A7,FDIFF_1:9;
    hence thesis by A8,A9,Th86;
  end;
  then
A10: (arccot)*f is_differentiable_on Z by A1,FDIFF_1:9;
  for x st x in Z holds (((arccot)*f)`|Z).x = -r/(1+(r*x+s)^2)
  proof
    let x;
    assume
A11: x in Z;
    then
A12: f.x > -1 by A2;
A13: f.x < 1 by A2,A11;
    f is_differentiable_in x by A5,A11,FDIFF_1:9;
    then diff((arccot)*f,x) = -diff(f,x)/(1+(f.x)^2) by A12,A13,Th86
      .= -(f`|Z).x/(1+(f.x)^2) by A5,A11,FDIFF_1:def 7
      .= -r/(1+(f.x)^2) by A4,A3,A11,FDIFF_1:23
      .= -r/(1+(r*x+s)^2) by A2,A11;
    hence thesis by A10,A11,FDIFF_1:def 7;
  end;
  hence thesis by A1,A6,FDIFF_1:9;
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,Th81;
    then
A6: arctan is_differentiable_in x by A5,FDIFF_1:9;
    arctan.x >0 by A3,A5;
    hence thesis by A6,TAYLOR_1:20;
  end;
  then
A7: ln*arctan is_differentiable_on Z by A1,FDIFF_1:9;
  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 by A2,XXREAL_1:4;
    arctan is_differentiable_on Z by A2,Th81;
    then
A10: arctan is_differentiable_in x by A8,FDIFF_1:9;
A11: x < 1 by A2,A8,XXREAL_1:4;
    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,A11,Th75
      .= 1/((1+x^2)*arctan.x) by XCMPLX_1:78;
    hence thesis by A7,A8,FDIFF_1:def 7;
  end;
  hence thesis by A1,A4,FDIFF_1:9;
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,Th82;
    then
A6: arccot is_differentiable_in x by A5,FDIFF_1:9;
    arccot.x >0 by A3,A5;
    hence thesis by A6,TAYLOR_1:20;
  end;
  then
A7: ln*arccot is_differentiable_on Z by A1,FDIFF_1:9;
  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 by A2,XXREAL_1:4;
    arccot is_differentiable_on Z by A2,Th82;
    then
A10: arccot is_differentiable_in x by A8,FDIFF_1:9;
A11: x < 1 by A2,A8,XXREAL_1:4;
    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,A11,Th76
      .= -(1/(1+x^2))/arccot.x
      .= -1/((1+x^2)*arccot.x) by XCMPLX_1:78;
    hence thesis by A7,A8,FDIFF_1:def 7;
  end;
  hence thesis by A1,A4,FDIFF_1:9;
end;

::f.x=(arctan)|^n

theorem Th91:
  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,Th81;
    then arctan is_differentiable_in x by A4,FDIFF_1:9;
    hence thesis by TAYLOR_1:3;
  end;
  then
A5: ( #Z n)*(arctan) is_differentiable_on Z by A1,FDIFF_1:9;
  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 by A2,XXREAL_1:4;
    arctan is_differentiable_on Z by A2,Th81;
    then
A8: arctan is_differentiable_in x by A6,FDIFF_1:9;
A9: x < 1 by A2,A6,XXREAL_1:4;
    ((( #Z n)*arctan)`|Z).x = diff(( #Z n)*arctan,x) by A5,A6,FDIFF_1:def 7
      .= (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,A9,Th75
      .= n*(arctan.x) #Z (n-1) / (1+x^2);
    hence thesis;
  end;
  hence thesis by A1,A3,FDIFF_1:9;
end;

::f.x=(arccot)|^n

theorem Th92:
  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,Th82;
    then arccot is_differentiable_in x by A4,FDIFF_1:9;
    hence thesis by TAYLOR_1:3;
  end;
  then
A5: ( #Z n)*(arccot) is_differentiable_on Z by A1,FDIFF_1:9;
  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 by A2,XXREAL_1:4;
    arccot is_differentiable_on Z by A2,Th82;
    then
A8: arccot is_differentiable_in x by A6,FDIFF_1:9;
A9: x < 1 by A2,A6,XXREAL_1:4;
    ((( #Z n)*arccot)`|Z).x = diff(( #Z n)*arccot,x) by A5,A6,FDIFF_1:def 7
      .= (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,A9,Th76
      .= -n*(arccot.x) #Z (n-1) / (1+x^2);
    hence thesis;
  end;
  hence thesis by A1,A3,FDIFF_1:9;
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 by A2,Th91;
  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:20
      .= (1/2)*((( #Z 2)*(arctan))`|Z).x by A4,A5,FDIFF_1:def 7
      .= (1/2)*((2*(arctan.x) #Z (2-1)) / (1+x^2)) by A2,A3,A5,Th91
      .= (1/2)*(2*arctan.x / (1+x^2)) by PREPOWER:35
      .= arctan.x / (1+x^2);
    hence thesis;
  end;
  hence thesis by A1,A4,FDIFF_1:20;
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 by A2,Th92;
  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:20
      .= (1/2)*((( #Z 2)*(arccot))`|Z).x by A4,A5,FDIFF_1:def 7
      .= (1/2)*(-2*(arccot.x) #Z (2-1) / (1+x^2)) by A2,A3,A5,Th92
      .= -(1/2)*(2*(arccot.x) #Z 1 / (1+x^2))
      .= -(1/2)*(2*arccot.x / (1+x^2)) by PREPOWER:35
      .= -arccot.x / (1+x^2);
    hence thesis;
  end;
  hence thesis by A1,A4,FDIFF_1:20;
end;

::f.x=x*arctan.x

theorem Th95:
  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:17;
  ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
  then ].-1,1.[ c= dom arctan by Th23;
  then Z c= dom arctan by A1;
  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:18;
  then
A5: id Z is_differentiable_on Z by A2,FDIFF_1:23;
A6: arctan is_differentiable_on Z by A1,Th81;
  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 by A1,XXREAL_1:4;
A9: x < 1 by A1,A7,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:21
      .= (arctan.x)*((id Z)`|Z).x + ((id Z).x)*diff(arctan,x) by A5,A7,
FDIFF_1:def 7
      .= (arctan.x)*1 + ((id Z).x)*diff(arctan,x) by A2,A4,A7,FDIFF_1:23
      .= arctan.x + x*diff(arctan,x) by A7,FUNCT_1:18
      .= arctan.x + x*(1/(1+x^2)) by A8,A9,Th75
      .= arctan.x + x/(1+x^2);
    hence thesis;
  end;
  hence thesis by A3,A5,A6,FDIFF_1:21;
end;

::f.x=x*arccot.x

theorem Th96:
  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:17;
  ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
  then ].-1,1.[ c= dom arccot by Th24;
  then Z c= dom arccot by A1;
  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:18;
  then
A5: id Z is_differentiable_on Z by A2,FDIFF_1:23;
A6: arccot is_differentiable_on Z by A1,Th82;
  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 by A1,XXREAL_1:4;
A9: x < 1 by A1,A7,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:21
      .= (arccot.x)*((id Z)`|Z).x + ((id Z).x)*diff(arccot,x) by A5,A7,
FDIFF_1:def 7
      .= (arccot.x)*1 + ((id Z).x)*diff(arccot,x) by A2,A4,A7,FDIFF_1:23
      .= arccot.x + x*diff(arccot,x) by A7,FUNCT_1:18
      .= arccot.x + x*(-1/(1+x^2)) by A8,A9,Th76
      .= arccot.x - x/(1+x^2);
    hence thesis;
  end;
  hence thesis by A3,A5,A6,FDIFF_1:21;
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 by A3,FDIFF_1:23;
A6: arctan is_differentiable_on Z by A2,Th81;
  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 by A2,XXREAL_1:4;
A9: x < 1 by A2,A7,XXREAL_1:4;
    ((f(#)(arctan))`|Z).x = (arctan.x)*diff(f,x) + (f.x)*diff(arctan,x)
    by A1,A5,A6,A7,FDIFF_1:21
      .= (arctan.x)*(f`|Z).x + (f.x)*diff(arctan,x) by A5,A7,FDIFF_1:def 7
      .= (arctan.x)*r + (f.x)*diff(arctan,x) by A3,A4,A7,FDIFF_1:23
      .= (arctan.x)*r + (f.x)*(1/(1+x^2)) by A8,A9,Th75
      .= r*arctan.x + (r*x+s)/(1+x^2) by A3,A7;
    hence thesis;
  end;
  hence thesis by A1,A5,A6,FDIFF_1:21;
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 by A3,FDIFF_1:23;
A6: arccot is_differentiable_on Z by A2,Th82;
  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 by A2,XXREAL_1:4;
A9: x < 1 by A2,A7,XXREAL_1:4;
    ((f(#)(arccot))`|Z).x = (arccot.x)*diff(f,x) + (f.x)*diff(arccot,x)
    by A1,A5,A6,A7,FDIFF_1:21
      .= (arccot.x)*(f`|Z).x + (f.x)*diff(arccot,x) by A5,A7,FDIFF_1:def 7
      .= (arccot.x)*r + (f.x)*diff(arccot,x) by A3,A4,A7,FDIFF_1:23
      .= (arccot.x)*r + (f.x)*(-1/(1+x^2)) by A8,A9,Th76
      .= (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:21;
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: for x st x in Z holds f.x=2*x+0 & f.x > -1 & f.x < 1 by A2;
A4: Z c= dom ((arctan)*f) by A1,VALUED_1:def 5;
  then
A5: (arctan)*f is_differentiable_on Z by A3,Th87;
  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:20
      .= (1/2)*(((arctan)*f)`|Z).x by A5,A6,FDIFF_1:def 7
      .= (1/2)*(2/(1+(2*x+0)^2)) by A4,A3,A6,Th87
      .= 1/(1+(2*x)^2);
    hence thesis;
  end;
  hence thesis by A1,A5,FDIFF_1:20;
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: for x st x in Z holds f.x=2*x+0 & f.x > -1 & f.x < 1 by A2;
A4: Z c= dom ((arccot)*f) by A1,VALUED_1:def 5;
  then
A5: (arccot)*f is_differentiable_on Z by A3,Th88;
  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:20
      .= (1/2)*(((arccot)*f)`|Z).x by A5,A6,FDIFF_1:def 7
      .= (1/2)*(-2/(1+(2*x+0)^2)) by A4,A3,A6,Th88
      .= -1/(1+(2*x)^2);
    hence thesis;
  end;
  hence thesis by A1,A5,FDIFF_1:20;
end;

::f.x=1+x|^2

theorem Th101:
  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 that
A1: Z c= dom (f1+f2) and
A2: for x st x in Z holds f1.x=1 and
A3: f2=#Z 2;
A4: for x st x in Z holds f2 is_differentiable_in x by A3,TAYLOR_1:2;
A5: Z c= dom f1 /\ dom f2 by A1,VALUED_1:def 1;
  then
A6: Z c= dom f1 by XBOOLE_1:18;
A7: for x st x in Z holds f1.x=0*x+1 by A2;
  then
A8: f1 is_differentiable_on Z by A6,FDIFF_1:23;
  Z c= dom f2 by A5,XBOOLE_1:18;
  then
A9: f2 is_differentiable_on Z by A4,FDIFF_1:9;
A10: for x st x in Z holds (f2`|Z).x=2*x
  proof
    let x;
    2*(x #Z (2-1)) = 2*x by PREPOWER:35;
    then
A11: diff(f2,x) = 2*x by A3,TAYLOR_1:2;
    assume x in Z;
    hence thesis by A9,A11,FDIFF_1:def 7;
  end;
  for x st x in Z holds ((f1+f2)`|Z).x = 2*x
  proof
    let x;
    assume
A12: x in Z;
    then ((f1+f2)`|Z).x = diff(f1,x) + diff(f2,x) by A1,A8,A9,FDIFF_1:18
      .= (f1`|Z).x + diff(f2,x) by A8,A12,FDIFF_1:def 7
      .= (f1`|Z).x + (f2`|Z).x by A9,A12,FDIFF_1:def 7
      .= 0 + (f2`|Z).x by A6,A7,A12,FDIFF_1:23
      .= 2*x by A10,A12;
    hence thesis;
  end;
  hence thesis by A1,A8,A9,FDIFF_1:18;
end;

::f.x=(1/2)ln(1+x|^2)

theorem Th102:
  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 being object st y in Z holds y in dom (f1+f2) by FUNCT_1:11;
  then
A5: Z c= dom (f1+f2);
  then
A6: f1+f2 is_differentiable_on Z by A2,A3,Th101;
  for x st x in Z holds ln*(f1+f2) is_differentiable_in x
  proof
    let x;
    assume
A7: x in Z;
    then (f1+f2).x = f1.x+f2.x by A5,VALUED_1:def 1
      .= 1+f2.x by A3,A7
      .= 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:35
      .= 1+x*x by PREPOWER:35;
    then
A8: (f1+f2).x > 0 by XREAL_1:34,63;
    (f1+f2) is_differentiable_in x by A6,A7,FDIFF_1:9;
    hence thesis by A8,TAYLOR_1:20;
  end;
  then
A9: ln*(f1+f2) is_differentiable_on Z by A4,FDIFF_1:9;
  for x st x in Z holds (((1/2)(#)(ln*(f1+f2)))`|Z).x = x/(1+x^2)
  proof
    let x;
    assume
A10: x in Z;
    then
A11: (f1+f2) is_differentiable_in x by A6,FDIFF_1:9;
A12: (f1+f2).x = f1.x+f2.x by A5,A10,VALUED_1:def 1
      .= 1+f2.x by A3,A10
      .= 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:35
      .= 1+x*x by PREPOWER:35;
    then (f1+f2).x > 0 by XREAL_1:34,63;
    then diff(ln*(f1+f2),x) = diff((f1+f2),x)/((f1+f2).x) by A11,TAYLOR_1:20
      .= ((f1+f2)`|Z).x/((f1+f2).x) by A6,A10,FDIFF_1:def 7
      .= (2*x)/(1+x^2) by A2,A3,A5,A10,A12,Th101;
    hence (((1/2)(#)(ln*(f1+f2)))`|Z).x = (1/2)*((2*x)/(1+x^2)) by A1,A9,A10,
FDIFF_1:20
      .= x/(1+x^2);
  end;
  hence thesis by A1,A9,FDIFF_1:20;
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 and
A4: for x st x in Z holds f1.x=1;
  Z c= dom ((id Z)(#)(arctan)) /\ dom ((1/2)(#)(ln*(f1+f2))) by A1,VALUED_1:12;
  then
A5: Z c= dom ((1/2)(#)(ln*(f1+f2))) by XBOOLE_1:18;
  then
A6: ((1/2)(#)(ln*(f1+f2))) is_differentiable_on Z by A3,A4,Th102;
A7: (id Z)(#)(arctan) is_differentiable_on Z by A2,Th95;
  for x st x in Z holds (((id Z)(#)(arctan)-(1/2)(#)(ln*(f1+f2)))`|Z).x =
  arctan.x
  proof
    let x;
    assume
A8: 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,A6,FDIFF_1:19
      .= (((id Z)(#)(arctan))`|Z).x-diff((1/2)(#)(ln*(f1+f2)),x) by A7,A8,
FDIFF_1:def 7
      .= (((id Z)(#)(arctan))`|Z).x-(((1/2)(#)(ln*(f1+f2)))`|Z).x by A6,A8,
FDIFF_1:def 7
      .= arctan.x+x/(1+x^2)-(((1/2)(#)(ln*(f1+f2)))`|Z).x by A2,A8,Th95
      .= arctan.x+x/(1+x^2)-x/(1+x^2) by A3,A4,A5,A8,Th102
      .= arctan.x;
  end;
  hence thesis by A1,A7,A6,FDIFF_1:19;
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 and
A4: for x st x in Z holds f1.x=1;
  Z c= dom ((id Z)(#)(arccot)) /\ dom ((1/2)(#)(ln*(f1+f2))) by A1,
VALUED_1:def 1;
  then
A5: Z c= dom ((1/2)(#)(ln*(f1+f2))) by XBOOLE_1:18;
  then
A6: ((1/2)(#)(ln*(f1+f2))) is_differentiable_on Z by A3,A4,Th102;
A7: (id Z)(#)(arccot) is_differentiable_on Z by A2,Th96;
  for x st x in Z holds (((id Z)(#)(arccot)+(1/2)(#)(ln*(f1+f2)))`|Z).x =
  arccot.x
  proof
    let x;
    assume
A8: 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,A6,FDIFF_1:18
      .= (((id Z)(#)(arccot))`|Z).x+diff((1/2)(#)(ln*(f1+f2)),x) by A7,A8,
FDIFF_1:def 7
      .= (((id Z)(#)(arccot))`|Z).x+(((1/2)(#)(ln*(f1+f2)))`|Z).x by A6,A8,
FDIFF_1:def 7
      .= arccot.x-x/(1+x^2)+(((1/2)(#)(ln*(f1+f2)))`|Z).x by A2,A8,Th96
      .= arccot.x-x/(1+x^2)+x/(1+x^2) by A3,A4,A5,A8,Th102
      .= arccot.x;
  end;
  hence thesis by A1,A7,A6,FDIFF_1:18;
end;

::f.x=x*arctan(x/r)

theorem Th105:
  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;
A3: Z c= dom (id Z) /\ dom ((arctan)*f) by A1,VALUED_1:def 4;
  then
A4: Z c= dom (id Z) by XBOOLE_1:18;
A5: Z c= dom ((arctan)*f) by A3,XBOOLE_1:18;
  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 thesis;
  end;
  then
A6: for x st x in Z holds f.x=(1/r)*x+0 & f.x > -1 & f.x < 1 by A2;
  then
A7: (arctan)*f is_differentiable_on Z by A5,Th87;
A8: for x st x in Z holds (id Z).x = 1*x+0 by FUNCT_1:18;
  then
A9: id Z is_differentiable_on Z by A4,FDIFF_1:23;
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 A6,A5,Th87
      .= 1/(r*(1+(x/r)^2)) by XCMPLX_1:78;
    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 A5,FUNCT_1:12
      .= 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,A9,A7,A11,FDIFF_1:21
      .= ((arctan)*f).x*((id Z)`|Z).x + ((id Z).x)*diff((arctan)*f,x) by A9,A11
,FDIFF_1:def 7
      .= ((arctan)*f).x*1 + ((id Z).x)*diff((arctan)*f,x) by A4,A8,A11,
FDIFF_1:23
      .= ((arctan)*f).x*1 + ((id Z).x)*(((arctan)*f)`|Z).x by A7,A11,
FDIFF_1:def 7
      .= ((arctan)*f).x + x*(((arctan)*f)`|Z).x by A11,FUNCT_1:18
      .= 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,A9,A7,FDIFF_1:21;
end;

::f.x=x*arccot(x/r)

theorem Th106:
  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;
A3: Z c= dom (id Z) /\ dom ((arccot)*f) by A1,VALUED_1:def 4;
  then
A4: Z c= dom (id Z) by XBOOLE_1:18;
A5: Z c= dom ((arccot)*f) by A3,XBOOLE_1:18;
  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 thesis;
  end;
  then
A6: for x st x in Z holds f.x=(1/r)*x+0 & f.x > -1 & f.x < 1 by A2;
  then
A7: (arccot)*f is_differentiable_on Z by A5,Th88;
A8: for x st x in Z holds (id Z).x = 1*x+0 by FUNCT_1:18;
  then
A9: id Z is_differentiable_on Z by A4,FDIFF_1:23;
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 A6,A5,Th88
      .= -1/(r*(1+(x/r)^2)) by XCMPLX_1:78;
    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 A5,FUNCT_1:12
      .= 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,A9,A7,A11,FDIFF_1:21
      .= ((arccot)*f).x*((id Z)`|Z).x + ((id Z).x)*diff((arccot)*f,x) by A9,A11
,FDIFF_1:def 7
      .= ((arccot)*f).x*1 + ((id Z).x)*diff((arccot)*f,x) by A4,A8,A11,
FDIFF_1:23
      .= ((arccot)*f).x*1 + ((id Z).x)*(((arccot)*f)`|Z).x by A7,A11,
FDIFF_1:def 7
      .= ((arccot)*f).x + x*(((arccot)*f)`|Z).x by A11,FUNCT_1:18
      .= 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,A9,A7,FDIFF_1:21;
end;

::f.x=1+(x/r)^2

theorem Th107:
  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 and
A4: for x st x in Z holds f.x=x/r;
A5: for x st x in Z holds f1.x=0*x+1 by A2;
A6: Z c= dom f1 /\ dom f2 by A1,VALUED_1:def 1;
  then
A7: Z c= dom f1 by XBOOLE_1:18;
  then
A8: f1 is_differentiable_on Z by A5,FDIFF_1:23;
A9: 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 A4
      .= (1/r)*x+0;
  end;
A10: for x st x in Z holds f2 is_differentiable_in x
  proof
    let x;
    Z c= dom (( #Z 2)*f) by A3,A6,XBOOLE_1:18;
    then for y being object st y in Z holds y in dom f by FUNCT_1:11;
    then Z c= dom f;
    then
A11: f is_differentiable_on Z by A9,FDIFF_1:23;
    assume x in Z;
    then f is_differentiable_in x by A11,FDIFF_1:9;
    hence thesis by A3,TAYLOR_1:3;
  end;
  Z c= dom f2 by A6,XBOOLE_1:18;
  then
A12: f2 is_differentiable_on Z by A10,FDIFF_1:9;
A13: for x st x in Z holds (f2`|Z).x = (2*x)/(r^2)
  proof
    let x;
    assume
A14: x in Z;
    Z c= dom (( #Z 2)*f) by A3,A6,XBOOLE_1:18;
    then for y being object st y in Z holds y in dom f by FUNCT_1:11;
    then
A15: Z c= dom f;
    then
A16: f is_differentiable_on Z by A9,FDIFF_1:23;
    then
A17: f is_differentiable_in x by A14,FDIFF_1:9;
    (f2`|Z).x = diff(( #Z 2)*f,x) by A3,A12,A14,FDIFF_1:def 7
      .= 2 * (f.x) #Z (2-1) *diff(f,x) by A17,TAYLOR_1:3
      .= 2*(f.x)*diff(f,x) by PREPOWER:35
      .= 2*(x/r)*diff(f,x) by A4,A14
      .= 2*(x/r)*(f`|Z).x by A14,A16,FDIFF_1:def 7
      .= 2*(x/r)*(1/r) by A9,A14,A15,FDIFF_1:23
      .= 2*((x/r)*(1/r))
      .= 2*((x*1)/(r*r)) by XCMPLX_1:76
      .= (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
A18: x in Z;
    then ((f1+f2)`|Z).x = diff(f1,x) + diff(f2,x) by A1,A8,A12,FDIFF_1:18
      .= (f1`|Z).x + diff(f2,x) by A8,A18,FDIFF_1:def 7
      .= (f1`|Z).x + (f2`|Z).x by A12,A18,FDIFF_1:def 7
      .= 0 + (f2`|Z).x by A7,A5,A18,FDIFF_1:23
      .= (2*x)/(r^2) by A13,A18;
    hence thesis;
  end;
  hence thesis by A1,A8,A12,FDIFF_1:18;
end;

::f.x=(r/2)ln(1+(x/r)^2)

theorem Th108:
  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 and
A5: for x st x in Z holds f.x=x/r;
A6: Z c= dom (ln*(f1+f2)) by A1,VALUED_1:def 5;
  then for y being object st y in Z holds y in dom (f1+f2) by FUNCT_1:11;
  then
A7: Z c= dom (f1+f2);
  then
A8: f1+f2 is_differentiable_on Z by A2,A4,A5,Th107;
  dom (f1+f2) = dom f1 /\ dom f2 by VALUED_1:def 1;
  then
A9: Z c= dom f2 by A7,XBOOLE_1:18;
  for x st x in Z holds ln*(f1+f2) is_differentiable_in x
  proof
    let x;
    set g = #Z 2;
    assume
A10: x in Z;
    then (f1+f2).x = f1.x+f2.x by A7,VALUED_1:def 1
      .= 1+(g*f).x by A2,A4,A10
      .= 1+g.(f.x) by A4,A9,A10,FUNCT_1:12
      .= 1+g.(x/r) by A5,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:35
      .= 1+(x/r)*(x/r) by PREPOWER:35;
    then
A11: (f1+f2).x > 0 by XREAL_1:34,63;
    (f1+f2) is_differentiable_in x by A8,A10,FDIFF_1:9;
    hence thesis by A11,TAYLOR_1:20;
  end;
  then
A12: ln*(f1+f2) is_differentiable_on Z by A6,FDIFF_1:9;
  for x st x in Z holds (((r/2)(#)(ln*(f1+f2)))`|Z).x = x/(r*(1+(x/r)^2))
  proof
    let x;
    set g = #Z 2;
    assume
A13: x in Z;
    then
A14: (f1+f2) is_differentiable_in x by A8,FDIFF_1:9;
A15: (f1+f2).x = f1.x+f2.x by A7,A13,VALUED_1:def 1
      .= 1+(g*f).x by A2,A4,A13
      .= 1+g.(f.x) by A4,A9,A13,FUNCT_1:12
      .= 1+g.(x/r) by A5,A13
      .= 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:35
      .= 1+(x/r)*(x/r) by PREPOWER:35;
    then (f1+f2).x > 0 by XREAL_1:34,63;
    then
A16: diff(ln*(f1+f2),x) = diff((f1+f2),x)/((f1+f2).x) by A14,TAYLOR_1:20
      .= ((f1+f2)`|Z).x/((f1+f2).x) by A8,A13,FDIFF_1:def 7
      .= ((2*x)/(r^2))/(1+(x/r)^2) by A2,A4,A5,A7,A13,A15,Th107;
    thus (((r/2)(#)(ln*(f1+f2)))`|Z).x = (r/2)*diff((ln*(f1+f2)),x) by A1,A12
,A13,FDIFF_1:20
      .= (r*x)/(r^2)/(1+(x/r)^2) by A16
      .= ((r/r)*(x/r))/(1+(x/r)^2) by XCMPLX_1:76
      .= (1*(x/r))/(1+(x/r)^2) by A3,XCMPLX_1:60
      .= x/(r*(1+(x/r)^2)) by XCMPLX_1:78;
  end;
  hence thesis by A1,A12,FDIFF_1:20;
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 and
A6: for x st x in Z holds f.x=x/r;
A7: Z c= dom ((id Z)(#)((arctan)*f)) /\ dom ((r/2)(#)(ln*(f1+f2))) by A1,
VALUED_1:12;
  then
A8: Z c= dom ((r/2)(#)(ln*(f1+f2))) by XBOOLE_1:18;
  then
A9: (r/2)(#)(ln*(f1+f2)) is_differentiable_on Z by A2,A4,A5,A6,Th108;
A10: Z c= dom ((id Z)(#)((arctan)*f)) by A7,XBOOLE_1:18;
  then
A11: (id Z)(#)((arctan)*f) is_differentiable_on Z by A3,Th105;
  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
A12: 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,A11,A9,FDIFF_1:19
      .= (((id Z)(#)((arctan)*f))`|Z).x-diff((r/2)(#)(ln*(f1+f2)),x) by A11,A12
,FDIFF_1:def 7
      .= (((id Z)(#)((arctan)*f))`|Z).x-(((r/2)(#)(ln*(f1+f2)))`|Z).x by A9,A12
,FDIFF_1:def 7
      .= arctan.(x/r)+x/(r*(1+(x/r)^2))-(((r/2)(#)(ln*(f1+f2)))`|Z).x by A3,A10
,A12,Th105
      .= arctan.(x/r)+x/(r*(1+(x/r)^2))-x/(r*(1+(x/r)^2)) by A2,A4,A5,A6,A8,A12
,Th108
      .= arctan.(x/r);
  end;
  hence thesis by A1,A11,A9,FDIFF_1:19;
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 and
A6: for x st x in Z holds f.x=x/r;
A7: Z c= dom ((id Z)(#)((arccot)*f)) /\ dom ((r/2)(#)(ln*(f1+f2))) by A1,
VALUED_1:def 1;
  then
A8: Z c= dom ((r/2)(#)(ln*(f1+f2))) by XBOOLE_1:18;
  then
A9: (r/2)(#)(ln*(f1+f2)) is_differentiable_on Z by A2,A4,A5,A6,Th108;
A10: Z c= dom ((id Z)(#)((arccot)*f)) by A7,XBOOLE_1:18;
  then
A11: (id Z)(#)((arccot)*f) is_differentiable_on Z by A3,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
A12: 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,A11,A9,FDIFF_1:18
      .= (((id Z)(#)((arccot)*f))`|Z).x+diff((r/2)(#)(ln*(f1+f2)),x) by A11,A12
,FDIFF_1:def 7
      .= (((id Z)(#)((arccot)*f))`|Z).x+(((r/2)(#)(ln*(f1+f2)))`|Z).x by A9,A12
,FDIFF_1:def 7
      .= arccot.(x/r)-x/(r*(1+(x/r)^2))+(((r/2)(#)(ln*(f1+f2)))`|Z).x by A3,A10
,A12,Th106
      .= arccot.(x/r)-x/(r*(1+(x/r)^2))+x/(r*(1+(x/r)^2)) by A2,A4,A5,A6,A8,A12
,Th108
      .= arccot.(x/r);
  end;
  hence thesis by A1,A11,A9,FDIFF_1:18;
end;

::f.x=arctan.(1/x)

theorem
  not 0 in Z & Z c= dom (arctan*((id Z)^)) & (for x st x in Z holds ((id
Z)^).x > -1 & ((id Z)^).x < 1) implies (arctan*((id Z)^)) is_differentiable_on
  Z & for x st x in Z holds ((arctan*((id Z)^))`|Z).x = -1/(1+x^2)
proof
  set f = id Z;
  assume that
A1: not 0 in Z and
A2: Z c= dom (arctan*((id Z)^)) and
A3: for x st x in Z holds ((id Z)^).x > -1 & ((id Z)^).x < 1;
  dom (arctan*(f^)) c= dom (f^) by RELAT_1:25;
  then
A4: Z c= dom(f^) by A2;
A5: f^ is_differentiable_on Z by A1,FDIFF_5:4;
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^).x > -1 by A3;
A9: (f^).x < 1 by A3,A7;
    f^ is_differentiable_in x by A5,A7,FDIFF_1:9;
    hence thesis by A8,A9,Th85;
  end;
  then
A10: arctan*(f^) is_differentiable_on Z by A2,FDIFF_1:9;
  for x st x in Z holds ((arctan*(f^))`|Z).x = -1/(1+x^2)
  proof
    let x;
    assume
A11: x in Z;
    then
A12: f^ is_differentiable_in x by A5,FDIFF_1:9;
A13: (f^).x < 1 by A3,A11;
A14: (f^).x > -1 by A3,A11;
    f.x = x by A11,FUNCT_1:18;
    then x <> 0 by A4,A11,RFUNCT_1:3;
    then
A15: x^2 <> 0;
    ((arctan*(f^))`|Z).x = diff((arctan)*(f^),x) by A10,A11,FDIFF_1:def 7
      .= diff((f^),x)/(1+((f^).x)^2) by A12,A14,A13,Th85
      .= ((f^)`|Z).x/(1+((f^).x)^2) by A5,A11,FDIFF_1:def 7
      .= (-1/x^2)/(1+((f^).x)^2) by A1,A11,FDIFF_5:4
      .= (-1/x^2)/(1+((f.x)")^2) by A4,A11,RFUNCT_1:def 2
      .= (-1/x^2)/(1+(1/x)^2) by A11,FUNCT_1:18
      .= -(1/x^2)/(1+(1/x)^2)
      .= -1/((x^2)*(1+(1/x)^2)) by XCMPLX_1:78
      .= -1/((x^2)*1+(x^2)*(1/x)^2)
      .= -1/((x^2)+(x^2)*(1/(x*x))) by XCMPLX_1:102
      .= -1/((x^2)+((x^2)*1)/(x^2))
      .= -1/(1+x^2) by A15,XCMPLX_1:60;
    hence thesis;
  end;
  hence thesis by A2,A6,FDIFF_1:9;
end;

::f.x=arccot.(1/x)

theorem
  not 0 in Z & Z c= dom (arccot*((id Z)^)) & (for x st x in Z holds ((id
Z)^).x > -1 & ((id Z)^).x < 1) implies (arccot*((id Z)^)) is_differentiable_on
  Z & for x st x in Z holds ((arccot*((id Z)^))`|Z).x = 1/(1+x^2)
proof
  set f = id Z;
  assume that
A1: not 0 in Z and
A2: Z c= dom (arccot*(f^)) and
A3: for x st x in Z holds (f^).x > -1 & (f^).x < 1;
  dom (arccot*(f^)) c= dom (f^) by RELAT_1:25;
  then
A4: Z c= dom(f^) by A2;
A5: f^ is_differentiable_on Z by A1,FDIFF_5:4;
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^).x > -1 by A3;
A9: (f^).x < 1 by A3,A7;
    f^ is_differentiable_in x by A5,A7,FDIFF_1:9;
    hence thesis by A8,A9,Th86;
  end;
  then
A10: arccot*(f^) is_differentiable_on Z by A2,FDIFF_1:9;
  for x st x in Z holds ((arccot*(f^))`|Z).x = 1/(1+x^2)
  proof
    let x;
    assume
A11: x in Z;
    then
A12: f^ is_differentiable_in x by A5,FDIFF_1:9;
A13: (f^).x < 1 by A3,A11;
A14: (f^).x > -1 by A3,A11;
    f.x = x by A11,FUNCT_1:18;
    then x <> 0 by A4,A11,RFUNCT_1:3;
    then
A15: x^2 <> 0;
    ((arccot*(f^))`|Z).x = diff((arccot)*(f^),x) by A10,A11,FDIFF_1:def 7
      .= -diff((f^),x)/(1+((f^).x)^2) by A12,A14,A13,Th86
      .= -((f^)`|Z).x/(1+((f^).x)^2) by A5,A11,FDIFF_1:def 7
      .= -(-1/x^2)/(1+((f^).x)^2) by A1,A11,FDIFF_5:4
      .= -(-1/x^2)/(1+((f.x)")^2) by A4,A11,RFUNCT_1:def 2
      .= -(-1/x^2)/(1+(1/x)^2) by A11,FUNCT_1:18
      .= (1/x^2)/(1+(1/x)^2)
      .= 1/((x^2)*(1+(1/x)^2)) by XCMPLX_1:78
      .= 1/((x^2)*1+(x^2)*(1/x)^2)
      .= 1/((x^2)+(x^2)*(1/(x*x))) by XCMPLX_1:102
      .= 1/((x^2)+((x^2)*1)/(x^2))
      .= 1/(1+x^2) by A15,XCMPLX_1:60;
    hence thesis;
  end;
  hence thesis by A2,A6,FDIFF_1:9;
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) and
A2: f=f1+h(#)f2 and
A3: for x st x in Z holds f.x > -1 & f.x < 1 and
A4: for x st x in Z holds f1.x = r+s*x and
A5: f2=#Z 2;
  dom (arctan*f) c= dom f by RELAT_1:25;
  then
A6: Z c= dom (f1+h(#)f2) by A1,A2;
  then Z c= dom f1 /\ dom (h(#)f2) by VALUED_1:def 1;
  then
A7: Z c= dom (h(#)f2) by XBOOLE_1:18;
A8: (f1+h(#)f2) is_differentiable_on Z by A4,A5,A6,FDIFF_4:12;
A9: for x st x in Z holds arctan*(f1+h(#)f2) is_differentiable_in x
  proof
    let x;
    assume
A10: x in Z;
    then
A11: f.x > -1 by A3;
A12: f.x < 1 by A3,A10;
    f is_differentiable_in x by A2,A8,A10,FDIFF_1:9;
    hence thesis by A2,A11,A12,Th85;
  end;
  then
A13: arctan*(f1+h(#)f2) is_differentiable_on Z by A1,A2,FDIFF_1:9;
  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
A14: x in Z;
    then
A15: (f1+h(#)f2).x = f1.x+(h(#)f2).x by A6,VALUED_1:def 1
      .= f1.x+h*f2.x by A7,A14,VALUED_1:def 5
      .= r+s*x+h*(f2.x) by A4,A14
      .= r+s*x+h*(x #Z (1+1)) by A5,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:35
      .= r+s*x+h*x^2 by PREPOWER:35;
A16: f is_differentiable_in x by A2,A8,A14,FDIFF_1:9;
A17: f.x > -1 by A3,A14;
A18: f.x < 1 by A3,A14;
    ((arctan*(f1+h(#)f2))`|Z).x = diff((arctan)*f,x) by A2,A13,A14,
FDIFF_1:def 7
      .= diff(f,x)/(1+(f.x)^2) by A16,A17,A18,Th85
      .= ((f1+h(#)f2)`|Z).x/(1+(f.x)^2) by A2,A8,A14,FDIFF_1:def 7
      .= (s+2*h*x)/(1+(r+s*x+h*x^2)^2) by A2,A4,A5,A6,A14,A15,FDIFF_4:12;
    hence thesis;
  end;
  hence thesis by A1,A2,A9,FDIFF_1:9;
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) and
A2: f=f1+h(#)f2 and
A3: for x st x in Z holds f.x > -1 & f.x < 1 and
A4: for x st x in Z holds f1.x = r+s*x and
A5: f2=#Z 2;
  dom (arccot*f) c= dom f by RELAT_1:25;
  then
A6: Z c= dom (f1+h(#)f2) by A1,A2;
  then Z c= dom f1 /\ dom (h(#)f2) by VALUED_1:def 1;
  then
A7: Z c= dom (h(#)f2) by XBOOLE_1:18;
A8: (f1+h(#)f2) is_differentiable_on Z by A4,A5,A6,FDIFF_4:12;
A9: for x st x in Z holds arccot*(f1+h(#)f2) is_differentiable_in x
  proof
    let x;
    assume
A10: x in Z;
    then
A11: f.x > -1 by A3;
A12: f.x < 1 by A3,A10;
    f is_differentiable_in x by A2,A8,A10,FDIFF_1:9;
    hence thesis by A2,A11,A12,Th86;
  end;
  then
A13: arccot*(f1+h(#)f2) is_differentiable_on Z by A1,A2,FDIFF_1:9;
  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
A14: x in Z;
    then
A15: (f1+h(#)f2).x = f1.x+(h(#)f2).x by A6,VALUED_1:def 1
      .= f1.x+h*f2.x by A7,A14,VALUED_1:def 5
      .= r+s*x+h*(f2.x) by A4,A14
      .= r+s*x+h*(x #Z (1+1)) by A5,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:35
      .= r+s*x+h*x^2 by PREPOWER:35;
A16: f is_differentiable_in x by A2,A8,A14,FDIFF_1:9;
A17: f.x > -1 by A3,A14;
A18: f.x < 1 by A3,A14;
    ((arccot*(f1+h(#)f2))`|Z).x = diff((arccot)*f,x) by A2,A13,A14,
FDIFF_1:def 7
      .= -diff(f,x)/(1+(f.x)^2) by A16,A17,A18,Th86
      .= -((f1+h(#)f2)`|Z).x/(1+(f.x)^2) by A2,A8,A14,FDIFF_1:def 7
      .= -(s+2*h*x)/(1+(r+s*x+h*x^2)^2) by A2,A4,A5,A6,A14,A15,FDIFF_4:12;
    hence thesis;
  end;
  hence thesis by A1,A2,A9,FDIFF_1:9;
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;
A4: exp_R is_differentiable_in x by SIN_COS:65;
    assume x in Z;
    then
A5: exp_R.x < 1 by A2;
    exp_R.x + 0 > 0 + (-1) by SIN_COS:54;
    hence thesis by A5,A4,Th85;
  end;
  then
A6: arctan*exp_R is_differentiable_on Z by A1,FDIFF_1:9;
  for x st x in Z holds ((arctan*exp_R)`|Z).x = exp_R.x/(1+(exp_R.x)^2)
  proof
    let x;
A7: exp_R.x + 0 > 0 + (-1) by SIN_COS:54;
A8: exp_R is_differentiable_in x by SIN_COS:65;
    assume
A9: x in Z;
    then
A10: exp_R.x < 1 by A2;
    ((arctan*exp_R)`|Z).x = diff(arctan*exp_R,x) by A6,A9,FDIFF_1:def 7
      .= diff(exp_R,x)/(1+(exp_R.x)^2) by A7,A10,A8,Th85
      .= (exp_R.x)/(1+(exp_R.x)^2) by SIN_COS:65;
    hence thesis;
  end;
  hence thesis by A1,A3,FDIFF_1:9;
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;
A4: exp_R is_differentiable_in x by SIN_COS:65;
    assume x in Z;
    then
A5: exp_R.x < 1 by A2;
    exp_R.x + 0 > 0 + (-1) by SIN_COS:54;
    hence thesis by A5,A4,Th86;
  end;
  then
A6: arccot*exp_R is_differentiable_on Z by A1,FDIFF_1:9;
  for x st x in Z holds ((arccot*exp_R)`|Z).x = -exp_R.x/(1+(exp_R.x)^2)
  proof
    let x;
A7: exp_R.x + 0 > 0 + (-1) by SIN_COS:54;
A8: exp_R is_differentiable_in x by SIN_COS:65;
    assume
A9: x in Z;
    then
A10: exp_R.x < 1 by A2;
    ((arccot*exp_R)`|Z).x = diff(arccot*exp_R,x) by A6,A9,FDIFF_1:def 7
      .= -diff(exp_R,x)/(1+(exp_R.x)^2) by A7,A10,A8,Th86
      .= -(exp_R.x)/(1+(exp_R.x)^2) by SIN_COS:65;
    hence thesis;
  end;
  hence thesis by A1,A3,FDIFF_1:9;
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
A1: right_open_halfline 0 = {g where g is Real: 0 < g} by XXREAL_1:230;
  assume that
A2: Z c= dom (arctan*ln) and
A3: for x st x in Z holds ln.x > -1 & ln.x < 1;
  dom (arctan*ln) c= dom ln by RELAT_1:25;
  then
A4: Z c= dom ln by A2;
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 A1;
    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
A8: ln.x > -1 by A3;
A9: ln.x < 1 by A3,A7;
    ln is_differentiable_in x by A5,A7,TAYLOR_1:18;
    hence thesis by A8,A9,Th85;
  end;
  then
A10: arctan*ln is_differentiable_on Z by A2,FDIFF_1:9;
  for x st x in Z holds ((arctan*ln)`|Z).x = 1/(x*(1+(ln.x)^2))
  proof
    let x;
    assume
A11: x in Z;
    then
A12: ln is_differentiable_in x by A5,TAYLOR_1:18;
A13: ln.x < 1 by A3,A11;
A14: ln.x > -1 by A3,A11;
    x > 0 by A5,A11;
    then
A15: x in right_open_halfline(0) by A1;
    ((arctan*ln)`|Z).x = diff(arctan*ln,x) by A10,A11,FDIFF_1:def 7
      .= diff(ln,x)/(1+(ln.x)^2) by A12,A14,A13,Th85
      .= (1/x)/(1+(ln.x)^2) by A15,TAYLOR_1:18
      .= 1/(x*(1+(ln.x)^2)) by XCMPLX_1:78;
    hence thesis;
  end;
  hence thesis by A2,A6,FDIFF_1:9;
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
A1: right_open_halfline 0 = {g where g is Real: 0 < g} by XXREAL_1:230;
  assume that
A2: Z c= dom (arccot*ln) and
A3: for x st x in Z holds ln.x > -1 & ln.x < 1;
  dom (arccot*ln) c= dom ln by RELAT_1:25;
  then
A4: Z c= dom ln by A2;
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 A1;
    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
A8: ln.x > -1 by A3;
A9: ln.x < 1 by A3,A7;
    ln is_differentiable_in x by A5,A7,TAYLOR_1:18;
    hence thesis by A8,A9,Th86;
  end;
  then
A10: arccot*ln is_differentiable_on Z by A2,FDIFF_1:9;
  for x st x in Z holds ((arccot*ln)`|Z).x = -1/(x*(1+(ln.x)^2))
  proof
    let x;
    assume
A11: x in Z;
    then
A12: ln is_differentiable_in x by A5,TAYLOR_1:18;
A13: ln.x < 1 by A3,A11;
A14: ln.x > -1 by A3,A11;
    x > 0 by A5,A11;
    then
A15: x in right_open_halfline(0) by A1;
    ((arccot*ln)`|Z).x = diff(arccot*ln,x) by A10,A11,FDIFF_1:def 7
      .= -diff(ln,x)/(1+(ln.x)^2) by A12,A14,A13,Th86
      .= -(1/x)/(1+(ln.x)^2) by A15,TAYLOR_1:18
      .= -1/(x*(1+(ln.x)^2)) by XCMPLX_1:78;
    hence thesis;
  end;
  hence thesis by A2,A6,FDIFF_1:9;
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,Th81;
    then
A5: arctan is_differentiable_in x by A4,FDIFF_1:9;
    exp_R is_differentiable_in arctan.x by SIN_COS:65;
    hence thesis by A5,FDIFF_2:13;
  end;
  then
A6: exp_R*arctan is_differentiable_on Z by A1,FDIFF_1:9;
  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: exp_R is_differentiable_in arctan.x by SIN_COS:65;
A9: arctan is_differentiable_on Z by A2,Th81;
    then arctan is_differentiable_in x by A7,FDIFF_1:9;
    then diff(exp_R*arctan,x) = diff(exp_R,arctan.x)*diff(arctan,x) by A8,
FDIFF_2:13
      .= diff(exp_R,arctan.x)*((arctan)`|Z).x by A7,A9,FDIFF_1:def 7
      .= diff(exp_R,arctan.x)*(1/(1+x^2)) by A2,A7,Th81
      .= exp_R.(arctan.x)/(1+x^2) by SIN_COS:65;
    hence thesis by A6,A7,FDIFF_1:def 7;
  end;
  hence thesis by A1,A3,FDIFF_1:9;
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,Th82;
    then
A5: arccot is_differentiable_in x by A4,FDIFF_1:9;
    exp_R is_differentiable_in arccot.x by SIN_COS:65;
    hence thesis by A5,FDIFF_2:13;
  end;
  then
A6: exp_R*arccot is_differentiable_on Z by A1,FDIFF_1:9;
  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: exp_R is_differentiable_in arccot.x by SIN_COS:65;
A9: arccot is_differentiable_on Z by A2,Th82;
    then arccot is_differentiable_in x by A7,FDIFF_1:9;
    then diff(exp_R*arccot,x) = diff(exp_R,arccot.x)*diff(arccot,x) by A8,
FDIFF_2:13
      .= diff(exp_R,arccot.x)*((arccot)`|Z).x by A7,A9,FDIFF_1:def 7
      .= diff(exp_R,arccot.x)*(-1/(1+x^2)) by A2,A7,Th82
      .= -diff(exp_R,arccot.x)*(1/(1+x^2))
      .= -exp_R.(arccot.x)/(1+x^2) by SIN_COS:65;
    hence thesis by A6,A7,FDIFF_1:def 7;
  end;
  hence thesis by A1,A3,FDIFF_1:9;
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.[;
A3: for x st x in Z holds (id Z).x = 1*x+0 by FUNCT_1:18;
  Z c= dom arctan /\ dom (id Z) by A1,VALUED_1:12;
  then
A4: Z c= dom (id Z) by XBOOLE_1:18;
  then
A5: id Z is_differentiable_on Z by A3,FDIFF_1:23;
A6: arctan is_differentiable_on Z by A2,Th81;
  for x st x in Z holds ((arctan-id Z)`|Z).x = -x^2/(1+x^2)
  proof
    let x;
A7: 1+x^2 > 0 by XREAL_1:34,63;
    assume
A8: x in Z;
    then ((arctan-id Z)`|Z).x = diff(arctan,x)-diff(id Z,x) by A1,A5,A6,
FDIFF_1:19
      .= ((arctan)`|Z).x-diff(id Z,x) by A6,A8,FDIFF_1:def 7
      .= 1/(1+x^2)-diff(id Z,x) by A2,A8,Th81
      .= 1/(1+x^2)-((id Z)`|Z).x by A5,A8,FDIFF_1:def 7
      .= 1/(1+x^2)-1 by A4,A3,A8,FDIFF_1:23
      .= 1/(1+x^2)-(1+x^2)/(1+x^2) by A7,XCMPLX_1:60
      .= -x^2/(1+x^2);
    hence thesis;
  end;
  hence thesis by A1,A5,A6,FDIFF_1:19;
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.[;
A3: arccot is_differentiable_on Z by A2,Th82;
A4: Z c= dom (-arccot) /\ dom (id Z) by A1,VALUED_1:12;
  then
A5: Z c= dom (id Z) by XBOOLE_1:18;
A6: for x st x in Z holds (id Z).x = 1*x+0 by FUNCT_1:18;
  then
A7: id Z is_differentiable_on Z by A5,FDIFF_1:23;
A8: Z c= dom ((-1)(#)arccot) by A4,XBOOLE_1:18;
  then
A9: -arccot is_differentiable_on Z by A3,FDIFF_1:20;
  for x st x in Z holds ((-arccot-id Z)`|Z).x = -x^2/(1+x^2)
  proof
    let x;
A10: 1+x^2 > 0 by XREAL_1:34,63;
    assume
A11: x in Z;
    then ((-arccot-id Z)`|Z).x = diff(-arccot,x)-diff(id Z,x) by A1,A7,A9,
FDIFF_1:19
      .= ((-arccot)`|Z).x-diff(id Z,x) by A9,A11,FDIFF_1:def 7
      .= (-1)*diff(arccot,x)-diff(id Z,x) by A8,A3,A11,FDIFF_1:20
      .= (-1)*((arccot)`|Z).x-diff(id Z,x) by A3,A11,FDIFF_1:def 7
      .= (-1)*(-1/(1+x^2))-diff(id Z,x) by A2,A11,Th82
      .= 1/(1+x^2)-((id Z)`|Z).x by A7,A11,FDIFF_1:def 7
      .= 1/(1+x^2)-1 by A5,A6,A11,FDIFF_1:23
      .= 1/(1+x^2)-(1+x^2)/(1+x^2) by A10,XCMPLX_1:60
      .= -x^2/(1+x^2);
    hence thesis;
  end;
  hence thesis by A1,A7,A9,FDIFF_1:19;
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.[;
  then
A2: arctan is_differentiable_on Z by Th81;
  ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
  then ].-1,1.[ c= dom arctan by Th23;
  then Z c= dom arctan by A1;
  then Z c= dom (exp_R) /\ dom arctan by SIN_COS:47,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:65;
  then
A4: exp_R is_differentiable_on Z by FDIFF_1:9,SIN_COS:47;
  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
A5: x in Z;
    then ((exp_R(#)arctan)`|Z).x = (arctan.x)*diff(exp_R,x)+(exp_R.x)*diff(
    arctan,x) by A3,A4,A2,FDIFF_1:21
      .= (arctan.x)*exp_R.x+(exp_R.x)*diff(arctan,x) by SIN_COS:65
      .= exp_R.x*arctan.x+(exp_R.x)*((arctan)`|Z).x by A2,A5,FDIFF_1:def 7
      .= exp_R.x*arctan.x+(exp_R.x)*(1/(1+x^2)) by A1,A5,Th81
      .= exp_R.x*arctan.x+exp_R.x/(1+x^2);
    hence thesis;
  end;
  hence thesis by A3,A4,A2,FDIFF_1:21;
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.[;
  then
A2: arccot is_differentiable_on Z by Th82;
  ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
  then ].-1,1.[ c= dom arccot by Th24;
  then Z c= dom arccot by A1;
  then Z c= dom (exp_R) /\ dom arccot by SIN_COS:47,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:65;
  then
A4: exp_R is_differentiable_on Z by FDIFF_1:9,SIN_COS:47;
  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
A5: x in Z;
    then ((exp_R(#)arccot)`|Z).x = (arccot.x)*diff(exp_R,x)+(exp_R.x)*diff(
    arccot,x) by A3,A4,A2,FDIFF_1:21
      .= (arccot.x)*exp_R.x+(exp_R.x)*diff(arccot,x) by SIN_COS:65
      .= exp_R.x*arccot.x+(exp_R.x)*((arccot)`|Z).x by A2,A5,FDIFF_1:def 7
      .= exp_R.x*arccot.x+(exp_R.x)*(-1/(1+x^2)) by A1,A5,Th82
      .= exp_R.x*arccot.x-exp_R.x/(1+x^2);
    hence thesis;
  end;
  hence thesis by A3,A4,A2,FDIFF_1:21;
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;
  set g = (1/r)(#)(arctan*f);
A4: for x st x in Z holds (id Z).x = 1*x+0 by FUNCT_1:18;
A5: Z c= dom ((1/r)(#)(arctan*f)) /\ dom (id Z) by A1,VALUED_1:12;
  then
A6: Z c= dom ((1/r)(#)(arctan*f)) by XBOOLE_1:18;
A7: Z c= dom (id Z) by A5,XBOOLE_1:18;
  then
A8: id Z is_differentiable_on Z by A4,FDIFF_1:23;
A9: Z c= dom (arctan*f) by A6,VALUED_1:def 5;
  then
A10: arctan*f is_differentiable_on Z by A3,Th87;
  then
A11: (1/r)(#)(arctan*f) is_differentiable_on Z by A6,FDIFF_1:20;
  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;
A12: 1+(r*x)^2 > 0 by XREAL_1:34,63;
    assume
A13: x in Z;
    then
A14: r <> 0 by A2;
    ((g-id Z)`|Z).x = diff(g,x)-diff(id Z,x) by A1,A11,A8,A13,FDIFF_1:19
      .= (g`|Z).x-diff(id Z,x) by A11,A13,FDIFF_1:def 7
      .= (1/r)*diff(arctan*f,x)-diff(id Z,x) by A6,A10,A13,FDIFF_1:20
      .= (1/r)*((arctan*f)`|Z).x-diff(id Z,x) by A10,A13,FDIFF_1:def 7
      .= (1/r)*((arctan*f)`|Z).x-((id Z)`|Z).x by A8,A13,FDIFF_1:def 7
      .= (1/r)*(r/(1+(r*x+0)^2))-((id Z)`|Z).x by A3,A9,A13,Th87
      .= (1/r)*(r/(1+(r*x)^2))-1 by A7,A4,A13,FDIFF_1:23
      .= (1*r)/(r*(1+(r*x)^2))-1 by XCMPLX_1:76
      .= 1/(1+(r*x)^2)-1 by A14,XCMPLX_1:91
      .= 1/(1+(r*x)^2)-(1+(r*x)^2)/(1+(r*x)^2) by A12,XCMPLX_1:60
      .= -(r*x)^2/(1+(r*x)^2);
    hence thesis;
  end;
  hence thesis by A1,A11,A8,FDIFF_1:19;
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;
  set g = (-1/r)(#)(arccot*f);
A4: for x st x in Z holds (id Z).x = 1*x+0 by FUNCT_1:18;
A5: Z c= dom ((-1/r)(#)(arccot*f)) /\ dom (id Z) by A1,VALUED_1:12;
  then
A6: Z c= dom ((-1/r)(#)(arccot*f)) by XBOOLE_1:18;
A7: Z c= dom (id Z) by A5,XBOOLE_1:18;
  then
A8: id Z is_differentiable_on Z by A4,FDIFF_1:23;
A9: Z c= dom (arccot*f) by A6,VALUED_1:def 5;
  then
A10: arccot*f is_differentiable_on Z by A3,Th88;
  then
A11: (-1/r)(#)(arccot*f) is_differentiable_on Z by A6,FDIFF_1:20;
  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;
A12: 1+(r*x)^2 > 0 by XREAL_1:34,63;
    assume
A13: x in Z;
    then
A14: r <> 0 by A2;
    ((g-id Z)`|Z).x = diff(g,x)-diff(id Z,x) by A1,A11,A8,A13,FDIFF_1:19
      .= (g`|Z).x-diff(id Z,x) by A11,A13,FDIFF_1:def 7
      .= (-1/r)*diff(arccot*f,x)-diff(id Z,x) by A6,A10,A13,FDIFF_1:20
      .= (-1/r)*((arccot*f)`|Z).x-diff(id Z,x) by A10,A13,FDIFF_1:def 7
      .= (-1/r)*((arccot*f)`|Z).x-((id Z)`|Z).x by A8,A13,FDIFF_1:def 7
      .= (-1/r)*(-r/(1+(r*x+0)^2))-((id Z)`|Z).x by A3,A9,A13,Th88
      .= ((-1)/r)*((-r)/(1+(r*x)^2))-1 by A7,A4,A13,FDIFF_1:23
      .= ((-1)*(-r))/(r*(1+(r*x)^2))-1 by XCMPLX_1:76
      .= (1*r)/(r*(1+(r*x)^2))-1
      .= 1/(1+(r*x)^2)-1 by A14,XCMPLX_1:91
      .= 1/(1+(r*x)^2)-(1+(r*x)^2)/(1+(r*x)^2) by A12,XCMPLX_1:60
      .= -(r*x)^2/(1+(r*x)^2);
    hence thesis;
  end;
  hence thesis by A1,A11,A8,FDIFF_1:19;
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
A1: right_open_halfline 0 = {g where g is Real: 0 < g} by XXREAL_1:230;
  assume that
A2: Z c= dom (ln(#)arctan) and
A3: Z c= ].-1,1.[;
A4: arctan is_differentiable_on Z by A3,Th81;
  Z c= dom ln /\ dom arctan by A2,VALUED_1:def 4;
  then
A5: Z c= dom ln by XBOOLE_1:18;
A6: for x st x in Z holds x > 0
  proof
    let x;
    assume x in Z;
    then x in right_open_halfline(0) by A5,TAYLOR_1:18;
    then ex g being Real st x = g & 0 < g by A1;
    hence thesis;
  end;
  then for x st x in Z holds ln is_differentiable_in x by TAYLOR_1:18;
  then
A7: ln is_differentiable_on Z by A5,FDIFF_1:9;
A8: for x st x in Z holds diff(ln,x) = 1/x
  proof
    let x;
    assume x in Z;
    then x > 0 by A6;
    then x in right_open_halfline(0) by A1;
    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 A2,A7
,A4,FDIFF_1:21
      .= (arctan.x)*(1/x)+(ln.x)*diff(arctan,x) by A8,A9
      .= (arctan.x)*(1/x)+(ln.x)*((arctan)`|Z).x by A4,A9,FDIFF_1:def 7
      .= ((arctan.x)*1)/x+(ln.x)*(1/(1+x^2)) by A3,A9,Th81
      .= arctan.x/x+ln.x/(1+x^2);
    hence thesis;
  end;
  hence thesis by A2,A7,A4,FDIFF_1:21;
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
A1: right_open_halfline 0 = {g where g is Real: 0 < g} by XXREAL_1:230;
  assume that
A2: Z c= dom (ln(#)arccot) and
A3: Z c= ].-1,1.[;
A4: arccot is_differentiable_on Z by A3,Th82;
  Z c= dom ln /\ dom arccot by A2,VALUED_1:def 4;
  then
A5: Z c= dom ln by XBOOLE_1:18;
A6: for x st x in Z holds x > 0
  proof
    let x;
    assume x in Z;
    then x in right_open_halfline(0) by A5,TAYLOR_1:18;
    then ex g being Real st x = g & 0 < g by A1;
    hence thesis;
  end;
  then for x st x in Z holds ln is_differentiable_in x by TAYLOR_1:18;
  then
A7: ln is_differentiable_on Z by A5,FDIFF_1:9;
A8: for x st x in Z holds diff(ln,x) = 1/x
  proof
    let x;
    assume x in Z;
    then x > 0 by A6;
    then x in right_open_halfline(0) by A1;
    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 A2,A7
,A4,FDIFF_1:21
      .= (arccot.x)*(1/x)+(ln.x)*diff(arccot,x) by A8,A9
      .= (arccot.x)*(1/x)+(ln.x)*((arccot)`|Z).x by A4,A9,FDIFF_1:def 7
      .= (arccot.x)*(1/x)+(ln.x)*(-1/(1+x^2)) by A3,A9,Th82
      .= arccot.x/x-ln.x/(1+x^2);
    hence thesis;
  end;
  hence thesis by A2,A7,A4,FDIFF_1:21;
end;

::f.x=1/x*arctan.x

theorem
  not 0 in Z & Z c= dom ((id Z)^(#)arctan) & 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^2)+1/(x*(1+x^2))
proof
  set f = id Z;
  assume that
A1: not 0 in Z and
A2: Z c= dom (f^(#)arctan) and
A3: Z c= ].-1,1.[;
A4: f^ is_differentiable_on Z by A1,FDIFF_5:4;
A5: arctan is_differentiable_on Z by A3,Th81;
  Z c= dom (f^) /\ dom arctan by A2,VALUED_1:def 4;
  then
A6: Z c= dom (f^) by XBOOLE_1:18;
  for x st x in Z holds ((f^(#)arctan)`|Z).x = -arctan.x/(x^2)+1/(x*(1+x^2 ))
  proof
    let x;
    assume
A7: x in Z;
    then ((f^(#)arctan)`|Z).x = (arctan.x)*diff(f^,x)+((f^).x)*diff(arctan,x)
    by A2,A4,A5,FDIFF_1:21
      .= (arctan.x)*((f^)`|Z).x+((f^).x)*diff(arctan,x) by A4,A7,FDIFF_1:def 7
      .= (arctan.x)*(-1/x^2)+((f^).x)*diff(arctan,x) by A1,A7,FDIFF_5:4
      .= -(arctan.x)*(1/x^2)+((f^).x)*((arctan)`|Z).x by A5,A7,FDIFF_1:def 7
      .= -((arctan.x)*1)/(x^2)+((f^).x)*(1/(1+x^2)) by A3,A7,Th81
      .= -arctan.x/(x^2)+(f.x)"*(1/(1+x^2)) by A6,A7,RFUNCT_1:def 2
      .= -arctan.x/(x^2)+(1/x)*(1/(1+x^2)) by A7,FUNCT_1:18
      .= -arctan.x/(x^2)+(1*1)/(x*(1+x^2)) by XCMPLX_1:76
      .= -arctan.x/(x^2)+1/(x*(1+x^2));
    hence thesis;
  end;
  hence thesis by A2,A4,A5,FDIFF_1:21;
end;

::f.x=1/x*arccot.x

theorem
  not 0 in Z & Z c= dom ((id Z)^(#)arccot) & 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^2)-1/(x*(1+x^2))
proof
  set f = id Z;
  assume that
A1: not 0 in Z and
A2: Z c= dom (f^(#)arccot) and
A3: Z c= ].-1,1.[;
A4: f^ is_differentiable_on Z by A1,FDIFF_5:4;
A5: arccot is_differentiable_on Z by A3,Th82;
  Z c= dom (f^) /\ dom arccot by A2,VALUED_1:def 4;
  then
A6: Z c= dom (f^) by XBOOLE_1:18;
  for x st x in Z holds ((f^(#)arccot)`|Z).x = -arccot.x/(x^2)-1/(x*(1+x^2 ))
  proof
    let x;
    assume
A7: x in Z;
    then ((f^(#)arccot)`|Z).x = (arccot.x)*diff(f^,x)+((f^).x)*diff(arccot,x)
    by A2,A4,A5,FDIFF_1:21
      .= (arccot.x)*((f^)`|Z).x+((f^).x)*diff(arccot,x) by A4,A7,FDIFF_1:def 7
      .= (arccot.x)*(-1/x^2)+((f^).x)*diff(arccot,x) by A1,A7,FDIFF_5:4
      .= -(arccot.x)*(1/x^2)+((f^).x)*((arccot)`|Z).x by A5,A7,FDIFF_1:def 7
      .= -(arccot.x)*(1/x^2)+((f^).x)*(-1/(1+x^2)) by A3,A7,Th82
      .= -((arccot.x)*1)/(x^2)-((f^).x)*(1/(1+x^2))
      .= -arccot.x/(x^2)-(f.x)"*(1/(1+x^2)) by A6,A7,RFUNCT_1:def 2
      .= -arccot.x/(x^2)-(1/x)*(1/(1+x^2)) by A7,FUNCT_1:18
      .= -arccot.x/(x^2)-(1*1)/(x*(1+x^2)) by XCMPLX_1:76
      .= -arccot.x/(x^2)-1/(x*(1+x^2));
    hence thesis;
  end;
  hence thesis by A2,A4,A5,FDIFF_1:21;
end;