:: Several Differentiation Formulas of Special Functions -- Part {VII}
::  by Fuguo Ge and Bing Xie
::
:: Received September 23, 2008
:: Copyright (c) 2008-2012 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, REAL_1, SUBSET_1, RCOMP_1, PARTFUN1, TARSKI, RELAT_1,
      SIN_COS9, SIN_COS, FUNCT_1, XXREAL_0, ARYTM_1, ARYTM_3, FDIFF_1,
      SQUARE_1, CARD_1, XXREAL_1, SIN_COS4, VALUED_1, XBOOLE_0, ORDINAL4,
      PREPOWER;
 notations TARSKI, SUBSET_1, XXREAL_0, RELSET_1, PARTFUN1, RCOMP_1, SIN_COS,
      RFUNCT_1, SQUARE_1, VALUED_1, NUMBERS, REAL_1, SEQ_1, FDIFF_1, PARTFUN2,
      TAYLOR_1, PREPOWER, FDIFF_9, SIN_COS9;
 constructors REAL_1, SQUARE_1, RCOMP_1, RFUNCT_1, FDIFF_1, SIN_COS, PARTFUN2,
      TOPALG_2, TAYLOR_1, PREPOWER, LIMFUNC1, SEQ_1, FDIFF_9, SIN_COS9;
 registrations XCMPLX_0, XXREAL_0, XREAL_0, MEMBERED, RCOMP_1, RELSET_1,
      SIN_COS6, NUMBERS, INT_1, VALUED_0;
 requirements SUBSET, BOOLE, NUMERALS, ARITHM, REAL;
 definitions XCMPLX_0, SIN_COS, SQUARE_1, FDIFF_9, SUBSET_1;
 theorems FDIFF_2, XCMPLX_1, FDIFF_1, RELAT_1, SIN_COS, FUNCT_1, SQUARE_1,
      XREAL_1, TARSKI, XBOOLE_1, FDIFF_7, RFUNCT_1, TAYLOR_1, PREPOWER,
      VALUED_1, FDIFF_9, SIN_COS9, FDIFF_8, XXREAL_1;

begin

reserve x for Real,

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

     g for PartFunc of REAL,REAL;

::f.x=arctan.(sin.x)

theorem
  Z c= dom (arctan*sin) & (for x st x in Z holds sin.x > -1 & sin.x < 1)
implies arctan*sin is_differentiable_on Z & for x st x in Z holds ((arctan*sin)
  `|Z).x = cos.x/(1+(sin.x)^2)
proof
  assume that
A1: Z c= dom (arctan*sin) and
A2: for x st x in Z holds sin.x > -1 & sin.x < 1;
A3: for x st x in Z holds arctan*sin is_differentiable_in x
  proof
    let x;
    assume x in Z;
    then
A4: sin.x > -1 & sin.x < 1 by A2;
    sin is_differentiable_in x by SIN_COS:64;
    hence thesis by A4,SIN_COS9:85;
  end;
  then
A5: arctan*sin is_differentiable_on Z by A1,FDIFF_1:9;
  for x st x in Z holds ((arctan*sin)`|Z).x = cos.x/(1+(sin.x)^2)
  proof
    let x;
A6: sin is_differentiable_in x by SIN_COS:64;
    assume
A7: x in Z;
    then
A8: sin.x > -1 & sin.x < 1 by A2;
    ((arctan*sin)`|Z).x = diff(arctan*sin,x) by A5,A7,FDIFF_1:def 7
      .= diff(sin,x)/(1+(sin.x)^2) by A6,A8,SIN_COS9:85
      .= cos.x/(1+(sin.x)^2) by SIN_COS:64;
    hence thesis;
  end;
  hence thesis by A1,A3,FDIFF_1:9;
end;

::f.x=arccot.(sin.x)

theorem
  Z c= dom (arccot*sin) & (for x st x in Z holds sin.x > -1 & sin.x < 1)
implies arccot*sin is_differentiable_on Z & for x st x in Z holds ((arccot*sin)
  `|Z).x = -cos.x/(1+(sin.x)^2)
proof
  assume that
A1: Z c= dom (arccot*sin) and
A2: for x st x in Z holds sin.x > -1 & sin.x < 1;
A3: for x st x in Z holds arccot*sin is_differentiable_in x
  proof
    let x;
    assume x in Z;
    then
A4: sin.x > -1 & sin.x < 1 by A2;
    sin is_differentiable_in x by SIN_COS:64;
    hence thesis by A4,SIN_COS9:86;
  end;
  then
A5: arccot*sin is_differentiable_on Z by A1,FDIFF_1:9;
  for x st x in Z holds ((arccot*sin)`|Z).x = -cos.x/(1+(sin.x)^2)
  proof
    let x;
A6: sin is_differentiable_in x by SIN_COS:64;
    assume
A7: x in Z;
    then
A8: sin.x > -1 & sin.x < 1 by A2;
    ((arccot*sin)`|Z).x = diff(arccot*sin,x) by A5,A7,FDIFF_1:def 7
      .= -diff(sin,x)/(1+(sin.x)^2) by A6,A8,SIN_COS9:86
      .= -cos.x/(1+(sin.x)^2) by SIN_COS:64;
    hence thesis;
  end;
  hence thesis by A1,A3,FDIFF_1:9;
end;

::f.x=arctan.(cos.x)

theorem
  Z c= dom (arctan*cos) & (for x st x in Z holds cos.x > -1 & cos.x < 1)
implies arctan*cos is_differentiable_on Z & for x st x in Z holds ((arctan*cos)
  `|Z).x = -sin.x/(1+(cos.x)^2)
proof
  assume that
A1: Z c= dom (arctan*cos) and
A2: for x st x in Z holds cos.x > -1 & cos.x < 1;
A3: for x st x in Z holds arctan*cos is_differentiable_in x
  proof
    let x;
    assume x in Z;
    then
A4: cos.x > -1 & cos.x < 1 by A2;
    cos is_differentiable_in x by SIN_COS:63;
    hence thesis by A4,SIN_COS9:85;
  end;
  then
A5: arctan*cos is_differentiable_on Z by A1,FDIFF_1:9;
  for x st x in Z holds ((arctan*cos)`|Z).x = -sin.x/(1+(cos.x)^2)
  proof
    let x;
A6: cos is_differentiable_in x by SIN_COS:63;
    assume
A7: x in Z;
    then
A8: cos.x > -1 & cos.x < 1 by A2;
    ((arctan*cos)`|Z).x = diff(arctan*cos,x) by A5,A7,FDIFF_1:def 7
      .= diff(cos,x)/(1+(cos.x)^2) by A6,A8,SIN_COS9:85
      .= (-sin.x)/(1+(cos.x)^2) by SIN_COS:63
      .= -sin.x/(1+(cos.x)^2);
    hence thesis;
  end;
  hence thesis by A1,A3,FDIFF_1:9;
end;

::f.x=arccot.(cos.x)

theorem
  Z c= dom (arccot*cos) & (for x st x in Z holds cos.x > -1 & cos.x < 1)
implies arccot*cos is_differentiable_on Z & for x st x in Z holds ((arccot*cos)
  `|Z).x = sin.x/(1+(cos.x)^2)
proof
  assume that
A1: Z c= dom (arccot*cos) and
A2: for x st x in Z holds cos.x > -1 & cos.x < 1;
A3: for x st x in Z holds arccot*cos is_differentiable_in x
  proof
    let x;
    assume x in Z;
    then
A4: cos.x > -1 & cos.x < 1 by A2;
    cos is_differentiable_in x by SIN_COS:63;
    hence thesis by A4,SIN_COS9:86;
  end;
  then
A5: arccot*cos is_differentiable_on Z by A1,FDIFF_1:9;
  for x st x in Z holds ((arccot*cos)`|Z).x = sin.x/(1+(cos.x)^2)
  proof
    let x;
A6: cos is_differentiable_in x by SIN_COS:63;
    assume
A7: x in Z;
    then
A8: cos.x > -1 & cos.x < 1 by A2;
    ((arccot*cos)`|Z).x = diff(arccot*cos,x) by A5,A7,FDIFF_1:def 7
      .= -diff(cos,x)/(1+(cos.x)^2) by A6,A8,SIN_COS9:86
      .= -(-sin.x)/(1+(cos.x)^2) by SIN_COS:63
      .= sin.x/(1+(cos.x)^2);
    hence thesis;
  end;
  hence thesis by A1,A3,FDIFF_1:9;
end;

::f.x=arctan.(tan.x)

theorem
  Z c= dom (arctan*tan) & (for x st x in Z holds tan.x > -1 & tan.x < 1)
implies arctan*tan is_differentiable_on Z & for x st x in Z holds ((arctan*tan)
  `|Z).x = 1
proof
  assume that
A1: Z c= dom (arctan*tan) and
A2: for x st x in Z holds tan.x > -1 & tan.x < 1;
  dom (arctan*tan) c= dom tan by RELAT_1:25;
  then
A3: Z c= dom tan by A1,XBOOLE_1:1;
A4: for x st x in Z holds arctan*tan is_differentiable_in x
  proof
    let x;
    assume
A5: x in Z;
    then cos.x <> 0 by A3,FDIFF_8:1;
    then
A6: tan is_differentiable_in x by FDIFF_7:46;
    tan.x > -1 & tan.x < 1 by A2,A5;
    hence thesis by A6,SIN_COS9:85;
  end;
  then
A7: arctan*tan is_differentiable_on Z by A1,FDIFF_1:9;
  for x st x in Z holds ((arctan*tan)`|Z).x = 1
  proof
    let x;
    assume
A8: x in Z;
    then
A9: tan.x > -1 & tan.x < 1 by A2;
A10: tan.x = sin.x/cos.x by A3,A8,RFUNCT_1:def 1;
A11: cos.x <> 0 by A3,A8,FDIFF_8:1;
    then
A12: tan is_differentiable_in x by FDIFF_7:46;
A13: (cos.x)^2 <> 0 by A11,SQUARE_1:12;
    ((arctan*tan)`|Z).x = diff(arctan*tan,x) by A7,A8,FDIFF_1:def 7
      .= diff(tan,x)/(1+(tan.x)^2) by A12,A9,SIN_COS9:85
      .= (1/(cos.x)^2)/(1+(tan.x)^2) by A11,FDIFF_7:46
      .= 1/((cos.x)^2*(1+(sin.x/cos.x)*(sin.x/cos.x))) by A10,XCMPLX_1:78
      .= 1/((cos.x)^2*(1+(sin.x)^2/(cos.x)^2)) by XCMPLX_1:76
      .= 1/((cos.x)^2+((cos.x)^2*(sin.x)^2)/(cos.x)^2)
      .= 1/((cos.x)^2+(sin.x)^2) by A13,XCMPLX_1:89
      .= 1/1 by SIN_COS:28
      .= 1;
    hence thesis;
  end;
  hence thesis by A1,A4,FDIFF_1:9;
end;

::f.x=arccot.(tan.x)

theorem
  Z c= dom (arccot*tan) & (for x st x in Z holds tan.x > -1 & tan.x < 1)
implies arccot*tan is_differentiable_on Z & for x st x in Z holds ((arccot*tan)
  `|Z).x = -1
proof
  assume that
A1: Z c= dom (arccot*tan) and
A2: for x st x in Z holds tan.x > -1 & tan.x < 1;
  dom (arccot*tan) c= dom tan by RELAT_1:25;
  then
A3: Z c= dom tan by A1,XBOOLE_1:1;
A4: for x st x in Z holds arccot*tan is_differentiable_in x
  proof
    let x;
    assume
A5: x in Z;
    then cos.x <> 0 by A3,FDIFF_8:1;
    then
A6: tan is_differentiable_in x by FDIFF_7:46;
    tan.x > -1 & tan.x < 1 by A2,A5;
    hence thesis by A6,SIN_COS9:86;
  end;
  then
A7: arccot*tan is_differentiable_on Z by A1,FDIFF_1:9;
  for x st x in Z holds ((arccot*tan)`|Z).x = -1
  proof
    let x;
    assume
A8: x in Z;
    then
A9: tan.x > -1 & tan.x < 1 by A2;
A10: tan.x = sin.x/cos.x by A3,A8,RFUNCT_1:def 1;
A11: cos.x <> 0 by A3,A8,FDIFF_8:1;
    then
A12: tan is_differentiable_in x by FDIFF_7:46;
A13: (cos.x)^2 <> 0 by A11,SQUARE_1:12;
    ((arccot*tan)`|Z).x = diff(arccot*tan,x) by A7,A8,FDIFF_1:def 7
      .= -diff(tan,x)/(1+(tan.x)^2) by A12,A9,SIN_COS9:86
      .= -(1/(cos.x)^2)/(1+(tan.x)^2) by A11,FDIFF_7:46
      .= -1/((cos.x)^2*(1+(sin.x/cos.x)*(sin.x/cos.x))) by A10,XCMPLX_1:78
      .= -1/((cos.x)^2*(1+(sin.x)^2/(cos.x)^2)) by XCMPLX_1:76
      .= -1/((cos.x)^2+((cos.x)^2*(sin.x)^2)/(cos.x)^2)
      .= -1/((cos.x)^2+(sin.x)^2) by A13,XCMPLX_1:89
      .= -1/1 by SIN_COS:28
      .= -1;
    hence thesis;
  end;
  hence thesis by A1,A4,FDIFF_1:9;
end;

::f.x=arctan.(cot.x)

theorem
  Z c= dom (arctan*cot) & (for x st x in Z holds cot.x > -1 & cot.x < 1)
implies arctan*cot is_differentiable_on Z & for x st x in Z holds ((arctan*cot)
  `|Z).x = -1
proof
  assume that
A1: Z c= dom (arctan*cot) and
A2: for x st x in Z holds cot.x > -1 & cot.x < 1;
  dom (arctan*cot) c= dom cot by RELAT_1:25;
  then
A3: Z c= dom cot by A1,XBOOLE_1:1;
A4: for x st x in Z holds arctan*cot is_differentiable_in x
  proof
    let x;
    assume
A5: x in Z;
    then sin.x <> 0 by A3,FDIFF_8:2;
    then
A6: cot is_differentiable_in x by FDIFF_7:47;
    cot.x > -1 & cot.x < 1 by A2,A5;
    hence thesis by A6,SIN_COS9:85;
  end;
  then
A7: arctan*cot is_differentiable_on Z by A1,FDIFF_1:9;
  for x st x in Z holds ((arctan*cot)`|Z).x = -1
  proof
    let x;
    assume
A8: x in Z;
    then
A9: cot.x > -1 & cot.x < 1 by A2;
A10: cot.x = cos.x/sin.x by A3,A8,RFUNCT_1:def 1;
A11: sin.x <> 0 by A3,A8,FDIFF_8:2;
    then
A12: cot is_differentiable_in x by FDIFF_7:47;
A13: (sin.x)^2 <> 0 by A11,SQUARE_1:12;
    ((arctan*cot)`|Z).x = diff(arctan*cot,x) by A7,A8,FDIFF_1:def 7
      .= diff(cot,x)/(1+(cot.x)^2) by A12,A9,SIN_COS9:85
      .= (-1/(sin.x)^2)/(1+(cot.x)^2) by A11,FDIFF_7:47
      .= -1/(sin.x)^2/(1+(cot.x)^2)
      .= -1/((sin.x)^2*(1+(cos.x/sin.x)*(cos.x/sin.x))) by A10,XCMPLX_1:78
      .= -1/((sin.x)^2*(1+(cos.x)^2/(sin.x)^2)) by XCMPLX_1:76
      .= -1/((sin.x)^2+((sin.x)^2*(cos.x)^2)/(sin.x)^2)
      .= -1/((sin.x)^2+(cos.x)^2) by A13,XCMPLX_1:89
      .= -1/1 by SIN_COS:28
      .= -1;
    hence thesis;
  end;
  hence thesis by A1,A4,FDIFF_1:9;
end;

::f.x=arccot.(cot.x)

theorem
  Z c= dom (arccot*cot) & (for x st x in Z holds cot.x > -1 & cot.x < 1)
implies arccot*cot is_differentiable_on Z & for x st x in Z holds ((arccot*cot)
  `|Z).x = 1
proof
  assume that
A1: Z c= dom (arccot*cot) and
A2: for x st x in Z holds cot.x > -1 & cot.x < 1;
  dom (arccot*cot) c= dom cot by RELAT_1:25;
  then
A3: Z c= dom cot by A1,XBOOLE_1:1;
A4: for x st x in Z holds arccot*cot is_differentiable_in x
  proof
    let x;
    assume
A5: x in Z;
    then sin.x <> 0 by A3,FDIFF_8:2;
    then
A6: cot is_differentiable_in x by FDIFF_7:47;
    cot.x > -1 & cot.x < 1 by A2,A5;
    hence thesis by A6,SIN_COS9:86;
  end;
  then
A7: arccot*cot is_differentiable_on Z by A1,FDIFF_1:9;
  for x st x in Z holds ((arccot*cot)`|Z).x = 1
  proof
    let x;
    assume
A8: x in Z;
    then
A9: cot.x > -1 & cot.x < 1 by A2;
A10: cot.x = cos.x/sin.x by A3,A8,RFUNCT_1:def 1;
A11: sin.x <> 0 by A3,A8,FDIFF_8:2;
    then
A12: cot is_differentiable_in x by FDIFF_7:47;
A13: (sin.x)^2 <> 0 by A11,SQUARE_1:12;
    ((arccot*cot)`|Z).x = diff(arccot*cot,x) by A7,A8,FDIFF_1:def 7
      .= -diff(cot,x)/(1+(cot.x)^2) by A12,A9,SIN_COS9:86
      .= -(-1/(sin.x)^2)/(1+(cot.x)^2) by A11,FDIFF_7:47
      .= 1/(sin.x)^2/(1+(cot.x)^2)
      .= 1/((sin.x)^2*(1+(cos.x/sin.x)*(cos.x/sin.x))) by A10,XCMPLX_1:78
      .= 1/((sin.x)^2*(1+(cos.x)^2/(sin.x)^2)) by XCMPLX_1:76
      .= 1/((sin.x)^2+((sin.x)^2*(cos.x)^2)/(sin.x)^2)
      .= 1/((sin.x)^2+(cos.x)^2) by A13,XCMPLX_1:89
      .= 1/1 by SIN_COS:28
      .= 1;
    hence thesis;
  end;
  hence thesis by A1,A4,FDIFF_1:9;
end;

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

theorem
  Z c= dom (arctan*arctan) & Z c= ].-1,1.[ & (for x st x in Z holds
  arctan.x > -1 & arctan.x < 1) implies arctan*arctan is_differentiable_on Z &
  for x st x in Z holds ((arctan*arctan)`|Z).x = 1/((1+x^2)*(1+(arctan.x)^2))
proof
  assume that
A1: Z c= dom (arctan*arctan) and
A2: Z c= ].-1,1.[ and
A3: for x st x in Z holds arctan.x > -1 & arctan.x < 1;
A4: for x st x in Z holds arctan*arctan is_differentiable_in x
  proof
    let x;
    assume
A5: x in Z;
    then
A6: arctan.x > -1 & arctan.x < 1 by A3;
    arctan is_differentiable_on Z by A2,SIN_COS9:81;
    then arctan is_differentiable_in x by A5,FDIFF_1:9;
    hence thesis by A6,SIN_COS9:85;
  end;
  then
A7: arctan*arctan is_differentiable_on Z by A1,FDIFF_1:9;
  for x st x in Z holds ((arctan*arctan)`|Z).x = 1/((1+x^2)*(1+(arctan.x) ^2))
  proof
    let x;
    assume
A8: x in Z;
    then
A9: arctan.x > -1 & arctan.x < 1 by A3;
A10: arctan is_differentiable_on Z by A2,SIN_COS9:81;
    then
A11: arctan is_differentiable_in x by A8,FDIFF_1:9;
    ((arctan*arctan)`|Z).x = diff(arctan*arctan,x) by A7,A8,FDIFF_1:def 7
      .= diff(arctan,x)/(1+(arctan.x)^2) by A11,A9,SIN_COS9:85
      .= ((arctan)`|Z).x/(1+(arctan.x)^2) by A8,A10,FDIFF_1:def 7
      .= (1/(1+x^2))/(1+(arctan.x)^2) by A2,A8,SIN_COS9:81
      .= 1/((1+x^2)*(1+(arctan.x)^2)) by XCMPLX_1:78;
    hence thesis;
  end;
  hence thesis by A1,A4,FDIFF_1:9;
end;

::f.x=arccot.(arctan.x)

theorem
  Z c= dom (arccot*arctan) & Z c= ].-1,1.[ & (for x st x in Z holds
  arctan.x > -1 & arctan.x < 1) implies arccot*arctan is_differentiable_on Z &
  for x st x in Z holds ((arccot*arctan)`|Z).x = -1/((1+x^2)*(1+(arctan.x)^2))
proof
  assume that
A1: Z c= dom (arccot*arctan) and
A2: Z c= ].-1,1.[ and
A3: for x st x in Z holds arctan.x > -1 & arctan.x < 1;
A4: for x st x in Z holds arccot*arctan is_differentiable_in x
  proof
    let x;
    assume
A5: x in Z;
    then
A6: arctan.x > -1 & arctan.x < 1 by A3;
    arctan is_differentiable_on Z by A2,SIN_COS9:81;
    then arctan is_differentiable_in x by A5,FDIFF_1:9;
    hence thesis by A6,SIN_COS9:86;
  end;
  then
A7: arccot*arctan is_differentiable_on Z by A1,FDIFF_1:9;
  for x st x in Z holds ((arccot*arctan)`|Z).x = -1/((1+x^2)*(1+(arctan.x )^2))
  proof
    let x;
    assume
A8: x in Z;
    then
A9: arctan.x > -1 & arctan.x < 1 by A3;
A10: arctan is_differentiable_on Z by A2,SIN_COS9:81;
    then
A11: arctan is_differentiable_in x by A8,FDIFF_1:9;
    ((arccot*arctan)`|Z).x = diff(arccot*arctan,x) by A7,A8,FDIFF_1:def 7
      .= -diff(arctan,x)/(1+(arctan.x)^2) by A11,A9,SIN_COS9:86
      .= -((arctan)`|Z).x/(1+(arctan.x)^2) by A8,A10,FDIFF_1:def 7
      .= -(1/(1+x^2))/(1+(arctan.x)^2) by A2,A8,SIN_COS9:81
      .= -1/((1+x^2)*(1+(arctan.x)^2)) by XCMPLX_1:78;
    hence thesis;
  end;
  hence thesis by A1,A4,FDIFF_1:9;
end;

::f.x=arctan.(arccot.x)

theorem
  Z c= dom (arctan*arccot) & Z c= ].-1,1.[ & (for x st x in Z holds
  arccot.x > -1 & arccot.x < 1) implies arctan*arccot is_differentiable_on Z &
  for x st x in Z holds ((arctan*arccot)`|Z).x = -1/((1+x^2)*(1+(arccot.x)^2))
proof
  assume that
A1: Z c= dom (arctan*arccot) and
A2: Z c= ].-1,1.[ and
A3: for x st x in Z holds arccot.x > -1 & arccot.x < 1;
A4: for x st x in Z holds arctan*arccot is_differentiable_in x
  proof
    let x;
    assume
A5: x in Z;
    then
A6: arccot.x > -1 & arccot.x < 1 by A3;
    arccot is_differentiable_on Z by A2,SIN_COS9:82;
    then arccot is_differentiable_in x by A5,FDIFF_1:9;
    hence thesis by A6,SIN_COS9:85;
  end;
  then
A7: arctan*arccot is_differentiable_on Z by A1,FDIFF_1:9;
  for x st x in Z holds ((arctan*arccot)`|Z).x = -1/((1+x^2)*(1+(arccot.x )^2))
  proof
    let x;
    assume
A8: x in Z;
    then
A9: arccot.x > -1 & arccot.x < 1 by A3;
A10: arccot is_differentiable_on Z by A2,SIN_COS9:82;
    then
A11: arccot is_differentiable_in x by A8,FDIFF_1:9;
    ((arctan*arccot)`|Z).x = diff(arctan*arccot,x) by A7,A8,FDIFF_1:def 7
      .= diff(arccot,x)/(1+(arccot.x)^2) by A11,A9,SIN_COS9:85
      .= ((arccot)`|Z).x/(1+(arccot.x)^2) by A8,A10,FDIFF_1:def 7
      .= (-1/(1+x^2))/(1+(arccot.x)^2) by A2,A8,SIN_COS9:82
      .= -1/(1+x^2)/(1+(arccot.x)^2)
      .= -1/((1+x^2)*(1+(arccot.x)^2)) by XCMPLX_1:78;
    hence thesis;
  end;
  hence thesis by A1,A4,FDIFF_1:9;
end;

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

theorem
  Z c= dom (arccot*arccot) & Z c= ].-1,1.[ & (for x st x in Z holds
  arccot.x > -1 & arccot.x < 1) implies arccot*arccot is_differentiable_on Z &
  for x st x in Z holds ((arccot*arccot)`|Z).x = 1/((1+x^2)*(1+(arccot.x)^2))
proof
  assume that
A1: Z c= dom (arccot*arccot) and
A2: Z c= ].-1,1.[ and
A3: for x st x in Z holds arccot.x > -1 & arccot.x < 1;
A4: for x st x in Z holds arccot*arccot is_differentiable_in x
  proof
    let x;
    assume
A5: x in Z;
    then
A6: arccot.x > -1 & arccot.x < 1 by A3;
    arccot is_differentiable_on Z by A2,SIN_COS9:82;
    then arccot is_differentiable_in x by A5,FDIFF_1:9;
    hence thesis by A6,SIN_COS9:86;
  end;
  then
A7: arccot*arccot is_differentiable_on Z by A1,FDIFF_1:9;
  for x st x in Z holds ((arccot*arccot)`|Z).x = 1/((1+x^2)*(1+(arccot.x) ^2))
  proof
    let x;
    assume
A8: x in Z;
    then
A9: arccot.x > -1 & arccot.x < 1 by A3;
A10: arccot is_differentiable_on Z by A2,SIN_COS9:82;
    then
A11: arccot is_differentiable_in x by A8,FDIFF_1:9;
    ((arccot*arccot)`|Z).x = diff(arccot*arccot,x) by A7,A8,FDIFF_1:def 7
      .= -diff(arccot,x)/(1+(arccot.x)^2) by A11,A9,SIN_COS9:86
      .= -((arccot)`|Z).x/(1+(arccot.x)^2) by A8,A10,FDIFF_1:def 7
      .= -(-1/(1+x^2))/(1+(arccot.x)^2) by A2,A8,SIN_COS9:82
      .= 1/(1+x^2)/(1+(arccot.x)^2)
      .= 1/((1+x^2)*(1+(arccot.x)^2)) by XCMPLX_1:78;
    hence thesis;
  end;
  hence thesis by A1,A4,FDIFF_1:9;
end;

::f.x=sin.(arctan.x)

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

::f.x=sin.(arccot.x)

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

::f.x=cos.(arctan.x)

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

::f.x=cos.(arccot.x)

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

::f.x=tan.(arctan.x)

theorem
  Z c= dom (tan*arctan) & Z c= ].-1,1.[ implies tan*arctan
is_differentiable_on Z & for x st x in Z holds ((tan*arctan)`|Z).x = 1/((cos.(
  arctan.x))^2*(1+x^2))
proof
  assume that
A1: Z c= dom (tan*arctan) and
A2: Z c= ].-1,1.[;
A3: for x st x in Z holds tan*arctan is_differentiable_in x
  proof
    let x;
    assume
A4: x in Z;
    then arctan.x in dom tan by A1,FUNCT_1:11;
    then cos.(arctan.x) <> 0 by FDIFF_8:1;
    then
A5: tan is_differentiable_in arctan.x by FDIFF_7:46;
    arctan is_differentiable_on Z by A2,SIN_COS9:81;
    then arctan is_differentiable_in x by A4,FDIFF_1:9;
    hence thesis by A5,FDIFF_2:13;
  end;
  then
A6: tan*arctan is_differentiable_on Z by A1,FDIFF_1:9;
  for x st x in Z holds ((tan*arctan)`|Z).x = 1/((cos.(arctan.x))^2*(1+x ^2))
  proof
    let x;
    assume
A7: x in Z;
    then arctan.x in dom tan by A1,FUNCT_1:11;
    then
A8: cos.(arctan.x) <> 0 by FDIFF_8:1;
    then
A9: tan is_differentiable_in arctan.x by FDIFF_7:46;
A10: arctan is_differentiable_on Z by A2,SIN_COS9:81;
    then
A11: arctan is_differentiable_in x by A7,FDIFF_1:9;
    ((tan*arctan)`|Z).x = diff(tan*arctan,x) by A6,A7,FDIFF_1:def 7
      .= diff(tan,arctan.x)*diff(arctan,x) by A11,A9,FDIFF_2:13
      .= (1/(cos.(arctan.x))^2)*diff(arctan,x) by A8,FDIFF_7:46
      .= (1/(cos.(arctan.x))^2)*((arctan)`|Z).x by A7,A10,FDIFF_1:def 7
      .= (1/(cos.(arctan.x))^2)*(1/(1+x^2)) by A2,A7,SIN_COS9:81
      .= 1/((cos.(arctan.x))^2*(1+x^2)) by XCMPLX_1:102;
    hence thesis;
  end;
  hence thesis by A1,A3,FDIFF_1:9;
end;

::f.x=tan.(arccot.x)

theorem
  Z c= dom (tan*arccot) & Z c= ].-1,1.[ implies tan*arccot
is_differentiable_on Z & for x st x in Z holds ((tan*arccot)`|Z).x = -1/((cos.(
  arccot.x))^2*(1+x^2))
proof
  assume that
A1: Z c= dom (tan*arccot) and
A2: Z c= ].-1,1.[;
A3: for x st x in Z holds tan*arccot is_differentiable_in x
  proof
    let x;
    assume
A4: x in Z;
    then arccot.x in dom tan by A1,FUNCT_1:11;
    then cos.(arccot.x) <> 0 by FDIFF_8:1;
    then
A5: tan is_differentiable_in arccot.x by FDIFF_7:46;
    arccot is_differentiable_on Z by A2,SIN_COS9:82;
    then arccot is_differentiable_in x by A4,FDIFF_1:9;
    hence thesis by A5,FDIFF_2:13;
  end;
  then
A6: tan*arccot is_differentiable_on Z by A1,FDIFF_1:9;
  for x st x in Z holds ((tan*arccot)`|Z).x = -1/((cos.(arccot.x))^2*(1+x ^2))
  proof
    let x;
    assume
A7: x in Z;
    then arccot.x in dom tan by A1,FUNCT_1:11;
    then
A8: cos.(arccot.x) <> 0 by FDIFF_8:1;
    then
A9: tan is_differentiable_in arccot.x by FDIFF_7:46;
A10: arccot is_differentiable_on Z by A2,SIN_COS9:82;
    then
A11: arccot is_differentiable_in x by A7,FDIFF_1:9;
    ((tan*arccot)`|Z).x = diff(tan*arccot,x) by A6,A7,FDIFF_1:def 7
      .= diff(tan,arccot.x)*diff(arccot,x) by A11,A9,FDIFF_2:13
      .= (1/(cos.(arccot.x))^2)*diff(arccot,x) by A8,FDIFF_7:46
      .= (1/(cos.(arccot.x))^2)*((arccot)`|Z).x by A7,A10,FDIFF_1:def 7
      .= (1/(cos.(arccot.x))^2)*(-1/(1+x^2)) by A2,A7,SIN_COS9:82
      .= -(1/(cos.(arccot.x))^2)*(1/(1+x^2))
      .= -1/((cos.(arccot.x))^2*(1+x^2)) by XCMPLX_1:102;
    hence thesis;
  end;
  hence thesis by A1,A3,FDIFF_1:9;
end;

::f.x=cot.(arctan.x)

theorem
  Z c= dom (cot*arctan) & Z c= ].-1,1.[ implies cot*arctan
is_differentiable_on Z & for x st x in Z holds ((cot*arctan)`|Z).x = -1/((sin.(
  arctan.x))^2*(1+x^2))
proof
  assume that
A1: Z c= dom (cot*arctan) and
A2: Z c= ].-1,1.[;
A3: for x st x in Z holds cot*arctan is_differentiable_in x
  proof
    let x;
    assume
A4: x in Z;
    then arctan.x in dom cot by A1,FUNCT_1:11;
    then sin.(arctan.x) <> 0 by FDIFF_8:2;
    then
A5: cot is_differentiable_in arctan.x by FDIFF_7:47;
    arctan is_differentiable_on Z by A2,SIN_COS9:81;
    then arctan is_differentiable_in x by A4,FDIFF_1:9;
    hence thesis by A5,FDIFF_2:13;
  end;
  then
A6: cot*arctan is_differentiable_on Z by A1,FDIFF_1:9;
  for x st x in Z holds ((cot*arctan)`|Z).x = -1/((sin.(arctan.x))^2*(1+x ^2))
  proof
    let x;
    assume
A7: x in Z;
    then arctan.x in dom cot by A1,FUNCT_1:11;
    then
A8: sin.(arctan.x) <> 0 by FDIFF_8:2;
    then
A9: cot is_differentiable_in arctan.x by FDIFF_7:47;
A10: arctan is_differentiable_on Z by A2,SIN_COS9:81;
    then
A11: arctan is_differentiable_in x by A7,FDIFF_1:9;
    ((cot*arctan)`|Z).x = diff(cot*arctan,x) by A6,A7,FDIFF_1:def 7
      .= diff(cot,arctan.x)*diff(arctan,x) by A11,A9,FDIFF_2:13
      .= (-1/(sin.(arctan.x))^2)*diff(arctan,x) by A8,FDIFF_7:47
      .= -(1/(sin.(arctan.x))^2)*diff(arctan,x)
      .= -(1/(sin.(arctan.x))^2)*((arctan)`|Z).x by A7,A10,FDIFF_1:def 7
      .= -(1/(sin.(arctan.x))^2)*(1/(1+x^2)) by A2,A7,SIN_COS9:81
      .= -1/((sin.(arctan.x))^2*(1+x^2)) by XCMPLX_1:102;
    hence thesis;
  end;
  hence thesis by A1,A3,FDIFF_1:9;
end;

::f.x=cot.(arccot.x)

theorem
  Z c= dom (cot*arccot) & Z c= ].-1,1.[ implies cot*arccot
is_differentiable_on Z & for x st x in Z holds ((cot*arccot)`|Z).x = 1/((sin.(
  arccot.x))^2*(1+x^2))
proof
  assume that
A1: Z c= dom (cot*arccot) and
A2: Z c= ].-1,1.[;
A3: for x st x in Z holds cot*arccot is_differentiable_in x
  proof
    let x;
    assume
A4: x in Z;
    then arccot.x in dom cot by A1,FUNCT_1:11;
    then sin.(arccot.x) <> 0 by FDIFF_8:2;
    then
A5: cot is_differentiable_in arccot.x by FDIFF_7:47;
    arccot is_differentiable_on Z by A2,SIN_COS9:82;
    then arccot is_differentiable_in x by A4,FDIFF_1:9;
    hence thesis by A5,FDIFF_2:13;
  end;
  then
A6: cot*arccot is_differentiable_on Z by A1,FDIFF_1:9;
  for x st x in Z holds ((cot*arccot)`|Z).x = 1/((sin.(arccot.x))^2*(1+x ^2))
  proof
    let x;
    assume
A7: x in Z;
    then arccot.x in dom cot by A1,FUNCT_1:11;
    then
A8: sin.(arccot.x) <> 0 by FDIFF_8:2;
    then
A9: cot is_differentiable_in arccot.x by FDIFF_7:47;
A10: arccot is_differentiable_on Z by A2,SIN_COS9:82;
    then
A11: arccot is_differentiable_in x by A7,FDIFF_1:9;
    ((cot*arccot)`|Z).x = diff(cot*arccot,x) by A6,A7,FDIFF_1:def 7
      .= diff(cot,arccot.x)*diff(arccot,x) by A11,A9,FDIFF_2:13
      .= (-1/(sin.(arccot.x))^2)*diff(arccot,x) by A8,FDIFF_7:47
      .= -(1/(sin.(arccot.x))^2)*diff(arccot,x)
      .= -(1/(sin.(arccot.x))^2)*((arccot)`|Z).x by A7,A10,FDIFF_1:def 7
      .= -(1/(sin.(arccot.x))^2)*(-1/(1+x^2)) by A2,A7,SIN_COS9:82
      .= (1/(sin.(arccot.x))^2)*(1/(1+x^2))
      .= 1/((sin.(arccot.x))^2*(1+x^2)) by XCMPLX_1:102;
    hence thesis;
  end;
  hence thesis by A1,A3,FDIFF_1:9;
end;

::f.x=sec.(arctan.x)

theorem
  Z c= dom (sec*arctan) & Z c= ].-1,1.[ implies sec*arctan
  is_differentiable_on Z & for x st x in Z holds ((sec*arctan)`|Z).x = sin.(
  arctan.x)/((cos.(arctan.x))^2*(1+x^2))
proof
  assume that
A1: Z c= dom (sec*arctan) and
A2: Z c= ].-1,1.[;
A3: for x st x in Z holds cos.(arctan.x) <> 0
  proof
    let x;
    assume x in Z;
    then arctan.x in dom sec by A1,FUNCT_1:11;
    hence thesis by RFUNCT_1:3;
  end;
A4: for x st x in Z holds sec*arctan is_differentiable_in x
  proof
    let x;
    assume
A5: x in Z;
    then cos.(arctan.x) <> 0 by A3;
    then
A6: sec is_differentiable_in arctan.x by FDIFF_9:1;
    arctan is_differentiable_on Z by A2,SIN_COS9:81;
    then arctan is_differentiable_in x by A5,FDIFF_1:9;
    hence thesis by A6,FDIFF_2:13;
  end;
  then
A7: sec*arctan is_differentiable_on Z by A1,FDIFF_1:9;
  for x st x in Z holds ((sec*arctan)`|Z).x = sin.(arctan.x)/((cos.(
  arctan.x))^2*(1+x^2))
  proof
    let x;
    assume
A8: x in Z;
    then
A9: cos.(arctan.x) <> 0 by A3;
    cos.(arctan.x) <> 0 by A3,A8;
    then
A10: sec is_differentiable_in arctan.x by FDIFF_9:1;
A11: arctan is_differentiable_on Z by A2,SIN_COS9:81;
    then
A12: arctan is_differentiable_in x by A8,FDIFF_1:9;
    ((sec*arctan)`|Z).x = diff(sec*arctan,x) by A7,A8,FDIFF_1:def 7
      .= diff(sec,arctan.x)*diff(arctan,x) by A12,A10,FDIFF_2:13
      .= (sin.(arctan.x)/(cos.(arctan.x))^2)*diff(arctan,x) by A9,FDIFF_9:1
      .= (sin.(arctan.x)/(cos.(arctan.x))^2)*((arctan)`|Z).x by A8,A11,
FDIFF_1:def 7
      .= (sin.(arctan.x)/(cos.(arctan.x))^2)*(1/(1+x^2)) by A2,A8,SIN_COS9:81
      .= (sin.(arctan.x)*1)/((cos.(arctan.x))^2*(1+x^2)) by XCMPLX_1:76
      .= sin.(arctan.x)/((cos.(arctan.x))^2*(1+x^2));
    hence thesis;
  end;
  hence thesis by A1,A4,FDIFF_1:9;
end;

::f.x=sec.(arccot.x)

theorem
  Z c= dom (sec*arccot) & Z c= ].-1,1.[ implies sec*arccot
  is_differentiable_on Z & for x st x in Z holds ((sec*arccot)`|Z).x = -sin.(
  arccot.x)/((cos.(arccot.x))^2*(1+x^2))
proof
  assume that
A1: Z c= dom (sec*arccot) and
A2: Z c= ].-1,1.[;
A3: for x st x in Z holds cos.(arccot.x) <> 0
  proof
    let x;
    assume x in Z;
    then arccot.x in dom sec by A1,FUNCT_1:11;
    hence thesis by RFUNCT_1:3;
  end;
A4: for x st x in Z holds sec*arccot is_differentiable_in x
  proof
    let x;
    assume
A5: x in Z;
    then cos.(arccot.x) <> 0 by A3;
    then
A6: sec is_differentiable_in arccot.x by FDIFF_9:1;
    arccot is_differentiable_on Z by A2,SIN_COS9:82;
    then arccot is_differentiable_in x by A5,FDIFF_1:9;
    hence thesis by A6,FDIFF_2:13;
  end;
  then
A7: sec*arccot is_differentiable_on Z by A1,FDIFF_1:9;
  for x st x in Z holds ((sec*arccot)`|Z).x = -sin.(arccot.x)/((cos.(
  arccot.x))^2*(1+x^2))
  proof
    let x;
    assume
A8: x in Z;
    then
A9: cos.(arccot.x) <> 0 by A3;
    cos.(arccot.x) <> 0 by A3,A8;
    then
A10: sec is_differentiable_in arccot.x by FDIFF_9:1;
A11: arccot is_differentiable_on Z by A2,SIN_COS9:82;
    then
A12: arccot is_differentiable_in x by A8,FDIFF_1:9;
    ((sec*arccot)`|Z).x = diff(sec*arccot,x) by A7,A8,FDIFF_1:def 7
      .= diff(sec,arccot.x)*diff(arccot,x) by A12,A10,FDIFF_2:13
      .= (sin.(arccot.x)/(cos.(arccot.x))^2)*diff(arccot,x) by A9,FDIFF_9:1
      .= (sin.(arccot.x)/(cos.(arccot.x))^2)*((arccot)`|Z).x by A8,A11,
FDIFF_1:def 7
      .= (sin.(arccot.x)/(cos.(arccot.x))^2)*(-1/(1+x^2)) by A2,A8,SIN_COS9:82
      .= -(sin.(arccot.x)/(cos.(arccot.x))^2)*(1/(1+x^2))
      .= -(sin.(arccot.x)*1)/((cos.(arccot.x))^2*(1+x^2)) by XCMPLX_1:76
      .= -sin.(arccot.x)/((cos.(arccot.x))^2*(1+x^2));
    hence thesis;
  end;
  hence thesis by A1,A4,FDIFF_1:9;
end;

::f.x=cosec.(arctan.x)

theorem
  Z c= dom (cosec*arctan) & Z c= ].-1,1.[ implies cosec*arctan
  is_differentiable_on Z & for x st x in Z holds ((cosec*arctan)`|Z).x = -cos.(
  arctan.x)/((sin.(arctan.x))^2*(1+x^2))
proof
  assume that
A1: Z c= dom (cosec*arctan) and
A2: Z c= ].-1,1.[;
A3: for x st x in Z holds sin.(arctan.x) <> 0
  proof
    let x;
    assume x in Z;
    then arctan.x in dom cosec by A1,FUNCT_1:11;
    hence thesis by RFUNCT_1:3;
  end;
A4: for x st x in Z holds cosec*arctan is_differentiable_in x
  proof
    let x;
    assume
A5: x in Z;
    then sin.(arctan.x) <> 0 by A3;
    then
A6: cosec is_differentiable_in arctan.x by FDIFF_9:2;
    arctan is_differentiable_on Z by A2,SIN_COS9:81;
    then arctan is_differentiable_in x by A5,FDIFF_1:9;
    hence thesis by A6,FDIFF_2:13;
  end;
  then
A7: cosec*arctan is_differentiable_on Z by A1,FDIFF_1:9;
  for x st x in Z holds ((cosec*arctan)`|Z).x = -cos.(arctan.x)/((sin.(
  arctan.x))^2*(1+x^2))
  proof
    let x;
    assume
A8: x in Z;
    then
A9: sin.(arctan.x) <> 0 by A3;
    sin.(arctan.x) <> 0 by A3,A8;
    then
A10: cosec is_differentiable_in arctan.x by FDIFF_9:2;
A11: arctan is_differentiable_on Z by A2,SIN_COS9:81;
    then
A12: arctan is_differentiable_in x by A8,FDIFF_1:9;
    ((cosec*arctan)`|Z).x = diff(cosec*arctan,x) by A7,A8,FDIFF_1:def 7
      .= diff(cosec,arctan.x)*diff(arctan,x) by A12,A10,FDIFF_2:13
      .= (-cos.(arctan.x)/(sin.(arctan.x))^2)*diff(arctan,x) by A9,FDIFF_9:2
      .= -(cos.(arctan.x)/(sin.(arctan.x))^2)*diff(arctan,x)
      .= -(cos.(arctan.x)/(sin.(arctan.x))^2)*((arctan)`|Z).x by A8,A11,
FDIFF_1:def 7
      .= -(cos.(arctan.x)/(sin.(arctan.x))^2)*(1/(1+x^2)) by A2,A8,SIN_COS9:81
      .= -(cos.(arctan.x)*1)/((sin.(arctan.x))^2*(1+x^2)) by XCMPLX_1:76
      .= -cos.(arctan.x)/((sin.(arctan.x))^2*(1+x^2));
    hence thesis;
  end;
  hence thesis by A1,A4,FDIFF_1:9;
end;

::f.x=cosec.(arccot.x)

theorem
  Z c= dom (cosec*arccot) & Z c= ].-1,1.[ implies cosec*arccot
  is_differentiable_on Z & for x st x in Z holds ((cosec*arccot)`|Z).x = cos.(
  arccot.x)/((sin.(arccot.x))^2*(1+x^2))
proof
  assume that
A1: Z c= dom (cosec*arccot) and
A2: Z c= ].-1,1.[;
A3: for x st x in Z holds sin.(arccot.x) <> 0
  proof
    let x;
    assume x in Z;
    then arccot.x in dom cosec by A1,FUNCT_1:11;
    hence thesis by RFUNCT_1:3;
  end;
A4: for x st x in Z holds cosec*arccot is_differentiable_in x
  proof
    let x;
    assume
A5: x in Z;
    then sin.(arccot.x) <> 0 by A3;
    then
A6: cosec is_differentiable_in arccot.x by FDIFF_9:2;
    arccot is_differentiable_on Z by A2,SIN_COS9:82;
    then arccot is_differentiable_in x by A5,FDIFF_1:9;
    hence thesis by A6,FDIFF_2:13;
  end;
  then
A7: cosec*arccot is_differentiable_on Z by A1,FDIFF_1:9;
  for x st x in Z holds ((cosec*arccot)`|Z).x = cos.(arccot.x)/((sin.(
  arccot.x))^2*(1+x^2))
  proof
    let x;
    assume
A8: x in Z;
    then
A9: sin.(arccot.x) <> 0 by A3;
    sin.(arccot.x) <> 0 by A3,A8;
    then
A10: cosec is_differentiable_in arccot.x by FDIFF_9:2;
A11: arccot is_differentiable_on Z by A2,SIN_COS9:82;
    then
A12: arccot is_differentiable_in x by A8,FDIFF_1:9;
    ((cosec*arccot)`|Z).x = diff(cosec*arccot,x) by A7,A8,FDIFF_1:def 7
      .= diff(cosec,arccot.x)*diff(arccot,x) by A12,A10,FDIFF_2:13
      .= (-cos.(arccot.x)/(sin.(arccot.x))^2)*diff(arccot,x) by A9,FDIFF_9:2
      .= -(cos.(arccot.x)/(sin.(arccot.x))^2)*diff(arccot,x)
      .= -(cos.(arccot.x)/(sin.(arccot.x))^2)*((arccot)`|Z).x by A8,A11,
FDIFF_1:def 7
      .= -(cos.(arccot.x)/(sin.(arccot.x))^2)*(-1/(1+x^2)) by A2,A8,SIN_COS9:82
      .= (cos.(arccot.x)/(sin.(arccot.x))^2)*(1/(1+x^2))
      .= (cos.(arccot.x)*1)/((sin.(arccot.x))^2*(1+x^2)) by XCMPLX_1:76
      .= cos.(arccot.x)/((sin.(arccot.x))^2*(1+x^2));
    hence thesis;
  end;
  hence thesis by A1,A4,FDIFF_1:9;
end;

::f.x=sin.x*arctan.x

theorem
  Z c= dom (sin(#)arctan) & Z c= ].-1,1.[ implies (sin(#)arctan)
  is_differentiable_on Z & for x st x in Z holds ((sin(#)arctan)`|Z).x = cos.x*
  arctan.x+sin.x/(1+x^2)
proof
  assume that
A1: Z c= dom (sin(#)arctan) and
A2: Z c= ].-1,1.[;
A3: arctan is_differentiable_on Z by A2,SIN_COS9:81;
A4: for x st x in Z holds sin is_differentiable_in x by SIN_COS:64;
  Z c= dom sin /\ dom arctan by A1,VALUED_1:def 4;
  then Z c= dom sin by XBOOLE_1:18;
  then
A5: sin is_differentiable_on Z by A4,FDIFF_1:9;
  for x st x in Z holds ((sin(#)arctan)`|Z).x = cos.x*arctan.x+sin.x/(1+x ^2)
  proof
    let x;
    assume
A6: x in Z;
    then
    ((sin(#)arctan)`|Z).x = (arctan.x)*diff(sin,x)+(sin.x)*diff(arctan,x)
    by A1,A5,A3,FDIFF_1:21
      .= (arctan.x)*(cos.x)+(sin.x)*diff(arctan,x) by SIN_COS:64
      .= cos.x*arctan.x+(sin.x)*((arctan)`|Z).x by A3,A6,FDIFF_1:def 7
      .= cos.x*arctan.x+(sin.x)*(1/(1+x^2)) by A2,A6,SIN_COS9:81
      .= cos.x*arctan.x+sin.x/(1+x^2);
    hence thesis;
  end;
  hence thesis by A1,A5,A3,FDIFF_1:21;
end;

::f.x=sin.x*arccot.x

theorem
  Z c= dom (sin(#)arccot) & Z c= ].-1,1.[ implies (sin(#)arccot)
  is_differentiable_on Z & for x st x in Z holds ((sin(#)arccot)`|Z).x = cos.x*
  arccot.x-sin.x/(1+x^2)
proof
  assume that
A1: Z c= dom (sin(#)arccot) and
A2: Z c= ].-1,1.[;
A3: arccot is_differentiable_on Z by A2,SIN_COS9:82;
A4: for x st x in Z holds sin is_differentiable_in x by SIN_COS:64;
  Z c= dom sin /\ dom arccot by A1,VALUED_1:def 4;
  then Z c= dom sin by XBOOLE_1:18;
  then
A5: sin is_differentiable_on Z by A4,FDIFF_1:9;
  for x st x in Z holds ((sin(#)arccot)`|Z).x = cos.x*arccot.x-sin.x/(1+x ^2)
  proof
    let x;
    assume
A6: x in Z;
    then
    ((sin(#)arccot)`|Z).x = (arccot.x)*diff(sin,x)+(sin.x)*diff(arccot,x)
    by A1,A5,A3,FDIFF_1:21
      .= (arccot.x)*(cos.x)+(sin.x)*diff(arccot,x) by SIN_COS:64
      .= cos.x*arccot.x+(sin.x)*((arccot)`|Z).x by A3,A6,FDIFF_1:def 7
      .= cos.x*arccot.x+(sin.x)*(-1/(1+x^2)) by A2,A6,SIN_COS9:82
      .= cos.x*arccot.x-sin.x/(1+x^2);
    hence thesis;
  end;
  hence thesis by A1,A5,A3,FDIFF_1:21;
end;

::f.x=cos.x*arctan.x

theorem
  Z c= dom (cos(#)arctan) & Z c= ].-1,1.[ implies (cos(#)arctan)
is_differentiable_on Z & for x st x in Z holds ((cos(#)arctan)`|Z).x = -sin.x*
  arctan.x+cos.x/(1+x^2)
proof
  assume that
A1: Z c= dom (cos(#)arctan) and
A2: Z c= ].-1,1.[;
A3: arctan is_differentiable_on Z by A2,SIN_COS9:81;
A4: for x st x in Z holds cos is_differentiable_in x by SIN_COS:63;
  Z c= dom cos /\ dom arctan by A1,VALUED_1:def 4;
  then Z c= dom cos by XBOOLE_1:18;
  then
A5: cos is_differentiable_on Z by A4,FDIFF_1:9;
  for x st x in Z holds ((cos(#)arctan)`|Z).x = -sin.x*arctan.x+cos.x/(1+x ^2)
  proof
    let x;
    assume
A6: x in Z;
    then
    ((cos(#)arctan)`|Z).x = (arctan.x)*diff(cos,x)+(cos.x)*diff(arctan,x)
    by A1,A5,A3,FDIFF_1:21
      .= (arctan.x)*(-sin.x)+(cos.x)*diff(arctan,x) by SIN_COS:63
      .= -sin.x*arctan.x+(cos.x)*((arctan)`|Z).x by A3,A6,FDIFF_1:def 7
      .= -sin.x*arctan.x+(cos.x)*(1/(1+x^2)) by A2,A6,SIN_COS9:81
      .= -sin.x*arctan.x+cos.x/(1+x^2);
    hence thesis;
  end;
  hence thesis by A1,A5,A3,FDIFF_1:21;
end;

::f.x=cos.x*arccot.x

theorem
  Z c= dom (cos(#)arccot) & Z c= ].-1,1.[ implies (cos(#)arccot)
is_differentiable_on Z & for x st x in Z holds ((cos(#)arccot)`|Z).x = -sin.x*
  arccot.x-cos.x/(1+x^2)
proof
  assume that
A1: Z c= dom (cos(#)arccot) and
A2: Z c= ].-1,1.[;
A3: arccot is_differentiable_on Z by A2,SIN_COS9:82;
A4: for x st x in Z holds cos is_differentiable_in x by SIN_COS:63;
  Z c= dom cos /\ dom arccot by A1,VALUED_1:def 4;
  then Z c= dom cos by XBOOLE_1:18;
  then
A5: cos is_differentiable_on Z by A4,FDIFF_1:9;
  for x st x in Z holds ((cos(#)arccot)`|Z).x = -sin.x*arccot.x-cos.x/(1+x ^2)
  proof
    let x;
    assume
A6: x in Z;
    then
    ((cos(#)arccot)`|Z).x = (arccot.x)*diff(cos,x)+(cos.x)*diff(arccot,x)
    by A1,A5,A3,FDIFF_1:21
      .= (arccot.x)*(-sin.x)+(cos.x)*diff(arccot,x) by SIN_COS:63
      .= -sin.x*arccot.x+(cos.x)*((arccot)`|Z).x by A3,A6,FDIFF_1:def 7
      .= -sin.x*arccot.x+(cos.x)*(-1/(1+x^2)) by A2,A6,SIN_COS9:82
      .= -sin.x*arccot.x-cos.x/(1+x^2);
    hence thesis;
  end;
  hence thesis by A1,A5,A3,FDIFF_1:21;
end;

::f.x=tan.x*arctan.x

theorem
  Z c= dom (tan(#)arctan) & Z c= ].-1,1.[ implies (tan(#)arctan)
is_differentiable_on Z & for x st x in Z holds ((tan(#)arctan)`|Z).x = arctan.x
  /(cos.x)^2+tan.x/(1+x^2)
proof
  assume that
A1: Z c= dom (tan(#)arctan) and
A2: Z c= ].-1,1.[;
A3: arctan is_differentiable_on Z by A2,SIN_COS9:81;
  Z c= dom tan /\ dom arctan by A1,VALUED_1:def 4;
  then
A4: Z c= dom tan by XBOOLE_1:18;
  for x st x in Z holds tan is_differentiable_in x
  proof
    let x;
    assume x in Z;
    then cos.x <> 0 by A4,FDIFF_8:1;
    hence thesis by FDIFF_7:46;
  end;
  then
A5: tan is_differentiable_on Z by A4,FDIFF_1:9;
  for x st x in Z holds ((tan(#)arctan)`|Z).x = arctan.x/(cos.x)^2+tan.x/
  (1+x^2)
  proof
    let x;
    assume
A6: x in Z;
    then
A7: cos.x <> 0 by A4,FDIFF_8:1;
    ((tan(#)arctan)`|Z).x = (arctan.x)*diff(tan,x)+(tan.x)*diff(arctan,x)
    by A1,A5,A3,A6,FDIFF_1:21
      .= (arctan.x)*(1/(cos.x)^2)+(tan.x)*diff(arctan,x) by A7,FDIFF_7:46
      .= arctan.x/(cos.x)^2+(tan.x)*((arctan)`|Z).x by A3,A6,FDIFF_1:def 7
      .= arctan.x/(cos.x)^2+(tan.x)*(1/(1+x^2)) by A2,A6,SIN_COS9:81
      .= arctan.x/(cos.x)^2+tan.x/(1+x^2);
    hence thesis;
  end;
  hence thesis by A1,A5,A3,FDIFF_1:21;
end;

::f.x=tan.x*arccot.x

theorem
  Z c= dom (tan(#)arccot) & Z c= ].-1,1.[ implies (tan(#)arccot)
is_differentiable_on Z & for x st x in Z holds ((tan(#)arccot)`|Z).x = arccot.x
  /(cos.x)^2-tan.x/(1+x^2)
proof
  assume that
A1: Z c= dom (tan(#)arccot) and
A2: Z c= ].-1,1.[;
A3: arccot is_differentiable_on Z by A2,SIN_COS9:82;
  Z c= dom tan /\ dom arccot by A1,VALUED_1:def 4;
  then
A4: Z c= dom tan by XBOOLE_1:18;
  for x st x in Z holds tan is_differentiable_in x
  proof
    let x;
    assume x in Z;
    then cos.x <> 0 by A4,FDIFF_8:1;
    hence thesis by FDIFF_7:46;
  end;
  then
A5: tan is_differentiable_on Z by A4,FDIFF_1:9;
  for x st x in Z holds ((tan(#)arccot)`|Z).x = arccot.x/(cos.x)^2-tan.x/
  (1+x^2)
  proof
    let x;
    assume
A6: x in Z;
    then
A7: cos.x <> 0 by A4,FDIFF_8:1;
    ((tan(#)arccot)`|Z).x = (arccot.x)*diff(tan,x)+(tan.x)*diff(arccot,x)
    by A1,A5,A3,A6,FDIFF_1:21
      .= (arccot.x)*(1/(cos.x)^2)+(tan.x)*diff(arccot,x) by A7,FDIFF_7:46
      .= arccot.x/(cos.x)^2+(tan.x)*((arccot)`|Z).x by A3,A6,FDIFF_1:def 7
      .= arccot.x/(cos.x)^2+(tan.x)*(-1/(1+x^2)) by A2,A6,SIN_COS9:82
      .= arccot.x/(cos.x)^2-tan.x/(1+x^2);
    hence thesis;
  end;
  hence thesis by A1,A5,A3,FDIFF_1:21;
end;

::f.x=cot.x*arctan.x

theorem
  Z c= dom (cot(#)arctan) & Z c= ].-1,1.[ implies (cot(#)arctan)
is_differentiable_on Z & for x st x in Z holds ((cot(#)arctan)`|Z).x = -arctan.
  x/(sin.x)^2+cot.x/(1+x^2)
proof
  assume that
A1: Z c= dom (cot(#)arctan) and
A2: Z c= ].-1,1.[;
A3: arctan is_differentiable_on Z by A2,SIN_COS9:81;
  Z c= dom cot /\ dom arctan by A1,VALUED_1:def 4;
  then
A4: Z c= dom cot by XBOOLE_1:18;
  for x st x in Z holds cot is_differentiable_in x
  proof
    let x;
    assume x in Z;
    then sin.x <> 0 by A4,FDIFF_8:2;
    hence thesis by FDIFF_7:47;
  end;
  then
A5: cot is_differentiable_on Z by A4,FDIFF_1:9;
  for x st x in Z holds ((cot(#)arctan)`|Z).x = -arctan.x/(sin.x)^2+cot.x
  /(1+x^2)
  proof
    let x;
    assume
A6: x in Z;
    then
A7: sin.x <> 0 by A4,FDIFF_8:2;
    ((cot(#)arctan)`|Z).x = (arctan.x)*diff(cot,x)+(cot.x)*diff(arctan,x)
    by A1,A5,A3,A6,FDIFF_1:21
      .= (arctan.x)*(-1/(sin.x)^2)+(cot.x)*diff(arctan,x) by A7,FDIFF_7:47
      .= -arctan.x/(sin.x)^2+(cot.x)*((arctan)`|Z).x by A3,A6,FDIFF_1:def 7
      .= -arctan.x/(sin.x)^2+(cot.x)*(1/(1+x^2)) by A2,A6,SIN_COS9:81
      .= -arctan.x/(sin.x)^2+cot.x/(1+x^2);
    hence thesis;
  end;
  hence thesis by A1,A5,A3,FDIFF_1:21;
end;

::f.x=cot.x*arccot.x

theorem
  Z c= dom (cot(#)arccot) & Z c= ].-1,1.[ implies (cot(#)arccot)
is_differentiable_on Z & for x st x in Z holds ((cot(#)arccot)`|Z).x = -arccot.
  x/(sin.x)^2-cot.x/(1+x^2)
proof
  assume that
A1: Z c= dom (cot(#)arccot) and
A2: Z c= ].-1,1.[;
A3: arccot is_differentiable_on Z by A2,SIN_COS9:82;
  Z c= dom cot /\ dom arccot by A1,VALUED_1:def 4;
  then
A4: Z c= dom cot by XBOOLE_1:18;
  for x st x in Z holds cot is_differentiable_in x
  proof
    let x;
    assume x in Z;
    then sin.x <> 0 by A4,FDIFF_8:2;
    hence thesis by FDIFF_7:47;
  end;
  then
A5: cot is_differentiable_on Z by A4,FDIFF_1:9;
  for x st x in Z holds ((cot(#)arccot)`|Z).x = -arccot.x/(sin.x)^2-cot.x
  /(1+x^2)
  proof
    let x;
    assume
A6: x in Z;
    then
A7: sin.x <> 0 by A4,FDIFF_8:2;
    ((cot(#)arccot)`|Z).x = (arccot.x)*diff(cot,x)+(cot.x)*diff(arccot,x)
    by A1,A5,A3,A6,FDIFF_1:21
      .= (arccot.x)*(-1/(sin.x)^2)+(cot.x)*diff(arccot,x) by A7,FDIFF_7:47
      .= -arccot.x/(sin.x)^2+(cot.x)*((arccot)`|Z).x by A3,A6,FDIFF_1:def 7
      .= -arccot.x/(sin.x)^2+(cot.x)*(-1/(1+x^2)) by A2,A6,SIN_COS9:82
      .= -arccot.x/(sin.x)^2-cot.x/(1+x^2);
    hence thesis;
  end;
  hence thesis by A1,A5,A3,FDIFF_1:21;
end;

::f.x=sec.x*arctan.x

theorem
  Z c= dom (sec(#)arctan) & Z c= ].-1,1.[ implies (sec(#)arctan)
is_differentiable_on Z & for x st x in Z holds ((sec(#)arctan)`|Z).x = (sin.x*
  arctan.x)/(cos.x)^2+1/(cos.x*(1+x^2))
proof
  assume that
A1: Z c= dom (sec(#)arctan) and
A2: Z c= ].-1,1.[;
A3: arctan is_differentiable_on Z by A2,SIN_COS9:81;
  Z c= dom sec /\ dom arctan by A1,VALUED_1:def 4;
  then
A4: Z c= dom sec by XBOOLE_1:18;
  for x st x in Z holds sec is_differentiable_in x
  proof
    let x;
    assume x in Z;
    then cos.x <> 0 by A4,RFUNCT_1:3;
    hence thesis by FDIFF_9:1;
  end;
  then
A5: sec is_differentiable_on Z by A4,FDIFF_1:9;
  for x st x in Z holds ((sec(#)arctan)`|Z).x = (sin.x*arctan.x)/(cos.x)
  ^2+1/(cos.x*(1+x^2))
  proof
    let x;
    assume
A6: x in Z;
    then
A7: cos.x <> 0 by A4,RFUNCT_1:3;
    ((sec(#)arctan)`|Z).x = (arctan.x)*diff(sec,x)+(sec.x)*diff(arctan,x)
    by A1,A5,A3,A6,FDIFF_1:21
      .= (arctan.x)*(sin.x/(cos.x)^2)+(sec.x)*diff(arctan,x) by A7,FDIFF_9:1
      .= (sin.x*arctan.x)/(cos.x)^2+(sec.x)*((arctan)`|Z).x by A3,A6,
FDIFF_1:def 7
      .= (sin.x*arctan.x)/(cos.x)^2+(sec.x)*(1/(1+x^2)) by A2,A6,SIN_COS9:81
      .= (sin.x*arctan.x)/(cos.x)^2+(1/cos.x)*(1/(1+x^2)) by A4,A6,
RFUNCT_1:def 2
      .= (sin.x*arctan.x)/(cos.x)^2+1/(cos.x*(1+x^2)) by XCMPLX_1:102;
    hence thesis;
  end;
  hence thesis by A1,A5,A3,FDIFF_1:21;
end;

::f.x=sec.x*arccot.x

theorem
  Z c= dom (sec(#)arccot) & Z c= ].-1,1.[ implies (sec(#)arccot)
is_differentiable_on Z & for x st x in Z holds ((sec(#)arccot)`|Z).x = (sin.x*
  arccot.x)/(cos.x)^2-1/(cos.x*(1+x^2))
proof
  assume that
A1: Z c= dom (sec(#)arccot) and
A2: Z c= ].-1,1.[;
A3: arccot is_differentiable_on Z by A2,SIN_COS9:82;
  Z c= dom sec /\ dom arccot by A1,VALUED_1:def 4;
  then
A4: Z c= dom sec by XBOOLE_1:18;
  for x st x in Z holds sec is_differentiable_in x
  proof
    let x;
    assume x in Z;
    then cos.x <> 0 by A4,RFUNCT_1:3;
    hence thesis by FDIFF_9:1;
  end;
  then
A5: sec is_differentiable_on Z by A4,FDIFF_1:9;
  for x st x in Z holds ((sec(#)arccot)`|Z).x = (sin.x*arccot.x)/(cos.x)
  ^2-1/(cos.x*(1+x^2))
  proof
    let x;
    assume
A6: x in Z;
    then
A7: cos.x <> 0 by A4,RFUNCT_1:3;
    ((sec(#)arccot)`|Z).x = (arccot.x)*diff(sec,x)+(sec.x)*diff(arccot,x)
    by A1,A5,A3,A6,FDIFF_1:21
      .= (arccot.x)*(sin.x/(cos.x)^2)+(sec.x)*diff(arccot,x) by A7,FDIFF_9:1
      .= (sin.x*arccot.x)/(cos.x)^2+(sec.x)*((arccot)`|Z).x by A3,A6,
FDIFF_1:def 7
      .= (sin.x*arccot.x)/(cos.x)^2+(sec.x)*(-1/(1+x^2)) by A2,A6,SIN_COS9:82
      .= (sin.x*arccot.x)/(cos.x)^2-(sec.x)*(1/(1+x^2))
      .= (sin.x*arccot.x)/(cos.x)^2-(1/cos.x)*(1/(1+x^2)) by A4,A6,
RFUNCT_1:def 2
      .= (sin.x*arccot.x)/(cos.x)^2-1/(cos.x*(1+x^2)) by XCMPLX_1:102;
    hence thesis;
  end;
  hence thesis by A1,A5,A3,FDIFF_1:21;
end;

::f.x=cosec.x*arctan.x

theorem
  Z c= dom (cosec(#)arctan) & Z c= ].-1,1.[ implies (cosec(#)arctan)
is_differentiable_on Z & for x st x in Z holds ((cosec(#)arctan)`|Z).x = -(cos.
  x*arctan.x)/(sin.x)^2+1/(sin.x*(1+x^2))
proof
  assume that
A1: Z c= dom (cosec(#)arctan) and
A2: Z c= ].-1,1.[;
A3: arctan is_differentiable_on Z by A2,SIN_COS9:81;
  Z c= dom cosec /\ dom arctan by A1,VALUED_1:def 4;
  then
A4: Z c= dom cosec by XBOOLE_1:18;
  for x st x in Z holds cosec is_differentiable_in x
  proof
    let x;
    assume x in Z;
    then sin.x <> 0 by A4,RFUNCT_1:3;
    hence thesis by FDIFF_9:2;
  end;
  then
A5: cosec is_differentiable_on Z by A4,FDIFF_1:9;
  for x st x in Z holds ((cosec(#)arctan)`|Z).x = -(cos.x*arctan.x)/(sin.
  x)^2+1/(sin.x*(1+x^2))
  proof
    let x;
    assume
A6: x in Z;
    then
A7: sin.x <> 0 by A4,RFUNCT_1:3;
    ((cosec(#)arctan)`|Z).x = (arctan.x)*diff(cosec,x)+(cosec.x)*diff(
    arctan,x) by A1,A5,A3,A6,FDIFF_1:21
      .= (arctan.x)*(-cos.x/(sin.x)^2)+(cosec.x)*diff(arctan,x) by A7,FDIFF_9:2
      .= -(cos.x*arctan.x)/(sin.x)^2+(cosec.x)*((arctan)`|Z).x by A3,A6,
FDIFF_1:def 7
      .= -(cos.x*arctan.x)/(sin.x)^2+(cosec.x)*(1/(1+x^2)) by A2,A6,SIN_COS9:81
      .= -(cos.x*arctan.x)/(sin.x)^2+(1/sin.x)*(1/(1+x^2)) by A4,A6,
RFUNCT_1:def 2
      .= -(cos.x*arctan.x)/(sin.x)^2+1/(sin.x*(1+x^2)) by XCMPLX_1:102;
    hence thesis;
  end;
  hence thesis by A1,A5,A3,FDIFF_1:21;
end;

::f.x=cosec.x*arccot.x

theorem
  Z c= dom (cosec(#)arccot) & Z c= ].-1,1.[ implies (cosec(#)arccot)
is_differentiable_on Z & for x st x in Z holds ((cosec(#)arccot)`|Z).x = -(cos.
  x*arccot.x)/(sin.x)^2-1/(sin.x*(1+x^2))
proof
  assume that
A1: Z c= dom (cosec(#)arccot) and
A2: Z c= ].-1,1.[;
A3: arccot is_differentiable_on Z by A2,SIN_COS9:82;
  Z c= dom cosec /\ dom arccot by A1,VALUED_1:def 4;
  then
A4: Z c= dom cosec by XBOOLE_1:18;
  for x st x in Z holds cosec is_differentiable_in x
  proof
    let x;
    assume x in Z;
    then sin.x <> 0 by A4,RFUNCT_1:3;
    hence thesis by FDIFF_9:2;
  end;
  then
A5: cosec is_differentiable_on Z by A4,FDIFF_1:9;
  for x st x in Z holds ((cosec(#)arccot)`|Z).x = -(cos.x*arccot.x)/(sin.
  x)^2-1/(sin.x*(1+x^2))
  proof
    let x;
    assume
A6: x in Z;
    then
A7: sin.x <> 0 by A4,RFUNCT_1:3;
    ((cosec(#)arccot)`|Z).x = (arccot.x)*diff(cosec,x)+(cosec.x)*diff(
    arccot,x) by A1,A5,A3,A6,FDIFF_1:21
      .= (arccot.x)*(-cos.x/(sin.x)^2)+(cosec.x)*diff(arccot,x) by A7,FDIFF_9:2
      .= -(cos.x*arccot.x)/(sin.x)^2+(cosec.x)*((arccot)`|Z).x by A3,A6,
FDIFF_1:def 7
      .= -(cos.x*arccot.x)/(sin.x)^2+(cosec.x)*(-1/(1+x^2)) by A2,A6,
SIN_COS9:82
      .= -(cos.x*arccot.x)/(sin.x)^2-(cosec.x)*(1/(1+x^2))
      .= -(cos.x*arccot.x)/(sin.x)^2-(1/sin.x)*(1/(1+x^2)) by A4,A6,
RFUNCT_1:def 2
      .= -(cos.x*arccot.x)/(sin.x)^2-1/(sin.x*(1+x^2)) by XCMPLX_1:102;
    hence thesis;
  end;
  hence thesis by A1,A5,A3,FDIFF_1:21;
end;

::f.x=arctan.x+arccot.x

theorem Th37:
  Z c= ].-1,1.[ implies (arctan+arccot) is_differentiable_on Z &
  for x st x in Z holds ((arctan+arccot)`|Z).x = 0
proof
  assume
A1: Z c= ].-1,1.[;
  then
A2: arctan is_differentiable_on Z by SIN_COS9:81;
A3: ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
  then ].-1,1.[ c= dom arccot by SIN_COS9:24,XBOOLE_1:1;
  then
A4: Z c= dom arccot by A1,XBOOLE_1:1;
A5: arccot is_differentiable_on Z by A1,SIN_COS9:82;
  ].-1,1.[ c= dom arctan by A3,SIN_COS9:23,XBOOLE_1:1;
  then Z c= dom arctan by A1,XBOOLE_1:1;
  then Z c= dom arctan /\ dom arccot by A4,XBOOLE_1:19;
  then
A6: Z c= dom (arctan+arccot) by VALUED_1:def 1;
  for x st x in Z holds ((arctan+arccot)`|Z).x = 0
  proof
    let x;
    assume
A7: x in Z;
    then ((arctan+arccot)`|Z).x = diff(arctan,x)+diff(arccot,x) by A6,A2,A5,
FDIFF_1:18
      .= ((arctan)`|Z).x+diff(arccot,x) by A2,A7,FDIFF_1:def 7
      .= 1/(1+x^2)+diff(arccot,x) by A1,A7,SIN_COS9:81
      .= 1/(1+x^2)+((arccot)`|Z).x by A5,A7,FDIFF_1:def 7
      .= 1/(1+x^2)+(-1/(1+x^2)) by A1,A7,SIN_COS9:82
      .= 0;
    hence thesis;
  end;
  hence thesis by A6,A2,A5,FDIFF_1:18;
end;

::f.x=arctan.x-arccot.x

theorem Th38:
  Z c= ].-1,1.[ implies (arctan-arccot) is_differentiable_on Z &
  for x st x in Z holds ((arctan-arccot)`|Z).x = 2/(1+x^2)
proof
  assume
A1: Z c= ].-1,1.[;
  then
A2: arctan is_differentiable_on Z by SIN_COS9:81;
A3: ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
  then ].-1,1.[ c= dom arccot by SIN_COS9:24,XBOOLE_1:1;
  then
A4: Z c= dom arccot by A1,XBOOLE_1:1;
A5: arccot is_differentiable_on Z by A1,SIN_COS9:82;
  ].-1,1.[ c= dom arctan by A3,SIN_COS9:23,XBOOLE_1:1;
  then Z c= dom arctan by A1,XBOOLE_1:1;
  then Z c= dom arctan /\ dom arccot by A4,XBOOLE_1:19;
  then
A6: Z c= dom (arctan-arccot) by VALUED_1:12;
  for x st x in Z holds ((arctan-arccot)`|Z).x = 2/(1+x^2)
  proof
    let x;
    assume
A7: x in Z;
    then ((arctan-arccot)`|Z).x = diff(arctan,x)-diff(arccot,x) by A6,A2,A5,
FDIFF_1:19
      .= ((arctan)`|Z).x-diff(arccot,x) by A2,A7,FDIFF_1:def 7
      .= 1/(1+x^2)-diff(arccot,x) by A1,A7,SIN_COS9:81
      .= 1/(1+x^2)-((arccot)`|Z).x by A5,A7,FDIFF_1:def 7
      .= 1/(1+x^2)-(-1/(1+x^2)) by A1,A7,SIN_COS9:82
      .= 2/(1+x^2);
    hence thesis;
  end;
  hence thesis by A6,A2,A5,FDIFF_1:19;
end;

::f.x=sin.x*(arctan.x+arccot.x)

theorem
  Z c= ].-1,1.[ implies sin(#)(arctan+arccot) is_differentiable_on Z &
for x st x in Z holds ((sin(#)(arctan+arccot))`|Z).x = cos.x*(arctan.x+arccot.x
  )
proof
  for x st x in Z holds sin is_differentiable_in x by SIN_COS:64;
  then
A1: sin is_differentiable_on Z by FDIFF_1:9,SIN_COS:24;
  assume
A2: Z c= ].-1,1.[;
  then
A3: arctan+arccot is_differentiable_on Z by Th37;
A4: ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
  then ].-1,1.[ c= dom arccot by SIN_COS9:24,XBOOLE_1:1;
  then
A5: Z c= dom arccot by A2,XBOOLE_1:1;
  ].-1,1.[ c= dom arctan by A4,SIN_COS9:23,XBOOLE_1:1;
  then Z c= dom arctan by A2,XBOOLE_1:1;
  then Z c= dom arctan /\ dom arccot by A5,XBOOLE_1:19;
  then
A6: Z c= dom (arctan+arccot) by VALUED_1:def 1;
  then Z c= dom sin /\ dom (arctan+arccot) by SIN_COS:24,XBOOLE_1:19;
  then
A7: Z c= dom (sin(#)(arctan+arccot)) by VALUED_1:def 4;
  for x st x in Z holds (sin(#)(arctan+arccot)`|Z).x = cos.x*(arctan.x+
  arccot.x)
  proof
    let x;
    assume
A8: x in Z;
    then
    (sin(#)(arctan+arccot)`|Z).x = ((arctan+arccot).x)*diff(sin,x)+sin.x*
    diff(arctan+arccot,x) by A7,A1,A3,FDIFF_1:21
      .= (arctan.x+arccot.x)*diff(sin,x)+sin.x*diff(arctan+arccot,x) by A6,A8,
VALUED_1:def 1
      .= (arctan.x+arccot.x)*cos.x+sin.x*diff(arctan+arccot,x) by SIN_COS:64
      .= (arctan.x+arccot.x)*cos.x+sin.x*((arctan+arccot)`|Z).x by A3,A8,
FDIFF_1:def 7
      .= (arctan.x+arccot.x)*cos.x+sin.x*0 by A2,A8,Th37
      .= cos.x*(arctan.x+arccot.x);
    hence thesis;
  end;
  hence thesis by A7,A1,A3,FDIFF_1:21;
end;

::f.x=sin.x*(arctan.x-arccot.x)

theorem
  Z c= ].-1,1.[ implies sin(#)(arctan-arccot) is_differentiable_on Z &
for x st x in Z holds ((sin(#)(arctan-arccot))`|Z).x = cos.x*(arctan.x-arccot.x
  )+2*sin.x/(1+x^2)
proof
  for x st x in Z holds sin is_differentiable_in x by SIN_COS:64;
  then
A1: sin is_differentiable_on Z by FDIFF_1:9,SIN_COS:24;
  assume
A2: Z c= ].-1,1.[;
  then
A3: arctan-arccot is_differentiable_on Z by Th38;
A4: ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
  then ].-1,1.[ c= dom arccot by SIN_COS9:24,XBOOLE_1:1;
  then
A5: Z c= dom arccot by A2,XBOOLE_1:1;
  ].-1,1.[ c= dom arctan by A4,SIN_COS9:23,XBOOLE_1:1;
  then Z c= dom arctan by A2,XBOOLE_1:1;
  then Z c= dom arctan /\ dom arccot by A5,XBOOLE_1:19;
  then
A6: Z c= dom (arctan-arccot) by VALUED_1:12;
  then Z c= dom sin /\ dom (arctan-arccot) by SIN_COS:24,XBOOLE_1:19;
  then
A7: Z c= dom (sin(#)(arctan-arccot)) by VALUED_1:def 4;
  for x st x in Z holds (sin(#)(arctan-arccot)`|Z).x = cos.x*(arctan.x-
  arccot.x)+2*sin.x/(1+x^2)
  proof
    let x;
    assume
A8: x in Z;
    then
    (sin(#)(arctan-arccot)`|Z).x = ((arctan-arccot).x)*diff(sin,x)+sin.x*
    diff(arctan-arccot,x) by A7,A1,A3,FDIFF_1:21
      .= (arctan.x-arccot.x)*diff(sin,x)+sin.x*diff(arctan-arccot,x) by A6,A8,
VALUED_1:13
      .= (arctan.x-arccot.x)*cos.x+sin.x*diff(arctan-arccot,x) by SIN_COS:64
      .= (arctan.x-arccot.x)*cos.x+sin.x*((arctan-arccot)`|Z).x by A3,A8,
FDIFF_1:def 7
      .= (arctan.x-arccot.x)*cos.x+sin.x*(2/(1+x^2)) by A2,A8,Th38
      .= cos.x*(arctan.x-arccot.x)+2*sin.x/(1+x^2);
    hence thesis;
  end;
  hence thesis by A7,A1,A3,FDIFF_1:21;
end;

::f.x=cos.x*(arctan.x+arccot.x)

theorem
  Z c= ].-1,1.[ implies cos(#)(arctan+arccot) is_differentiable_on Z &
for x st x in Z holds ((cos(#)(arctan+arccot))`|Z).x = -sin.x*(arctan.x+arccot.
  x)
proof
  for x st x in Z holds cos is_differentiable_in x by SIN_COS:63;
  then
A1: cos is_differentiable_on Z by FDIFF_1:9,SIN_COS:24;
  assume
A2: Z c= ].-1,1.[;
  then
A3: arctan+arccot is_differentiable_on Z by Th37;
A4: ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
  then ].-1,1.[ c= dom arccot by SIN_COS9:24,XBOOLE_1:1;
  then
A5: Z c= dom arccot by A2,XBOOLE_1:1;
  ].-1,1.[ c= dom arctan by A4,SIN_COS9:23,XBOOLE_1:1;
  then Z c= dom arctan by A2,XBOOLE_1:1;
  then Z c= dom arctan /\ dom arccot by A5,XBOOLE_1:19;
  then
A6: Z c= dom (arctan+arccot) by VALUED_1:def 1;
  then Z c= dom cos /\ dom (arctan+arccot) by SIN_COS:24,XBOOLE_1:19;
  then
A7: Z c= dom (cos(#)(arctan+arccot)) by VALUED_1:def 4;
  for x st x in Z holds (cos(#)(arctan+arccot)`|Z).x = -sin.x*(arctan.x+
  arccot.x)
  proof
    let x;
    assume
A8: x in Z;
    then
    (cos(#)(arctan+arccot)`|Z).x = ((arctan+arccot).x)*diff(cos,x)+cos.x*
    diff(arctan+arccot,x) by A7,A1,A3,FDIFF_1:21
      .= (arctan.x+arccot.x)*diff(cos,x)+cos.x*diff(arctan+arccot,x) by A6,A8,
VALUED_1:def 1
      .= (arctan.x+arccot.x)*(-sin.x)+cos.x*diff(arctan+arccot,x) by SIN_COS:63
      .= (arctan.x+arccot.x)*(-sin.x)+cos.x*((arctan+arccot)`|Z).x by A3,A8,
FDIFF_1:def 7
      .= -(arctan.x+arccot.x)*sin.x+cos.x*0 by A2,A8,Th37
      .= -sin.x*(arctan.x+arccot.x);
    hence thesis;
  end;
  hence thesis by A7,A1,A3,FDIFF_1:21;
end;

::f.x=cos.x*(arctan.x-arccot.x)

theorem
  Z c= ].-1,1.[ implies cos(#)(arctan-arccot) is_differentiable_on Z &
for x st x in Z holds ((cos(#)(arctan-arccot))`|Z).x = -sin.x*(arctan.x-arccot.
  x)+2*cos.x/(1+x^2)
proof
  for x st x in Z holds cos is_differentiable_in x by SIN_COS:63;
  then
A1: cos is_differentiable_on Z by FDIFF_1:9,SIN_COS:24;
  assume
A2: Z c= ].-1,1.[;
  then
A3: arctan-arccot is_differentiable_on Z by Th38;
A4: ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
  then ].-1,1.[ c= dom arccot by SIN_COS9:24,XBOOLE_1:1;
  then
A5: Z c= dom arccot by A2,XBOOLE_1:1;
  ].-1,1.[ c= dom arctan by A4,SIN_COS9:23,XBOOLE_1:1;
  then Z c= dom arctan by A2,XBOOLE_1:1;
  then Z c= dom arctan /\ dom arccot by A5,XBOOLE_1:19;
  then
A6: Z c= dom (arctan-arccot) by VALUED_1:12;
  then Z c= dom cos /\ dom (arctan-arccot) by SIN_COS:24,XBOOLE_1:19;
  then
A7: Z c= dom (cos(#)(arctan-arccot)) by VALUED_1:def 4;
  for x st x in Z holds (cos(#)(arctan-arccot)`|Z).x = -sin.x*(arctan.x-
  arccot.x)+2*cos.x/(1+x^2)
  proof
    let x;
    assume
A8: x in Z;
    then
    (cos(#)(arctan-arccot)`|Z).x = ((arctan-arccot).x)*diff(cos,x)+cos.x*
    diff(arctan-arccot,x) by A7,A1,A3,FDIFF_1:21
      .= (arctan.x-arccot.x)*diff(cos,x)+cos.x*diff(arctan-arccot,x) by A6,A8,
VALUED_1:13
      .= (arctan.x-arccot.x)*(-sin.x)+cos.x*diff(arctan-arccot,x) by SIN_COS:63
      .= (arctan.x-arccot.x)*(-sin.x)+cos.x*((arctan-arccot)`|Z).x by A3,A8,
FDIFF_1:def 7
      .= -(arctan.x-arccot.x)*sin.x+cos.x*(2/(1+x^2)) by A2,A8,Th38
      .= -sin.x*(arctan.x-arccot.x)+2*cos.x/(1+x^2);
    hence thesis;
  end;
  hence thesis by A7,A1,A3,FDIFF_1:21;
end;

::f.x=tan.x*(arctan.x+arccot.x)

theorem
  Z c= dom tan & Z c= ].-1,1.[ implies tan(#)(arctan+arccot)
is_differentiable_on Z & for x st x in Z holds ((tan(#)(arctan+arccot))`|Z).x =
  (arctan.x+arccot.x)/(cos.x)^2
proof
  assume that
A1: Z c= dom tan and
A2: Z c= ].-1,1.[;
A3: arctan+arccot is_differentiable_on Z by A2,Th37;
  for x st x in Z holds tan is_differentiable_in x
  proof
    let x;
    assume x in Z;
    then cos.x <> 0 by A1,FDIFF_8:1;
    hence thesis by FDIFF_7:46;
  end;
  then
A4: tan is_differentiable_on Z by A1,FDIFF_1:9;
A5: ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
  then ].-1,1.[ c= dom arccot by SIN_COS9:24,XBOOLE_1:1;
  then
A6: Z c= dom arccot by A2,XBOOLE_1:1;
  ].-1,1.[ c= dom arctan by A5,SIN_COS9:23,XBOOLE_1:1;
  then Z c= dom arctan by A2,XBOOLE_1:1;
  then Z c= dom arctan /\ dom arccot by A6,XBOOLE_1:19;
  then
A7: Z c= dom (arctan+arccot) by VALUED_1:def 1;
  then Z c= dom tan /\ dom (arctan+arccot) by A1,XBOOLE_1:19;
  then
A8: Z c= dom (tan(#)(arctan+arccot)) by VALUED_1:def 4;
  for x st x in Z holds (tan(#)(arctan+arccot)`|Z).x = (arctan.x+arccot.x
  )/(cos.x)^2
  proof
    let x;
    assume
A9: x in Z;
    then
A10: cos.x <> 0 by A1,FDIFF_8:1;
    (tan(#)(arctan+arccot)`|Z).x = ((arctan+arccot).x)*diff(tan,x)+tan.x*
    diff(arctan+arccot,x) by A8,A4,A3,A9,FDIFF_1:21
      .= (arctan.x+arccot.x)*diff(tan,x)+tan.x*diff(arctan+arccot,x) by A7,A9,
VALUED_1:def 1
      .= (arctan.x+arccot.x)*(1/(cos.x)^2)+tan.x*diff(arctan+arccot,x) by A10,
FDIFF_7:46
      .= (arctan.x+arccot.x)/(cos.x)^2+tan.x*((arctan+arccot)`|Z).x by A3,A9,
FDIFF_1:def 7
      .= (arctan.x+arccot.x)/(cos.x)^2+tan.x*0 by A2,A9,Th37
      .= (arctan.x+arccot.x)/(cos.x)^2;
    hence thesis;
  end;
  hence thesis by A8,A4,A3,FDIFF_1:21;
end;

::f.x=tan.x*(arctan.x-arccot.x)

theorem
  Z c= dom tan & Z c= ].-1,1.[ implies tan(#)(arctan-arccot)
is_differentiable_on Z & for x st x in Z holds ((tan(#)(arctan-arccot))`|Z).x =
  (arctan.x-arccot.x)/(cos.x)^2+2*tan.x/(1+x^2)
proof
  assume that
A1: Z c= dom tan and
A2: Z c= ].-1,1.[;
A3: arctan-arccot is_differentiable_on Z by A2,Th38;
  for x st x in Z holds tan is_differentiable_in x
  proof
    let x;
    assume x in Z;
    then cos.x <> 0 by A1,FDIFF_8:1;
    hence thesis by FDIFF_7:46;
  end;
  then
A4: tan is_differentiable_on Z by A1,FDIFF_1:9;
A5: ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
  then ].-1,1.[ c= dom arccot by SIN_COS9:24,XBOOLE_1:1;
  then
A6: Z c= dom arccot by A2,XBOOLE_1:1;
  ].-1,1.[ c= dom arctan by A5,SIN_COS9:23,XBOOLE_1:1;
  then Z c= dom arctan by A2,XBOOLE_1:1;
  then Z c= dom arctan /\ dom arccot by A6,XBOOLE_1:19;
  then
A7: Z c= dom (arctan-arccot) by VALUED_1:12;
  then Z c= dom tan /\ dom (arctan-arccot) by A1,XBOOLE_1:19;
  then
A8: Z c= dom (tan(#)(arctan-arccot)) by VALUED_1:def 4;
  for x st x in Z holds (tan(#)(arctan-arccot)`|Z).x = (arctan.x-arccot.x
  )/(cos.x)^2+2*tan.x/(1+x^2)
  proof
    let x;
    assume
A9: x in Z;
    then
A10: cos.x <> 0 by A1,FDIFF_8:1;
    (tan(#)(arctan-arccot)`|Z).x = ((arctan-arccot).x)*diff(tan,x)+tan.x*
    diff(arctan-arccot,x) by A8,A4,A3,A9,FDIFF_1:21
      .= (arctan.x-arccot.x)*diff(tan,x)+tan.x*diff(arctan-arccot,x) by A7,A9,
VALUED_1:13
      .= (arctan.x-arccot.x)*(1/(cos.x)^2)+tan.x*diff(arctan-arccot,x) by A10,
FDIFF_7:46
      .= (arctan.x-arccot.x)/(cos.x)^2+tan.x*((arctan-arccot)`|Z).x by A3,A9,
FDIFF_1:def 7
      .= (arctan.x-arccot.x)/(cos.x)^2+tan.x*(2/(1+x^2)) by A2,A9,Th38
      .= (arctan.x-arccot.x)/(cos.x)^2+2*tan.x/(1+x^2);
    hence thesis;
  end;
  hence thesis by A8,A4,A3,FDIFF_1:21;
end;

::f.x=cot.x*(arctan.x+arccot.x)

theorem
  Z c= dom cot & Z c= ].-1,1.[ implies cot(#)(arctan+arccot)
is_differentiable_on Z & for x st x in Z holds ((cot(#)(arctan+arccot))`|Z).x =
  -(arctan.x+arccot.x)/(sin.x)^2
proof
  assume that
A1: Z c= dom cot and
A2: Z c= ].-1,1.[;
A3: arctan+arccot is_differentiable_on Z by A2,Th37;
  for x st x in Z holds cot is_differentiable_in x
  proof
    let x;
    assume x in Z;
    then sin.x <> 0 by A1,FDIFF_8:2;
    hence thesis by FDIFF_7:47;
  end;
  then
A4: cot is_differentiable_on Z by A1,FDIFF_1:9;
A5: ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
  then ].-1,1.[ c= dom arccot by SIN_COS9:24,XBOOLE_1:1;
  then
A6: Z c= dom arccot by A2,XBOOLE_1:1;
  ].-1,1.[ c= dom arctan by A5,SIN_COS9:23,XBOOLE_1:1;
  then Z c= dom arctan by A2,XBOOLE_1:1;
  then Z c= dom arctan /\ dom arccot by A6,XBOOLE_1:19;
  then
A7: Z c= dom (arctan+arccot) by VALUED_1:def 1;
  then Z c= dom cot /\ dom (arctan+arccot) by A1,XBOOLE_1:19;
  then
A8: Z c= dom (cot(#)(arctan+arccot)) by VALUED_1:def 4;
  for x st x in Z holds (cot(#)(arctan+arccot)`|Z).x = -(arctan.x+arccot.
  x)/(sin.x)^2
  proof
    let x;
    assume
A9: x in Z;
    then
A10: sin.x <> 0 by A1,FDIFF_8:2;
    (cot(#)(arctan+arccot)`|Z).x = ((arctan+arccot).x)*diff(cot,x)+cot.x*
    diff(arctan+arccot,x) by A8,A4,A3,A9,FDIFF_1:21
      .= (arctan.x+arccot.x)*diff(cot,x)+cot.x*diff(arctan+arccot,x) by A7,A9,
VALUED_1:def 1
      .= (arctan.x+arccot.x)*(-1/(sin.x)^2)+cot.x*diff(arctan+arccot,x) by A10,
FDIFF_7:47
      .= -(arctan.x+arccot.x)/(sin.x)^2+cot.x*((arctan+arccot)`|Z).x by A3,A9,
FDIFF_1:def 7
      .= -(arctan.x+arccot.x)/(sin.x)^2+cot.x*0 by A2,A9,Th37
      .= -(arctan.x+arccot.x)/(sin.x)^2;
    hence thesis;
  end;
  hence thesis by A8,A4,A3,FDIFF_1:21;
end;

::f.x=cot.x*(arctan.x-arccot.x)

theorem
  Z c= dom cot & Z c= ].-1,1.[ implies cot(#)(arctan-arccot)
is_differentiable_on Z & for x st x in Z holds ((cot(#)(arctan-arccot))`|Z).x =
  -(arctan.x-arccot.x)/(sin.x)^2+2*cot.x/(1+x^2)
proof
  assume that
A1: Z c= dom cot and
A2: Z c= ].-1,1.[;
A3: arctan-arccot is_differentiable_on Z by A2,Th38;
  for x st x in Z holds cot is_differentiable_in x
  proof
    let x;
    assume x in Z;
    then sin.x <> 0 by A1,FDIFF_8:2;
    hence thesis by FDIFF_7:47;
  end;
  then
A4: cot is_differentiable_on Z by A1,FDIFF_1:9;
A5: ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
  then ].-1,1.[ c= dom arccot by SIN_COS9:24,XBOOLE_1:1;
  then
A6: Z c= dom arccot by A2,XBOOLE_1:1;
  ].-1,1.[ c= dom arctan by A5,SIN_COS9:23,XBOOLE_1:1;
  then Z c= dom arctan by A2,XBOOLE_1:1;
  then Z c= dom arctan /\ dom arccot by A6,XBOOLE_1:19;
  then
A7: Z c= dom (arctan-arccot) by VALUED_1:12;
  then Z c= dom cot /\ dom (arctan-arccot) by A1,XBOOLE_1:19;
  then
A8: Z c= dom (cot(#)(arctan-arccot)) by VALUED_1:def 4;
  for x st x in Z holds (cot(#)(arctan-arccot)`|Z).x = -(arctan.x-arccot.
  x)/(sin.x)^2+2*cot.x/(1+x^2)
  proof
    let x;
    assume
A9: x in Z;
    then
A10: sin.x <> 0 by A1,FDIFF_8:2;
    (cot(#)(arctan-arccot)`|Z).x = ((arctan-arccot).x)*diff(cot,x)+cot.x*
    diff(arctan-arccot,x) by A8,A4,A3,A9,FDIFF_1:21
      .= (arctan.x-arccot.x)*diff(cot,x)+cot.x*diff(arctan-arccot,x) by A7,A9,
VALUED_1:13
      .= (arctan.x-arccot.x)*(-1/(sin.x)^2)+cot.x*diff(arctan-arccot,x) by A10,
FDIFF_7:47
      .= -(arctan.x-arccot.x)/(sin.x)^2+cot.x*((arctan-arccot)`|Z).x by A3,A9,
FDIFF_1:def 7
      .= -(arctan.x-arccot.x)/(sin.x)^2+cot.x*(2/(1+x^2)) by A2,A9,Th38
      .= -(arctan.x-arccot.x)/(sin.x)^2+2*cot.x/(1+x^2);
    hence thesis;
  end;
  hence thesis by A8,A4,A3,FDIFF_1:21;
end;

::f.x=sec.x*(arctan.x+arccot.x)

theorem
  Z c= dom sec & Z c= ].-1,1.[ implies sec(#)(arctan+arccot)
is_differentiable_on Z & for x st x in Z holds ((sec(#)(arctan+arccot))`|Z).x =
  (arctan.x+arccot.x)*sin.x/(cos.x)^2
proof
  assume that
A1: Z c= dom sec and
A2: Z c= ].-1,1.[;
A3: arctan+arccot is_differentiable_on Z by A2,Th37;
  for x st x in Z holds sec is_differentiable_in x
  proof
    let x;
    assume x in Z;
    then cos.x <> 0 by A1,RFUNCT_1:3;
    hence thesis by FDIFF_9:1;
  end;
  then
A4: sec is_differentiable_on Z by A1,FDIFF_1:9;
A5: ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
  then ].-1,1.[ c= dom arccot by SIN_COS9:24,XBOOLE_1:1;
  then
A6: Z c= dom arccot by A2,XBOOLE_1:1;
  ].-1,1.[ c= dom arctan by A5,SIN_COS9:23,XBOOLE_1:1;
  then Z c= dom arctan by A2,XBOOLE_1:1;
  then Z c= dom arctan /\ dom arccot by A6,XBOOLE_1:19;
  then
A7: Z c= dom (arctan+arccot) by VALUED_1:def 1;
  then Z c= dom sec /\ dom (arctan+arccot) by A1,XBOOLE_1:19;
  then
A8: Z c= dom (sec(#)(arctan+arccot)) by VALUED_1:def 4;
  for x st x in Z holds (sec(#)(arctan+arccot)`|Z).x = (arctan.x+arccot.x
  )*sin.x/(cos.x)^2
  proof
    let x;
    assume
A9: x in Z;
    then
A10: cos.x <> 0 by A1,RFUNCT_1:3;
    (sec(#)(arctan+arccot)`|Z).x = ((arctan+arccot).x)*diff(sec,x)+sec.x*
    diff(arctan+arccot,x) by A8,A4,A3,A9,FDIFF_1:21
      .= (arctan.x+arccot.x)*diff(sec,x)+sec.x*diff(arctan+arccot,x) by A7,A9,
VALUED_1:def 1
      .= (arctan.x+arccot.x)*(sin.x/(cos.x)^2)+sec.x*diff(arctan+arccot,x)
    by A10,FDIFF_9:1
      .= (arctan.x+arccot.x)*sin.x/(cos.x)^2+sec.x*((arctan+arccot)`|Z).x by A3
,A9,FDIFF_1:def 7
      .= (arctan.x+arccot.x)*sin.x/(cos.x)^2+sec.x*0 by A2,A9,Th37
      .= (arctan.x+arccot.x)*sin.x/(cos.x)^2;
    hence thesis;
  end;
  hence thesis by A8,A4,A3,FDIFF_1:21;
end;

::f.x=sec.x*(arctan.x-arccot.x)

theorem
  Z c= dom sec & Z c= ].-1,1.[ implies sec(#)(arctan-arccot)
is_differentiable_on Z & for x st x in Z holds ((sec(#)(arctan-arccot))`|Z).x =
  (arctan.x-arccot.x)*sin.x/(cos.x)^2+2*sec.x/(1+x^2)
proof
  assume that
A1: Z c= dom sec and
A2: Z c= ].-1,1.[;
A3: arctan-arccot is_differentiable_on Z by A2,Th38;
  for x st x in Z holds sec is_differentiable_in x
  proof
    let x;
    assume x in Z;
    then cos.x <> 0 by A1,RFUNCT_1:3;
    hence thesis by FDIFF_9:1;
  end;
  then
A4: sec is_differentiable_on Z by A1,FDIFF_1:9;
A5: ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
  then ].-1,1.[ c= dom arccot by SIN_COS9:24,XBOOLE_1:1;
  then
A6: Z c= dom arccot by A2,XBOOLE_1:1;
  ].-1,1.[ c= dom arctan by A5,SIN_COS9:23,XBOOLE_1:1;
  then Z c= dom arctan by A2,XBOOLE_1:1;
  then Z c= dom arctan /\ dom arccot by A6,XBOOLE_1:19;
  then
A7: Z c= dom (arctan-arccot) by VALUED_1:12;
  then Z c= dom sec /\ dom (arctan-arccot) by A1,XBOOLE_1:19;
  then
A8: Z c= dom (sec(#)(arctan-arccot)) by VALUED_1:def 4;
  for x st x in Z holds ((sec(#)(arctan-arccot))`|Z).x = (arctan.x-arccot
  .x)*sin.x/(cos.x)^2+2*sec.x/(1+x^2)
  proof
    let x;
    assume
A9: x in Z;
    then
A10: cos.x <> 0 by A1,RFUNCT_1:3;
    (sec(#)(arctan-arccot)`|Z).x = ((arctan-arccot).x)*diff(sec,x)+sec.x*
    diff(arctan-arccot,x) by A8,A4,A3,A9,FDIFF_1:21
      .= (arctan.x-arccot.x)*diff(sec,x)+sec.x*diff(arctan-arccot,x) by A7,A9,
VALUED_1:13
      .= (arctan.x-arccot.x)*(sin.x/(cos.x)^2)+sec.x*diff(arctan-arccot,x)
    by A10,FDIFF_9:1
      .= (arctan.x-arccot.x)*sin.x/(cos.x)^2+sec.x*((arctan-arccot)`|Z).x by A3
,A9,FDIFF_1:def 7
      .= (arctan.x-arccot.x)*sin.x/(cos.x)^2+sec.x*(2/(1+x^2)) by A2,A9,Th38
      .= (arctan.x-arccot.x)*sin.x/(cos.x)^2+2*sec.x/(1+x^2);
    hence thesis;
  end;
  hence thesis by A8,A4,A3,FDIFF_1:21;
end;

::f.x=cosec.x*(arctan.x+arccot.x)

theorem
  Z c= dom cosec & Z c= ].-1,1.[ implies cosec(#)(arctan+arccot)
is_differentiable_on Z & for x st x in Z holds ((cosec(#)(arctan+arccot))`|Z).x
  = -(arctan.x+arccot.x)*cos.x/(sin.x)^2
proof
  assume that
A1: Z c= dom cosec and
A2: Z c= ].-1,1.[;
A3: arctan+arccot is_differentiable_on Z by A2,Th37;
  for x st x in Z holds cosec is_differentiable_in x
  proof
    let x;
    assume x in Z;
    then sin.x <> 0 by A1,RFUNCT_1:3;
    hence thesis by FDIFF_9:2;
  end;
  then
A4: cosec is_differentiable_on Z by A1,FDIFF_1:9;
A5: ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
  then ].-1,1.[ c= dom arccot by SIN_COS9:24,XBOOLE_1:1;
  then
A6: Z c= dom arccot by A2,XBOOLE_1:1;
  ].-1,1.[ c= dom arctan by A5,SIN_COS9:23,XBOOLE_1:1;
  then Z c= dom arctan by A2,XBOOLE_1:1;
  then Z c= dom arctan /\ dom arccot by A6,XBOOLE_1:19;
  then
A7: Z c= dom (arctan+arccot) by VALUED_1:def 1;
  then Z c= dom cosec /\ dom (arctan+arccot) by A1,XBOOLE_1:19;
  then
A8: Z c= dom (cosec(#)(arctan+arccot)) by VALUED_1:def 4;
  for x st x in Z holds (cosec(#)(arctan+arccot)`|Z).x = -(arctan.x+
  arccot.x)*cos.x/(sin.x)^2
  proof
    let x;
    assume
A9: x in Z;
    then
A10: sin.x <> 0 by A1,RFUNCT_1:3;
    (cosec(#)(arctan+arccot)`|Z).x = ((arctan+arccot).x)*diff(cosec,x)+
    cosec.x*diff(arctan+arccot,x) by A8,A4,A3,A9,FDIFF_1:21
      .= (arctan.x+arccot.x)*diff(cosec,x)+cosec.x*diff(arctan+arccot,x) by A7
,A9,VALUED_1:def 1
      .= (arctan.x+arccot.x)*(-cos.x/(sin.x)^2) +cosec.x*diff(arctan+arccot,
    x) by A10,FDIFF_9:2
      .= -(arctan.x+arccot.x)*cos.x/(sin.x)^2+cosec.x*((arctan+arccot)`|Z).x
    by A3,A9,FDIFF_1:def 7
      .= -(arctan.x+arccot.x)*cos.x/(sin.x)^2+cosec.x*0 by A2,A9,Th37
      .= -(arctan.x+arccot.x)*cos.x/(sin.x)^2;
    hence thesis;
  end;
  hence thesis by A8,A4,A3,FDIFF_1:21;
end;

::f.x=cosec.x*(arctan.x-arccot.x)

theorem
  Z c= dom cosec & Z c= ].-1,1.[ implies cosec(#)(arctan-arccot)
is_differentiable_on Z & for x st x in Z holds ((cosec(#)(arctan-arccot))`|Z).x
  = -(arctan.x-arccot.x)*cos.x/(sin.x)^2+2*cosec.x/(1+x^2)
proof
  assume that
A1: Z c= dom cosec and
A2: Z c= ].-1,1.[;
A3: arctan-arccot is_differentiable_on Z by A2,Th38;
  for x st x in Z holds cosec is_differentiable_in x
  proof
    let x;
    assume x in Z;
    then sin.x <> 0 by A1,RFUNCT_1:3;
    hence thesis by FDIFF_9:2;
  end;
  then
A4: cosec is_differentiable_on Z by A1,FDIFF_1:9;
A5: ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
  then ].-1,1.[ c= dom arccot by SIN_COS9:24,XBOOLE_1:1;
  then
A6: Z c= dom arccot by A2,XBOOLE_1:1;
  ].-1,1.[ c= dom arctan by A5,SIN_COS9:23,XBOOLE_1:1;
  then Z c= dom arctan by A2,XBOOLE_1:1;
  then Z c= dom arctan /\ dom arccot by A6,XBOOLE_1:19;
  then
A7: Z c= dom (arctan-arccot) by VALUED_1:12;
  then Z c= dom cosec /\ dom (arctan-arccot) by A1,XBOOLE_1:19;
  then
A8: Z c= dom (cosec(#)(arctan-arccot)) by VALUED_1:def 4;
  for x st x in Z holds (cosec(#)(arctan-arccot)`|Z).x = -(arctan.x-
  arccot.x)*cos.x/(sin.x)^2+2*cosec.x/(1+x^2)
  proof
    let x;
    assume
A9: x in Z;
    then
A10: sin.x <> 0 by A1,RFUNCT_1:3;
    (cosec(#)(arctan-arccot)`|Z).x = ((arctan-arccot).x)*diff(cosec,x)+
    cosec.x*diff(arctan-arccot,x) by A8,A4,A3,A9,FDIFF_1:21
      .= (arctan.x-arccot.x)*diff(cosec,x)+cosec.x*diff(arctan-arccot,x) by A7
,A9,VALUED_1:13
      .= (arctan.x-arccot.x)*(-cos.x/(sin.x)^2) +cosec.x*diff(arctan-arccot,
    x) by A10,FDIFF_9:2
      .= -(arctan.x-arccot.x)*cos.x/(sin.x)^2+cosec.x*((arctan-arccot)`|Z).x
    by A3,A9,FDIFF_1:def 7
      .= -(arctan.x-arccot.x)*cos.x/(sin.x)^2+cosec.x*(2/(1+x^2)) by A2,A9,Th38
      .= -(arctan.x-arccot.x)*cos.x/(sin.x)^2+2*cosec.x/(1+x^2);
    hence thesis;
  end;
  hence thesis by A8,A4,A3,FDIFF_1:21;
end;

::f.x=exp_R.x*(arctan.x+arccot.x)

theorem
  Z c= ].-1,1.[ implies exp_R(#)(arctan+arccot) is_differentiable_on Z &
  for x st x in Z holds ((exp_R(#)(arctan+arccot))`|Z).x = exp_R.x*(arctan.x+
  arccot.x)
proof
  assume
A1: Z c= ].-1,1.[;
  then
A2: arctan+arccot is_differentiable_on Z by Th37;
A3: ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
  then ].-1,1.[ c= dom arccot by SIN_COS9:24,XBOOLE_1:1;
  then
A4: Z c= dom arccot by A1,XBOOLE_1:1;
  ].-1,1.[ c= dom arctan by A3,SIN_COS9:23,XBOOLE_1:1;
  then Z c= dom arctan by A1,XBOOLE_1:1;
  then Z c= dom arctan /\ dom arccot by A4,XBOOLE_1:19;
  then
A5: Z c= dom (arctan+arccot) by VALUED_1:def 1;
  then Z c= dom exp_R /\ dom (arctan+arccot) by TAYLOR_1:16,XBOOLE_1:19;
  then
A6: Z c= dom (exp_R(#)(arctan+arccot)) by VALUED_1:def 4;
A7: exp_R is_differentiable_on Z by FDIFF_1:26,TAYLOR_1:16;
  for x st x in Z holds (exp_R(#)(arctan+arccot)`|Z).x = exp_R.x*(arctan.
  x+arccot.x)
  proof
    let x;
    assume
A8: x in Z;
    then (exp_R(#)(arctan+arccot)`|Z).x = ((arctan+arccot).x)*diff(exp_R,x)+
    exp_R.x*diff(arctan+arccot,x) by A6,A7,A2,FDIFF_1:21
      .= (arctan.x+arccot.x)*diff(exp_R,x)+exp_R.x*diff(arctan+arccot,x) by A5
,A8,VALUED_1:def 1
      .= (arctan.x+arccot.x)*exp_R.x+exp_R.x*diff(arctan+arccot,x) by
TAYLOR_1:16
      .= (arctan.x+arccot.x)*exp_R.x+exp_R.x*((arctan+arccot)`|Z).x by A2,A8,
FDIFF_1:def 7
      .= (arctan.x+arccot.x)*exp_R.x+exp_R.x*0 by A1,A8,Th37
      .= exp_R.x*(arctan.x+arccot.x);
    hence thesis;
  end;
  hence thesis by A6,A7,A2,FDIFF_1:21;
end;

::f.x=exp_R.x*(arctan.x-arccot.x)

theorem
  Z c= ].-1,1.[ implies exp_R(#)(arctan-arccot) is_differentiable_on Z &
  for x st x in Z holds ((exp_R(#)(arctan-arccot))`|Z).x = exp_R.x*(arctan.x-
  arccot.x)+2*exp_R.x/(1+x^2)
proof
  assume
A1: Z c= ].-1,1.[;
  then
A2: arctan-arccot is_differentiable_on Z by Th38;
A3: ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
  then ].-1,1.[ c= dom arccot by SIN_COS9:24,XBOOLE_1:1;
  then
A4: Z c= dom arccot by A1,XBOOLE_1:1;
  ].-1,1.[ c= dom arctan by A3,SIN_COS9:23,XBOOLE_1:1;
  then Z c= dom arctan by A1,XBOOLE_1:1;
  then Z c= dom arctan /\ dom arccot by A4,XBOOLE_1:19;
  then
A5: Z c= dom (arctan-arccot) by VALUED_1:12;
  then Z c= dom exp_R /\ dom (arctan-arccot) by TAYLOR_1:16,XBOOLE_1:19;
  then
A6: Z c= dom (exp_R(#)(arctan-arccot)) by VALUED_1:def 4;
A7: exp_R is_differentiable_on Z by FDIFF_1:26,TAYLOR_1:16;
  for x st x in Z holds (exp_R(#)(arctan-arccot)`|Z).x = exp_R.x*(arctan.
  x-arccot.x)+2*exp_R.x/(1+x^2)
  proof
    let x;
    assume
A8: x in Z;
    then (exp_R(#)(arctan-arccot)`|Z).x = ((arctan-arccot).x)*diff(exp_R,x)+
    exp_R.x*diff(arctan-arccot,x) by A6,A7,A2,FDIFF_1:21
      .= (arctan.x-arccot.x)*diff(exp_R,x)+exp_R.x*diff(arctan-arccot,x) by A5
,A8,VALUED_1:13
      .= (arctan.x-arccot.x)*exp_R.x+exp_R.x*diff(arctan-arccot,x) by
TAYLOR_1:16
      .= (arctan.x-arccot.x)*exp_R.x+exp_R.x*((arctan-arccot)`|Z).x by A2,A8,
FDIFF_1:def 7
      .= (arctan.x-arccot.x)*exp_R.x+exp_R.x*(2/(1+x^2)) by A1,A8,Th38
      .= exp_R.x*(arctan.x-arccot.x)+2*exp_R.x/(1+x^2);
    hence thesis;
  end;
  hence thesis by A6,A7,A2,FDIFF_1:21;
end;

::f.x=(arctan.x+arccot.x)/exp_R.x

theorem
  Z c= ].-1,1.[ implies (arctan+arccot)/exp_R is_differentiable_on Z &
  for x st x in Z holds (((arctan+arccot)/exp_R)`|Z).x = -(arctan.x+arccot.x)/
  exp_R.x
proof
  assume
A1: Z c= ].-1,1.[;
  then
A2: arctan+arccot is_differentiable_on Z by Th37;
A3: ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
  then ].-1,1.[ c= dom arccot by SIN_COS9:24,XBOOLE_1:1;
  then
A4: Z c= dom arccot by A1,XBOOLE_1:1;
  ].-1,1.[ c= dom arctan by A3,SIN_COS9:23,XBOOLE_1:1;
  then Z c= dom arctan by A1,XBOOLE_1:1;
  then Z c= dom arctan /\ dom arccot by A4,XBOOLE_1:19;
  then
A5: Z c= dom (arctan+arccot) by VALUED_1:def 1;
A6: exp_R is_differentiable_on Z & for x st x in Z holds exp_R.x<>0 by
FDIFF_1:26,SIN_COS:54,TAYLOR_1:16;
  then
A7: (arctan+arccot)/exp_R is_differentiable_on Z by A2,FDIFF_2:21;
  for x st x in Z holds (((arctan+arccot)/exp_R)`|Z).x = -(arctan.x+
  arccot.x)/exp_R.x
  proof
    let x;
A8: exp_R is_differentiable_in x by SIN_COS:65;
A9: exp_R.x <>0 by SIN_COS:54;
    assume
A10: x in Z;
    then
A11: arctan+arccot is_differentiable_in x by A2,FDIFF_1:9;
    (((arctan+arccot)/exp_R)`|Z).x = diff((arctan+arccot)/exp_R,x) by A7,A10,
FDIFF_1:def 7
      .= (diff(arctan+arccot,x)*exp_R.x-diff(exp_R,x)*(arctan+arccot).x) /(
    exp_R.x)^2 by A11,A8,A9,FDIFF_2:14
      .= (((arctan+arccot)`|Z).x*exp_R.x-diff(exp_R,x)*(arctan+arccot).x) /(
    exp_R.x)^2 by A2,A10,FDIFF_1:def 7
      .= (0*exp_R.x-diff(exp_R,x)*(arctan+arccot).x)/(exp_R.x)^2 by A1,A10,Th37
      .= -diff(exp_R,x)*(arctan+arccot).x/(exp_R.x)^2
      .= -exp_R.x*(arctan+arccot).x/(exp_R.x)^2 by SIN_COS:65
      .= -(arctan.x+arccot.x)*exp_R.x/(exp_R.x*exp_R.x) by A5,A10,
VALUED_1:def 1
      .= -(arctan.x+arccot.x)*(exp_R.x/(exp_R.x*exp_R.x))
      .= -(arctan.x+arccot.x)*(exp_R.x/exp_R.x/exp_R.x) by XCMPLX_1:78
      .= -(arctan.x+arccot.x)*(1/exp_R.x) by A9,XCMPLX_1:60
      .= -(arctan.x+arccot.x)/exp_R.x;
    hence thesis;
  end;
  hence thesis by A2,A6,FDIFF_2:21;
end;

::f.x=(arctan.x-arccot.x)/exp_R.x

theorem
  Z c= ].-1,1.[ implies (arctan-arccot)/exp_R is_differentiable_on Z &
  for x st x in Z holds (((arctan-arccot)/exp_R)`|Z).x = ((2/(1+x^2))-arctan.x+
  arccot.x)/exp_R.x
proof
  assume
A1: Z c= ].-1,1.[;
  then
A2: arctan-arccot is_differentiable_on Z by Th38;
A3: ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
  then ].-1,1.[ c= dom arccot by SIN_COS9:24,XBOOLE_1:1;
  then
A4: Z c= dom arccot by A1,XBOOLE_1:1;
  ].-1,1.[ c= dom arctan by A3,SIN_COS9:23,XBOOLE_1:1;
  then Z c= dom arctan by A1,XBOOLE_1:1;
  then Z c= dom arctan /\ dom arccot by A4,XBOOLE_1:19;
  then
A5: Z c= dom (arctan-arccot) by VALUED_1:12;
A6: exp_R is_differentiable_on Z & for x st x in Z holds exp_R.x<>0 by
FDIFF_1:26,SIN_COS:54,TAYLOR_1:16;
  then
A7: (arctan-arccot)/exp_R is_differentiable_on Z by A2,FDIFF_2:21;
  for x st x in Z holds (((arctan-arccot)/exp_R)`|Z).x = ((2/(1+x^2))-
  arctan.x+arccot.x)/exp_R.x
  proof
    let x;
A8: exp_R is_differentiable_in x by SIN_COS:65;
A9: exp_R.x <>0 by SIN_COS:54;
    assume
A10: x in Z;
    then
A11: arctan-arccot is_differentiable_in x by A2,FDIFF_1:9;
    (((arctan-arccot)/exp_R)`|Z).x = diff((arctan-arccot)/exp_R,x) by A7,A10,
FDIFF_1:def 7
      .= (diff(arctan-arccot,x)*exp_R.x-diff(exp_R,x)*(arctan-arccot).x) /(
    exp_R.x)^2 by A11,A8,A9,FDIFF_2:14
      .= (((arctan-arccot)`|Z).x*exp_R.x-diff(exp_R,x)*(arctan-arccot).x) /(
    exp_R.x)^2 by A2,A10,FDIFF_1:def 7
      .= ((2/(1+x^2))*exp_R.x-diff(exp_R,x)*(arctan-arccot).x)/(exp_R.x)^2
    by A1,A10,Th38
      .= ((2/(1+x^2))*exp_R.x-exp_R.x*(arctan-arccot).x)/(exp_R.x)^2 by
SIN_COS:65
      .= ((2/(1+x^2))*exp_R.x-exp_R.x*(arctan.x-arccot.x))/(exp_R.x)^2 by A5
,A10,VALUED_1:13
      .= ((2/(1+x^2))-(arctan.x-arccot.x))*(exp_R.x/(exp_R.x*exp_R.x))
      .= ((2/(1+x^2))-(arctan.x-arccot.x))*(exp_R.x/exp_R.x/exp_R.x) by
XCMPLX_1:78
      .= ((2/(1+x^2))-(arctan.x-arccot.x))*(1/exp_R.x) by A9,XCMPLX_1:60
      .= ((2/(1+x^2))-arctan.x+arccot.x)/exp_R.x;
    hence thesis;
  end;
  hence thesis by A2,A6,FDIFF_2:21;
end;

::f.x=exp_R.(arctan.x+arccot.x)

theorem
  Z c= dom (exp_R*(arctan+arccot)) & Z c= ].-1,1.[ implies exp_R*(arctan
+arccot) is_differentiable_on Z & for x st x in Z holds (exp_R*(arctan+arccot)
  `|Z).x = 0
proof
  assume that
A1: Z c= dom (exp_R*(arctan+arccot)) and
A2: Z c= ].-1,1.[;
A3: arctan+arccot is_differentiable_on Z by A2,Th37;
A4: for x st x in Z holds exp_R*(arctan+arccot) is_differentiable_in x
  proof
    let x;
    assume x in Z;
    then
A5: (arctan+arccot) is_differentiable_in x by A3,FDIFF_1:9;
    exp_R is_differentiable_in (arctan+arccot).x by SIN_COS:65;
    hence thesis by A5,FDIFF_2:13;
  end;
  then
A6: exp_R*(arctan+arccot) is_differentiable_on Z by A1,FDIFF_1:9;
  for x st x in Z holds (exp_R*(arctan+arccot)`|Z).x = 0
  proof
    let x;
A7: exp_R is_differentiable_in (arctan+arccot).x by SIN_COS:65;
    assume
A8: x in Z;
    then
A9: arctan+arccot is_differentiable_in x by A3,FDIFF_1:9;
    (exp_R*(arctan+arccot)`|Z).x = diff(exp_R*(arctan+arccot),x) by A6,A8,
FDIFF_1:def 7
      .= diff(exp_R,(arctan+arccot).x)*diff((arctan+arccot),x) by A9,A7,
FDIFF_2:13
      .= exp_R.((arctan+arccot).x)*diff((arctan+arccot),x) by SIN_COS:65
      .= exp_R.((arctan+arccot).x)*((arctan+arccot)`|Z).x by A3,A8,
FDIFF_1:def 7
      .= exp_R.((arctan+arccot).x)*0 by A2,A8,Th37
      .= 0;
    hence thesis;
  end;
  hence thesis by A1,A4,FDIFF_1:9;
end;

::f.x=exp_R.(arctan.x-arccot.x)

theorem
  Z c= dom (exp_R*(arctan-arccot)) & Z c= ].-1,1.[ implies exp_R*(arctan
-arccot) is_differentiable_on Z & for x st x in Z holds (exp_R*(arctan-arccot)
  `|Z).x = 2*exp_R.(arctan.x-arccot.x)/(1+x^2)
proof
  assume that
A1: Z c= dom (exp_R*(arctan-arccot)) and
A2: Z c= ].-1,1.[;
A3: ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
  then ].-1,1.[ c= dom arccot by SIN_COS9:24,XBOOLE_1:1;
  then
A4: Z c= dom arccot by A2,XBOOLE_1:1;
  ].-1,1.[ c= dom arctan by A3,SIN_COS9:23,XBOOLE_1:1;
  then Z c= dom arctan by A2,XBOOLE_1:1;
  then Z c= dom arctan /\ dom arccot by A4,XBOOLE_1:19;
  then
A5: Z c= dom (arctan-arccot) by VALUED_1:12;
A6: arctan-arccot is_differentiable_on Z by A2,Th38;
A7: for x st x in Z holds exp_R*(arctan-arccot) is_differentiable_in x
  proof
    let x;
    assume x in Z;
    then
A8: (arctan-arccot) is_differentiable_in x by A6,FDIFF_1:9;
    exp_R is_differentiable_in (arctan-arccot).x by SIN_COS:65;
    hence thesis by A8,FDIFF_2:13;
  end;
  then
A9: exp_R*(arctan-arccot) is_differentiable_on Z by A1,FDIFF_1:9;
  for x st x in Z holds (exp_R*(arctan-arccot)`|Z).x = 2*exp_R.(arctan.x-
  arccot.x)/(1+x^2)
  proof
    let x;
A10: exp_R is_differentiable_in (arctan-arccot).x by SIN_COS:65;
    assume
A11: x in Z;
    then
A12: arctan-arccot is_differentiable_in x by A6,FDIFF_1:9;
    (exp_R*(arctan-arccot)`|Z).x = diff(exp_R*(arctan-arccot),x) by A9,A11,
FDIFF_1:def 7
      .= diff(exp_R,(arctan-arccot).x)*diff((arctan-arccot),x) by A12,A10,
FDIFF_2:13
      .= exp_R.((arctan-arccot).x)*diff((arctan-arccot),x) by SIN_COS:65
      .= exp_R.((arctan-arccot).x)*((arctan-arccot)`|Z).x by A6,A11,
FDIFF_1:def 7
      .= exp_R.((arctan-arccot).x)*(2/(1+x^2)) by A2,A11,Th38
      .= exp_R.(arctan.x-arccot.x)*(2/(1+x^2)) by A5,A11,VALUED_1:13
      .= 2*exp_R.(arctan.x-arccot.x)/(1+x^2);
    hence thesis;
  end;
  hence thesis by A1,A7,FDIFF_1:9;
end;

::f.x=sin.(arctan.x+arccot.x)

theorem
  Z c= dom (sin*(arctan+arccot)) & Z c= ].-1,1.[ implies sin*(arctan+
arccot) is_differentiable_on Z & for x st x in Z holds (sin*(arctan+arccot)`|Z)
  .x = 0
proof
  assume that
A1: Z c= dom (sin*(arctan+arccot)) and
A2: Z c= ].-1,1.[;
A3: arctan+arccot is_differentiable_on Z by A2,Th37;
A4: for x st x in Z holds sin*(arctan+arccot) is_differentiable_in x
  proof
    let x;
    assume x in Z;
    then
A5: (arctan+arccot) is_differentiable_in x by A3,FDIFF_1:9;
    sin is_differentiable_in (arctan+arccot).x by SIN_COS:64;
    hence thesis by A5,FDIFF_2:13;
  end;
  then
A6: sin*(arctan+arccot) is_differentiable_on Z by A1,FDIFF_1:9;
  for x st x in Z holds (sin*(arctan+arccot)`|Z).x = 0
  proof
    let x;
A7: sin is_differentiable_in (arctan+arccot).x by SIN_COS:64;
    assume
A8: x in Z;
    then
A9: arctan+arccot is_differentiable_in x by A3,FDIFF_1:9;
    (sin*(arctan+arccot)`|Z).x = diff(sin*(arctan+arccot),x) by A6,A8,
FDIFF_1:def 7
      .= diff(sin,(arctan+arccot).x)*diff((arctan+arccot),x) by A9,A7,
FDIFF_2:13
      .= cos.((arctan+arccot).x)*diff((arctan+arccot),x) by SIN_COS:64
      .= cos.((arctan+arccot).x)*((arctan+arccot)`|Z).x by A3,A8,FDIFF_1:def 7
      .= cos.((arctan+arccot).x)*0 by A2,A8,Th37
      .= 0;
    hence thesis;
  end;
  hence thesis by A1,A4,FDIFF_1:9;
end;

::f.x=sin.(arctan.x-arccot.x)

theorem
  Z c= dom (sin*(arctan-arccot)) & Z c= ].-1,1.[ implies sin*(arctan-
arccot) is_differentiable_on Z & for x st x in Z holds (sin*(arctan-arccot)`|Z)
  .x = 2*cos.(arctan.x-arccot.x)/(1+x^2)
proof
  assume that
A1: Z c= dom (sin*(arctan-arccot)) and
A2: Z c= ].-1,1.[;
A3: ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
  then ].-1,1.[ c= dom arccot by SIN_COS9:24,XBOOLE_1:1;
  then
A4: Z c= dom arccot by A2,XBOOLE_1:1;
  ].-1,1.[ c= dom arctan by A3,SIN_COS9:23,XBOOLE_1:1;
  then Z c= dom arctan by A2,XBOOLE_1:1;
  then Z c= dom arctan /\ dom arccot by A4,XBOOLE_1:19;
  then
A5: Z c= dom (arctan-arccot) by VALUED_1:12;
A6: arctan-arccot is_differentiable_on Z by A2,Th38;
A7: for x st x in Z holds sin*(arctan-arccot) is_differentiable_in x
  proof
    let x;
    assume x in Z;
    then
A8: (arctan-arccot) is_differentiable_in x by A6,FDIFF_1:9;
    sin is_differentiable_in (arctan-arccot).x by SIN_COS:64;
    hence thesis by A8,FDIFF_2:13;
  end;
  then
A9: sin*(arctan-arccot) is_differentiable_on Z by A1,FDIFF_1:9;
  for x st x in Z holds (sin*(arctan-arccot)`|Z).x = 2*cos.(arctan.x-
  arccot.x)/(1+x^2)
  proof
    let x;
A10: sin is_differentiable_in (arctan-arccot).x by SIN_COS:64;
    assume
A11: x in Z;
    then
A12: arctan-arccot is_differentiable_in x by A6,FDIFF_1:9;
    (sin*(arctan-arccot)`|Z).x = diff(sin*(arctan-arccot),x) by A9,A11,
FDIFF_1:def 7
      .= diff(sin,(arctan-arccot).x)*diff((arctan-arccot),x) by A12,A10,
FDIFF_2:13
      .= cos.((arctan-arccot).x)*diff((arctan-arccot),x) by SIN_COS:64
      .= cos.((arctan-arccot).x)*((arctan-arccot)`|Z).x by A6,A11,FDIFF_1:def 7
      .= cos.((arctan-arccot).x)*(2/(1+x^2)) by A2,A11,Th38
      .= cos.(arctan.x-arccot.x)*(2/(1+x^2)) by A5,A11,VALUED_1:13
      .= 2*cos.(arctan.x-arccot.x)/(1+x^2);
    hence thesis;
  end;
  hence thesis by A1,A7,FDIFF_1:9;
end;

::f.x=cos.(arctan.x+arccot.x)

theorem
  Z c= dom (cos*(arctan+arccot)) & Z c= ].-1,1.[ implies cos*(arctan+
arccot) is_differentiable_on Z & for x st x in Z holds (cos*(arctan+arccot)`|Z)
  .x = 0
proof
  assume that
A1: Z c= dom (cos*(arctan+arccot)) and
A2: Z c= ].-1,1.[;
A3: arctan+arccot is_differentiable_on Z by A2,Th37;
A4: for x st x in Z holds cos*(arctan+arccot) is_differentiable_in x
  proof
    let x;
    assume x in Z;
    then
A5: (arctan+arccot) is_differentiable_in x by A3,FDIFF_1:9;
    cos is_differentiable_in (arctan+arccot).x by SIN_COS:63;
    hence thesis by A5,FDIFF_2:13;
  end;
  then
A6: cos*(arctan+arccot) is_differentiable_on Z by A1,FDIFF_1:9;
  for x st x in Z holds (cos*(arctan+arccot)`|Z).x = 0
  proof
    let x;
A7: cos is_differentiable_in (arctan+arccot).x by SIN_COS:63;
    assume
A8: x in Z;
    then
A9: arctan+arccot is_differentiable_in x by A3,FDIFF_1:9;
    (cos*(arctan+arccot)`|Z).x = diff(cos*(arctan+arccot),x) by A6,A8,
FDIFF_1:def 7
      .= diff(cos,(arctan+arccot).x)*diff((arctan+arccot),x) by A9,A7,
FDIFF_2:13
      .= (-sin.((arctan+arccot).x))*diff((arctan+arccot),x) by SIN_COS:63
      .= (-sin.((arctan+arccot).x))*((arctan+arccot)`|Z).x by A3,A8,
FDIFF_1:def 7
      .= (-sin.((arctan+arccot).x))*0 by A2,A8,Th37
      .= 0;
    hence thesis;
  end;
  hence thesis by A1,A4,FDIFF_1:9;
end;

::f.x=cos.(arctan.x-arccot.x)

theorem
  Z c= dom (cos*(arctan-arccot)) & Z c= ].-1,1.[ implies cos*(arctan-
arccot) is_differentiable_on Z & for x st x in Z holds (cos*(arctan-arccot)`|Z)
  .x = -2*sin.(arctan.x-arccot.x)/(1+x^2)
proof
  assume that
A1: Z c= dom (cos*(arctan-arccot)) and
A2: Z c= ].-1,1.[;
A3: ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
  then ].-1,1.[ c= dom arccot by SIN_COS9:24,XBOOLE_1:1;
  then
A4: Z c= dom arccot by A2,XBOOLE_1:1;
  ].-1,1.[ c= dom arctan by A3,SIN_COS9:23,XBOOLE_1:1;
  then Z c= dom arctan by A2,XBOOLE_1:1;
  then Z c= dom arctan /\ dom arccot by A4,XBOOLE_1:19;
  then
A5: Z c= dom (arctan-arccot) by VALUED_1:12;
A6: arctan-arccot is_differentiable_on Z by A2,Th38;
A7: for x st x in Z holds cos*(arctan-arccot) is_differentiable_in x
  proof
    let x;
    assume x in Z;
    then
A8: (arctan-arccot) is_differentiable_in x by A6,FDIFF_1:9;
    cos is_differentiable_in (arctan-arccot).x by SIN_COS:63;
    hence thesis by A8,FDIFF_2:13;
  end;
  then
A9: cos*(arctan-arccot) is_differentiable_on Z by A1,FDIFF_1:9;
  for x st x in Z holds (cos*(arctan-arccot)`|Z).x = -2*sin.(arctan.x-
  arccot.x)/(1+x^2)
  proof
    let x;
A10: cos is_differentiable_in (arctan-arccot).x by SIN_COS:63;
    assume
A11: x in Z;
    then
A12: arctan-arccot is_differentiable_in x by A6,FDIFF_1:9;
    (cos*(arctan-arccot)`|Z).x = diff(cos*(arctan-arccot),x) by A9,A11,
FDIFF_1:def 7
      .= diff(cos,(arctan-arccot).x)*diff((arctan-arccot),x) by A12,A10,
FDIFF_2:13
      .= (-sin.((arctan-arccot).x))*diff((arctan-arccot),x) by SIN_COS:63
      .= (-sin.((arctan-arccot).x))*((arctan-arccot)`|Z).x by A6,A11,
FDIFF_1:def 7
      .= (-sin.((arctan-arccot).x))*(2/(1+x^2)) by A2,A11,Th38
      .= (-sin.(arctan.x-arccot.x))*(2/(1+x^2)) by A5,A11,VALUED_1:13
      .= -2*sin.(arctan.x-arccot.x)/(1+x^2);
    hence thesis;
  end;
  hence thesis by A1,A7,FDIFF_1:9;
end;

::f.x=arctan.x*arccot.x

theorem
  Z c= ].-1,1.[ implies arctan(#)arccot is_differentiable_on Z & for x
  st x in Z holds ((arctan(#)arccot)`|Z).x = (arccot.x-arctan.x)/(1+x^2)
proof
  assume
A1: Z c= ].-1,1.[;
  then
A2: arctan is_differentiable_on Z by SIN_COS9:81;
A3: ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
  then ].-1,1.[ c= dom arccot by SIN_COS9:24,XBOOLE_1:1;
  then
A4: Z c= dom arccot by A1,XBOOLE_1:1;
A5: arccot is_differentiable_on Z by A1,SIN_COS9:82;
  ].-1,1.[ c= dom arctan by A3,SIN_COS9:23,XBOOLE_1:1;
  then Z c= dom arctan by A1,XBOOLE_1:1;
  then Z c= dom arctan /\ dom arccot by A4,XBOOLE_1:19;
  then
A6: Z c= dom(arctan(#)arccot) by VALUED_1:def 4;
  for x st x in Z holds ((arctan(#)arccot)`|Z).x = (arccot.x-arctan.x)/(1 +x^2)
  proof
    let x;
    assume
A7: x in Z;
    then
    ((arctan(#)arccot)`|Z).x = (arccot.x)*diff(arctan,x)+(arctan.x)*diff(
    arccot,x) by A6,A2,A5,FDIFF_1:21
      .= arccot.x*((arctan)`|Z).x+arctan.x*diff(arccot,x) by A2,A7,
FDIFF_1:def 7
      .= arccot.x*(1/(1+x^2))+arctan.x*diff(arccot,x) by A1,A7,SIN_COS9:81
      .= arccot.x*(1/(1+x^2))+arctan.x*((arccot)`|Z).x by A5,A7,FDIFF_1:def 7
      .= arccot.x*(1/(1+x^2))+arctan.x*(-1/(1+x^2)) by A1,A7,SIN_COS9:82
      .= (arccot.x-arctan.x)/(1+x^2);
    hence thesis;
  end;
  hence thesis by A6,A2,A5,FDIFF_1:21;
end;

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

theorem
  not 0 in Z & Z c= dom((arctan*((id Z)^))(#)(arccot*((id Z)^))) & (for
x st x in Z holds ((id Z)^).x > -1 & ((id Z)^).x < 1) implies (arctan*((id Z)^)
)(#)(arccot*((id Z)^)) is_differentiable_on Z & for x st x in Z holds (((arctan
  *((id Z)^))(#)(arccot*((id Z)^)))`|Z).x = (arctan.(1/x)-arccot.(1/x))/(1+x^2)
proof
  set f = id Z;
  assume that
A1: not 0 in Z and
A2: Z c= dom((arctan*(f^))(#)(arccot*(f^))) and
A3: for x st x in Z holds (f^).x > -1 & (f^).x < 1;
A4: Z c= dom(arctan*(f^)) /\ dom(arccot*(f^)) by A2,VALUED_1:def 4;
  then
A5: Z c= dom (arctan*(f^)) by XBOOLE_1:18;
  then
A6: arctan*(f^) is_differentiable_on Z by A1,A3,SIN_COS9:111;
A7: Z c= dom (arccot*(f^)) by A4,XBOOLE_1:18;
  then
A8: arccot*(f^) is_differentiable_on Z by A1,A3,SIN_COS9:112;
  for y st y in Z holds y in dom (f^) by A5,FUNCT_1:11;
  then
A9: Z c= dom (f^) by TARSKI:def 3;
  for x st x in Z holds (((arctan*(f^))(#)(arccot*(f^)))`|Z).x = (arctan.
  (1/x)-arccot.(1/x))/(1+x^2)
  proof
    let x;
    assume
A10: x in Z;
    then (((arctan*(f^))(#)(arccot*(f^)))`|Z).x = ((arccot*(f^)).x)*diff((
    arctan*(f^)),x)+ ((arctan*(f^)).x)*diff(arccot*(f^),x) by A2,A6,A8,
FDIFF_1:21
      .= ((arccot*(f^)).x)*((arctan*(f^))`|Z).x+ ((arctan*(f^)).x)*diff(
    arccot*(f^),x) by A6,A10,FDIFF_1:def 7
      .= ((arccot*(f^)).x)*(-1/(1+x^2))+((arctan*(f^)).x)*diff(arccot*(f^),x
    ) by A1,A3,A5,A10,SIN_COS9:111
      .= ((arccot*(f^)).x)*(-1/(1+x^2))+((arctan*(f^)).x)*((arccot*(f^))`|Z)
    .x by A8,A10,FDIFF_1:def 7
      .= ((arccot*(f^)).x)*(-1/(1+x^2))+((arctan*(f^)).x)*(1/(1+x^2)) by A1,A3
,A7,A10,SIN_COS9:112
      .= (arccot.((f^).x))*(-1/(1+x^2))+((arctan*(f^)).x)*(1/(1+x^2)) by A7,A10
,FUNCT_1:12
      .= (arccot.((f.x)"))*(-1/(1+x^2))+((arctan*(f^)).x)*(1/(1+x^2)) by A9,A10
,RFUNCT_1:def 2
      .= (arccot.(1/x))*(-1/(1+x^2))+((arctan*(f^)).x)*(1/(1+x^2)) by A10,
FUNCT_1:18
      .= (arccot.(1/x))*(-1/(1+x^2))+(arctan.((f^).x))*(1/(1+x^2)) by A5,A10,
FUNCT_1:12
      .= (arccot.(1/x))*(-1/(1+x^2))+(arctan.((f.x)"))*(1/(1+x^2)) by A9,A10,
RFUNCT_1:def 2
      .= -(arccot.(1/x))*(1/(1+x^2))+(arctan.(1/x))*(1/(1+x^2)) by A10,
FUNCT_1:18
      .= (arctan.(1/x)-arccot.(1/x))/(1+x^2);
    hence thesis;
  end;
  hence thesis by A2,A6,A8,FDIFF_1:21;
end;

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

theorem
  not 0 in Z & Z c= dom ((id Z)(#)(arctan*((id Z)^))) & (for x st x in Z
  holds ((id Z)^).x > -1 & ((id Z)^).x < 1) implies (id Z)(#)(arctan*((id Z)^))
is_differentiable_on Z & for x st x in Z holds (((id Z)(#)(arctan*((id Z)^)))`|
  Z).x = arctan.(1/x)-x/(1+x^2)
proof
  set f = id Z;
  assume that
A1: not 0 in Z and
A2: Z c= dom ((id Z)(#)(arctan*(f^))) and
A3: for x st x in Z holds (f^).x > -1 & (f^).x < 1;
A4: Z c= dom (id Z) /\ dom (arctan*(f^)) by A2,VALUED_1:def 4;
  then
A5: Z c= dom (arctan*(f^)) by XBOOLE_1:18;
  then
A6: arctan*(f^) is_differentiable_on Z by A1,A3,SIN_COS9:111;
A7: for x st x in Z holds (id Z).x = 1*x+0 by FUNCT_1:18;
A8: Z c= dom id Z by A4,XBOOLE_1:18;
  then
A9: id Z is_differentiable_on Z by A7,FDIFF_1:23;
  for y st y in Z holds y in dom (f^) by A5,FUNCT_1:11;
  then
A10: Z c= dom (f^) by TARSKI:def 3;
  for x st x in Z holds (((id Z)(#)(arctan*(f^)))`|Z).x = arctan.(1/x)-x/
  (1+x^2)
  proof
    let x;
    assume
A11: x in Z;
    then
    (((id Z)(#)(arctan*(f^)))`|Z).x = ((arctan*(f^)).x)*diff((id Z),x)+((
    id Z).x)*diff(arctan*(f^),x) by A2,A6,A9,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 A8,A7,A11,
FDIFF_1:23
      .= ((arctan*(f^)).x)*1+x*diff(arctan*(f^),x) by A11,FUNCT_1:18
      .= (arctan*(f^)).x+x*(((arctan*(f^))`|Z).x) by A6,A11,FDIFF_1:def 7
      .= (arctan*(f^)).x+x*(-1/(1+x^2)) by A1,A3,A5,A11,SIN_COS9:111
      .= arctan.((f^).x)-x/(1+x^2) by A5,A11,FUNCT_1:12
      .= arctan.((f.x)")-x/(1+x^2) by A10,A11,RFUNCT_1:def 2
      .= arctan.(1/x)-x/(1+x^2) by A11,FUNCT_1:18;
    hence thesis;
  end;
  hence thesis by A2,A6,A9,FDIFF_1:21;
end;

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

theorem
  not 0 in Z & Z c= dom ((id Z)(#)(arccot*((id Z)^))) & (for x st x in Z
  holds ((id Z)^).x > -1 & ((id Z)^).x < 1) implies (id Z)(#)(arccot*((id Z)^))
is_differentiable_on Z & for x st x in Z holds (((id Z)(#)(arccot*((id Z)^)))`|
  Z).x = arccot.(1/x)+x/(1+x^2)
proof
  set f = id Z;
  assume that
A1: not 0 in Z and
A2: Z c= dom ((id Z)(#)(arccot*(f^))) and
A3: for x st x in Z holds (f^).x > -1 & (f^).x < 1;
A4: Z c= dom (id Z) /\ dom (arccot*(f^)) by A2,VALUED_1:def 4;
  then
A5: Z c= dom (arccot*(f^)) by XBOOLE_1:18;
  then
A6: arccot*(f^) is_differentiable_on Z by A1,A3,SIN_COS9:112;
A7: for x st x in Z holds (id Z).x = 1*x+0 by FUNCT_1:18;
A8: Z c= dom id Z by A4,XBOOLE_1:18;
  then
A9: id Z is_differentiable_on Z by A7,FDIFF_1:23;
  for y st y in Z holds y in dom (f^) by A5,FUNCT_1:11;
  then
A10: Z c= dom (f^) by TARSKI:def 3;
  for x st x in Z holds (((id Z)(#)(arccot*(f^)))`|Z).x = arccot.(1/x)+x/
  (1+x^2)
  proof
    let x;
    assume
A11: x in Z;
    then
    (((id Z)(#)(arccot*(f^)))`|Z).x = ((arccot*(f^)).x)*diff((id Z),x)+((
    id Z).x)*diff(arccot*(f^),x) by A2,A6,A9,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 A8,A7,A11,
FDIFF_1:23
      .= ((arccot*(f^)).x)*1+x*diff(arccot*(f^),x) by A11,FUNCT_1:18
      .= (arccot*(f^)).x+x*(((arccot*(f^))`|Z).x) by A6,A11,FDIFF_1:def 7
      .= (arccot*(f^)).x+x*(1/(1+x^2)) by A1,A3,A5,A11,SIN_COS9:112
      .= arccot.((f^).x)+x/(1+x^2) by A5,A11,FUNCT_1:12
      .= arccot.((f.x)")+x/(1+x^2) by A10,A11,RFUNCT_1:def 2
      .= arccot.(1/x)+x/(1+x^2) by A11,FUNCT_1:18;
    hence thesis;
  end;
  hence thesis by A2,A6,A9,FDIFF_1:21;
end;

::f.x=x^2*arctan(1/x)

theorem
  not 0 in Z & Z c= dom (g(#)(arctan*((id Z)^))) & g=#Z 2 & (for x st x
  in Z holds ((id Z)^).x > -1 & ((id Z)^).x < 1) implies g(#)(arctan*((id Z)^))
is_differentiable_on Z & for x st x in Z holds ((g(#)(arctan*((id Z)^)))`|Z).x
  = 2*x*arctan.(1/x)-x^2/(1+x^2)
proof
  set f = id Z;
  assume that
A1: not 0 in Z and
A2: Z c= dom (g(#)(arctan*(f^))) and
A3: g=#Z 2 and
A4: for x st x in Z holds (f^).x > -1 & (f^).x < 1;
A5: for x st x in Z holds g is_differentiable_in x by A3,TAYLOR_1:2;
A6: Z c= dom g /\ dom (arctan*(f^)) by A2,VALUED_1:def 4;
  then
A7: Z c= dom (arctan*(f^)) by XBOOLE_1:18;
  then
A8: arctan*(f^) is_differentiable_on Z by A1,A4,SIN_COS9:111;
  Z c= dom g by A6,XBOOLE_1:18;
  then
A9: g is_differentiable_on Z by A5,FDIFF_1:9;
A10: for x st x in Z holds (g`|Z).x = 2*x
  proof
    let x;
    assume x in Z;
    then (g`|Z).x = diff(g,x) by A9,FDIFF_1:def 7
      .= 2*(x #Z (2-1)) by A3,TAYLOR_1:2
      .= 2*x by PREPOWER:35;
    hence thesis;
  end;
  for y st y in Z holds y in dom (f^) by A7,FUNCT_1:11;
  then
A11: Z c= dom (f^) by TARSKI:def 3;
  for x st x in Z holds ((g(#)(arctan*(f^)))`|Z).x = 2*x*arctan.(1/x)-x^2
  /(1+x^2)
  proof
    let x;
    assume
A12: x in Z;
    then ((g(#)(arctan*(f^)))`|Z).x = ((arctan*(f^)).x)*diff(g,x)+(g.x)*diff(
    arctan*(f^),x) by A2,A8,A9,FDIFF_1:21
      .= ((arctan*(f^)).x)*(g`|Z).x+(g.x)*diff(arctan*(f^),x) by A9,A12,
FDIFF_1:def 7
      .= ((arctan*(f^)).x)*(2*x)+(g.x)*diff(arctan*(f^),x) by A10,A12
      .= ((arctan*(f^)).x)*(2*x)+(x #Z 2)*diff(arctan*(f^),x) by A3,
TAYLOR_1:def 1
      .= ((arctan*(f^)).x)*(2*x)+(x #Z 2)*(((arctan*(f^))`|Z).x ) by A8,A12,
FDIFF_1:def 7
      .= ((arctan*(f^)).x)*(2*x)+(x #Z (1+1))*(-1/(1+x^2)) by A1,A4,A7,A12,
SIN_COS9:111
      .= ((arctan*(f^)).x)*(2*x)+((x #Z 1)*(x #Z 1))*(-1/(1+x^2)) by TAYLOR_1:1
      .= ((arctan*(f^)).x)*(2*x)+(x*(x #Z 1))*(-1/(1+x^2)) by PREPOWER:35
      .= ((arctan*(f^)).x)*(2*x)+x^2*(-1/(1+x^2)) by PREPOWER:35
      .= arctan.((f^).x)*(2*x)-x^2/(1+x^2) by A7,A12,FUNCT_1:12
      .= arctan.((f.x)")*(2*x)-x^2/(1+x^2) by A11,A12,RFUNCT_1:def 2
      .= 2*x*arctan.(1/x)-x^2/(1+x^2) by A12,FUNCT_1:18;
    hence thesis;
  end;
  hence thesis by A2,A8,A9,FDIFF_1:21;
end;

::f.x=x^2*arccot(1/x)

theorem
  not 0 in Z & Z c= dom (g(#)(arccot*((id Z)^))) & g=#Z 2 & (for x st x
  in Z holds ((id Z)^).x > -1 & ((id Z)^).x < 1) implies g(#)(arccot*((id Z)^))
is_differentiable_on Z & for x st x in Z holds ((g(#)(arccot*((id Z)^)))`|Z).x
  = 2*x*arccot.(1/x)+x^2/(1+x^2)
proof
  set f = id Z;
  assume that
A1: not 0 in Z and
A2: Z c= dom (g(#)(arccot*(f^))) and
A3: g=#Z 2 and
A4: for x st x in Z holds (f^).x > -1 & (f^).x < 1;
A5: for x st x in Z holds g is_differentiable_in x by A3,TAYLOR_1:2;
A6: Z c= dom g /\ dom (arccot*(f^)) by A2,VALUED_1:def 4;
  then
A7: Z c= dom (arccot*(f^)) by XBOOLE_1:18;
  then
A8: arccot*(f^) is_differentiable_on Z by A1,A4,SIN_COS9:112;
  Z c= dom g by A6,XBOOLE_1:18;
  then
A9: g is_differentiable_on Z by A5,FDIFF_1:9;
A10: for x st x in Z holds (g`|Z).x = 2*x
  proof
    let x;
    assume x in Z;
    then (g`|Z).x = diff(g,x) by A9,FDIFF_1:def 7
      .= 2*(x #Z (2-1)) by A3,TAYLOR_1:2
      .= 2*x by PREPOWER:35;
    hence thesis;
  end;
  for y st y in Z holds y in dom (f^) by A7,FUNCT_1:11;
  then
A11: Z c= dom (f^) by TARSKI:def 3;
  for x st x in Z holds ((g(#)(arccot*(f^)))`|Z).x = 2*x*arccot.(1/x)+x^2
  /(1+x^2)
  proof
    let x;
    assume
A12: x in Z;
    then ((g(#)(arccot*(f^)))`|Z).x = ((arccot*(f^)).x)*diff(g,x)+(g.x)*diff(
    arccot*(f^),x) by A2,A8,A9,FDIFF_1:21
      .= ((arccot*(f^)).x)*(g`|Z).x+(g.x)*diff(arccot*(f^),x) by A9,A12,
FDIFF_1:def 7
      .= ((arccot*(f^)).x)*(2*x)+(g.x)*diff(arccot*(f^),x) by A10,A12
      .= ((arccot*(f^)).x)*(2*x)+(x #Z 2)*diff(arccot*(f^),x) by A3,
TAYLOR_1:def 1
      .= ((arccot*(f^)).x)*(2*x)+(x #Z 2)*(((arccot*(f^))`|Z).x ) by A8,A12,
FDIFF_1:def 7
      .= ((arccot*(f^)).x)*(2*x)+(x #Z (1+1))*(1/(1+x^2)) by A1,A4,A7,A12,
SIN_COS9:112
      .= ((arccot*(f^)).x)*(2*x)+((x #Z 1)*(x #Z 1))*(1/(1+x^2)) by TAYLOR_1:1
      .= ((arccot*(f^)).x)*(2*x)+(x*(x #Z 1))*(1/(1+x^2)) by PREPOWER:35
      .= ((arccot*(f^)).x)*(2*x)+x^2/(1+x^2) by PREPOWER:35
      .= arccot.((f^).x)*(2*x)+x^2/(1+x^2) by A7,A12,FUNCT_1:12
      .= arccot.((f.x)")*(2*x)+x^2/(1+x^2) by A11,A12,RFUNCT_1:def 2
      .= 2*x*arccot.(1/x)+x^2/(1+x^2) by A12,FUNCT_1:18;
    hence thesis;
  end;
  hence thesis by A2,A8,A9,FDIFF_1:21;
end;

::f.x=1/arctan.x

theorem Th67:
  Z c= ].-1,1.[ & (for x st x in Z holds arctan.x<>0) implies
arctan^ is_differentiable_on Z & for x st x in Z holds ((arctan^)`|Z).x = -1/((
  arctan.x)^2*(1+x^2))
proof
  assume that
A1: Z c= ].-1,1.[ and
A2: for x st x in Z holds arctan.x<>0;
A3: arctan is_differentiable_on Z by A1,SIN_COS9:81;
  then
A4: arctan^ is_differentiable_on Z by A2,FDIFF_2:22;
  for x st x in Z holds ((arctan^)`|Z).x = -1/((arctan.x)^2*(1+x^2))
  proof
    let x;
    assume
A5: x in Z;
    then
A6: arctan.x<>0 & arctan is_differentiable_in x by A2,A3,FDIFF_1:9;
    ((arctan^)`|Z).x = diff(arctan^,x) by A4,A5,FDIFF_1:def 7
      .= -diff(arctan,x)/(arctan.x)^2 by A6,FDIFF_2:15
      .= -((arctan)`|Z).x/(arctan.x)^2 by A3,A5,FDIFF_1:def 7
      .= -(1/(1+x^2))/(arctan.x)^2 by A1,A5,SIN_COS9:81
      .= -1/((arctan.x)^2*(1+x^2)) by XCMPLX_1:78;
    hence thesis;
  end;
  hence thesis by A2,A3,FDIFF_2:22;
end;

::f.x=1/arccot.x

theorem Th68:
  Z c= ].-1,1.[ implies arccot^ is_differentiable_on Z & for x st
  x in Z holds ((arccot^)`|Z).x= 1/((arccot.x)^2*(1+x^2))
proof
  assume
A1: Z c= ].-1,1.[;
  then
A2: arccot is_differentiable_on Z by SIN_COS9:82;
A3: for x st x in Z holds arccot.x<>0
  proof
    PI in ].0,4.[ by SIN_COS:def 28;
    then PI > 0 by XXREAL_1:4;
    then
A4: PI/4 > 0/4 by XREAL_1:74;
    let x;
    assume
A5: x in Z;
    assume
A6: arccot.x=0;
    ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
    then Z c= [.-1,1.] by A1,XBOOLE_1:1;
    then x in [.-1,1.] by A5;
    then 0 in arccot.:[.-1,1.] by A6,FUNCT_1:def 6,SIN_COS9:24;
    then 0 in [.PI/4,3/4*PI.] by RELAT_1:115,SIN_COS9:56;
    hence contradiction by A4,XXREAL_1:1;
  end;
  then
A7: arccot^ is_differentiable_on Z by A2,FDIFF_2:22;
  for x st x in Z holds ((arccot^)`|Z).x = 1/((arccot.x)^2*(1+x^2))
  proof
    let x;
    assume
A8: x in Z;
    then
A9: arccot.x<>0 & arccot is_differentiable_in x by A3,A2,FDIFF_1:9;
    ((arccot^)`|Z).x = diff(arccot^,x) by A7,A8,FDIFF_1:def 7
      .= -diff(arccot,x)/(arccot.x)^2 by A9,FDIFF_2:15
      .= -((arccot)`|Z).x/(arccot.x)^2 by A2,A8,FDIFF_1:def 7
      .= -(-1/(1+x^2))/(arccot.x)^2 by A1,A8,SIN_COS9:82
      .= (1/(1+x^2))/(arccot.x)^2
      .= 1/((arccot.x)^2*(1+x^2)) by XCMPLX_1:78;
    hence thesis;
  end;
  hence thesis by A3,A2,FDIFF_2:22;
end;

::f.x=1/(n*(arctan.x)|^n)

theorem
  Z c= dom ((1/n)(#)(( #Z n)*(arctan^))) & Z c= ].-1,1.[ & n>0 & (for x
  st x in Z holds arctan.x<>0) implies (1/n)(#)(( #Z n)*(arctan^))
is_differentiable_on Z & for x st x in Z holds (((1/n)(#)(( #Z n)*(arctan^)))`|
  Z).x = -1/(((arctan.x) #Z (n+1))*(1+x^2))
proof
  assume that
A1: Z c= dom ((1/n)(#)(( #Z n)*(arctan^))) and
A2: Z c= ].-1,1.[ and
A3: n>0 and
A4: for x st x in Z holds arctan.x<>0;
A5: Z c= dom (( #Z n)*(arctan^)) by A1,VALUED_1:def 5;
A6: arctan^ is_differentiable_on Z by A2,A4,Th67;
  for x st x in Z holds ( #Z n)*(arctan^) is_differentiable_in x
  proof
    let x;
    assume x in Z;
    then arctan^ is_differentiable_in x by A6,FDIFF_1:9;
    hence thesis by TAYLOR_1:3;
  end;
  then
A7: ( #Z n)*(arctan^) is_differentiable_on Z by A5,FDIFF_1:9;
  for y st y in Z holds y in dom (arctan^) by A5,FUNCT_1:11;
  then
A8: Z c= dom (arctan^) by TARSKI:def 3;
  for x st x in Z holds (((1/n)(#)(( #Z n)*(arctan^)))`|Z).x = -1/(((
  arctan.x) #Z (n+1))*(1+x^2))
  proof
    let x;
    assume
A9: x in Z;
    then
A10: arctan^ is_differentiable_in x by A6,FDIFF_1:9;
A11: (arctan^).x = 1/arctan.x by A8,A9,RFUNCT_1:def 2;
    (((1/n)(#)(( #Z n)*(arctan^)))`|Z).x = (1/n)*diff((( #Z n)*(arctan^))
    ,x) by A1,A7,A9,FDIFF_1:20
      .= (1/n)*(n*(((arctan^).x) #Z (n-1))*diff(arctan^,x)) by A10,TAYLOR_1:3
      .= (1/n)*(n*(((arctan^).x) #Z (n-1))*((arctan^)`|Z).x) by A6,A9,
FDIFF_1:def 7
      .= (1/n)*(n*(((arctan^).x) #Z (n-1))*(-1/((arctan.x)^2*(1+x^2)))) by A2
,A4,A9,Th67
      .= -((1/n)*n)*(((arctan^).x) #Z (n-1))*(1/((arctan.x)^2*(1+x^2)))
      .= -1*(((arctan^).x) #Z (n-1))*(1/((arctan.x)^2*(1+x^2))) by A3,
XCMPLX_1:106
      .= -((1/arctan.x) #Z (n-1))*(1/(((arctan.x) #Z 2)*(1+x^2))) by A11,
FDIFF_7:1
      .= -(1/((arctan.x) #Z (n-1)))/(((arctan.x) #Z 2)*(1+x^2)) by PREPOWER:42
      .= -1/(((arctan.x) #Z (n-1))*(((arctan.x) #Z 2)*(1+x^2))) by XCMPLX_1:78
      .= -1/(((arctan.x) #Z (n-1))*((arctan.x) #Z 2)*(1+x^2))
      .= -1/(((arctan.x) #Z ((n-1)+2))*(1+x^2)) by A4,A9,PREPOWER:44
      .= -1/(((arctan.x) #Z (n+1))*(1+x^2));
    hence thesis;
  end;
  hence thesis by A1,A7,FDIFF_1:20;
end;

::f.x=1/(n*(arccot.x)|^n)

theorem
  Z c= dom ((1/n)(#)(( #Z n)*(arccot^))) & Z c= ].-1,1.[ & n>0 implies (
1/n)(#)(( #Z n)*(arccot^)) is_differentiable_on Z & for x st x in Z holds (((1/
  n)(#)(( #Z n)*(arccot^)))`|Z).x = 1/(((arccot.x) #Z (n+1))*(1+x^2))
proof
  assume that
A1: Z c= dom ((1/n)(#)(( #Z n)*(arccot^))) and
A2: Z c= ].-1,1.[ and
A3: n>0;
A4: Z c= dom (( #Z n)*(arccot^)) by A1,VALUED_1:def 5;
A5: for x st x in Z holds arccot.x<>0
  proof
    PI in ].0,4.[ by SIN_COS:def 28;
    then PI > 0 by XXREAL_1:4;
    then
A6: PI/4 > 0/4 by XREAL_1:74;
    let x;
    assume
A7: x in Z;
    assume
A8: arccot.x=0;
    ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
    then Z c= [.-1,1.] by A2,XBOOLE_1:1;
    then x in [.-1,1.] by A7;
    then 0 in arccot.:[.-1,1.] by A8,FUNCT_1:def 6,SIN_COS9:24;
    then 0 in [.PI/4,3/4*PI.] by RELAT_1:115,SIN_COS9:56;
    hence contradiction by A6,XXREAL_1:1;
  end;
A9: arccot^ is_differentiable_on Z by A2,Th68;
  for x st x in Z holds ( #Z n)*(arccot^) is_differentiable_in x
  proof
    let x;
    assume x in Z;
    then arccot^ is_differentiable_in x by A9,FDIFF_1:9;
    hence thesis by TAYLOR_1:3;
  end;
  then
A10: ( #Z n)*(arccot^) is_differentiable_on Z by A4,FDIFF_1:9;
  for y st y in Z holds y in dom (arccot^) by A4,FUNCT_1:11;
  then
A11: Z c= dom (arccot^) by TARSKI:def 3;
  for x st x in Z holds (((1/n)(#)(( #Z n)*(arccot^)))`|Z).x = 1/(((
  arccot.x) #Z (n+1))*(1+x^2))
  proof
    let x;
    assume
A12: x in Z;
    then
A13: arccot^ is_differentiable_in x by A9,FDIFF_1:9;
A14: (arccot^).x = 1/arccot.x by A11,A12,RFUNCT_1:def 2;
    (((1/n)(#)(( #Z n)*(arccot^)))`|Z).x = (1/n)*diff((( #Z n)*(arccot^))
    ,x) by A1,A10,A12,FDIFF_1:20
      .= (1/n)*(n*(((arccot^).x) #Z (n-1))*diff(arccot^,x)) by A13,TAYLOR_1:3
      .= (1/n)*(n*(((arccot^).x) #Z (n-1))*((arccot^)`|Z).x) by A9,A12,
FDIFF_1:def 7
      .= (1/n)*(n*(((arccot^).x) #Z (n-1))*(1/((arccot.x)^2*(1+x^2)))) by A2
,A12,Th68
      .= ((1/n)*n)*(((arccot^).x) #Z (n-1))*(1/((arccot.x)^2*(1+x^2)))
      .= 1*(((arccot^).x) #Z (n-1))*(1/((arccot.x)^2*(1+x^2))) by A3,
XCMPLX_1:106
      .= ((1/arccot.x) #Z (n-1))*(1/(((arccot.x) #Z 2)*(1+x^2))) by A14,
FDIFF_7:1
      .= (1/((arccot.x) #Z (n-1)))/(((arccot.x) #Z 2)*(1+x^2)) by PREPOWER:42
      .= 1/(((arccot.x) #Z (n-1))*(((arccot.x) #Z 2)*(1+x^2))) by XCMPLX_1:78
      .= 1/(((arccot.x) #Z (n-1))*((arccot.x) #Z 2)*(1+x^2))
      .= 1/(((arccot.x) #Z ((n-1)+2))*(1+x^2)) by A5,A12,PREPOWER:44
      .= 1/(((arccot.x) #Z (n+1))*(1+x^2));
    hence thesis;
  end;
  hence thesis by A1,A10,FDIFF_1:20;
end;

::f.x=2*(arctan #R (1/2))

theorem
  Z c= dom ((2(#)(( #R (1/2))*arctan))) & Z c= ].-1,1.[ & (for x st x in
Z holds arctan.x > 0) implies 2(#)(( #R (1/2))*arctan) is_differentiable_on Z &
for x st x in Z holds ((2(#)(( #R (1/2))*arctan))`|Z).x = (arctan.x) #R (-1/2)/
  (1+x^2)
proof
  assume that
A1: Z c= dom ((2(#)(( #R (1/2))*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 ( #R (1/2))*arctan is_differentiable_in x
  proof
    let x;
    assume
A5: x in Z;
    then
A6: arctan.x > 0 by A3;
    arctan is_differentiable_on Z by A2,SIN_COS9:81;
    then arctan is_differentiable_in x by A5,FDIFF_1:9;
    hence thesis by A6,TAYLOR_1:22;
  end;
  Z c= dom (( #R (1/2))*arctan) by A1,VALUED_1:def 5;
  then
A7: ( #R (1/2))*arctan is_differentiable_on Z by A4,FDIFF_1:9;
  for x st x in Z holds ((2(#)(( #R (1/2))*arctan))`|Z).x = ((arctan.x)
  #R (-1/2))/(1+x^2)
  proof
    let x;
    assume
A8: x in Z;
    then
A9: arctan.x > 0 by A3;
A10: arctan is_differentiable_on Z by A2,SIN_COS9:81;
    then
A11: arctan is_differentiable_in x by A8,FDIFF_1:9;
    ((2(#)(( #R (1/2))*arctan))`|Z).x = 2*diff((( #R (1/2))*arctan),x) by A1,A7
,A8,FDIFF_1:20
      .= 2*((1/2)*((arctan.x) #R (1/2-1))*diff(arctan,x)) by A11,A9,TAYLOR_1:22
      .= 2*((1/2)*((arctan.x) #R (1/2-1))*((arctan)`|Z).x) by A8,A10,
FDIFF_1:def 7
      .= 2*((1/2)*((arctan.x) #R (1/2-1))*(1/(1+x^2))) by A2,A8,SIN_COS9:81
      .= ((arctan.x) #R (-1/2))/(1+x^2);
    hence thesis;
  end;
  hence thesis by A1,A7,FDIFF_1:20;
end;

::f.x=2*(arccot #R (1/2))

theorem
  Z c= dom ((2(#)(( #R (1/2))*arccot))) & Z c= ].-1,1.[ implies 2(#)((
#R (1/2))*arccot) is_differentiable_on Z & for x st x in Z holds ((2(#)(( #R (1
  /2))*arccot))`|Z).x = -(arccot.x) #R (-1/2)/(1+x^2)
proof
  assume that
A1: Z c= dom ((2(#)(( #R (1/2))*arccot))) and
A2: Z c= ].-1,1.[;
A3: for x st x in Z holds arccot.x > 0
  proof
    let x;
    ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
    then
A4: Z c= [.-1,1.] by A2,XBOOLE_1:1;
    assume x in Z;
    then x in [.-1,1.] by A4;
    then arccot.x in arccot.:[.-1,1.] by FUNCT_1:def 6,SIN_COS9:24;
    then arccot.x in [.PI/4,3/4*PI.] by RELAT_1:115,SIN_COS9:56;
    then arccot.x >= PI/4 by XXREAL_1:1;
    then
A5: arccot.x + 0 > PI/4 + (-PI/4) by XREAL_1:8;
    assume arccot.x <= 0;
    hence contradiction by A5;
  end;
A6: for x st x in Z holds ( #R (1/2))*arccot is_differentiable_in x
  proof
    let x;
    assume
A7: x in Z;
    then
A8: arccot.x > 0 by A3;
    arccot is_differentiable_on Z by A2,SIN_COS9:82;
    then arccot is_differentiable_in x by A7,FDIFF_1:9;
    hence thesis by A8,TAYLOR_1:22;
  end;
  Z c= dom (( #R (1/2))*arccot) by A1,VALUED_1:def 5;
  then
A9: ( #R (1/2))*arccot is_differentiable_on Z by A6,FDIFF_1:9;
  for x st x in Z holds ((2(#)(( #R (1/2))*arccot))`|Z).x = -(arccot.x)
  #R (-1/2)/(1+x^2)
  proof
    let x;
    assume
A10: x in Z;
    then
A11: arccot.x > 0 by A3;
A12: arccot is_differentiable_on Z by A2,SIN_COS9:82;
    then
A13: arccot is_differentiable_in x by A10,FDIFF_1:9;
    ((2(#)(( #R (1/2))*arccot))`|Z).x = 2*diff((( #R (1/2))*arccot),x) by A1,A9
,A10,FDIFF_1:20
      .= 2*((1/2)*((arccot.x) #R (1/2-1))*diff(arccot,x)) by A13,A11,
TAYLOR_1:22
      .= 2*((1/2)*((arccot.x) #R (1/2-1))*((arccot)`|Z).x) by A10,A12,
FDIFF_1:def 7
      .= 2*((1/2)*((arccot.x) #R (1/2-1))*(-1/(1+x^2))) by A2,A10,SIN_COS9:82
      .= -((arccot.x) #R (-1/2))/(1+x^2);
    hence thesis;
  end;
  hence thesis by A1,A9,FDIFF_1:20;
end;

::f.x=(2/3)*(arctan #R (3/2))

theorem
  Z c= dom (((2/3)(#)(( #R (3/2))*arctan))) & Z c= ].-1,1.[ & (for x st
  x in Z holds arctan.x > 0) implies (2/3)(#)(( #R (3/2))*arctan)
is_differentiable_on Z & for x st x in Z holds (((2/3)(#)(( #R (3/2))*arctan))
  `|Z).x = (arctan.x) #R (1/2)/(1+x^2)
proof
  assume that
A1: Z c= dom (((2/3)(#)(( #R (3/2))*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 ( #R (3/2))*arctan is_differentiable_in x
  proof
    let x;
    assume
A5: x in Z;
    then
A6: arctan.x > 0 by A3;
    arctan is_differentiable_on Z by A2,SIN_COS9:81;
    then arctan is_differentiable_in x by A5,FDIFF_1:9;
    hence thesis by A6,TAYLOR_1:22;
  end;
  Z c= dom (( #R (3/2))*arctan) by A1,VALUED_1:def 5;
  then
A7: ( #R (3/2))*arctan is_differentiable_on Z by A4,FDIFF_1:9;
  for x st x in Z holds (((2/3)(#)(( #R (3/2))*arctan))`|Z).x = ((arctan.
  x) #R (1/2))/(1+x^2)
  proof
    let x;
    assume
A8: x in Z;
    then
A9: arctan.x > 0 by A3;
A10: arctan is_differentiable_on Z by A2,SIN_COS9:81;
    then
A11: arctan is_differentiable_in x by A8,FDIFF_1:9;
    (((2/3)(#)(( #R (3/2))*arctan))`|Z).x = (2/3)*diff((( #R (3/2))*
    arctan),x) by A1,A7,A8,FDIFF_1:20
      .= (2/3)*((3/2)*((arctan.x) #R (3/2-1))*diff(arctan,x)) by A11,A9,
TAYLOR_1:22
      .= (2/3)*((3/2)*((arctan.x) #R (3/2-1))*((arctan)`|Z).x) by A8,A10,
FDIFF_1:def 7
      .= (2/3)*((3/2)*((arctan.x) #R (3/2-1))*(1/(1+x^2))) by A2,A8,SIN_COS9:81
      .= ((arctan.x) #R (1/2))/(1+x^2);
    hence thesis;
  end;
  hence thesis by A1,A7,FDIFF_1:20;
end;

::f.x=(2/3)*(arccot #R (3/2))

theorem
  Z c= dom (((2/3)(#)(( #R (3/2))*arccot))) & Z c= ].-1,1.[ implies (2/3
)(#)(( #R (3/2))*arccot) is_differentiable_on Z & for x st x in Z holds (((2/3)
  (#)(( #R (3/2))*arccot))`|Z).x = -(arccot.x) #R (1/2)/(1+x^2)
proof
  assume that
A1: Z c= dom (((2/3)(#)(( #R (3/2))*arccot))) and
A2: Z c= ].-1,1.[;
A3: for x st x in Z holds arccot.x > 0
  proof
    let x;
    ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
    then
A4: Z c= [.-1,1.] by A2,XBOOLE_1:1;
    assume x in Z;
    then x in [.-1,1.] by A4;
    then arccot.x in arccot.:[.-1,1.] by FUNCT_1:def 6,SIN_COS9:24;
    then arccot.x in [.PI/4,3/4*PI.] by RELAT_1:115,SIN_COS9:56;
    then arccot.x >= PI/4 by XXREAL_1:1;
    then
A5: arccot.x + 0 > PI/4 + (-PI/4) by XREAL_1:8;
    assume arccot.x <= 0;
    hence contradiction by A5;
  end;
A6: for x st x in Z holds ( #R (3/2))*arccot is_differentiable_in x
  proof
    let x;
    assume
A7: x in Z;
    then
A8: arccot.x > 0 by A3;
    arccot is_differentiable_on Z by A2,SIN_COS9:82;
    then arccot is_differentiable_in x by A7,FDIFF_1:9;
    hence thesis by A8,TAYLOR_1:22;
  end;
  Z c= dom (( #R (3/2))*arccot) by A1,VALUED_1:def 5;
  then
A9: ( #R (3/2))*arccot is_differentiable_on Z by A6,FDIFF_1:9;
  for x st x in Z holds (((2/3)(#)(( #R (3/2))*arccot))`|Z).x = -(arccot.
  x) #R (1/2)/(1+x^2)
  proof
    let x;
    assume
A10: x in Z;
    then
A11: arccot.x > 0 by A3;
A12: arccot is_differentiable_on Z by A2,SIN_COS9:82;
    then
A13: arccot is_differentiable_in x by A10,FDIFF_1:9;
    (((2/3)(#)(( #R (3/2))*arccot))`|Z).x = (2/3)*diff((( #R (3/2))*
    arccot),x) by A1,A9,A10,FDIFF_1:20
      .= (2/3)*((3/2)*((arccot.x) #R (3/2-1))*diff(arccot,x)) by A13,A11,
TAYLOR_1:22
      .= (2/3)*((3/2)*((arccot.x) #R (3/2-1))*((arccot)`|Z).x) by A10,A12,
FDIFF_1:def 7
      .= (2/3)*((3/2)*((arccot.x) #R (3/2-1))*(-1/(1+x^2))) by A2,A10,
SIN_COS9:82
      .= -((arccot.x) #R (1/2))/(1+x^2);
    hence thesis;
  end;
  hence thesis by A1,A9,FDIFF_1:20;
end;