:: Several Differentiation Formulas of Special Functions -- Part {VII}
::  by Fuguo Ge and Bing Xie
:: 
:: Received September 23, 2008
:: Copyright (c) 2008 Association of Mizar Users

environ

 vocabularies FUNCT_1, RELAT_1, PRE_TOPC, ARYTM_1, ARYTM_3, PARTFUN1, SIN_COS,
      FDIFF_1, SQUARE_1, FINSEQ_1, SIN_COS4, ARYTM, BOOLE, SEQ_1, RCOMP_1,
      INT_1, SIN_COS9, PREPOWER;
 notations TARSKI, SUBSET_1, ORDINAL1, XXREAL_0, RELSET_1, PARTFUN1, RCOMP_1,
      SIN_COS, RFUNCT_1, SQUARE_1, VALUED_1, NUMBERS, REAL_1, SEQ_1, FDIFF_1,
      XREAL_0, INT_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,
      XXREAL_2;
 registrations XCMPLX_0, XXREAL_0, XREAL_0, MEMBERED, RCOMP_1, RELSET_1,
      SIN_COS6, NUMBERS, INT_1, VALUED_0, SIN_COS9;
 requirements SUBSET, BOOLE, NUMERALS, ARITHM, REAL;
 definitions XCMPLX_0, SIN_COS, SQUARE_1, FDIFF_9, SIN_COS9;
 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, r, s, h for Real,
        a, b, p, q, th for real number,
        i for integer number,
        n for Element of NAT,
        rr, y for set,
        Z for open Subset of REAL,
        X, Y for Subset of REAL,
        f, f1, f2, g for PartFunc of REAL,REAL;

::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;
AA: for x st x in Z holds arctan*sin is_differentiable_in x
    proof
        let x;
        assume
    A3: x in Z;
    A4: sin is_differentiable_in x by SIN_COS:69;
        sin.x > -1 & sin.x < 1 by A2,A3;
        hence arctan*sin is_differentiable_in x by A4,SIN_COS9:85;
    end;
    then
A5: arctan*sin is_differentiable_on Z by A1,FDIFF_1:16;
    for x st x in Z holds
    ((arctan*sin)`|Z).x = cos.x/(1+(sin.x)^2)
    proof
        let x;
        assume
    A6: x in Z;
    A7: sin is_differentiable_in x by SIN_COS:69;
    A8: sin.x > -1 & sin.x < 1 by A2,A6;
        ((arctan*sin)`|Z).x = diff(arctan*sin,x)
        by A5,A6,FDIFF_1:def 8
        .= diff(sin,x)/(1+(sin.x)^2) by A7,A8,SIN_COS9:85
        .= cos.x/(1+(sin.x)^2) by SIN_COS:69;
        hence thesis;
    end;
    hence thesis by A1,AA,FDIFF_1:16;
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;
AA: for x st x in Z holds arccot*sin is_differentiable_in x
    proof
        let x;
        assume
    A3: x in Z;
    A4: sin is_differentiable_in x by SIN_COS:69;
        sin.x > -1 & sin.x < 1 by A2,A3;
        hence arccot*sin is_differentiable_in x by A4,SIN_COS9:86;
    end; then
A5: arccot*sin is_differentiable_on Z by A1,FDIFF_1:16;
    for x st x in Z holds ((arccot*sin)`|Z).x = -cos.x/(1+(sin.x)^2)
    proof
        let x;
        assume
    A6: x in Z;
    A7: sin is_differentiable_in x by SIN_COS:69;
    A8: sin.x > -1 & sin.x < 1 by A2,A6;
        ((arccot*sin)`|Z).x = diff(arccot*sin,x) by A5,A6,FDIFF_1:def 8
        .= -diff(sin,x)/(1+(sin.x)^2) by A7,A8,SIN_COS9:86
        .= -cos.x/(1+(sin.x)^2) by SIN_COS:69;
        hence thesis;
    end;
    hence thesis by A1,AA,FDIFF_1:16;
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;
AA: for x st x in Z holds arctan*cos is_differentiable_in x
    proof
        let x;
        assume
    A3: x in Z;
    A4: cos is_differentiable_in x by SIN_COS:68;
        cos.x > -1 & cos.x < 1 by A2,A3;
        hence arctan*cos is_differentiable_in x by A4,SIN_COS9:85;
    end;
    then
A5: arctan*cos is_differentiable_on Z by A1,FDIFF_1:16;
    for x st x in Z holds ((arctan*cos)`|Z).x = -sin.x/(1+(cos.x)^2)
    proof
        let x;
        assume
    A6: x in Z;
    A7: cos is_differentiable_in x by SIN_COS:68;
    A8: cos.x > -1 & cos.x < 1 by A2,A6;
        ((arctan*cos)`|Z).x = diff(arctan*cos,x) by A5,A6,FDIFF_1:def 8
        .= diff(cos,x)/(1+(cos.x)^2) by A7,A8,SIN_COS9:85
        .= (-sin.x)/(1+(cos.x)^2) by SIN_COS:68
        .= -sin.x/(1+(cos.x)^2);
        hence thesis;
    end;
    hence thesis by A1,AA,FDIFF_1:16;
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;
AA: for x st x in Z holds arccot*cos is_differentiable_in x
    proof
        let x;
        assume
    A3: x in Z;
    A4: cos is_differentiable_in x by SIN_COS:68;
        cos.x > -1 & cos.x < 1 by A2,A3;
        hence arccot*cos is_differentiable_in x by A4,SIN_COS9:86;
    end;
    then
A5: arccot*cos is_differentiable_on Z by A1,FDIFF_1:16;
    for x st x in Z holds
    ((arccot*cos)`|Z).x = sin.x/(1+(cos.x)^2)
    proof
        let x;
        assume
    A6: x in Z;
    A7: cos is_differentiable_in x by SIN_COS:68;
    A8: cos.x > -1 & cos.x < 1 by A2,A6;
        ((arccot*cos)`|Z).x = diff(arccot*cos,x) by A5,A6,FDIFF_1:def 8
        .= -diff(cos,x)/(1+(cos.x)^2) by A7,A8,SIN_COS9:86
        .= -(-sin.x)/(1+(cos.x)^2) by SIN_COS:68
        .= sin.x/(1+(cos.x)^2);
        hence thesis;
    end;
    hence thesis by A1,AA,FDIFF_1:16;
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:44;then
A3: Z c= dom tan by A1,XBOOLE_1:1;
AA: for x st x in Z holds arctan*tan is_differentiable_in x
    proof
        let x;
        assume
    A4: x in Z;
        then cos.x <> 0 by A3,FDIFF_8:1;then
    A5: tan is_differentiable_in x by FDIFF_7:46;
        tan.x > -1 & tan.x < 1 by A2,A4;
        hence arctan*tan is_differentiable_in x by A5,SIN_COS9:85;
    end;
    then
A6: arctan*tan is_differentiable_on Z by A1,FDIFF_1:16;
    for x st x in Z holds ((arctan*tan)`|Z).x = 1
    proof
         let x;
         assume
    A7:  x in Z;then
    A8:  cos.x <> 0 by A3,FDIFF_8:1;then
    A9:  tan is_differentiable_in x by FDIFF_7:46;
    A10: tan.x > -1 & tan.x < 1 by A2,A7;
    A13: tan.x = sin.x/cos.x by A3,A7,RFUNCT_1:def 4;
    A14: (cos.x)^2 <> 0 by A8,SQUARE_1:74;
         ((arctan*tan)`|Z).x = diff(arctan*tan,x) by A6,A7,FDIFF_1:def 8
         .= diff(tan,x)/(1+(tan.x)^2) by A9,A10,SIN_COS9:85
         .= (1/(cos.x)^2)/(1+(tan.x)^2) by A8,FDIFF_7:46
         .= 1/((cos.x)^2*(1+(sin.x/cos.x)*(sin.x/cos.x))) by A13,XCMPLX_1:79
         .= 1/((cos.x)^2*(1+(sin.x)^2/(cos.x)^2)) by XCMPLX_1:77
         .= 1/((cos.x)^2+((cos.x)^2*(sin.x)^2)/(cos.x)^2)
         .= 1/((cos.x)^2+(sin.x)^2) by A14,XCMPLX_1:90
         .= 1/1 by SIN_COS:31
         .= 1;
         hence thesis;
    end;
    hence thesis by A1,AA,FDIFF_1:16;
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:44;then
A3: Z c= dom tan by A1,XBOOLE_1:1;
AA: for x st x in Z holds arccot*tan is_differentiable_in x
    proof
        let x;
        assume
    A4: x in Z;
        then cos.x <> 0 by A3,FDIFF_8:1;then
    A5: tan is_differentiable_in x by FDIFF_7:46;
        tan.x > -1 & tan.x < 1 by A2,A4;
        hence arccot*tan is_differentiable_in x by A5,SIN_COS9:86;
    end;
    then
A6: arccot*tan is_differentiable_on Z by A1,FDIFF_1:16;
    for x st x in Z holds ((arccot*tan)`|Z).x = -1
    proof
         let x;
         assume
    A7:  x in Z;then
    A8:  cos.x <> 0 by A3,FDIFF_8:1;then
    A9:  tan is_differentiable_in x by FDIFF_7:46;
    A10: tan.x > -1 & tan.x < 1 by A2,A7;
    A13: tan.x = sin.x/cos.x by A3,A7,RFUNCT_1:def 4;
    A14: (cos.x)^2 <> 0 by A8,SQUARE_1:74;
         ((arccot*tan)`|Z).x = diff(arccot*tan,x) by A6,A7,FDIFF_1:def 8
         .= -diff(tan,x)/(1+(tan.x)^2) by A9,A10,SIN_COS9:86
         .= -(1/(cos.x)^2)/(1+(tan.x)^2) by A8,FDIFF_7:46
         .= -1/((cos.x)^2*(1+(sin.x/cos.x)*(sin.x/cos.x))) by A13,XCMPLX_1:79
         .= -1/((cos.x)^2*(1+(sin.x)^2/(cos.x)^2)) by XCMPLX_1:77
         .= -1/((cos.x)^2+((cos.x)^2*(sin.x)^2)/(cos.x)^2)
         .= -1/((cos.x)^2+(sin.x)^2) by A14,XCMPLX_1:90
         .= -1/1 by SIN_COS:31
         .= -1;
         hence thesis;
    end;
    hence thesis by A1,AA,FDIFF_1:16;
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:44;then
A3: Z c= dom cot by A1,XBOOLE_1:1;
AA: for x st x in Z holds arctan*cot is_differentiable_in x
    proof
        let x;
        assume
    A4: x in Z;
        then sin.x <> 0 by A3,FDIFF_8:2;then
    A5: cot is_differentiable_in x by FDIFF_7:47;
        cot.x > -1 & cot.x < 1 by A2,A4;
        hence arctan*cot is_differentiable_in x by A5,SIN_COS9:85;
    end;
    then
A6: arctan*cot is_differentiable_on Z by A1,FDIFF_1:16;
    for x st x in Z holds ((arctan*cot)`|Z).x = -1
    proof
         let x;
         assume
    A7:  x in Z;then
    A8:  sin.x <> 0 by A3,FDIFF_8:2;then
    A9:  cot is_differentiable_in x by FDIFF_7:47;
    A10: cot.x > -1 & cot.x < 1 by A2,A7;
    A13: cot.x = cos.x/sin.x by A3,A7,RFUNCT_1:def 4;
    A14: (sin.x)^2 <> 0 by A8,SQUARE_1:74;
         ((arctan*cot)`|Z).x = diff(arctan*cot,x) by A6,A7,FDIFF_1:def 8
         .= diff(cot,x)/(1+(cot.x)^2) by A9,A10,SIN_COS9:85
         .= (-1/(sin.x)^2)/(1+(cot.x)^2) by A8,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 A13,XCMPLX_1:79
         .= -1/((sin.x)^2*(1+(cos.x)^2/(sin.x)^2)) by XCMPLX_1:77
         .= -1/((sin.x)^2+((sin.x)^2*(cos.x)^2)/(sin.x)^2)
         .= -1/((sin.x)^2+(cos.x)^2) by A14,XCMPLX_1:90
         .= -1/1 by SIN_COS:31
         .= -1;
         hence thesis;
    end;
    hence thesis by A1,AA,FDIFF_1:16;
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:44;then
A3: Z c= dom cot by A1,XBOOLE_1:1;
AA: for x st x in Z holds arccot*cot is_differentiable_in x
    proof
        let x;
        assume
    A4: x in Z;
        then sin.x <> 0 by A3,FDIFF_8:2;then
    A5: cot is_differentiable_in x by FDIFF_7:47;
        cot.x > -1 & cot.x < 1 by A2,A4;
        hence arccot*cot is_differentiable_in x by A5,SIN_COS9:86;
    end; then
A6: arccot*cot is_differentiable_on Z by A1,FDIFF_1:16;
    for x st x in Z holds ((arccot*cot)`|Z).x = 1
    proof
         let x;
         assume
    A7:  x in Z;then
    A8:  sin.x <> 0 by A3,FDIFF_8:2;then
    A9:  cot is_differentiable_in x by FDIFF_7:47;
    A10: cot.x > -1 & cot.x < 1 by A2,A7;
    A13: cot.x = cos.x/sin.x by A3,A7,RFUNCT_1:def 4;
    A14: (sin.x)^2 <> 0 by A8,SQUARE_1:74;
         ((arccot*cot)`|Z).x = diff(arccot*cot,x) by A6,A7,FDIFF_1:def 8
         .= -diff(cot,x)/(1+(cot.x)^2) by A9,A10,SIN_COS9:86
         .= -(-1/(sin.x)^2)/(1+(cot.x)^2) by A8,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 A13,XCMPLX_1:79
         .= 1/((sin.x)^2*(1+(cos.x)^2/(sin.x)^2)) by XCMPLX_1:77
         .= 1/((sin.x)^2+((sin.x)^2*(cos.x)^2)/(sin.x)^2)
         .= 1/((sin.x)^2+(cos.x)^2) by A14,XCMPLX_1:90
         .= 1/1 by SIN_COS:31
         .= 1;
         hence thesis;
    end;
    hence thesis by A1,AA,FDIFF_1:16;
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;
AA: for x st x in Z holds arctan*arctan is_differentiable_in x
    proof
        let x;
        assume
    A4: x in Z;
        arctan is_differentiable_on Z by A2,SIN_COS9:81;then
    A5: arctan is_differentiable_in x by A4,FDIFF_1:16;
        arctan.x > -1 & arctan.x < 1 by A3,A4;
        hence arctan*arctan is_differentiable_in x by A5,SIN_COS9:85;
    end;
    then
A6: arctan*arctan is_differentiable_on Z by A1,FDIFF_1:16;
    for x st x in Z holds
    ((arctan*arctan)`|Z).x = 1/((1+x^2)*(1+(arctan.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:16;
    A10: arctan.x > -1 & arctan.x < 1 by A3,A7;
         ((arctan*arctan)`|Z).x = diff(arctan*arctan,x)
           by A6,A7,FDIFF_1:def 8
         .= diff(arctan,x)/(1+(arctan.x)^2) by A9,A10,SIN_COS9:85
         .= ((arctan)`|Z).x/(1+(arctan.x)^2) by A7,A8,FDIFF_1:def 8
         .= (1/(1+x^2))/(1+(arctan.x)^2) by A2,A7,SIN_COS9:81
         .= 1/((1+x^2)*(1+(arctan.x)^2)) by XCMPLX_1:79;
         hence thesis;
    end;
    hence thesis by A1,AA,FDIFF_1:16;
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;
AA: for x st x in Z holds arccot*arctan is_differentiable_in x
    proof
        let x;
        assume
    A4: x in Z;
        arctan is_differentiable_on Z by A2,SIN_COS9:81;then
    A5: arctan is_differentiable_in x by A4,FDIFF_1:16;
        arctan.x > -1 & arctan.x < 1 by A3,A4;
        hence arccot*arctan is_differentiable_in x by A5,SIN_COS9:86;
    end; then
A6: arccot*arctan is_differentiable_on Z by A1,FDIFF_1:16;
    for x st x in Z holds
    ((arccot*arctan)`|Z).x = -1/((1+x^2)*(1+(arctan.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:16;
    A10: arctan.x > -1 & arctan.x < 1 by A3,A7;
         ((arccot*arctan)`|Z).x = diff(arccot*arctan,x)
         by A6,A7,FDIFF_1:def 8
         .= -diff(arctan,x)/(1+(arctan.x)^2) by A9,A10,SIN_COS9:86
         .= -((arctan)`|Z).x/(1+(arctan.x)^2) by A7,A8,FDIFF_1:def 8
         .= -(1/(1+x^2))/(1+(arctan.x)^2) by A2,A7,SIN_COS9:81
         .= -1/((1+x^2)*(1+(arctan.x)^2)) by XCMPLX_1:79;
         hence thesis;
    end;
    hence thesis by A1,AA,FDIFF_1:16;
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;
AA: for x st x in Z holds arctan*arccot is_differentiable_in x
    proof
        let x;
        assume
    A4: x in Z;
        arccot is_differentiable_on Z by A2,SIN_COS9:82;then
    A5: arccot is_differentiable_in x by A4,FDIFF_1:16;
        arccot.x > -1 & arccot.x < 1 by A3,A4;
        hence arctan*arccot is_differentiable_in x by A5,SIN_COS9:85;
    end;
    then
A6: arctan*arccot is_differentiable_on Z by A1,FDIFF_1:16;
    for x st x in Z holds
    ((arctan*arccot)`|Z).x = -1/((1+x^2)*(1+(arccot.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:16;
    A10: arccot.x > -1 & arccot.x < 1 by A3,A7;
         ((arctan*arccot)`|Z).x = diff(arctan*arccot,x)
         by A6,A7,FDIFF_1:def 8
         .= diff(arccot,x)/(1+(arccot.x)^2) by A9,A10,SIN_COS9:85
         .= ((arccot)`|Z).x/(1+(arccot.x)^2) by A7,A8,FDIFF_1:def 8
         .= (-1/(1+x^2))/(1+(arccot.x)^2) by A2,A7,SIN_COS9:82
         .= -1/(1+x^2)/(1+(arccot.x)^2)
         .= -1/((1+x^2)*(1+(arccot.x)^2)) by XCMPLX_1:79;
         hence thesis;
    end;
    hence thesis by A1,AA,FDIFF_1:16;
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;
AA: for x st x in Z holds arccot*arccot is_differentiable_in x
    proof
        let x;
        assume
    A4: x in Z;
        arccot is_differentiable_on Z by A2,SIN_COS9:82;then
    A5: arccot is_differentiable_in x by A4,FDIFF_1:16;
        arccot.x > -1 & arccot.x < 1 by A3,A4;
        hence arccot*arccot is_differentiable_in x by A5,SIN_COS9:86;
    end;
    then
A6: arccot*arccot is_differentiable_on Z by A1,FDIFF_1:16;
    for x st x in Z holds
    ((arccot*arccot)`|Z).x = 1/((1+x^2)*(1+(arccot.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:16;
    A10: arccot.x > -1 & arccot.x < 1 by A3,A7;
         ((arccot*arccot)`|Z).x = diff(arccot*arccot,x)
         by A6,A7,FDIFF_1:def 8
         .= -diff(arccot,x)/(1+(arccot.x)^2) by A9,A10,SIN_COS9:86
         .= -((arccot)`|Z).x/(1+(arccot.x)^2) by A7,A8,FDIFF_1:def 8
         .= -(-1/(1+x^2))/(1+(arccot.x)^2) by A2,A7,SIN_COS9:82
         .= 1/(1+x^2)/(1+(arccot.x)^2)
         .= 1/((1+x^2)*(1+(arccot.x)^2)) by XCMPLX_1:79;
         hence thesis;
    end;
    hence thesis by A1,AA,FDIFF_1:16;
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.[;
AA: for x st x in Z holds sin*arctan is_differentiable_in x
    proof
        let x;
        assume
    A3: x in Z;
        arctan is_differentiable_on Z by A2,SIN_COS9:81;then
    A4: arctan is_differentiable_in x by A3,FDIFF_1:16;
        sin is_differentiable_in arctan.x by SIN_COS:69;
        hence sin*arctan is_differentiable_in x by A4,FDIFF_2:13;
    end;
    then
A5: sin*arctan is_differentiable_on Z by A1,FDIFF_1:16;
    for x st x in Z holds
    ((sin*arctan)`|Z).x = cos.(arctan.x)/(1+x^2)
    proof
        let x;
        assume
    A6: x in Z;
    A7: arctan is_differentiable_on Z by A2,SIN_COS9:81;then
    A8: arctan is_differentiable_in x by A6,FDIFF_1:16;
    A9: sin is_differentiable_in arctan.x by SIN_COS:69;
        ((sin*arctan)`|Z).x = diff(sin*arctan,x) by A5,A6,FDIFF_1:def 8
        .= diff(sin,arctan.x)*diff(arctan,x) by A8,A9,FDIFF_2:13
        .= cos.(arctan.x)*diff(arctan,x) by SIN_COS:69
        .= cos.(arctan.x)*((arctan)`|Z).x by A6,A7,FDIFF_1:def 8
        .= cos.(arctan.x)*(1/(1+x^2)) by A2,A6,SIN_COS9:81
        .= cos.(arctan.x)/(1+x^2);
        hence thesis;
    end;
    hence thesis by A1,AA,FDIFF_1:16;
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.[;
AA: for x st x in Z holds sin*arccot is_differentiable_in x
    proof
        let x;
        assume
    A3: x in Z;
        arccot is_differentiable_on Z by A2,SIN_COS9:82;then
    A4: arccot is_differentiable_in x by A3,FDIFF_1:16;
        sin is_differentiable_in arccot.x by SIN_COS:69;
        hence sin*arccot is_differentiable_in x by A4,FDIFF_2:13;
    end;
    then
A5: sin*arccot is_differentiable_on Z by A1,FDIFF_1:16;
    for x st x in Z holds
    ((sin*arccot)`|Z).x = -cos.(arccot.x)/(1+x^2)
    proof
        let x;
        assume
    A6: x in Z;
    A7: arccot is_differentiable_on Z by A2,SIN_COS9:82;then
    A8: arccot is_differentiable_in x by A6,FDIFF_1:16;
    A9: sin is_differentiable_in arccot.x by SIN_COS:69;
        ((sin*arccot)`|Z).x = diff(sin*arccot,x) by A5,A6,FDIFF_1:def 8
        .= diff(sin,arccot.x)*diff(arccot,x) by A8,A9,FDIFF_2:13
        .= cos.(arccot.x)*diff(arccot,x) by SIN_COS:69
        .= cos.(arccot.x)*((arccot)`|Z).x by A6,A7,FDIFF_1:def 8
        .= cos.(arccot.x)*(-1/(1+x^2)) by A2,A6,SIN_COS9:82
        .= -cos.(arccot.x)/(1+x^2);
        hence thesis;
    end;
    hence thesis by A1,AA,FDIFF_1:16;
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.[;
AA: for x st x in Z holds cos*arctan is_differentiable_in x
    proof
        let x;
        assume
    A3: x in Z;
        arctan is_differentiable_on Z by A2,SIN_COS9:81;then
    A4: arctan is_differentiable_in x by A3,FDIFF_1:16;
        cos is_differentiable_in arctan.x by SIN_COS:68;
        hence cos*arctan is_differentiable_in x by A4,FDIFF_2:13;
    end;
    then
A5: cos*arctan is_differentiable_on Z by A1,FDIFF_1:16;
    for x st x in Z holds
    ((cos*arctan)`|Z).x = -sin.(arctan.x)/(1+x^2)
    proof
        let x;
        assume
    A6: x in Z;
    A7: arctan is_differentiable_on Z by A2,SIN_COS9:81;then
    A8: arctan is_differentiable_in x by A6,FDIFF_1:16;
    A9: cos is_differentiable_in arctan.x by SIN_COS:68;
        ((cos*arctan)`|Z).x = diff(cos*arctan,x) by A5,A6,FDIFF_1:def 8
        .= diff(cos,arctan.x)*diff(arctan,x) by A8,A9,FDIFF_2:13
        .= (-sin.(arctan.x))*diff(arctan,x) by SIN_COS:68
        .= -sin.(arctan.x)*diff(arctan,x)
        .= -sin.(arctan.x)*((arctan)`|Z).x by A6,A7,FDIFF_1:def 8
        .= -sin.(arctan.x)*(1/(1+x^2)) by A2,A6,SIN_COS9:81
        .= -sin.(arctan.x)/(1+x^2);
        hence thesis;
    end;
    hence thesis by A1,AA,FDIFF_1:16;
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.[;
AA: for x st x in Z holds cos*arccot is_differentiable_in x
    proof
        let x;
        assume
    A3: x in Z;
        arccot is_differentiable_on Z by A2,SIN_COS9:82;then
    A4: arccot is_differentiable_in x by A3,FDIFF_1:16;
        cos is_differentiable_in arccot.x by SIN_COS:68;
        hence cos*arccot is_differentiable_in x by A4,FDIFF_2:13;
    end;
    then
A5: cos*arccot is_differentiable_on Z by A1,FDIFF_1:16;
    for x st x in Z holds
    ((cos*arccot)`|Z).x = sin.(arccot.x)/(1+x^2)
    proof
        let x;
        assume
    A6: x in Z;
    A7: arccot is_differentiable_on Z by A2,SIN_COS9:82;then
    A8: arccot is_differentiable_in x by A6,FDIFF_1:16;
    A9: cos is_differentiable_in arccot.x by SIN_COS:68;
        ((cos*arccot)`|Z).x = diff(cos*arccot,x) by A5,A6,FDIFF_1:def 8
        .= diff(cos,arccot.x)*diff(arccot,x) by A8,A9,FDIFF_2:13
        .= (-sin.(arccot.x))*diff(arccot,x) by SIN_COS:68
        .= -sin.(arccot.x)*diff(arccot,x)
        .= -sin.(arccot.x)*((arccot)`|Z).x by A6,A7,FDIFF_1:def 8
        .= -sin.(arccot.x)*(-1/(1+x^2)) by A2,A6,SIN_COS9:82
        .= sin.(arccot.x)/(1+x^2);
        hence thesis;
    end;
    hence thesis by A1,AA,FDIFF_1:16;
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.[;
AA: for x st x in Z holds tan*arctan is_differentiable_in x
    proof
        let x;
        assume
    A3: x in Z;
        arctan is_differentiable_on Z by A2,SIN_COS9:81;then
    A4: arctan is_differentiable_in x by A3,FDIFF_1:16;
        arctan.x in dom tan by A1,A3,FUNCT_1:21;
        then cos.(arctan.x) <> 0 by FDIFF_8:1;
        then tan is_differentiable_in arctan.x by FDIFF_7:46;
        hence tan*arctan is_differentiable_in x by A4,FDIFF_2:13;
    end;
    then
A5: tan*arctan is_differentiable_on Z by A1,FDIFF_1:16;
    for x st x in Z holds
    ((tan*arctan)`|Z).x = 1/((cos.(arctan.x))^2*(1+x^2))
    proof
         let x;
         assume
    A6:  x in Z;
    A7:  arctan is_differentiable_on Z by A2,SIN_COS9:81;then
    A8:  arctan is_differentiable_in x by A6,FDIFF_1:16;
         arctan.x in dom tan by A1,A6,FUNCT_1:21;then
    A9:  cos.(arctan.x) <> 0 by FDIFF_8:1;then
    A10: tan is_differentiable_in arctan.x by FDIFF_7:46;
         ((tan*arctan)`|Z).x = diff(tan*arctan,x) by A5,A6,FDIFF_1:def 8
         .= diff(tan,arctan.x)*diff(arctan,x) by A8,A10,FDIFF_2:13
         .= (1/(cos.(arctan.x))^2)*diff(arctan,x) by A9,FDIFF_7:46
         .= (1/(cos.(arctan.x))^2)*((arctan)`|Z).x by A6,A7,FDIFF_1:def 8
         .= (1/(cos.(arctan.x))^2)*(1/(1+x^2)) by A2,A6,SIN_COS9:81
         .= 1/((cos.(arctan.x))^2*(1+x^2)) by XCMPLX_1:103;
         hence thesis;
    end;
    hence thesis by A1,AA,FDIFF_1:16;
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.[;
AA: for x st x in Z holds tan*arccot is_differentiable_in x
    proof
        let x;
        assume
    A3: x in Z;
        arccot is_differentiable_on Z by A2,SIN_COS9:82;then
    A4: arccot is_differentiable_in x by A3,FDIFF_1:16;
        arccot.x in dom tan by A1,A3,FUNCT_1:21;
        then cos.(arccot.x) <> 0 by FDIFF_8:1;
        then tan is_differentiable_in arccot.x by FDIFF_7:46;
        hence tan*arccot is_differentiable_in x by A4,FDIFF_2:13;
    end;
    then
A5: tan*arccot is_differentiable_on Z by A1,FDIFF_1:16;
    for x st x in Z holds
    ((tan*arccot)`|Z).x = -1/((cos.(arccot.x))^2*(1+x^2))
    proof
         let x;
         assume
    A6:  x in Z;
    A7:  arccot is_differentiable_on Z by A2,SIN_COS9:82;then
    A8:  arccot is_differentiable_in x by A6,FDIFF_1:16;
         arccot.x in dom tan by A1,A6,FUNCT_1:21;then
    A9:  cos.(arccot.x) <> 0 by FDIFF_8:1;then
    A10: tan is_differentiable_in arccot.x by FDIFF_7:46;
         ((tan*arccot)`|Z).x = diff(tan*arccot,x) by A5,A6,FDIFF_1:def 8
         .= diff(tan,arccot.x)*diff(arccot,x) by A8,A10,FDIFF_2:13
         .= (1/(cos.(arccot.x))^2)*diff(arccot,x) by A9,FDIFF_7:46
         .= (1/(cos.(arccot.x))^2)*((arccot)`|Z).x by A6,A7,FDIFF_1:def 8
         .= (1/(cos.(arccot.x))^2)*(-1/(1+x^2)) by A2,A6,SIN_COS9:82
         .= -(1/(cos.(arccot.x))^2)*(1/(1+x^2))
         .= -1/((cos.(arccot.x))^2*(1+x^2)) by XCMPLX_1:103;
         hence thesis;
    end;
    hence thesis by A1,AA,FDIFF_1:16;
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.[;
AA: for x st x in Z holds cot*arctan is_differentiable_in x
    proof
        let x;
        assume
    A3: x in Z;
        arctan is_differentiable_on Z by A2,SIN_COS9:81;then
    A4: arctan is_differentiable_in x by A3,FDIFF_1:16;
        arctan.x in dom cot by A1,A3,FUNCT_1:21;
        then sin.(arctan.x) <> 0 by FDIFF_8:2;
        then cot is_differentiable_in arctan.x by FDIFF_7:47;
        hence cot*arctan is_differentiable_in x by A4,FDIFF_2:13;
    end;
    then
A5: cot*arctan is_differentiable_on Z by A1,FDIFF_1:16;
    for x st x in Z holds
    ((cot*arctan)`|Z).x = -1/((sin.(arctan.x))^2*(1+x^2))
    proof
         let x;
         assume
    A6:  x in Z;
    A7:  arctan is_differentiable_on Z by A2,SIN_COS9:81;then
    A8:  arctan is_differentiable_in x by A6,FDIFF_1:16;
         arctan.x in dom cot by A1,A6,FUNCT_1:21;then
    A9:  sin.(arctan.x) <> 0 by FDIFF_8:2;then
    A10: cot is_differentiable_in arctan.x by FDIFF_7:47;
         ((cot*arctan)`|Z).x = diff(cot*arctan,x) by A5,A6,FDIFF_1:def 8
         .= diff(cot,arctan.x)*diff(arctan,x) by A8,A10,FDIFF_2:13
         .= (-1/(sin.(arctan.x))^2)*diff(arctan,x) by A9,FDIFF_7:47
         .= -(1/(sin.(arctan.x))^2)*diff(arctan,x)
         .= -(1/(sin.(arctan.x))^2)*((arctan)`|Z).x by A6,A7,FDIFF_1:def 8
         .= -(1/(sin.(arctan.x))^2)*(1/(1+x^2)) by A2,A6,SIN_COS9:81
         .= -1/((sin.(arctan.x))^2*(1+x^2)) by XCMPLX_1:103;
         hence thesis;
    end;
    hence thesis by A1,AA,FDIFF_1:16;
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.[;
AA: for x st x in Z holds cot*arccot is_differentiable_in x
    proof
        let x;
        assume
    A3: x in Z;
        arccot is_differentiable_on Z by A2,SIN_COS9:82;then
    A4: arccot is_differentiable_in x by A3,FDIFF_1:16;
        arccot.x in dom cot by A1,A3,FUNCT_1:21;
        then sin.(arccot.x) <> 0 by FDIFF_8:2;
        then cot is_differentiable_in arccot.x by FDIFF_7:47;
        hence cot*arccot is_differentiable_in x by A4,FDIFF_2:13;
    end;
    then
A5: cot*arccot is_differentiable_on Z by A1,FDIFF_1:16;
    for x st x in Z holds
    ((cot*arccot)`|Z).x = 1/((sin.(arccot.x))^2*(1+x^2))
    proof
         let x;
         assume
    A6:  x in Z;
    A7:  arccot is_differentiable_on Z by A2,SIN_COS9:82;then
    A8:  arccot is_differentiable_in x by A6,FDIFF_1:16;
         arccot.x in dom cot by A1,A6,FUNCT_1:21;then
    A9:  sin.(arccot.x) <> 0 by FDIFF_8:2;then
    A10: cot is_differentiable_in arccot.x by FDIFF_7:47;
         ((cot*arccot)`|Z).x = diff(cot*arccot,x) by A5,A6,FDIFF_1:def 8
         .= diff(cot,arccot.x)*diff(arccot,x) by A8,A10,FDIFF_2:13
         .= (-1/(sin.(arccot.x))^2)*diff(arccot,x) by A9,FDIFF_7:47
         .= -(1/(sin.(arccot.x))^2)*diff(arccot,x)
         .= -(1/(sin.(arccot.x))^2)*((arccot)`|Z).x
          by A6,A7,FDIFF_1:def 8
         .= -(1/(sin.(arccot.x))^2)*(-1/(1+x^2)) by A2,A6,SIN_COS9:82
         .= (1/(sin.(arccot.x))^2)*(1/(1+x^2))
         .= 1/((sin.(arccot.x))^2*(1+x^2)) by XCMPLX_1:103;
         hence thesis;
    end;
    hence thesis by A1,AA,FDIFF_1:16;
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:21;
      hence thesis by RFUNCT_1:13;
    end;
AA: for x st x in Z holds sec*arctan is_differentiable_in x
    proof
        let x;
        assume
    A4: x in Z;
        arctan is_differentiable_on Z by A2,SIN_COS9:81;then
    A5: arctan is_differentiable_in x by A4,FDIFF_1:16;
        cos.(arctan.x) <> 0 by A3,A4;
        then sec is_differentiable_in arctan.x by FDIFF_9:1;
        hence sec*arctan is_differentiable_in x by A5,FDIFF_2:13;
    end;
    then
A6: sec*arctan is_differentiable_on Z by A1,FDIFF_1:16;
    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
    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:16;
         cos.(arctan.x) <> 0 by A3,A7;then
    A10: sec is_differentiable_in arctan.x by FDIFF_9:1;
    A11: cos.(arctan.x) <> 0 by A3,A7;
         ((sec*arctan)`|Z).x = diff(sec*arctan,x) by A6,A7,FDIFF_1:def 8
         .= diff(sec,arctan.x)*diff(arctan,x) by A9,A10,FDIFF_2:13
         .= (sin.(arctan.x)/(cos.(arctan.x))^2)*diff(arctan,x)
         by A11,FDIFF_9:1
         .= (sin.(arctan.x)/(cos.(arctan.x))^2)*((arctan)`|Z).x
         by A7,A8,FDIFF_1:def 8
         .= (sin.(arctan.x)/(cos.(arctan.x))^2)*(1/(1+x^2))
         by A2,A7,SIN_COS9:81
         .= (sin.(arctan.x)*1)/((cos.(arctan.x))^2*(1+x^2)) by XCMPLX_1:77
         .= sin.(arctan.x)/((cos.(arctan.x))^2*(1+x^2));
         hence thesis;
    end;
    hence thesis by A1,AA,FDIFF_1:16;
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:21;
      hence thesis by RFUNCT_1:13;
    end;
AA: for x st x in Z holds sec*arccot is_differentiable_in x
    proof
        let x;
        assume
    A4: x in Z;
        arccot is_differentiable_on Z by A2,SIN_COS9:82;then
    A5: arccot is_differentiable_in x by A4,FDIFF_1:16;
        cos.(arccot.x) <> 0 by A3,A4;
        then sec is_differentiable_in arccot.x by FDIFF_9:1;
        hence sec*arccot is_differentiable_in x by A5,FDIFF_2:13;
    end;
    then
A6: sec*arccot is_differentiable_on Z by A1,FDIFF_1:16;
    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
    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:16;
         cos.(arccot.x) <> 0 by A3,A7;then
    A10: sec is_differentiable_in arccot.x by FDIFF_9:1;
    A11: cos.(arccot.x) <> 0 by A3,A7;
         ((sec*arccot)`|Z).x = diff(sec*arccot,x) by A6,A7,FDIFF_1:def 8
         .= diff(sec,arccot.x)*diff(arccot,x) by A9,A10,FDIFF_2:13
         .= (sin.(arccot.x)/(cos.(arccot.x))^2)*diff(arccot,x)
         by A11,FDIFF_9:1
         .= (sin.(arccot.x)/(cos.(arccot.x))^2)*((arccot)`|Z).x
         by A7,A8,FDIFF_1:def 8
         .= (sin.(arccot.x)/(cos.(arccot.x))^2)*(-1/(1+x^2))
         by A2,A7,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:77
         .= -sin.(arccot.x)/((cos.(arccot.x))^2*(1+x^2));
         hence thesis;
    end;
    hence thesis by A1,AA,FDIFF_1:16;
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:21;
      hence thesis by RFUNCT_1:13;
    end;
AA: for x st x in Z holds cosec*arctan is_differentiable_in x
    proof
        let x;
        assume
    A4: x in Z;
        arctan is_differentiable_on Z by A2,SIN_COS9:81;then
    A5: arctan is_differentiable_in x by A4,FDIFF_1:16;
        sin.(arctan.x) <> 0 by A3,A4;
        then cosec is_differentiable_in arctan.x by FDIFF_9:2;
        hence cosec*arctan is_differentiable_in x by A5,FDIFF_2:13;
    end;
    then
A6: cosec*arctan is_differentiable_on Z by A1,FDIFF_1:16;
    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
    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:16;
         sin.(arctan.x) <> 0 by A3,A7;then
    A10: cosec is_differentiable_in arctan.x by FDIFF_9:2;
    A11: sin.(arctan.x) <> 0 by A3,A7;
         ((cosec*arctan)`|Z).x = diff(cosec*arctan,x)
         by A6,A7,FDIFF_1:def 8
         .= diff(cosec,arctan.x)*diff(arctan,x) by A9,A10,FDIFF_2:13
         .= (-cos.(arctan.x)/(sin.(arctan.x))^2)*diff(arctan,x)
         by A11,FDIFF_9:2
         .= -(cos.(arctan.x)/(sin.(arctan.x))^2)*diff(arctan,x)
         .= -(cos.(arctan.x)/(sin.(arctan.x))^2)*((arctan)`|Z).x
         by A7,A8,FDIFF_1:def 8
         .= -(cos.(arctan.x)/(sin.(arctan.x))^2)*(1/(1+x^2))
         by A2,A7,SIN_COS9:81
         .= -(cos.(arctan.x)*1)/((sin.(arctan.x))^2*(1+x^2)) by XCMPLX_1:77
         .= -cos.(arctan.x)/((sin.(arctan.x))^2*(1+x^2));
         hence thesis;
    end;
    hence thesis by A1,AA,FDIFF_1:16;
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:21;
      hence thesis by RFUNCT_1:13;
    end;
AA: for x st x in Z holds cosec*arccot is_differentiable_in x
    proof
        let x;
        assume
    A4: x in Z;
        arccot is_differentiable_on Z by A2,SIN_COS9:82;then
    A5: arccot is_differentiable_in x by A4,FDIFF_1:16;
        sin.(arccot.x) <> 0 by A3,A4;
        then cosec is_differentiable_in arccot.x by FDIFF_9:2;
        hence cosec*arccot is_differentiable_in x by A5,FDIFF_2:13;
    end;
    then
A6: cosec*arccot is_differentiable_on Z by A1,FDIFF_1:16;
    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
    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:16;
         sin.(arccot.x) <> 0 by A3,A7;then
    A10: cosec is_differentiable_in arccot.x by FDIFF_9:2;
    A11: sin.(arccot.x) <> 0 by A3,A7;
         ((cosec*arccot)`|Z).x = diff(cosec*arccot,x)
         by A6,A7,FDIFF_1:def 8
         .= diff(cosec,arccot.x)*diff(arccot,x) by A9,A10,FDIFF_2:13
         .= (-cos.(arccot.x)/(sin.(arccot.x))^2)*diff(arccot,x)
         by A11,FDIFF_9:2
         .= -(cos.(arccot.x)/(sin.(arccot.x))^2)*diff(arccot,x)
         .= -(cos.(arccot.x)/(sin.(arccot.x))^2)*((arccot)`|Z).x
         by A7,A8,FDIFF_1:def 8
         .= -(cos.(arccot.x)/(sin.(arccot.x))^2)*(-1/(1+x^2))
         by A2,A7,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:77
         .= cos.(arccot.x)/((sin.(arccot.x))^2*(1+x^2));
         hence thesis;
    end;
    hence thesis by A1,AA,FDIFF_1:16;
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.[;
    Z c= dom sin /\ dom arctan by A1,VALUED_1:def 4;then
A3: Z c= dom sin by XBOOLE_1:18;
    for x st x in Z holds sin is_differentiable_in x by SIN_COS:69;then
A4: sin is_differentiable_on Z by A3,FDIFF_1:16;
A5: arctan is_differentiable_on Z by A2,SIN_COS9:81;
    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;
        ((sin(#)arctan)`|Z).x = (arctan.x)*diff(sin,x)+(sin.x)*diff(arctan,x)
        by A1,A4,A5,A6,FDIFF_1:29
        .= (arctan.x)*(cos.x)+(sin.x)*diff(arctan,x) by SIN_COS:69
        .= cos.x*arctan.x+(sin.x)*((arctan)`|Z).x by A5,A6,FDIFF_1:def 8
        .= 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,A4,A5,FDIFF_1:29;
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.[;
    Z c= dom sin /\ dom arccot by A1,VALUED_1:def 4;then
A3: Z c= dom sin by XBOOLE_1:18;
    for x st x in Z holds sin is_differentiable_in x by SIN_COS:69;then
A4: sin is_differentiable_on Z by A3,FDIFF_1:16;
A5: arccot is_differentiable_on Z by A2,SIN_COS9:82;
    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;
        ((sin(#)arccot)`|Z).x = (arccot.x)*diff(sin,x)+(sin.x)*diff(arccot,x)
        by A1,A4,A5,A6,FDIFF_1:29
        .= (arccot.x)*(cos.x)+(sin.x)*diff(arccot,x) by SIN_COS:69
        .= cos.x*arccot.x+(sin.x)*((arccot)`|Z).x by A5,A6,FDIFF_1:def 8
        .= 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,A4,A5,FDIFF_1:29;
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.[;
    Z c= dom cos /\ dom arctan by A1,VALUED_1:def 4;then
A3: Z c= dom cos by XBOOLE_1:18;
    for x st x in Z holds cos is_differentiable_in x by SIN_COS:68;then
A4: cos is_differentiable_on Z by A3,FDIFF_1:16;
A5: arctan is_differentiable_on Z by A2,SIN_COS9:81;
    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;
        ((cos(#)arctan)`|Z).x = (arctan.x)*diff(cos,x)+(cos.x)*diff(arctan,x)
        by A1,A4,A5,A6,FDIFF_1:29
        .= (arctan.x)*(-sin.x)+(cos.x)*diff(arctan,x) by SIN_COS:68
        .= -sin.x*arctan.x+(cos.x)*((arctan)`|Z).x by A5,A6,FDIFF_1:def 8
        .= -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,A4,A5,FDIFF_1:29;
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.[;
    Z c= dom cos /\ dom arccot by A1,VALUED_1:def 4;then
A3: Z c= dom cos by XBOOLE_1:18;
    for x st x in Z holds cos is_differentiable_in x by SIN_COS:68;then
A4: cos is_differentiable_on Z by A3,FDIFF_1:16;
A5: arccot is_differentiable_on Z by A2,SIN_COS9:82;
    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;
        ((cos(#)arccot)`|Z).x = (arccot.x)*diff(cos,x)+(cos.x)*diff(arccot,x)
        by A1,A4,A5,A6,FDIFF_1:29
        .= (arccot.x)*(-sin.x)+(cos.x)*diff(arccot,x) by SIN_COS:68
        .= -sin.x*arccot.x+(cos.x)*((arccot)`|Z).x by A5,A6,FDIFF_1:def 8
        .= -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,A4,A5,FDIFF_1:29;
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.[;
    Z c= dom tan /\ dom arctan by A1,VALUED_1:def 4;then
A3: 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 A3,FDIFF_8:1;
      hence thesis by FDIFF_7:46;
    end;
    then
A4: tan is_differentiable_on Z by A3,FDIFF_1:16;
A5: arctan is_differentiable_on Z by A2,SIN_COS9:81;
    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 A3,FDIFF_8:1;
        ((tan(#)arctan)`|Z).x = (arctan.x)*diff(tan,x)+(tan.x)*diff(arctan,x)
        by A1,A4,A5,A6,FDIFF_1:29
        .= (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 A5,A6,FDIFF_1:def 8
        .= 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,A4,A5,FDIFF_1:29;
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.[;
    Z c= dom tan /\ dom arccot by A1,VALUED_1:def 4;then
A3: 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 A3,FDIFF_8:1;
      hence thesis by FDIFF_7:46;
    end;
    then
A4: tan is_differentiable_on Z by A3,FDIFF_1:16;
A5: arccot is_differentiable_on Z by A2,SIN_COS9:82;
    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 A3,FDIFF_8:1;
        ((tan(#)arccot)`|Z).x = (arccot.x)*diff(tan,x)+(tan.x)*diff(arccot,x)
        by A1,A4,A5,A6,FDIFF_1:29
        .= (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 A5,A6,FDIFF_1:def 8
        .= 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,A4,A5,FDIFF_1:29;
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.[;
    Z c= dom cot /\ dom arctan by A1,VALUED_1:def 4;then
A3: 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 A3,FDIFF_8:2;
      hence thesis by FDIFF_7:47;
    end;
    then
A4: cot is_differentiable_on Z by A3,FDIFF_1:16;
A5: arctan is_differentiable_on Z by A2,SIN_COS9:81;
    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 A3,FDIFF_8:2;
        ((cot(#)arctan)`|Z).x = (arctan.x)*diff(cot,x)+(cot.x)*diff(arctan,x)
        by A1,A4,A5,A6,FDIFF_1:29
        .= (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 A5,A6,FDIFF_1:def 8
        .= -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,A4,A5,FDIFF_1:29;
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.[;
    Z c= dom cot /\ dom arccot by A1,VALUED_1:def 4;then
A3: 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 A3,FDIFF_8:2;
      hence thesis by FDIFF_7:47;
    end;
    then
A4: cot is_differentiable_on Z by A3,FDIFF_1:16;
A5: arccot is_differentiable_on Z by A2,SIN_COS9:82;
    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 A3,FDIFF_8:2;
        ((cot(#)arccot)`|Z).x = (arccot.x)*diff(cot,x)+(cot.x)*diff(arccot,x)
        by A1,A4,A5,A6,FDIFF_1:29
        .= (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 A5,A6,FDIFF_1:def 8
        .= -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,A4,A5,FDIFF_1:29;
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.[;
    Z c= dom sec /\ dom arctan by A1,VALUED_1:def 4;then
A3: 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 A3,RFUNCT_1:13;
      hence thesis by FDIFF_9:1;
    end;
    then
A4: sec is_differentiable_on Z by A3,FDIFF_1:16;
A5: arctan is_differentiable_on Z by A2,SIN_COS9:81;
    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 A3,RFUNCT_1:13;
        ((sec(#)arctan)`|Z).x = (arctan.x)*diff(sec,x)+(sec.x)*diff(arctan,x)
        by A1,A4,A5,A6,FDIFF_1:29
        .= (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 A5,A6,FDIFF_1:def 8
        .= (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 A3,A6,RFUNCT_1:def 8
        .= (sin.x*arctan.x)/(cos.x)^2+1/(cos.x*(1+x^2)) by XCMPLX_1:103;
        hence thesis;
    end;
    hence thesis by A1,A4,A5,FDIFF_1:29;
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.[;
    Z c= dom sec /\ dom arccot by A1,VALUED_1:def 4;then
A3: 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 A3,RFUNCT_1:13;
      hence thesis by FDIFF_9:1;
    end;
    then
A4: sec is_differentiable_on Z by A3,FDIFF_1:16;
A5: arccot is_differentiable_on Z by A2,SIN_COS9:82;
    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 A3,RFUNCT_1:13;
        ((sec(#)arccot)`|Z).x = (arccot.x)*diff(sec,x)+(sec.x)*diff(arccot,x)
        by A1,A4,A5,A6,FDIFF_1:29
        .= (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 A5,A6,FDIFF_1:def 8
        .= (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 A3,A6,RFUNCT_1:def 8
        .= (sin.x*arccot.x)/(cos.x)^2-1/(cos.x*(1+x^2)) by XCMPLX_1:103;
        hence thesis;
    end;
    hence thesis by A1,A4,A5,FDIFF_1:29;
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.[;
    Z c= dom cosec /\ dom arctan by A1,VALUED_1:def 4;then
A3: 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 A3,RFUNCT_1:13;
      hence thesis by FDIFF_9:2;
    end;
    then
A4: cosec is_differentiable_on Z by A3,FDIFF_1:16;
A5: arctan is_differentiable_on Z by A2,SIN_COS9:81;
    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 A3,RFUNCT_1:13;
        ((cosec(#)arctan)`|Z).x
        = (arctan.x)*diff(cosec,x)+(cosec.x)*diff(arctan,x)
        by A1,A4,A5,A6,FDIFF_1:29
        .= (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 A5,A6,FDIFF_1:def 8
        .= -(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 A3,A6,RFUNCT_1:def 8
        .= -(cos.x*arctan.x)/(sin.x)^2+1/(sin.x*(1+x^2)) by XCMPLX_1:103;
        hence thesis;
    end;
    hence thesis by A1,A4,A5,FDIFF_1:29;
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.[;
    Z c= dom cosec /\ dom arccot by A1,VALUED_1:def 4;then
A3: 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 A3,RFUNCT_1:13;
      hence thesis by FDIFF_9:2;
    end;
    then
A4: cosec is_differentiable_on Z by A3,FDIFF_1:16;
A5: arccot is_differentiable_on Z by A2,SIN_COS9:82;
    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 A3,RFUNCT_1:13;
        ((cosec(#)arccot)`|Z).x
        = (arccot.x)*diff(cosec,x)+(cosec.x)*diff(arccot,x)
        by A1,A4,A5,A6,FDIFF_1:29
        .= (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 A5,A6,FDIFF_1:def 8
        .= -(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 A3,A6,RFUNCT_1:def 8
        .= -(cos.x*arccot.x)/(sin.x)^2-1/(sin.x*(1+x^2)) by XCMPLX_1:103;
        hence thesis;
    end;
    hence thesis by A1,A4,A5,FDIFF_1:29;
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.[;
A2: ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
    then ].-1,1.[ c= dom arctan by SIN_COS9:23,XBOOLE_1:1;then
A3: Z c= dom arctan by A1,XBOOLE_1:1;
    ].-1,1.[ c= dom arccot by A2,SIN_COS9:24,XBOOLE_1:1;
    then Z c= dom arccot by A1,XBOOLE_1:1;
    then Z c= dom arctan /\ dom arccot by A3,XBOOLE_1:19;then
A4: Z c= dom (arctan+arccot) by VALUED_1:def 1;
A5: arctan is_differentiable_on Z by A1,SIN_COS9:81;
A6: arccot is_differentiable_on Z by A1,SIN_COS9:82;
    for x st x in Z holds ((arctan+arccot)`|Z).x = 0
    proof
        let x;
        assume
    A7: x in Z;
        ((arctan+arccot)`|Z).x = diff(arctan,x)+diff(arccot,x)
        by A4,A5,A6,A7,FDIFF_1:26
        .= ((arctan)`|Z).x+diff(arccot,x) by A5,A7,FDIFF_1:def 8
        .= 1/(1+x^2)+diff(arccot,x) by A1,A7,SIN_COS9:81
        .= 1/(1+x^2)+((arccot)`|Z).x by A6,A7,FDIFF_1:def 8
        .= 1/(1+x^2)+(-1/(1+x^2)) by A1,A7,SIN_COS9:82
        .= 0;
        hence thesis;
    end;
    hence thesis by A4,A5,A6,FDIFF_1:26;
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.[;
A2: ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
    then ].-1,1.[ c= dom arctan by SIN_COS9:23,XBOOLE_1:1;then
A3: Z c= dom arctan by A1,XBOOLE_1:1;
    ].-1,1.[ c= dom arccot by A2,SIN_COS9:24,XBOOLE_1:1;
    then Z c= dom arccot by A1,XBOOLE_1:1;
    then Z c= dom arctan /\ dom arccot by A3,XBOOLE_1:19;then
A4: Z c= dom (arctan-arccot) by VALUED_1:12;
A5: arctan is_differentiable_on Z by A1,SIN_COS9:81;
A6: arccot is_differentiable_on Z by A1,SIN_COS9:82;
    for x st x in Z holds ((arctan-arccot)`|Z).x = 2/(1+x^2)
    proof
        let x;
        assume
    A7: x in Z;
        ((arctan-arccot)`|Z).x = diff(arctan,x)-diff(arccot,x)
        by A4,A5,A6,A7,FDIFF_1:27
        .= ((arctan)`|Z).x-diff(arccot,x) by A5,A7,FDIFF_1:def 8
        .= 1/(1+x^2)-diff(arccot,x) by A1,A7,SIN_COS9:81
        .= 1/(1+x^2)-((arccot)`|Z).x by A6,A7,FDIFF_1:def 8
        .= 1/(1+x^2)-(-1/(1+x^2)) by A1,A7,SIN_COS9:82
        .= 2/(1+x^2);
        hence thesis;
    end;
    hence thesis by A4,A5,A6,FDIFF_1:27;
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
    assume
A1: Z c= ].-1,1.[;
A3: ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
    then ].-1,1.[ c= dom arctan by SIN_COS9:23,XBOOLE_1:1;then
A4: Z c= dom arctan by A1,XBOOLE_1:1;
    ].-1,1.[ c= dom arccot by A3,SIN_COS9:24,XBOOLE_1:1;
    then Z c= dom arccot 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 sin /\ dom (arctan+arccot)
    by SIN_COS:27,XBOOLE_1:19;then
A6: Z c= dom (sin(#)(arctan+arccot)) by VALUED_1:def 4;
    for x st x in Z holds sin is_differentiable_in x by SIN_COS:69;then
A7: sin is_differentiable_on Z by SIN_COS:27,FDIFF_1:16;
A8: arctan+arccot is_differentiable_on Z & for x st x in Z holds
    ((arctan+arccot)`|Z).x = 0 by A1,Th37;
    for x st x in Z holds
    (sin(#)(arctan+arccot)`|Z).x = cos.x*(arctan.x+arccot.x)
    proof
        let x;
        assume
    A9: x in Z;
        (sin(#)(arctan+arccot)`|Z).x
        = ((arctan+arccot).x)*diff(sin,x)+sin.x*diff(arctan+arccot,x)
        by A6,A7,A8,A9,FDIFF_1:29
        .= (arctan.x+arccot.x)*diff(sin,x)+sin.x*diff(arctan+arccot,x)
        by A5,A9,VALUED_1:def 1
        .= (arctan.x+arccot.x)*cos.x+sin.x*diff(arctan+arccot,x)
        by SIN_COS:69
        .= (arctan.x+arccot.x)*cos.x+sin.x*((arctan+arccot)`|Z).x
        by A8,A9,FDIFF_1:def 8
        .= (arctan.x+arccot.x)*cos.x+sin.x*0 by A1,A9,Th37
        .= cos.x*(arctan.x+arccot.x);
        hence thesis;
    end;
    hence thesis by A6,A7,A8,FDIFF_1:29;
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
    assume
A1: Z c= ].-1,1.[;
A3: ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
    then ].-1,1.[ c= dom arctan by SIN_COS9:23,XBOOLE_1:1;then
A4: Z c= dom arctan by A1,XBOOLE_1:1;
    ].-1,1.[ c= dom arccot by A3,SIN_COS9:24,XBOOLE_1:1;
    then Z c= dom arccot 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 sin /\ dom (arctan-arccot)
    by SIN_COS:27,XBOOLE_1:19;then
A6: Z c= dom (sin(#)(arctan-arccot)) by VALUED_1:def 4;
    for x st x in Z holds sin is_differentiable_in x by SIN_COS:69;then
A7: sin is_differentiable_on Z by SIN_COS:27,FDIFF_1:16;
A8: arctan-arccot is_differentiable_on Z & for x st x in Z holds
    ((arctan-arccot)`|Z).x = 2/(1+x^2) by A1,Th38;
    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
    A9: x in Z;
        (sin(#)(arctan-arccot)`|Z).x
        = ((arctan-arccot).x)*diff(sin,x)+sin.x*diff(arctan-arccot,x)
        by A6,A7,A8,A9,FDIFF_1:29
        .= (arctan.x-arccot.x)*diff(sin,x)+sin.x*diff(arctan-arccot,x)
        by A5,A9,VALUED_1:13
        .= (arctan.x-arccot.x)*cos.x+sin.x*diff(arctan-arccot,x)
        by SIN_COS:69
        .= (arctan.x-arccot.x)*cos.x+sin.x*((arctan-arccot)`|Z).x
        by A8,A9,FDIFF_1:def 8
        .= (arctan.x-arccot.x)*cos.x+sin.x*(2/(1+x^2)) by A1,A9,Th38
        .= cos.x*(arctan.x-arccot.x)+2*sin.x/(1+x^2);
        hence thesis;
    end;
    hence thesis by A6,A7,A8,FDIFF_1:29;
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
    assume
A1: Z c= ].-1,1.[;
A3: ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
    then ].-1,1.[ c= dom arctan by SIN_COS9:23,XBOOLE_1:1;then
A4: Z c= dom arctan by A1,XBOOLE_1:1;
    ].-1,1.[ c= dom arccot by A3,SIN_COS9:24,XBOOLE_1:1;
    then Z c= dom arccot 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 cos /\ dom (arctan+arccot)
    by SIN_COS:27,XBOOLE_1:19;then
A6: Z c= dom (cos(#)(arctan+arccot)) by VALUED_1:def 4;
    for x st x in Z holds cos is_differentiable_in x by SIN_COS:68;then
A7: cos is_differentiable_on Z by SIN_COS:27,FDIFF_1:16;
A8: arctan+arccot is_differentiable_on Z & for x st x in Z holds
    ((arctan+arccot)`|Z).x = 0 by A1,Th37;
    for x st x in Z holds
    (cos(#)(arctan+arccot)`|Z).x = -sin.x*(arctan.x+arccot.x)
    proof
        let x;
        assume
    A9: x in Z;
        (cos(#)(arctan+arccot)`|Z).x
        = ((arctan+arccot).x)*diff(cos,x)+cos.x*diff(arctan+arccot,x)
        by A6,A7,A8,A9,FDIFF_1:29
        .= (arctan.x+arccot.x)*diff(cos,x)+cos.x*diff(arctan+arccot,x)
        by A5,A9,VALUED_1:def 1
        .= (arctan.x+arccot.x)*(-sin.x)+cos.x*diff(arctan+arccot,x)
        by SIN_COS:68
        .= (arctan.x+arccot.x)*(-sin.x)+cos.x*((arctan+arccot)`|Z).x
        by A8,A9,FDIFF_1:def 8
        .= -(arctan.x+arccot.x)*sin.x+cos.x*0 by A1,A9,Th37
        .= -sin.x*(arctan.x+arccot.x);
        hence thesis;
    end;
    hence thesis by A6,A7,A8,FDIFF_1:29;
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
    assume
A1: Z c= ].-1,1.[;
A3: ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
    then ].-1,1.[ c= dom arctan by SIN_COS9:23,XBOOLE_1:1;then
A4: Z c= dom arctan by A1,XBOOLE_1:1;
    ].-1,1.[ c= dom arccot by A3,SIN_COS9:24,XBOOLE_1:1;
    then Z c= dom arccot 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 cos /\ dom (arctan-arccot)
    by SIN_COS:27,XBOOLE_1:19;then
A6: Z c= dom (cos(#)(arctan-arccot)) by VALUED_1:def 4;
    for x st x in Z holds cos is_differentiable_in x by SIN_COS:68;then
A7: cos is_differentiable_on Z by SIN_COS:27,FDIFF_1:16;
A8: arctan-arccot is_differentiable_on Z & for x st x in Z holds
    ((arctan-arccot)`|Z).x = 2/(1+x^2) by A1,Th38;
    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
    A9: x in Z;
        (cos(#)(arctan-arccot)`|Z).x
        = ((arctan-arccot).x)*diff(cos,x)+cos.x*diff(arctan-arccot,x)
        by A6,A7,A8,A9,FDIFF_1:29
        .= (arctan.x-arccot.x)*diff(cos,x)+cos.x*diff(arctan-arccot,x)
        by A5,A9,VALUED_1:13
        .= (arctan.x-arccot.x)*(-sin.x)+cos.x*diff(arctan-arccot,x)
        by SIN_COS:68
        .= (arctan.x-arccot.x)*(-sin.x)+cos.x*((arctan-arccot)`|Z).x
        by A8,A9,FDIFF_1:def 8
        .= -(arctan.x-arccot.x)*sin.x+cos.x*(2/(1+x^2)) by A1,A9,Th38
        .= -sin.x*(arctan.x-arccot.x)+2*cos.x/(1+x^2);
        hence thesis;
    end;
    hence thesis by A6,A7,A8,FDIFF_1:29;
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: ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
    then ].-1,1.[ c= dom arctan by SIN_COS9:23,XBOOLE_1:1;then
A4: Z c= dom arctan by A2,XBOOLE_1:1;
    ].-1,1.[ c= dom arccot by A3,SIN_COS9:24,XBOOLE_1:1;
    then Z c= dom arccot 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:def 1;
    then Z c= dom tan /\ dom (arctan+arccot) by A1,XBOOLE_1:19;then
A6: Z c= dom (tan(#)(arctan+arccot)) by VALUED_1:def 4;
    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
A7: tan is_differentiable_on Z by A1,FDIFF_1:16;
A8: arctan+arccot is_differentiable_on Z & for x st x in Z holds
    ((arctan+arccot)`|Z).x = 0 by A2,Th37;
    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 A6,A7,A8,A9,FDIFF_1:29
         .= (arctan.x+arccot.x)*diff(tan,x)+tan.x*diff(arctan+arccot,x)
         by A5,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 A8,A9,FDIFF_1:def 8
         .= (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 A6,A7,A8,FDIFF_1:29;
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: ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
    then ].-1,1.[ c= dom arctan by SIN_COS9:23,XBOOLE_1:1;then
A4: Z c= dom arctan by A2,XBOOLE_1:1;
    ].-1,1.[ c= dom arccot by A3,SIN_COS9:24,XBOOLE_1:1;
    then Z c= dom arccot 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;
    then Z c= dom tan /\ dom (arctan-arccot) by A1,XBOOLE_1:19;then
A6: Z c= dom (tan(#)(arctan-arccot)) by VALUED_1:def 4;
    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
A7: tan is_differentiable_on Z by A1,FDIFF_1:16;
A8: arctan-arccot is_differentiable_on Z & for x st x in Z holds
    ((arctan-arccot)`|Z).x = 2/(1+x^2) by A2,Th38;
    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 A6,A7,A8,A9,FDIFF_1:29
         .= (arctan.x-arccot.x)*diff(tan,x)+tan.x*diff(arctan-arccot,x)
         by A5,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 A8,A9,FDIFF_1:def 8
         .= (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 A6,A7,A8,FDIFF_1:29;
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: ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
    then ].-1,1.[ c= dom arctan by SIN_COS9:23,XBOOLE_1:1;then
A4: Z c= dom arctan by A2,XBOOLE_1:1;
    ].-1,1.[ c= dom arccot by A3,SIN_COS9:24,XBOOLE_1:1;
    then Z c= dom arccot 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:def 1;
    then Z c= dom cot /\ dom (arctan+arccot) by A1,XBOOLE_1:19;then
A6: Z c= dom (cot(#)(arctan+arccot)) by VALUED_1:def 4;
    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
A7: cot is_differentiable_on Z by A1,FDIFF_1:16;
A8: arctan+arccot is_differentiable_on Z & for x st x in Z holds
    ((arctan+arccot)`|Z).x = 0 by A2,Th37;
    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 A6,A7,A8,A9,FDIFF_1:29
         .= (arctan.x+arccot.x)*diff(cot,x)+cot.x*diff(arctan+arccot,x)
         by A5,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 A8,A9,FDIFF_1:def 8
         .= -(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 A6,A7,A8,FDIFF_1:29;
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: ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
    then ].-1,1.[ c= dom arctan by SIN_COS9:23,XBOOLE_1:1;then
A4: Z c= dom arctan by A2,XBOOLE_1:1;
    ].-1,1.[ c= dom arccot by A3,SIN_COS9:24,XBOOLE_1:1;
    then Z c= dom arccot 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;
    then Z c= dom cot /\ dom (arctan-arccot) by A1,XBOOLE_1:19;then
A6: Z c= dom (cot(#)(arctan-arccot)) by VALUED_1:def 4;
    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
A7: cot is_differentiable_on Z by A1,FDIFF_1:16;
A8: arctan-arccot is_differentiable_on Z & for x st x in Z holds
    ((arctan-arccot)`|Z).x = 2/(1+x^2) by A2,Th38;
    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 A6,A7,A8,A9,FDIFF_1:29
         .= (arctan.x-arccot.x)*diff(cot,x)+cot.x*diff(arctan-arccot,x)
         by A5,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 A8,A9,FDIFF_1:def 8
         .= -(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 A6,A7,A8,FDIFF_1:29;
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: ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
    then ].-1,1.[ c= dom arctan by SIN_COS9:23,XBOOLE_1:1;then
A4: Z c= dom arctan by A2,XBOOLE_1:1;
    ].-1,1.[ c= dom arccot by A3,SIN_COS9:24,XBOOLE_1:1;
    then Z c= dom arccot 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:def 1;
    then Z c= dom sec /\ dom (arctan+arccot) by A1,XBOOLE_1:19;then
A6: Z c= dom (sec(#)(arctan+arccot)) by VALUED_1:def 4;
    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:13;
      hence thesis by FDIFF_9:1;
    end;
    then
A7: sec is_differentiable_on Z by A1,FDIFF_1:16;
A8: arctan+arccot is_differentiable_on Z & for x st x in Z holds
    ((arctan+arccot)`|Z).x = 0 by A2,Th37;
    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:13;
         (sec(#)(arctan+arccot)`|Z).x
         = ((arctan+arccot).x)*diff(sec,x)+sec.x*diff(arctan+arccot,x)
         by A6,A7,A8,A9,FDIFF_1:29
         .= (arctan.x+arccot.x)*diff(sec,x)+sec.x*diff(arctan+arccot,x)
         by A5,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 A8,A9,FDIFF_1:def 8
         .= (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 A6,A7,A8,FDIFF_1:29;
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: ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
    then ].-1,1.[ c= dom arctan by SIN_COS9:23,XBOOLE_1:1;then
A4: Z c= dom arctan by A2,XBOOLE_1:1;
    ].-1,1.[ c= dom arccot by A3,SIN_COS9:24,XBOOLE_1:1;
    then Z c= dom arccot 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;
    then Z c= dom sec /\ dom (arctan-arccot) by A1,XBOOLE_1:19;then
A6: Z c= dom (sec(#)(arctan-arccot)) by VALUED_1:def 4;
    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:13;
      hence thesis by FDIFF_9:1;
    end;
    then
A7: sec is_differentiable_on Z by A1,FDIFF_1:16;
A8: arctan-arccot is_differentiable_on Z & for x st x in Z holds
    ((arctan-arccot)`|Z).x = 2/(1+x^2) by A2,Th38;
    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:13;
         (sec(#)(arctan-arccot)`|Z).x
         = ((arctan-arccot).x)*diff(sec,x)+sec.x*diff(arctan-arccot,x)
         by A6,A7,A8,A9,FDIFF_1:29
         .= (arctan.x-arccot.x)*diff(sec,x)+sec.x*diff(arctan-arccot,x)
         by A5,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 A8,A9,FDIFF_1:def 8
         .= (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 A6,A7,A8,FDIFF_1:29;
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: ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
    then ].-1,1.[ c= dom arctan by SIN_COS9:23,XBOOLE_1:1;then
A4: Z c= dom arctan by A2,XBOOLE_1:1;
    ].-1,1.[ c= dom arccot by A3,SIN_COS9:24,XBOOLE_1:1;
    then Z c= dom arccot 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:def 1;
    then Z c= dom cosec /\ dom (arctan+arccot) by A1,XBOOLE_1:19;then
A6: Z c= dom (cosec(#)(arctan+arccot)) by VALUED_1:def 4;
    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:13;
      hence thesis by FDIFF_9:2;
    end;
    then
A7: cosec is_differentiable_on Z by A1,FDIFF_1:16;
A8: arctan+arccot is_differentiable_on Z & for x st x in Z holds
    ((arctan+arccot)`|Z).x = 0 by A2,Th37;
    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:13;
         (cosec(#)(arctan+arccot)`|Z).x
         = ((arctan+arccot).x)*diff(cosec,x)+cosec.x*diff(arctan+arccot,x)
         by A6,A7,A8,A9,FDIFF_1:29
         .= (arctan.x+arccot.x)*diff(cosec,x)+cosec.x*diff(arctan+arccot,x)
         by A5,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 A8,A9,FDIFF_1:def 8
         .= -(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 A6,A7,A8,FDIFF_1:29;
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: ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
    then ].-1,1.[ c= dom arctan by SIN_COS9:23,XBOOLE_1:1;then
A4: Z c= dom arctan by A2,XBOOLE_1:1;
    ].-1,1.[ c= dom arccot by A3,SIN_COS9:24,XBOOLE_1:1;
    then Z c= dom arccot 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;
    then Z c= dom cosec /\ dom (arctan-arccot) by A1,XBOOLE_1:19;then
A6: Z c= dom (cosec(#)(arctan-arccot)) by VALUED_1:def 4;
    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:13;
      hence thesis by FDIFF_9:2;
    end;
    then
A7: cosec is_differentiable_on Z by A1,FDIFF_1:16;
A8: arctan-arccot is_differentiable_on Z & for x st x in Z holds
    ((arctan-arccot)`|Z).x = 2/(1+x^2) by A2,Th38;
    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:13;
         (cosec(#)(arctan-arccot)`|Z).x
         = ((arctan-arccot).x)*diff(cosec,x)+cosec.x*diff(arctan-arccot,x)
         by A6,A7,A8,A9,FDIFF_1:29
         .= (arctan.x-arccot.x)*diff(cosec,x)+cosec.x*diff(arctan-arccot,x)
         by A5,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 A8,A9,FDIFF_1:def 8
         .= -(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 A6,A7,A8,FDIFF_1:29;
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.[;
A3: ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
    then ].-1,1.[ c= dom arctan by SIN_COS9:23,XBOOLE_1:1;then
A4: Z c= dom arctan by A1,XBOOLE_1:1;
    ].-1,1.[ c= dom arccot by A3,SIN_COS9:24,XBOOLE_1:1;
    then Z c= dom arccot 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 TAYLOR_1:16,FDIFF_1:34;
A8: arctan+arccot is_differentiable_on Z & for x st x in Z holds
    ((arctan+arccot)`|Z).x = 0 by A1,Th37;
    for x st x in Z holds
    (exp_R(#)(arctan+arccot)`|Z).x = exp_R.x*(arctan.x+arccot.x)
    proof
        let x;
        assume
    A9: x in Z;
        (exp_R(#)(arctan+arccot)`|Z).x
        = ((arctan+arccot).x)*diff(exp_R,x)+exp_R.x*diff(arctan+arccot,x)
        by A6,A7,A8,A9,FDIFF_1:29
        .= (arctan.x+arccot.x)*diff(exp_R,x)+exp_R.x*diff(arctan+arccot,x)
        by A5,A9,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 A8,A9,FDIFF_1:def 8
        .= (arctan.x+arccot.x)*exp_R.x+exp_R.x*0 by A1,A9,Th37
        .= exp_R.x*(arctan.x+arccot.x);
        hence thesis;
    end;
    hence thesis by A6,A7,A8,FDIFF_1:29;
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.[;
A3: ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
    then ].-1,1.[ c= dom arctan by SIN_COS9:23,XBOOLE_1:1;then
A4: Z c= dom arctan by A1,XBOOLE_1:1;
    ].-1,1.[ c= dom arccot by A3,SIN_COS9:24,XBOOLE_1:1;
    then Z c= dom arccot 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 TAYLOR_1:16,FDIFF_1:34;
A8: arctan-arccot is_differentiable_on Z & for x st x in Z holds
    ((arctan-arccot)`|Z).x = 2/(1+x^2) by A1,Th38;
    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
    A9: x in Z;
        (exp_R(#)(arctan-arccot)`|Z).x
        = ((arctan-arccot).x)*diff(exp_R,x)+exp_R.x*diff(arctan-arccot,x)
        by A6,A7,A8,A9,FDIFF_1:29
        .= (arctan.x-arccot.x)*diff(exp_R,x)+exp_R.x*diff(arctan-arccot,x)
        by A5,A9,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 A8,A9,FDIFF_1:def 8
        .= (arctan.x-arccot.x)*exp_R.x+exp_R.x*(2/(1+x^2)) by A1,A9,Th38
        .= exp_R.x*(arctan.x-arccot.x)+2*exp_R.x/(1+x^2);
        hence thesis;
    end;
    hence thesis by A6,A7,A8,FDIFF_1:29;
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.[;
A2: ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
    then ].-1,1.[ c= dom arctan by SIN_COS9:23,XBOOLE_1:1;then
A3: Z c= dom arctan by A1,XBOOLE_1:1;
    ].-1,1.[ c= dom arccot by A2,SIN_COS9:24,XBOOLE_1:1;
    then Z c= dom arccot by A1,XBOOLE_1:1;
    then Z c= dom arctan /\ dom arccot by A3,XBOOLE_1:19;then
A4: Z c= dom (arctan+arccot) by VALUED_1:def 1;
A5: arctan+arccot is_differentiable_on Z & for x st x in Z holds
    ((arctan+arccot)`|Z).x = 0 by A1,Th37;
A6: exp_R is_differentiable_on Z by TAYLOR_1:16,FDIFF_1:34;
A7: for x st x in Z holds exp_R.x<>0 by SIN_COS:59;then
A8: (arctan+arccot)/exp_R is_differentiable_on Z by A5,A6,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;
         assume
    A9:  x in Z;
    A10: arctan+arccot is_differentiable_in x by A5,A9,FDIFF_1:16;
    A11: exp_R is_differentiable_in x by SIN_COS:70;
    A12: exp_R.x <>0 by SIN_COS:59;
         (((arctan+arccot)/exp_R)`|Z).x = diff((arctan+arccot)/exp_R,x)
         by A8,A9,FDIFF_1:def 8
         .= (diff(arctan+arccot,x)*exp_R.x-diff(exp_R,x)*(arctan+arccot).x)
         /(exp_R.x)^2 by A10,A11,A12,FDIFF_2:14
         .= (((arctan+arccot)`|Z).x*exp_R.x-diff(exp_R,x)*(arctan+arccot).x)
         /(exp_R.x)^2 by A5,A9,FDIFF_1:def 8
         .= (0*exp_R.x-diff(exp_R,x)*(arctan+arccot).x)/(exp_R.x)^2
         by A1,A9,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:70
         .= -(arctan.x+arccot.x)*exp_R.x/(exp_R.x*exp_R.x)
         by A4,A9,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:79
         .= -(arctan.x+arccot.x)*(1/exp_R.x) by A12,XCMPLX_1:60
         .= -(arctan.x+arccot.x)/exp_R.x;
         hence thesis;
    end;
    hence thesis by A5,A6,A7,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.[;
A2: ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
    then ].-1,1.[ c= dom arctan by SIN_COS9:23,XBOOLE_1:1;then
A3: Z c= dom arctan by A1,XBOOLE_1:1;
    ].-1,1.[ c= dom arccot by A2,SIN_COS9:24,XBOOLE_1:1;
    then Z c= dom arccot by A1,XBOOLE_1:1;
    then Z c= dom arctan /\ dom arccot by A3,XBOOLE_1:19;then
A4: Z c= dom (arctan-arccot) by VALUED_1:12;
A5: arctan-arccot is_differentiable_on Z & for x st x in Z holds
    ((arctan-arccot)`|Z).x = 2/(1+x^2) by A1,Th38;
A6: exp_R is_differentiable_on Z by TAYLOR_1:16,FDIFF_1:34;
A7: for x st x in Z holds exp_R.x<>0 by SIN_COS:59;then
A8: (arctan-arccot)/exp_R is_differentiable_on Z by A5,A6,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;
         assume
    A9:  x in Z;
    A10: arctan-arccot is_differentiable_in x by A5,A9,FDIFF_1:16;
    A11: exp_R is_differentiable_in x by SIN_COS:70;
    A12: exp_R.x <>0 by SIN_COS:59;
         (((arctan-arccot)/exp_R)`|Z).x = diff((arctan-arccot)/exp_R,x)
         by A8,A9,FDIFF_1:def 8
         .= (diff(arctan-arccot,x)*exp_R.x-diff(exp_R,x)*(arctan-arccot).x)
         /(exp_R.x)^2 by A10,A11,A12,FDIFF_2:14
         .= (((arctan-arccot)`|Z).x*exp_R.x-diff(exp_R,x)*(arctan-arccot).x)
         /(exp_R.x)^2 by A5,A9,FDIFF_1:def 8
         .= ((2/(1+x^2))*exp_R.x-diff(exp_R,x)*(arctan-arccot).x)/(exp_R.x)^2
         by A1,A9,Th38
         .= ((2/(1+x^2))*exp_R.x-exp_R.x*(arctan-arccot).x)/(exp_R.x)^2
         by SIN_COS:70
         .= ((2/(1+x^2))*exp_R.x-exp_R.x*(arctan.x-arccot.x))/(exp_R.x)^2
         by A4,A9,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:79
         .= ((2/(1+x^2))-(arctan.x-arccot.x))*(1/exp_R.x) by A12,XCMPLX_1:60
         .= ((2/(1+x^2))-arctan.x+arccot.x)/exp_R.x;
         hence thesis;
    end;
    hence thesis by A5,A6,A7,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 & for x st x in Z holds
    ((arctan+arccot)`|Z).x = 0 by A2,Th37;
A4: for x st x in Z holds exp_R*(arctan+arccot) is_differentiable_in x
    proof
        let x;
        assume
    A5: x in Z;
    A6: (arctan+arccot) is_differentiable_in x by A3,A5,FDIFF_1:16;
        exp_R is_differentiable_in (arctan+arccot).x by SIN_COS:70;
        hence exp_R*(arctan+arccot) is_differentiable_in x by A6,FDIFF_2:13;
    end;
    then
A7: exp_R*(arctan+arccot) is_differentiable_on Z by A1,FDIFF_1:16;
    for x st x in Z holds (exp_R*(arctan+arccot)`|Z).x = 0
    proof
         let x;
         assume
    A8:  x in Z;then
    A9:  arctan+arccot is_differentiable_in x by A3,FDIFF_1:16;
    A10: exp_R is_differentiable_in (arctan+arccot).x by SIN_COS:70;
         (exp_R*(arctan+arccot)`|Z).x = diff(exp_R*(arctan+arccot),x)
         by A7,A8,FDIFF_1:def 8
         .= diff(exp_R,(arctan+arccot).x)*diff((arctan+arccot),x)
         by A9,A10,FDIFF_2:13
         .= exp_R.((arctan+arccot).x)*diff((arctan+arccot),x)
         by SIN_COS:70
         .= exp_R.((arctan+arccot).x)*((arctan+arccot)`|Z).x
         by A3,A8,FDIFF_1:def 8
         .= exp_R.((arctan+arccot).x)*0 by A2,A8,Th37
         .= 0;
         hence thesis;
    end;
    hence thesis by A1,A4,FDIFF_1:16;
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 arctan by SIN_COS9:23,XBOOLE_1:1;then
A4:  Z c= dom arctan by A2,XBOOLE_1:1;
     ].-1,1.[ c= dom arccot by A3,SIN_COS9:24,XBOOLE_1:1;
     then Z c= dom arccot 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 & for x st x in Z holds
     ((arctan-arccot)`|Z).x = 2/(1+x^2) by A2,Th38;
A7:  for x st x in Z holds exp_R*(arctan-arccot) is_differentiable_in x
     proof
         let x;
         assume
     A8: x in Z;
     A9: (arctan-arccot) is_differentiable_in x by A6,A8,FDIFF_1:16;
         exp_R is_differentiable_in (arctan-arccot).x by SIN_COS:70;
         hence exp_R*(arctan-arccot) is_differentiable_in x by A9,FDIFF_2:13;
     end;
     then
A10: exp_R*(arctan-arccot) is_differentiable_on Z by A1,FDIFF_1:16;
     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;
          assume
     A11: x in Z;then
     A12: arctan-arccot is_differentiable_in x by A6,FDIFF_1:16;
     A13: exp_R is_differentiable_in (arctan-arccot).x by SIN_COS:70;
          (exp_R*(arctan-arccot)`|Z).x = diff(exp_R*(arctan-arccot),x)
          by A10,A11,FDIFF_1:def 8
          .= diff(exp_R,(arctan-arccot).x)*diff((arctan-arccot),x)
          by A12,A13,FDIFF_2:13
          .= exp_R.((arctan-arccot).x)*diff((arctan-arccot),x)
          by SIN_COS:70
          .= exp_R.((arctan-arccot).x)*((arctan-arccot)`|Z).x
          by A6,A11,FDIFF_1:def 8
          .= 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:16;
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 & for x st x in Z holds
    ((arctan+arccot)`|Z).x = 0 by A2,Th37;
A4: for x st x in Z holds sin*(arctan+arccot) is_differentiable_in x
    proof
        let x;
        assume
    A5: x in Z;
    A6: (arctan+arccot) is_differentiable_in x by A3,A5,FDIFF_1:16;
        sin is_differentiable_in (arctan+arccot).x by SIN_COS:69;
        hence sin*(arctan+arccot) is_differentiable_in x by A6,FDIFF_2:13;
    end;
    then
A7: sin*(arctan+arccot) is_differentiable_on Z by A1,FDIFF_1:16;
    for x st x in Z holds (sin*(arctan+arccot)`|Z).x = 0
    proof
         let x;
         assume
    A8:  x in Z;then
    A9:  arctan+arccot is_differentiable_in x by A3,FDIFF_1:16;
    A10: sin is_differentiable_in (arctan+arccot).x by SIN_COS:69;
         (sin*(arctan+arccot)`|Z).x = diff(sin*(arctan+arccot),x)
         by A7,A8,FDIFF_1:def 8
         .= diff(sin,(arctan+arccot).x)*diff((arctan+arccot),x)
         by A9,A10,FDIFF_2:13
         .= cos.((arctan+arccot).x)*diff((arctan+arccot),x)
         by SIN_COS:69
         .= cos.((arctan+arccot).x)*((arctan+arccot)`|Z).x
         by A3,A8,FDIFF_1:def 8
         .= cos.((arctan+arccot).x)*0 by A2,A8,Th37
         .= 0;
         hence thesis;
    end;
    hence thesis by A1,A4,FDIFF_1:16;
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 arctan by SIN_COS9:23,XBOOLE_1:1;then
A4:  Z c= dom arctan by A2,XBOOLE_1:1;
     ].-1,1.[ c= dom arccot by A3,SIN_COS9:24,XBOOLE_1:1;
     then Z c= dom arccot 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 & for x st x in Z holds
     ((arctan-arccot)`|Z).x = 2/(1+x^2) by A2,Th38;
A7:  for x st x in Z holds sin*(arctan-arccot) is_differentiable_in x
     proof
         let x;
         assume
     A8: x in Z;
     A9: (arctan-arccot) is_differentiable_in x by A6,A8,FDIFF_1:16;
         sin is_differentiable_in (arctan-arccot).x by SIN_COS:69;
         hence sin*(arctan-arccot) is_differentiable_in x by A9,FDIFF_2:13;
     end;
     then
A10: sin*(arctan-arccot) is_differentiable_on Z by A1,FDIFF_1:16;
     for x st x in Z holds
     (sin*(arctan-arccot)`|Z).x = 2*cos.(arctan.x-arccot.x)/(1+x^2)
     proof
          let x;
          assume
     A11: x in Z;then
     A12: arctan-arccot is_differentiable_in x by A6,FDIFF_1:16;
     A13: sin is_differentiable_in (arctan-arccot).x by SIN_COS:69;
          (sin*(arctan-arccot)`|Z).x = diff(sin*(arctan-arccot),x)
          by A10,A11,FDIFF_1:def 8
          .= diff(sin,(arctan-arccot).x)*diff((arctan-arccot),x)
          by A12,A13,FDIFF_2:13
          .= cos.((arctan-arccot).x)*diff((arctan-arccot),x)
          by SIN_COS:69
          .= cos.((arctan-arccot).x)*((arctan-arccot)`|Z).x
          by A6,A11,FDIFF_1:def 8
          .= 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:16;
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 & for x st x in Z holds
    ((arctan+arccot)`|Z).x = 0 by A2,Th37;
A4: for x st x in Z holds cos*(arctan+arccot) is_differentiable_in x
    proof
        let x;
        assume
    A5: x in Z;
    A6: (arctan+arccot) is_differentiable_in x by A3,A5,FDIFF_1:16;
        cos is_differentiable_in (arctan+arccot).x by SIN_COS:68;
        hence cos*(arctan+arccot) is_differentiable_in x by A6,FDIFF_2:13;
    end; then
A7: cos*(arctan+arccot) is_differentiable_on Z by A1,FDIFF_1:16;
    for x st x in Z holds (cos*(arctan+arccot)`|Z).x = 0
    proof
         let x;
         assume
    A8:  x in Z;then
    A9:  arctan+arccot is_differentiable_in x by A3,FDIFF_1:16;
    A10: cos is_differentiable_in (arctan+arccot).x by SIN_COS:68;
         (cos*(arctan+arccot)`|Z).x = diff(cos*(arctan+arccot),x)
         by A7,A8,FDIFF_1:def 8
         .= diff(cos,(arctan+arccot).x)*diff((arctan+arccot),x)
         by A9,A10,FDIFF_2:13
         .= (-sin.((arctan+arccot).x))*diff((arctan+arccot),x) by SIN_COS:68
         .= (-sin.((arctan+arccot).x))*((arctan+arccot)`|Z).x
         by A3,A8,FDIFF_1:def 8
         .= (-sin.((arctan+arccot).x))*0 by A2,A8,Th37
         .= 0;
         hence thesis;
    end;
    hence thesis by A1,A4,FDIFF_1:16;
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 arctan by SIN_COS9:23,XBOOLE_1:1;then
A4:  Z c= dom arctan by A2,XBOOLE_1:1;
     ].-1,1.[ c= dom arccot by A3,SIN_COS9:24,XBOOLE_1:1;
     then Z c= dom arccot 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 & for x st x in Z holds
     ((arctan-arccot)`|Z).x = 2/(1+x^2) by A2,Th38;
A7:  for x st x in Z holds cos*(arctan-arccot) is_differentiable_in x
     proof
         let x;
         assume
     A8: x in Z;
     A9: (arctan-arccot) is_differentiable_in x by A6,A8,FDIFF_1:16;
         cos is_differentiable_in (arctan-arccot).x by SIN_COS:68;
         hence cos*(arctan-arccot) is_differentiable_in x by A9,FDIFF_2:13;
     end;
     then
A10: cos*(arctan-arccot) is_differentiable_on Z by A1,FDIFF_1:16;
     for x st x in Z holds
     (cos*(arctan-arccot)`|Z).x = -2*sin.(arctan.x-arccot.x)/(1+x^2)
     proof
          let x;
          assume
     A11: x in Z;then
     A12: arctan-arccot is_differentiable_in x by A6,FDIFF_1:16;
     A13: cos is_differentiable_in (arctan-arccot).x by SIN_COS:68;
          (cos*(arctan-arccot)`|Z).x = diff(cos*(arctan-arccot),x)
          by A10,A11,FDIFF_1:def 8
          .= diff(cos,(arctan-arccot).x)*diff((arctan-arccot),x)
          by A12,A13,FDIFF_2:13
          .= (-sin.((arctan-arccot).x))*diff((arctan-arccot),x)
          by SIN_COS:68
          .= (-sin.((arctan-arccot).x))*((arctan-arccot)`|Z).x
          by A6,A11,FDIFF_1:def 8
          .= (-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:16;
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.[;
A2: ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
    then ].-1,1.[ c= dom arctan by SIN_COS9:23,XBOOLE_1:1;then
A3: Z c= dom arctan by A1,XBOOLE_1:1;
    ].-1,1.[ c= dom arccot by A2,SIN_COS9:24,XBOOLE_1:1;
    then Z c= dom arccot by A1,XBOOLE_1:1;
    then Z c= dom arctan /\ dom arccot by A3,XBOOLE_1:19;then
A4: Z c= dom(arctan(#)arccot) by VALUED_1:def 4;
A5: arctan is_differentiable_on Z by A1,SIN_COS9:81;
A6: arccot is_differentiable_on Z by A1,SIN_COS9:82;
    for x st x in Z holds
    ((arctan(#)arccot)`|Z).x = (arccot.x-arctan.x)/(1+x^2)
    proof
        let x;
        assume
    A8: x in Z;
        ((arctan(#)arccot)`|Z).x
        = (arccot.x)*diff(arctan,x)+(arctan.x)*diff(arccot,x)
        by A4,A5,A6,A8,FDIFF_1:29
        .= arccot.x*((arctan)`|Z).x+arctan.x*diff(arccot,x)
        by A5,A8,FDIFF_1:def 8
        .= arccot.x*(1/(1+x^2))+arctan.x*diff(arccot,x) by A1,A8,SIN_COS9:81
        .= arccot.x*(1/(1+x^2))+arctan.x*((arccot)`|Z).x
        by A6,A8,FDIFF_1:def 8
        .= arccot.x*(1/(1+x^2))+arctan.x*(-1/(1+x^2)) by A1,A8,SIN_COS9:82
        .= (arccot.x-arctan.x)/(1+x^2);
        hence thesis;
    end;
    hence thesis by A4,A5,A6,FDIFF_1:29;
end;

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

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

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

::f.x=x^2*arctan(1/x)
theorem
  Z c= dom (g(#)(arctan*(f^))) & g=#Z 2 &
  (for x st x in Z holds f.x = x & (f^).x > -1 & (f^).x < 1)
  implies g(#)(arctan*(f^)) is_differentiable_on Z &
  for x st x in Z holds
  ((g(#)(arctan*(f^)))`|Z).x = 2*x*arctan.(1/x)-x^2/(1+x^2)
proof
     assume that
A1:  Z c= dom (g(#)(arctan*(f^))) and
A2:  g=#Z 2 and
A3:  for x st x in Z holds f.x = x & (f^).x > -1 & (f^).x < 1;
     Z c= dom g /\ dom (arctan*(f^)) by A1,VALUED_1:def 4;then
A4:  Z c= dom g & Z c= dom (arctan*(f^)) by XBOOLE_1:18;
     then for y st y in Z holds y in dom (f^) by FUNCT_1:21;then
A5:  Z c= dom (f^) by TARSKI:def 3;
A6:  arctan*(f^) is_differentiable_on Z & for x st x in Z holds
     ((arctan*(f^))`|Z).x = -1/(1+x^2) by A3,A4,SIN_COS9:111;
     for x st x in Z holds g is_differentiable_in x by A2,TAYLOR_1:2;then
A7:  g is_differentiable_on Z by A4,FDIFF_1:16;
A8:  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 A7,FDIFF_1:def 8
                 .= 2*(x #Z (2-1)) by A2,TAYLOR_1:2
                 .= 2*x by PREPOWER:45;
         hence thesis;
     end;
     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
     A11: x in Z;
          ((g(#)(arctan*(f^)))`|Z).x
          = ((arctan*(f^)).x)*diff(g,x)+(g.x)*diff(arctan*(f^),x)
          by A1,A6,A7,A11,FDIFF_1:29
          .= ((arctan*(f^)).x)*(g`|Z).x+(g.x)*diff(arctan*(f^),x)
          by A7,A11,FDIFF_1:def 8
          .= ((arctan*(f^)).x)*(2*x)+(g.x)*diff(arctan*(f^),x) by A8,A11
          .= ((arctan*(f^)).x)*(2*x)+(x #Z 2)*diff(arctan*(f^),x)
          by A2,TAYLOR_1:def 1
          .= ((arctan*(f^)).x)*(2*x)+(x #Z 2)*(((arctan*(f^))`|Z).x )
          by A6,A11,FDIFF_1:def 8
          .= ((arctan*(f^)).x)*(2*x)+(x #Z (1+1))*(-1/(1+x^2))
          by A3,A4,A11,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:45
         .= ((arctan*(f^)).x)*(2*x)+x^2*(-1/(1+x^2)) by PREPOWER:45
         .= arctan.((f^).x)*(2*x)-x^2/(1+x^2) by A4,A11,FUNCT_1:22
         .= arctan.((f.x)")*(2*x)-x^2/(1+x^2) by A5,A11,RFUNCT_1:def 8
         .= 2*x*arctan.(1/x)-x^2/(1+x^2) by A3,A11;
         hence thesis;
     end;
     hence thesis by A1,A6,A7,FDIFF_1:29;
end;

::f.x=x^2*arccot(1/x)
theorem
  Z c= dom (g(#)(arccot*(f^))) & g=#Z 2 &
  (for x st x in Z holds f.x = x & (f^).x > -1 & (f^).x < 1)
  implies g(#)(arccot*(f^)) is_differentiable_on Z &
  for x st x in Z holds
  ((g(#)(arccot*(f^)))`|Z).x = 2*x*arccot.(1/x)+x^2/(1+x^2)
proof
     assume that
A1:  Z c= dom (g(#)(arccot*(f^))) and
A2:  g=#Z 2 and
A3:  for x st x in Z holds f.x = x & (f^).x > -1 & (f^).x < 1;
     Z c= dom g /\ dom (arccot*(f^)) by A1,VALUED_1:def 4;then
A4:  Z c= dom g & Z c= dom (arccot*(f^)) by XBOOLE_1:18;
     then for y st y in Z holds y in dom (f^) by FUNCT_1:21;then
A5:  Z c= dom (f^) by TARSKI:def 3;
A6:  arccot*(f^) is_differentiable_on Z & for x st x in Z holds
     ((arccot*(f^))`|Z).x = 1/(1+x^2) by A3,A4,SIN_COS9:112;
     for x st x in Z holds g is_differentiable_in x by A2,TAYLOR_1:2;then
A7:  g is_differentiable_on Z by A4,FDIFF_1:16;
A8:  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 A7,FDIFF_1:def 8
                 .= 2*(x #Z (2-1)) by A2,TAYLOR_1:2
                 .= 2*x by PREPOWER:45;
         hence thesis;
     end;
     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
     A11: x in Z;
          ((g(#)(arccot*(f^)))`|Z).x
          = ((arccot*(f^)).x)*diff(g,x)+(g.x)*diff(arccot*(f^),x)
          by A1,A6,A7,A11,FDIFF_1:29
          .= ((arccot*(f^)).x)*(g`|Z).x+(g.x)*diff(arccot*(f^),x)
          by A7,A11,FDIFF_1:def 8
          .= ((arccot*(f^)).x)*(2*x)+(g.x)*diff(arccot*(f^),x) by A8,A11
          .= ((arccot*(f^)).x)*(2*x)+(x #Z 2)*diff(arccot*(f^),x)
          by A2,TAYLOR_1:def 1
          .= ((arccot*(f^)).x)*(2*x)+(x #Z 2)*(((arccot*(f^))`|Z).x )
          by A6,A11,FDIFF_1:def 8
          .= ((arccot*(f^)).x)*(2*x)+(x #Z (1+1))*(1/(1+x^2))
          by A3,A4,A11,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:45
         .= ((arccot*(f^)).x)*(2*x)+x^2/(1+x^2) by PREPOWER:45
         .= arccot.((f^).x)*(2*x)+x^2/(1+x^2) by A4,A11,FUNCT_1:22
         .= arccot.((f.x)")*(2*x)+x^2/(1+x^2) by A5,A11,RFUNCT_1:def 8
         .= 2*x*arccot.(1/x)+x^2/(1+x^2) by A3,A11;
         hence thesis;
     end;
     hence thesis by A1,A6,A7,FDIFF_1:29;
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 by A2;
    A7: arctan is_differentiable_in x by A3,A5,FDIFF_1:16;
        ((arctan^)`|Z).x = diff(arctan^,x) by A4,A5,FDIFF_1:def 8
        .= -diff(arctan,x)/(arctan.x)^2 by A6,A7,FDIFF_2:15
        .= -((arctan)`|Z).x/(arctan.x)^2 by A3,A5,FDIFF_1:def 8
        .= -(1/(1+x^2))/(arctan.x)^2 by A1,A5,SIN_COS9:81
        .= -1/((arctan.x)^2*(1+x^2)) by XCMPLX_1:79;
        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.[;
A2: for x st x in Z holds arccot.x<>0
    proof
        let x;
        assume
    A3: x in Z;
        assume
    A4: 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 A3;
        then 0 in arccot.:[.-1,1.] by A4,SIN_COS9:24,FUNCT_1:def 12;then
    A6: 0 in [.PI/4,3/4*PI.] by SIN_COS9:56,RELAT_1:148;
        PI in ].0,4.[ by SIN_COS:def 32;
        then PI > 0 by XXREAL_1:4;
        then PI/4 > 0/4 by XREAL_1:76;
        hence contradiction by A6,XXREAL_1:1;
    end;
A7: arccot is_differentiable_on Z by A1,SIN_COS9:82;then
A8: 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
    A9:  x in Z;then
    A10: arccot.x<>0 by A2;
    A11: arccot is_differentiable_in x by A7,A9,FDIFF_1:16;
         ((arccot^)`|Z).x = diff(arccot^,x) by A8,A9,FDIFF_1:def 8
        .= -diff(arccot,x)/(arccot.x)^2 by A10,A11,FDIFF_2:15
        .= -((arccot)`|Z).x/(arccot.x)^2 by A7,A9,FDIFF_1:def 8
        .= -(-1/(1+x^2))/(arccot.x)^2 by A1,A9,SIN_COS9:82
        .= (1/(1+x^2))/(arccot.x)^2
        .= 1/((arccot.x)^2*(1+x^2)) by XCMPLX_1:79;
        hence thesis;
    end;
    hence thesis by A2,A7,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;
    then for y st y in Z holds y in dom (arctan^) by FUNCT_1:21;then
A6: Z c= dom (arctan^) by TARSKI:def 3;
A7: arctan^ is_differentiable_on Z & for x st x in Z holds
    ((arctan^)`|Z).x = -1/((arctan.x)^2*(1+x^2)) 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 A7,FDIFF_1:16;
      hence ( #Z n)*(arctan^) is_differentiable_in x by TAYLOR_1:3;
    end;
    then
A8: ( #Z n)*(arctan^) is_differentiable_on Z by A5,FDIFF_1:16;
    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
    A10: x in Z;then
    A11: arctan^ is_differentiable_in x by A7,FDIFF_1:16;
    A13: (arctan^).x = 1/arctan.x by A6,A10,RFUNCT_1:def 8;
         (((1/n)(#)(( #Z n)*(arctan^)))`|Z).x
         = (1/n)*diff((( #Z n)*(arctan^)),x) by A1,A8,A10,FDIFF_1:28
        .= (1/n)*(n*(((arctan^).x) #Z (n-1))*diff(arctan^,x)) by A11,TAYLOR_1:3
        .= (1/n)*(n*(((arctan^).x) #Z (n-1))*((arctan^)`|Z).x)
         by A7,A10,FDIFF_1:def 8
        .= (1/n)*(n*(((arctan^).x) #Z (n-1))*(-1/((arctan.x)^2*(1+x^2))))
         by A2,A4,A10,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:107
        .= -((1/arctan.x) #Z (n-1))*(1/(((arctan.x) #Z 2)*(1+x^2)))
         by A13,FDIFF_7:1
        .= -(1/((arctan.x) #Z (n-1)))/(((arctan.x) #Z 2)*(1+x^2))
         by PREPOWER:52
        .= -1/(((arctan.x) #Z (n-1))*(((arctan.x) #Z 2)*(1+x^2)))
         by XCMPLX_1:79
        .= -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,A10,PREPOWER:54
        .= -1/(((arctan.x) #Z (n+1))*(1+x^2));
         hence thesis;
    end;
    hence thesis by A1,A8,FDIFF_1:28;
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:  for x st x in Z holds arccot.x<>0
     proof
         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 A2,XBOOLE_1:1;
         then x in [.-1,1.] by A5;
         then 0 in arccot.:[.-1,1.]
         by A6,SIN_COS9:24,FUNCT_1:def 12;then
     A8: 0 in [.PI/4,3/4*PI.] by SIN_COS9:56,RELAT_1:148;
         PI in ].0,4.[ by SIN_COS:def 32;
         then PI > 0 by XXREAL_1:4;
         then PI/4 > 0/4 by XREAL_1:76;
         hence contradiction by A8,XXREAL_1:1;
     end;
A9:  Z c= dom (( #Z n)*(arccot^)) by A1,VALUED_1:def 5;
     then for y st y in Z holds y in dom (arccot^) by FUNCT_1:21;then
A10: Z c= dom (arccot^) by TARSKI:def 3;
A11: arccot^ is_differentiable_on Z & for x st x in Z holds
     ((arccot^)`|Z).x = 1/((arccot.x)^2*(1+x^2)) 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 A11,FDIFF_1:16;
       hence ( #Z n)*(arccot^) is_differentiable_in x by TAYLOR_1:3;
     end;
     then
A12: ( #Z n)*(arccot^) is_differentiable_on Z by A9,FDIFF_1:16;
     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
  A14: x in Z;then
  A15: arccot^ is_differentiable_in x by A11,FDIFF_1:16;
  A17: (arccot^).x = 1/arccot.x by A10,A14,RFUNCT_1:def 8;
       (((1/n)(#)(( #Z n)*(arccot^)))`|Z).x
       = (1/n)*diff((( #Z n)*(arccot^)),x) by A1,A12,A14,FDIFF_1:28
      .= (1/n)*(n*(((arccot^).x) #Z (n-1))*diff(arccot^,x))
       by A15,TAYLOR_1:3
      .= (1/n)*(n*(((arccot^).x) #Z (n-1))*((arccot^)`|Z).x)
       by A11,A14,FDIFF_1:def 8
      .= (1/n)*(n*(((arccot^).x) #Z (n-1))*(1/((arccot.x)^2*(1+x^2))))
       by A2,A14,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:107
      .= ((1/arccot.x) #Z (n-1))*(1/(((arccot.x) #Z 2)*(1+x^2)))
       by A17,FDIFF_7:1
      .= (1/((arccot.x) #Z (n-1)))/(((arccot.x) #Z 2)*(1+x^2))
       by PREPOWER:52
      .= 1/(((arccot.x) #Z (n-1))*(((arccot.x) #Z 2)*(1+x^2)))
       by XCMPLX_1:79
      .= 1/(((arccot.x) #Z (n-1))*((arccot.x) #Z 2)*(1+x^2))
      .= 1/(((arccot.x) #Z ((n-1)+2))*(1+x^2)) by A4,A14,PREPOWER:54
      .= 1/(((arccot.x) #Z (n+1))*(1+x^2));
       hence thesis;
     end;
     hence thesis by A1,A12,FDIFF_1:28;
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: Z c= dom (( #R (1/2))*arctan) by A1,VALUED_1:def 5;
    for x st x in Z holds ( #R (1/2))*arctan is_differentiable_in x
    proof
        let x;
        assume
    A5: x in Z;
        arctan is_differentiable_on Z by A2,SIN_COS9:81;then
    A6: arctan is_differentiable_in x by A5,FDIFF_1:16;
        arctan.x > 0 by A3,A5;
        hence ( #R (1/2))*arctan is_differentiable_in x by A6,TAYLOR_1:22;
    end;
    then
A7: ( #R (1/2))*arctan is_differentiable_on Z by A4,FDIFF_1:16;
    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
 A9:  x in Z;
 A10: arctan is_differentiable_on Z by A2,SIN_COS9:81;then
 A11: arctan is_differentiable_in x by A9,FDIFF_1:16;
 A12: arctan.x > 0 by A3,A9;
      ((2(#)(( #R (1/2))*arctan))`|Z).x = 2*diff((( #R (1/2))*arctan),x)
      by A1,A7,A9,FDIFF_1:28
      .= 2*((1/2)*((arctan.x) #R (1/2-1))*diff(arctan,x))
      by A11,A12,TAYLOR_1:22
      .= 2*((1/2)*((arctan.x) #R (1/2-1))*((arctan)`|Z).x)
      by A9,A10,FDIFF_1:def 8
      .= 2*((1/2)*((arctan.x) #R (1/2-1))*(1/(1+x^2))) by A2,A9,SIN_COS9:81
      .= ((arctan.x) #R (-1/2))/(1+x^2);
      hence thesis;
    end;
    hence thesis by A1,A7,FDIFF_1:28;
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;
       assume
   A4: x in Z;
       assume
   A5: 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 A4;
       then arccot.x in arccot.:[.-1,1.]
       by SIN_COS9:24,FUNCT_1:def 12;then
       arccot.x in [.PI/4,3/4*PI.] by SIN_COS9:56,RELAT_1:148;then
   A7: arccot.x >= PI/4 by XXREAL_1:1;
       arccot.x + 0 > PI/4 + (-PI/4) by A7,XREAL_1:10;
       hence contradiction by A5;
     end;
A8:  Z c= dom (( #R (1/2))*arccot) by A1,VALUED_1:def 5;
     for x st x in Z holds ( #R (1/2))*arccot is_differentiable_in x
     proof
       let x;
       assume
  A9:  x in Z;
       arccot is_differentiable_on Z by A2,SIN_COS9:82;then
  A10: arccot is_differentiable_in x by A9,FDIFF_1:16;
       arccot.x > 0 by A3,A9;
       hence ( #R (1/2))*arccot is_differentiable_in x by A10,TAYLOR_1:22;
     end;
     then
A11: ( #R (1/2))*arccot is_differentiable_on Z by A8,FDIFF_1:16;
     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
     A13:  x in Z;
     A14: arccot is_differentiable_on Z by A2,SIN_COS9:82;then
     A15: arccot is_differentiable_in x by A13,FDIFF_1:16;
     A16: arccot.x > 0 by A3,A13;
          ((2(#)(( #R (1/2))*arccot))`|Z).x = 2*diff((( #R (1/2))*arccot),x)
          by A1,A11,A13,FDIFF_1:28
          .= 2*((1/2)*((arccot.x) #R (1/2-1))*diff(arccot,x))
          by A15,A16,TAYLOR_1:22
          .= 2*((1/2)*((arccot.x) #R (1/2-1))*((arccot)`|Z).x)
          by A13,A14,FDIFF_1:def 8
          .= 2*((1/2)*((arccot.x) #R (1/2-1))*(-1/(1+x^2)))
          by A2,A13,SIN_COS9:82
          .= -((arccot.x) #R (-1/2))/(1+x^2);
          hence thesis;
     end;
     hence thesis by A1,A11,FDIFF_1:28;
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: Z c= dom (( #R (3/2))*arctan) by A1,VALUED_1:def 5;
    for x st x in Z holds ( #R (3/2))*arctan is_differentiable_in x
    proof
        let x;
        assume
    A5: x in Z;
        arctan is_differentiable_on Z by A2,SIN_COS9:81;then
    A6: arctan is_differentiable_in x by A5,FDIFF_1:16;
        arctan.x > 0 by A3,A5;
        hence ( #R (3/2))*arctan is_differentiable_in x by A6,TAYLOR_1:22;
    end;
    then
A7: ( #R (3/2))*arctan is_differentiable_on Z by A4,FDIFF_1:16;
    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
 A9:  x in Z;
 A10: arctan is_differentiable_on Z by A2,SIN_COS9:81;then
 A11: arctan is_differentiable_in x by A9,FDIFF_1:16;
 A12: arctan.x > 0 by A3,A9;
      (((2/3)(#)(( #R (3/2))*arctan))`|Z).x
      = (2/3)*diff((( #R (3/2))*arctan),x) by A1,A7,A9,FDIFF_1:28
     .= (2/3)*((3/2)*((arctan.x) #R (3/2-1))*diff(arctan,x))
      by A11,A12,TAYLOR_1:22
     .= (2/3)*((3/2)*((arctan.x) #R (3/2-1))*((arctan)`|Z).x)
      by A9,A10,FDIFF_1:def 8
     .= (2/3)*((3/2)*((arctan.x) #R (3/2-1))*(1/(1+x^2)))
      by A2,A9,SIN_COS9:81
     .= ((arctan.x) #R (1/2))/(1+x^2);
      hence thesis;
    end;
    hence thesis by A1,A7,FDIFF_1:28;
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;
         assume
     A4: x in Z;
         assume
     A5: 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 A4;
         then arccot.x in arccot.:[.-1,1.]
         by SIN_COS9:24,FUNCT_1:def 12;then
         arccot.x in [.PI/4,3/4*PI.] by SIN_COS9:56,RELAT_1:148;then
     A7: arccot.x >= PI/4 by XXREAL_1:1;
         arccot.x + 0 > PI/4 + (-PI/4) by A7,XREAL_1:10;
         hence contradiction by A5;
     end;
A8:  Z c= dom (( #R (3/2))*arccot) by A1,VALUED_1:def 5;
     for x st x in Z holds ( #R (3/2))*arccot is_differentiable_in x
     proof
          let x;
          assume
     A9:  x in Z;
          arccot is_differentiable_on Z by A2,SIN_COS9:82;then
     A10: arccot is_differentiable_in x by A9,FDIFF_1:16;
          arccot.x > 0 by A3,A9;
          hence ( #R (3/2))*arccot is_differentiable_in x by A10,TAYLOR_1:22;
     end;
     then
A11: ( #R (3/2))*arccot is_differentiable_on Z by A8,FDIFF_1:16;
     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
     A13:  x in Z;
     A14: arccot is_differentiable_on Z by A2,SIN_COS9:82;then
     A15: arccot is_differentiable_in x by A13,FDIFF_1:16;
     A16: arccot.x > 0 by A3,A13;
          (((2/3)(#)(( #R (3/2))*arccot))`|Z).x
          = (2/3)*diff((( #R (3/2))*arccot),x) by A1,A11,A13,FDIFF_1:28
         .= (2/3)*((3/2)*((arccot.x) #R (3/2-1))*diff(arccot,x))
          by A15,A16,TAYLOR_1:22
         .= (2/3)*((3/2)*((arccot.x) #R (3/2-1))*((arccot)`|Z).x)
          by A13,A14,FDIFF_1:def 8
         .= (2/3)*((3/2)*((arccot.x) #R (3/2-1))*(-1/(1+x^2)))
          by A2,A13,SIN_COS9:82
         .= -((arccot.x) #R (1/2))/(1+x^2);
          hence thesis;
     end;
     hence thesis by A1,A11,FDIFF_1:28;
end;