:: Several Differentiation Formulas of Special Functions -- Part {V}
::  by Bo Li and Pan Wang
::
:: Received September 19, 2007
:: Copyright (c) 2007 Association of Mizar Users

environ

 vocabularies FUNCT_1, RELAT_1, PRE_TOPC, BOOLE, ARYTM_1, ARYTM_3, SEQ_1,
      PARTFUN1, SIN_COS, FDIFF_1, LIMFUNC1, SQUARE_1, TAYLOR_1, SIN_COS4,
      ORDINAL2, ARYTM, RCOMP_1, SUPINF_1;
 notations TARSKI, SUBSET_1, ORDINAL1, XXREAL_0, RELSET_1, PARTFUN1, RCOMP_1,
      TAYLOR_1, SIN_COS, RFUNCT_1, SQUARE_1, NUMBERS, REAL_1, VALUED_1, SEQ_1,
      FDIFF_1, LIMFUNC1, FDIFF_9;
 constructors REAL_1, PARTFUN1, PARTFUN2, LIMFUNC1, RCOMP_1, TAYLOR_1, SIN_COS,
      FDIFF_1, RFUNCT_1, SQUARE_1, ARYTM_0, COMSEQ_3, FDIFF_9, SEQ_1;
 registrations RELSET_1, MEMBERED, RCOMP_1, XXREAL_0, NAT_1, VALUED_0, NUMBERS;
 requirements SUBSET, NUMERALS, ARITHM;
 definitions SQUARE_1, LIMFUNC1, XCMPLX_0, SIN_COS, FDIFF_9;
 theorems FDIFF_2, TAYLOR_1, XBOOLE_1, XCMPLX_1, FDIFF_1, FDIFF_7, RFUNCT_1,
      FUNCT_1, SIN_COS, RELAT_1, FDIFF_8, LIMFUNC1, FDIFF_9, VALUED_1,
      XXREAL_1;

begin

reserve x for Real,
  n for natural number,
  Z for open Subset of REAL,
  f for PartFunc of REAL,REAL;

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

theorem
  Z c= dom (tan*cot) implies tan*cot is_differentiable_on Z &
  for x st x in Z holds((tan*cot)`|Z).x = 1/(cos.(cot.x))^2 *(-1/(sin.x)^2)
proof
  assume
A1: Z c= dom (tan*cot);
A2: for x st x in Z holds sin.x <> 0
  proof
    let x;
    assume x in Z;
    then x in dom (cos/sin) by A1,FUNCT_1:21;
    hence thesis by FDIFF_8:2;
  end;
A3: for x st x in Z holds cos.(cot.x) <> 0
  proof
    let x;
    assume x in Z;
    then cot.x in dom (tan) by A1,FUNCT_1:21;
    hence thesis by FDIFF_8:1;
  end;
A4: for x st x in Z holds tan*cot is_differentiable_in x
  proof
    let x;
    assume
A5: x in Z;
    then sin.x <> 0 by A2;
    then
A6: cot is_differentiable_in x by FDIFF_7:47;
    cos.(cot.x)<>0 by A3,A5;
    then tan is_differentiable_in cot.x by FDIFF_7:46;
    hence tan*cot is_differentiable_in x by A6,FDIFF_2:13;
  end;
  then
A7: tan*cot is_differentiable_on Z by A1,FDIFF_1:16;
  for x st x in Z holds ((tan*cot)`|Z).x = 1/(cos.(cot.x))^2 *(-1/(sin.x)^2)
  proof
    let x;
    assume
A8: x in Z;
    then
A9: sin.x<>0 by A2;
    then
A10: cot is_differentiable_in x by FDIFF_7:47;
A11: cos.(cot.x)<>0 by A3,A8;
    then tan is_differentiable_in cot.x by FDIFF_7:46;
    then diff(tan*cot,x) = diff(tan, cot.x)*diff(cot,x) by A10,FDIFF_2:13
      .=1/(cos.(cot.x))^2 * diff(cot,x) by A11,FDIFF_7:46
      .=1/(cos.(cot.x))^2 *(-1/(sin.x)^2) by A9,FDIFF_7:47;
    hence thesis by A7,A8,FDIFF_1:def 8;
  end;
  hence thesis by A1,A4,FDIFF_1:16;
end;

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

theorem
  Z c= dom (tan*tan) implies tan*tan is_differentiable_on Z &
  for x st x in Z holds((tan*tan)`|Z).x = 1/(cos.(tan.x))^2 *(1/(cos.x)^2)
proof
  assume
A1: Z c= dom (tan*tan);
A2: for x st x in Z holds cos.x <> 0
  proof
    let x;
    assume x in Z;
    then x in dom (sin/cos) by A1,FUNCT_1:21;
    hence thesis by FDIFF_8:1;
  end;
A3: for x st x in Z holds cos.(tan.x) <> 0
  proof
    let x;
    assume x in Z;
    then tan.x in dom (tan) by A1,FUNCT_1:21;
    hence thesis by FDIFF_8:1;
  end;
A4: for x st x in Z holds tan*tan is_differentiable_in x
  proof
    let x;
    assume
A5: x in Z;
    then cos.x <> 0 by A2;
    then
A6: tan is_differentiable_in x by FDIFF_7:46;
    cos.(tan.x)<>0 by A3,A5;
    then tan is_differentiable_in tan.x by FDIFF_7:46;
    hence tan*tan is_differentiable_in x by A6,FDIFF_2:13;
  end;
  then
A7: tan*tan is_differentiable_on Z by A1,FDIFF_1:16;
  for x st x in Z holds ((tan*tan)`|Z).x = 1/(cos.(tan.x))^2 *(1/(cos.x)^2)
  proof
    let x;
    assume
A8: x in Z;
    then
A9: cos.x<>0 by A2;
    then
A10: tan is_differentiable_in x by FDIFF_7:46;
A11: cos.(tan.x)<>0 by A3,A8;
    then tan is_differentiable_in tan.x by FDIFF_7:46;
    then diff(tan*tan,x) = diff(tan, tan.x)*diff(tan,x) by A10,FDIFF_2:13
      .=1/(cos.(tan.x))^2 * diff(tan,x) by A11,FDIFF_7:46
      .=1/(cos.(tan.x))^2 *(1/(cos.x)^2) by A9,FDIFF_7:46;
    hence thesis by A7,A8,FDIFF_1:def 8;
  end;
  hence thesis by A1,A4,FDIFF_1:16;
end;

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

theorem
  Z c= dom (cot*cot) implies cot*cot is_differentiable_on Z &
  for x st x in Z holds((cot*cot)`|Z).x = (1/(sin.(cot.x))^2) *(1/(sin.x)^2)
proof
  assume
A1: Z c= dom (cot*cot);
A2: for x st x in Z holds sin.x <> 0
  proof
    let x;
    assume x in Z;
    then x in dom (cos/sin) by A1,FUNCT_1:21;
    hence thesis by FDIFF_8:2;
  end;
A3: for x st x in Z holds sin.(cot.x) <> 0
  proof
    let x;
    assume x in Z;
    then cot.x in dom cot by A1,FUNCT_1:21;
    hence thesis by FDIFF_8:2;
  end;
A4: for x st x in Z holds cot*cot is_differentiable_in x
  proof
    let x;
    assume
A5: x in Z;
    then sin.x <> 0 by A2;
    then
A6: cot is_differentiable_in x by FDIFF_7:47;
    sin.(cot.x)<>0 by A3,A5;
    then cot is_differentiable_in cot.x by FDIFF_7:47;
    hence cot*cot is_differentiable_in x by A6,FDIFF_2:13;
  end;
  then
A7: cot*cot is_differentiable_on Z by A1,FDIFF_1:16;
  for x st x in Z holds ((cot*cot)`|Z).x=(1/(sin.(cot.x))^2)*(1/(sin.x)^2)
  proof
    let x;
    assume
A8: x in Z;
    then
A9: sin.x<>0 by A2;
    then
A10: cot is_differentiable_in x by FDIFF_7:47;
A11: sin.(cot.x)<>0 by A3,A8;
    then cot is_differentiable_in cot.x by FDIFF_7:47;
    then diff(cot*cot,x) = diff(cot, cot.x)*diff(cot,x) by A10,FDIFF_2:13
      .=(-1/(sin.(cot.x))^2)* diff(cot,x) by A11,FDIFF_7:47
      .=(-1/(sin.(cot.x))^2) *(-1/(sin.x)^2) by A9,FDIFF_7:47;
    hence thesis by A7,A8,FDIFF_1:def 8;
  end;
  hence thesis by A1,A4,FDIFF_1:16;
end;

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

theorem
  Z c= dom (cot*tan) implies cot*tan is_differentiable_on Z &
  for x st x in Z holds((cot*tan)`|Z).x = (-1/(sin.(tan.x))^2)*(1/(cos.x)^2)
proof
  assume
A1: Z c= dom (cot*tan);
A2: for x st x in Z holds cos.x <> 0
  proof
    let x;
    assume x in Z;
    then x in dom (sin/cos) by A1,FUNCT_1:21;
    hence thesis by FDIFF_8:1;
  end;
A3: for x st x in Z holds sin.(tan.x) <> 0
  proof
    let x;
    assume x in Z;
    then tan.x in dom (cot) by A1,FUNCT_1:21;
    hence thesis by FDIFF_8:2;
  end;
A4: for x st x in Z holds cot*tan is_differentiable_in x
  proof
    let x;
    assume
A5: x in Z;
    then cos.x <> 0 by A2;
    then
A6: tan is_differentiable_in x by FDIFF_7:46;
    sin.(tan.x)<>0 by A3,A5;
    then cot is_differentiable_in tan.x by FDIFF_7:47;
    hence cot*tan is_differentiable_in x by A6,FDIFF_2:13;
  end;
  then
A7: cot*tan is_differentiable_on Z by A1,FDIFF_1:16;
  for x st x in Z holds ((cot*tan)`|Z).x=(-1/(sin.(tan.x))^2)*(1/(cos.x)^2)
  proof
    let x;
    assume
A8: x in Z;
    then
A9: cos.x<>0 by A2;
    then
A10: tan is_differentiable_in x by FDIFF_7:46;
A11: sin.(tan.x)<>0 by A3,A8;
    then cot is_differentiable_in tan.x by FDIFF_7:47;
    then diff(cot*tan,x) = diff(cot, tan.x)*diff(tan,x) by A10,FDIFF_2:13
      .=(-1/(sin.(tan.x))^2)* diff(tan,x) by A11,FDIFF_7:47
      .=(-1/(sin.(tan.x))^2)*(1/(cos.x)^2) by A9,FDIFF_7:46;
    hence thesis by A7,A8,FDIFF_1:def 8;
  end;
  hence thesis by A1,A4,FDIFF_1:16;
end;

::f.x= tan.x - cot.x

theorem Th5:
  Z c= dom(tan-cot) implies (tan - cot) is_differentiable_on Z &
  for x st x in Z holds((tan - cot)`|Z).x = 1/(cos.x)^2+1/(sin.x)^2
proof
  assume
A1: Z c= dom (tan-cot);
  then Z c= dom tan /\ dom cot by VALUED_1:12;
  then
A2: Z c= dom tan & 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 A2,FDIFF_8:2;
    hence thesis by FDIFF_7:47;
  end;
  then
A3: cot is_differentiable_on Z by A2,FDIFF_1:16;
  for x st x in Z holds tan is_differentiable_in x
  proof
    let x;
    assume x in Z;
    then cos.x <> 0 by A2,FDIFF_8:1;
    hence thesis by FDIFF_7:46;
  end;
  then
A4: tan is_differentiable_on Z by A2,FDIFF_1:16;
  for x st x in Z holds ((tan-cot)`|Z).x =1/(cos.x)^2+1/(sin.x)^2
  proof
    let x;
    assume
A5: x in Z;
    then
A6: sin.x<> 0 & cos.x<> 0 by A2,FDIFF_8:1,2;
    ((tan-cot)`|Z).x = diff(tan,x)-diff(cot,x)by A1,A3,A4,A5,FDIFF_1:27
      .=1/(cos.x)^2-diff(cot,x) by A6,FDIFF_7:46
      .=1/(cos.x)^2-(-1/(sin.x)^2) by A6,FDIFF_7:47
      .=1/(cos.x)^2+1/(sin.x)^2;
    hence thesis;
  end;
  hence thesis by A1,A3,A4,FDIFF_1:27;
end;

::f.x= tan.x + cot.x

theorem Th6:
  Z c= dom(tan+cot) implies (tan + cot) is_differentiable_on Z &
  for x st x in Z holds((tan + cot)`|Z).x = 1/(cos.x)^2-1/(sin.x)^2
proof
  assume
A1: Z c= dom (tan+cot);
  then Z c= dom tan /\ dom cot by VALUED_1:def 1;
  then
A2: Z c= dom tan & 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 A2,FDIFF_8:2;
    hence thesis by FDIFF_7:47;
  end;
  then
A3: cot is_differentiable_on Z by A2,FDIFF_1:16;
  for x st x in Z holds tan is_differentiable_in x
  proof
    let x;
    assume x in Z;
    then cos.x <> 0 by A2,FDIFF_8:1;
    hence thesis by FDIFF_7:46;
  end;
  then
A4: tan is_differentiable_on Z by A2,FDIFF_1:16;
  for x st x in Z holds ((tan+cot)`|Z).x =1/(cos.x)^2-1/(sin.x)^2
  proof
    let x;
    assume
A5: x in Z;
    then
A6: sin.x<> 0 & cos.x<> 0 by A2,FDIFF_8:1,2;
    ((tan+cot)`|Z).x = diff(tan,x)+diff(cot,x)by A1,A3,A4,A5,FDIFF_1:26
      .=1/(cos.x)^2+diff(cot,x) by A6,FDIFF_7:46
      .=1/(cos.x)^2-1/(sin.x)^2 by A6,FDIFF_7:47;
    hence thesis;
  end;
  hence thesis by A1,A3,A4,FDIFF_1:26;
end;

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

theorem
  sin*sin is_differentiable_on Z &
  for x st x in Z holds((sin*sin)`|Z).x = cos.(sin.x)*cos.x
proof
  dom sin = REAL & rng sin c= REAL by SIN_COS:27;
  then
A1: dom (sin*sin) = REAL by RELAT_1:46;
A2: for x st x in Z holds sin*sin is_differentiable_in x
  proof
    let x;
    assume x in Z;
A3: sin is_differentiable_in x by SIN_COS:69;
    sin is_differentiable_in sin.x by SIN_COS:69;
    hence sin*sin is_differentiable_in x by A3,FDIFF_2:13;
  end;
  then
A4: sin*sin is_differentiable_on Z by A1,FDIFF_1:16;
  for x st x in Z holds((sin*sin)`|Z).x = cos.(sin.x)*cos.x
  proof
    let x;
    assume
A5: x in Z;
A6: sin is_differentiable_in x by SIN_COS:69;
    sin is_differentiable_in sin.x by SIN_COS:69;
    then diff(sin*sin,x) = diff(sin,sin.x)*diff(sin,x) by A6,FDIFF_2:13
      .=cos.(sin.x)*diff(sin,x) by SIN_COS:69
      .=cos.(sin.x)*cos.x by SIN_COS:69;
    hence thesis by A4,A5,FDIFF_1:def 8;
  end;
  hence thesis by A1,A2,FDIFF_1:16;
end;

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

theorem
  sin*cos is_differentiable_on Z &
  for x st x in Z holds((sin*cos)`|Z).x = -cos.(cos.x)*sin.x
proof
A1: dom cos = REAL by SIN_COS:27;
  rng cos c= dom cos & dom sin = dom cos by SIN_COS:27;
  then
A2: dom (sin*cos) = REAL by A1,RELAT_1:46;
A3: for x st x in Z holds sin*cos is_differentiable_in x
  proof
    let x;
    assume x in Z;
A4: cos is_differentiable_in x by SIN_COS:68;
    sin is_differentiable_in cos.x by SIN_COS:69;
    hence sin*cos is_differentiable_in x by A4,FDIFF_2:13;
  end;
  then
A5: sin*cos is_differentiable_on Z by A2,FDIFF_1:16;
  for x st x in Z holds((sin*cos)`|Z).x = -cos.(cos.x)*sin.x
  proof
    let x;
    assume
A6: x in Z;
A7: cos is_differentiable_in x by SIN_COS:68;
    sin is_differentiable_in cos.x by SIN_COS:69;
    then diff(sin*cos,x) =diff(sin,cos.x)*diff(cos,x) by A7,FDIFF_2:13
      .=cos.(cos.x)*diff(cos,x) by SIN_COS:69
      .=cos.(cos.x)*(-sin.x) by SIN_COS:68;
    hence thesis by A5,A6,FDIFF_1:def 8;
  end;
  hence thesis by A2,A3,FDIFF_1:16;
end;

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

theorem
  cos*sin is_differentiable_on Z &
  for x st x in Z holds((cos*sin)`|Z).x = -sin.(sin.x)*cos.x
proof
A1: dom sin = REAL by SIN_COS:27;
  rng sin c= dom sin & dom sin = dom cos by SIN_COS:27;
  then
A2: dom (cos*sin) = REAL by A1,RELAT_1:46;
A3: for x st x in Z holds cos*sin is_differentiable_in x
  proof
    let x;
    assume x in Z;
A4: sin is_differentiable_in x by SIN_COS:69;
    cos is_differentiable_in sin.x by SIN_COS:68;
    hence cos*sin is_differentiable_in x by A4,FDIFF_2:13;
  end;
  then
A5: cos*sin is_differentiable_on Z by A2,FDIFF_1:16;
  for x st x in Z holds((cos*sin)`|Z).x = -sin.(sin.x)*cos.x
  proof
    let x;
    assume
A6: x in Z;
A7: sin is_differentiable_in x by SIN_COS:69;
    cos is_differentiable_in sin.x by SIN_COS:68;
    then diff(cos*sin,x) =diff(cos,sin.x)*diff(sin,x) by A7,FDIFF_2:13
      .=(-sin.(sin.x))*diff(sin,x) by SIN_COS:68
      .=(-sin.(sin.x))*cos.x by SIN_COS:69;
    hence thesis by A5,A6,FDIFF_1:def 8;
  end;
  hence thesis by A2,A3,FDIFF_1:16;
end;

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

theorem
  cos*cos is_differentiable_on Z &
  for x st x in Z holds((cos*cos)`|Z).x = sin.(cos.x)*sin.x
proof
  dom cos = REAL & rng cos c= REAL by SIN_COS:27;
  then
A1: dom (cos*cos) = REAL by RELAT_1:46;
A2: for x st x in Z holds cos*cos is_differentiable_in x
  proof
    let x;
    assume x in Z;
A3: cos is_differentiable_in x by SIN_COS:68;
    cos is_differentiable_in cos.x by SIN_COS:68;
    hence cos*cos is_differentiable_in x by A3,FDIFF_2:13;
  end;
  then
A4: cos*cos is_differentiable_on Z by A1,FDIFF_1:16;
  for x st x in Z holds((cos*cos)`|Z).x = sin.(cos.x)*sin.x
  proof
    let x;
    assume
A5: x in Z;
A6: cos is_differentiable_in x by SIN_COS:68;
    cos is_differentiable_in cos.x by SIN_COS:68;
    then diff(cos*cos,x) =diff(cos,cos.x)*diff(cos,x) by A6,FDIFF_2:13
      .=(-sin.(cos.x))*diff(cos,x) by SIN_COS:68
      .=(-sin.(cos.x))*(-sin.x) by SIN_COS:68;
    hence thesis by A4,A5,FDIFF_1:def 8;
  end;
  hence thesis by A1,A2,FDIFF_1:16;
end;

:: f.x=cos.x * cot.x

theorem
  Z c= dom (cos (#) cot) implies (cos (#) cot) is_differentiable_on Z &
  for x st x in Z holds((cos (#) cot)`|Z).x = -cos.x-cos.x/(sin.x)^2
proof
  assume
A1: Z c= dom (cos (#) cot);
  then Z c= dom cos /\ dom cot by VALUED_1:def 4;
  then
A2: Z c= dom cos & 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 A2,FDIFF_8:2;
    hence thesis by FDIFF_7:47;
  end;
  then
A3: cot is_differentiable_on Z by A2,FDIFF_1:16;
  for x st x in Z holds cos is_differentiable_in x by SIN_COS:68;
  then
A4: cos is_differentiable_on Z by A2,FDIFF_1:16;
A5: for x st x in Z holds diff(cot, x)=-1/(sin.x)^2
  proof
    let x;
    assume x in Z;
    then sin.x<>0 by A2,FDIFF_8:2;
    hence thesis by FDIFF_7:47;
  end;
  for x st x in Z holds((cos (#) cot)`|Z).x =-cos.x-cos.x/(sin.x)^2
  proof
    let x;
    assume
A6: x in Z;
    then ((cos (#) cot)`|Z).x=
    diff(cos,x)*cot.x+cos.x*diff(cot,x) by A1,A3,A4,FDIFF_1:29
      .=cot.x*(-sin.x)+cos.x*diff(cot,x) by SIN_COS:68
      .=cot.x*(-sin.x)+cos.x*(-1/(sin.x)^2) by A5,A6
      .=(cos.x/sin.x)*(-sin.x/1)-cos.x/(sin.x)^2 by A2,A6,RFUNCT_1:def 4
      .=-cos.x*(sin.x/sin.x)-cos.x/(sin.x)^2
      .=-cos.x*1-cos.x/(sin.x)^2 by A2,A6,FDIFF_8:2,XCMPLX_1:60
      .=-cos.x-cos.x/(sin.x)^2;
    hence thesis;
  end;
  hence thesis by A1,A3,A4,FDIFF_1:29;
end;

:: f.x=sin.x * tan.x

theorem
  Z c= dom (sin (#) tan) implies (sin (#)tan) is_differentiable_on Z &
  for x st x in Z holds((sin (#) tan)`|Z).x = sin.x + sin.x/(cos.x)^2
proof
  assume
A1: Z c= dom (sin (#) tan);
  then Z c= dom sin /\ dom tan by VALUED_1:def 4;
  then
A2: Z c= dom sin & 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 A2,FDIFF_8:1;
    hence thesis by FDIFF_7:46;
  end;
  then
A3: tan is_differentiable_on Z by A2,FDIFF_1:16;
  for x st x in Z holds sin is_differentiable_in x by SIN_COS:69;
  then
A4: sin is_differentiable_on Z by A2,FDIFF_1:16;
A5: for x st x in Z holds diff(tan, x)=1/(cos.x)^2
  proof
    let x;
    assume x in Z;
    then cos.x<>0 by A2,FDIFF_8:1;
    hence thesis by FDIFF_7:46;
  end;
  for x st x in Z holds((sin (#) tan)`|Z).x = sin.x + sin.x/(cos.x)^2
  proof
    let x;
    assume
A6: x in Z;
    then ((sin (#) tan)`|Z).x =
    diff(sin,x)*tan.x+sin.x*diff(tan,x) by A1,A3,A4,FDIFF_1:29
      .=cos.x*tan.x+sin.x*diff(tan,x) by SIN_COS:69
      .=cos.x*tan.x+sin.x*(1/(cos.x)^2) by A5,A6
      .=(sin.x/cos.x)*(cos.x/1)+sin.x/(cos.x)^2 by A2,A6,RFUNCT_1:def 4
      .=sin.x*(cos.x/cos.x) + sin.x/(cos.x)^2
      .=sin.x* 1 + sin.x/(cos.x)^2 by A2,A6,FDIFF_8:1,XCMPLX_1:60
      .= sin.x +sin.x/(cos.x)^2;
    hence thesis;
  end;
  hence thesis by A1,A3,A4,FDIFF_1:29;
end;

:: f.x=sin.x * cot.x

theorem
  Z c= dom (sin (#) cot) implies (sin (#) cot) is_differentiable_on Z &
  for x st x in Z holds((sin (#) cot)`|Z).x = cos.x*cot.x - 1/sin.x
proof
  assume
A1: Z c= dom (sin (#) cot);
  then Z c= dom sin /\ dom cot by VALUED_1:def 4;
  then
A2: Z c= dom sin & 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 A2,FDIFF_8:2;
    hence thesis by FDIFF_7:47;
  end;
  then
A3: cot is_differentiable_on Z by A2,FDIFF_1:16;
  for x st x in Z holds sin is_differentiable_in x by SIN_COS:69;
  then
A4: sin is_differentiable_on Z by A2,FDIFF_1:16;
A5: for x st x in Z holds diff(cot, x)=-1/(sin.x)^2
  proof
    let x;
    assume x in Z;
    then sin.x<>0 by A2,FDIFF_8:2;
    hence thesis by FDIFF_7:47;
  end;
  for x st x in Z holds((sin (#) cot)`|Z).x = cos.x*cot.x- 1/sin.x
  proof
    let x;
    assume
A6: x in Z;
    then ((sin (#) cot)`|Z).x =
    diff(sin,x)*cot.x+sin.x*diff(cot,x) by A1,A3,A4,FDIFF_1:29
      .=cos.x*cot.x+sin.x*diff(cot,x) by SIN_COS:69
      .=cos.x*cot.x+sin.x*(-1/(sin.x)^2) by A5,A6
      .=cos.x*cot.x-sin.x/(sin.x)^2
      .=cos.x*cot.x-sin.x/sin.x/sin.x by XCMPLX_1:79
      .=cos.x*cot.x-1/sin.x by A2,A6,FDIFF_8:2,XCMPLX_1:60;
    hence thesis;
  end;
  hence thesis by A1,A3,A4,FDIFF_1:29;
end;

:: f.x=cos.x * tan.x

theorem
  Z c= dom (cos (#) tan) implies (cos (#) tan) is_differentiable_on Z &
  for x st x in Z holds((cos (#) tan)`|Z).x = -(sin.x)^2/cos.x+1/cos.x
proof
  assume
A1: Z c= dom (cos (#) tan);
  then Z c= dom cos /\ dom tan by VALUED_1:def 4;
  then
A2: Z c= dom cos & 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 A2,FDIFF_8:1;
    hence thesis by FDIFF_7:46;
  end;
  then
A3: tan is_differentiable_on Z by A2,FDIFF_1:16;
  for x st x in Z holds cos is_differentiable_in x by SIN_COS:68;
  then
A4: cos is_differentiable_on Z by A2,FDIFF_1:16;
A5: for x st x in Z holds diff(tan, x)=1/(cos.x)^2
  proof
    let x;
    assume x in Z;
    then cos.x<>0 by A2,FDIFF_8:1;
    hence thesis by FDIFF_7:46;
  end;
  for x st x in Z holds((cos (#) tan)`|Z).x = -(sin.x)^2/cos.x+1/cos.x
  proof
    let x;
    assume
A6: x in Z;
    then ((cos (#) tan)`|Z).x=
    diff(cos,x)*tan.x+cos.x*diff(tan,x) by A1,A3,A4,FDIFF_1:29
      .=tan.x*(-sin.x)+cos.x*diff(tan,x) by SIN_COS:68
      .=tan.x*(-sin.x)+cos.x*(1/(cos.x)^2) by A5,A6
      .=(sin.x/cos.x)*(-sin.x/1)+cos.x/(cos.x)^2 by A2,A6,RFUNCT_1:def 4
      .=-(sin.x)^2/cos.x+cos.x/cos.x/cos.x by XCMPLX_1:79
      .=-(sin.x)^2/cos.x+1/cos.x by A2,A6,FDIFF_8:1,XCMPLX_1:60;
    hence thesis;
  end;
  hence thesis by A1,A3,A4,FDIFF_1:29;
end;

:: f.x=sin.x * cos.x

theorem
  Z c= dom (sin (#) cos) implies (sin (#) cos) is_differentiable_on Z &
  for x st x in Z holds((sin (#) cos)`|Z).x =(cos.x)^2-(sin.x)^2
proof
  assume
A1: Z c= dom (sin (#) cos);
  then Z c= dom sin /\ dom cos by VALUED_1:def 4;
  then
A2: Z c= dom sin & Z c= dom cos by XBOOLE_1:18;
  for x st x in Z holds sin is_differentiable_in x by SIN_COS:69;
  then
A3: sin is_differentiable_on Z by A2,FDIFF_1:16;
  for x st x in Z holds cos is_differentiable_in x by SIN_COS:68;
  then
A4: cos is_differentiable_on Z by A2,FDIFF_1:16;
  for x st x in Z holds ((sin (#) cos)`|Z).x =(cos.x)^2-(sin.x)^2
  proof
    let x;
    assume x in Z;
    then ((sin (#) cos)`|Z).x =
    diff(sin,x)*cos.x + sin.x*diff(cos,x) by A1,A3,A4,FDIFF_1:29
      .=cos.x*cos.x +sin.x*diff(cos,x) by SIN_COS:69
      .=cos.x*cos.x +sin.x*(-sin.x) by SIN_COS:68
      .=(cos.x)^2-(sin.x)^2;
    hence thesis;
  end;
  hence thesis by A1,A3,A4,FDIFF_1:29;
end;

:: f.x=ln.x * sin.x

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

:: f.x=ln.x * cos.x

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

:: f.x=ln.x * exp_R.x

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

::f.x=ln.(ln.x)

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

::f.x=exp_R.(exp_R.x)

theorem
  Z c= dom (exp_R*exp_R) implies exp_R*exp_R is_differentiable_on Z &
  for x st x in Z holds ((exp_R*exp_R)`|Z).x = exp_R.(exp_R.x)*exp_R.x
proof
  assume
A1: Z c= dom (exp_R*exp_R);
A2: for x st x in Z holds exp_R*exp_R is_differentiable_in x
  proof
    let x;
    assume x in Z;
A3: exp_R is_differentiable_in x by SIN_COS:70;
    exp_R is_differentiable_in exp_R.x by SIN_COS:70;
    hence exp_R*exp_R is_differentiable_in x by A3,FDIFF_2:13;
  end;
  then
A4: exp_R*exp_R is_differentiable_on Z by A1,FDIFF_1:16;
  for x st x in Z holds ((exp_R*exp_R)`|Z).x = exp_R.(exp_R.x)*exp_R.x
  proof
    let x;
    assume
A5: x in Z;
A6: exp_R is_differentiable_in x by SIN_COS:70;
    exp_R is_differentiable_in exp_R.x by SIN_COS:70;
    then diff(exp_R*exp_R,x)
    = diff(exp_R,exp_R.x)*diff(exp_R,x) by A6,FDIFF_2:13
      .=exp_R.(exp_R.x)*diff(exp_R,x) by SIN_COS:70
      .=exp_R.(exp_R.x)*exp_R.x by SIN_COS:70;
    hence thesis by A4,A5,FDIFF_1:def 8;
  end;
  hence thesis by A1,A2,FDIFF_1:16;
end;

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

theorem
  Z c= dom (sin*tan) implies sin*tan is_differentiable_on Z &
  for x st x in Z holds ((sin*tan)`|Z).x = cos(tan.x)/(cos.x)^2
proof
  assume
A1: Z c= dom (sin*tan);
A2: for x st x in Z holds cos.x<>0
  proof
    let x;
    assume x in Z;
    then x in dom (sin/cos) by A1,FUNCT_1:21;
    hence thesis by FDIFF_8:1;
  end;
A3: for x st x in Z holds sin*tan is_differentiable_in x
  proof
    let x;
    assume x in Z;
    then cos.x<>0 by A2;
    then
A4: tan is_differentiable_in x by FDIFF_7:46;
    sin is_differentiable_in tan.x by SIN_COS:69;
    hence sin*tan is_differentiable_in x by A4,FDIFF_2:13;
  end;
  then
A5: sin*tan is_differentiable_on Z by A1,FDIFF_1:16;
  for x st x in Z holds ((sin*tan)`|Z).x = cos(tan.x)/(cos.x)^2
  proof
    let x;
    assume
A6: x in Z;
    then
A7: cos.x<>0 by A2;
    then
A8: tan is_differentiable_in x by FDIFF_7:46;
    sin is_differentiable_in tan.x by SIN_COS:69;
    then diff(sin*tan,x) = diff(sin,tan.x)*diff(tan,x) by A8,FDIFF_2:13
      .=cos(tan.x) * diff(tan,x) by SIN_COS:69
      .=cos(tan.x) * (1/(cos.x)^2) by A7,FDIFF_7:46
      .=cos(tan.x)/(cos.x)^2;
    hence thesis by A5,A6,FDIFF_1:def 8;
  end;
  hence thesis by A1,A3,FDIFF_1:16;
end;

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

theorem
  Z c= dom (sin*cot) implies sin*cot is_differentiable_on Z &
  for x st x in Z holds ((sin*cot)`|Z).x =-cos(cot.x)/(sin.x)^2
proof
  assume
A1: Z c= dom (sin*cot);
A2: for x st x in Z holds sin.x<>0
  proof
    let x;
    assume x in Z;
    then x in dom (cos/sin) by A1,FUNCT_1:21;
    hence thesis by FDIFF_8:2;
  end;
A3: for x st x in Z holds sin*cot is_differentiable_in x
  proof
    let x;
    assume x in Z;
    then sin.x<>0 by A2;
    then
A4: cot is_differentiable_in x by FDIFF_7:47;
    sin is_differentiable_in cot.x by SIN_COS:69;
    hence sin*cot is_differentiable_in x by A4,FDIFF_2:13;
  end;
  then
A5: sin*cot is_differentiable_on Z by A1,FDIFF_1:16;
  for x st x in Z holds ((sin*cot)`|Z).x = -cos(cot.x)/(sin.x)^2
  proof
    let x;
    assume
A6: x in Z;
    then
A7: sin.x<>0 by A2;
    then
A8: cot is_differentiable_in x by FDIFF_7:47;
    sin is_differentiable_in cot.x by SIN_COS:69;
    then diff(sin*cot,x) = diff(sin,cot.x)*diff(cot,x) by A8,FDIFF_2:13
      .=cos(cot.x) *diff(cot,x) by SIN_COS:69
      .=cos(cot.x) * (-1/(sin.x)^2) by A7,FDIFF_7:47
      .=-cos(cot.x)/(sin.x)^2;
    hence thesis by A5,A6,FDIFF_1:def 8;
  end;
  hence thesis by A1,A3,FDIFF_1:16;
end;

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

theorem
  Z c= dom (cos*tan) implies cos*tan is_differentiable_on Z &
  for x st x in Z holds ((cos*tan)`|Z).x =-sin(tan.x)/(cos.x)^2
proof
  assume
A1: Z c= dom (cos*tan);
A2: for x st x in Z holds cos.x<>0
  proof
    let x;
    assume x in Z;
    then x in dom (sin/cos) by A1,FUNCT_1:21;
    hence thesis by FDIFF_8:1;
  end;
A3: for x st x in Z holds cos*tan is_differentiable_in x
  proof
    let x;
    assume x in Z;
    then cos.x<>0 by A2;
    then
A4: tan is_differentiable_in x by FDIFF_7:46;
    cos is_differentiable_in tan.x by SIN_COS:68;
    hence cos*tan is_differentiable_in x by A4,FDIFF_2:13;
  end;
  then
A5: cos*tan is_differentiable_on Z by A1,FDIFF_1:16;
  for x st x in Z holds ((cos*tan)`|Z).x = -sin(tan.x)/(cos.x)^2
  proof
    let x;
    assume
A6: x in Z;
    then
A7: cos.x<>0 by A2;
    then
A8: tan is_differentiable_in x by FDIFF_7:46;
    cos is_differentiable_in tan.x by SIN_COS:68;
    then diff(cos*tan,x) = diff(cos,tan.x)*diff(tan,x) by A8,FDIFF_2:13
      .=(-sin(tan.x))*diff(tan,x) by SIN_COS:68
      .=(-sin(tan.x)) * (1/(cos.x)^2) by A7,FDIFF_7:46
      .=-sin(tan.x)/(cos.x)^2;
    hence thesis by A5,A6,FDIFF_1:def 8;
  end;
  hence thesis by A1,A3,FDIFF_1:16;
end;

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

theorem
  Z c= dom (cos*cot) implies cos*cot is_differentiable_on Z &
  for x st x in Z holds ((cos*cot)`|Z).x =sin(cot.x)/(sin.x)^2
proof
  assume
A1: Z c= dom (cos*cot);
A2: for x st x in Z holds sin.x<>0
  proof
    let x;
    assume x in Z;
    then x in dom (cos/sin) by A1,FUNCT_1:21;
    hence thesis by FDIFF_8:2;
  end;
A3: for x st x in Z holds cos*cot is_differentiable_in x
  proof
    let x;
    assume x in Z;
    then sin.x<>0 by A2;
    then
A4: cot is_differentiable_in x by FDIFF_7:47;
    cos is_differentiable_in cot.x by SIN_COS:68;
    hence cos*cot is_differentiable_in x by A4,FDIFF_2:13;
  end;
  then
A5: cos*cot is_differentiable_on Z by A1,FDIFF_1:16;
  for x st x in Z holds ((cos*cot)`|Z).x =sin(cot.x)/(sin.x)^2
  proof
    let x;
    assume
A6: x in Z;
    then
A7: sin.x<>0 by A2;
    then
A8: cot is_differentiable_in x by FDIFF_7:47;
    cos is_differentiable_in cot.x by SIN_COS:68;
    then diff(cos*cot,x) = diff(cos,cot.x)*diff(cot,x) by A8,FDIFF_2:13
      .=(-sin(cot.x))*diff(cot,x) by SIN_COS:68
      .=(-sin(cot.x)) * (-1/(sin.x)^2) by A7,FDIFF_7:47
      .=sin(cot.x)/(sin.x)^2;
    hence thesis by A5,A6,FDIFF_1:def 8;
  end;
  hence thesis by A1,A3,FDIFF_1:16;
end;

::f.x=sin.x*(tan.x+cot.x)

theorem
  Z c= dom (sin(#)(tan+cot)) implies sin(#)(tan+cot) is_differentiable_on Z
  & for x st x in Z holds ((sin(#)(tan+cot))`|Z).x
  =cos.x*(tan.x+cot.x)+sin.x*(1/(cos.x)^2-1/(sin.x)^2)
proof
  assume
A1: Z c= dom (sin(#)(tan+cot));
  then
A2: Z c= dom (tan+cot) /\ dom sin by VALUED_1:def 4;
  then
A3: Z c=dom sin by XBOOLE_1:18;
A4: Z c= dom (tan+cot) by A2,XBOOLE_1:18;
  then
A5: tan+cot is_differentiable_on Z & for x st x in Z holds ((tan+cot)`|Z ).x
  =1/(cos.x)^2-1/(sin.x)^2 by Th6;
  for x st x in Z holds sin is_differentiable_in x by SIN_COS:69;
  then
A6: sin is_differentiable_on Z by A3,FDIFF_1:16;
  for x st x in Z holds (sin(#)(tan+cot)`|Z).x
  =cos.x*(tan.x+cot.x)+sin.x*(1/(cos.x)^2-1/(sin.x)^2)
  proof
    let x;
    assume
A7: x in Z;
    then (sin(#)(tan+cot)`|Z).x
    = ((tan+cot).x)*diff(sin,x)+sin.x*diff(tan+cot,x) by A1,A5,A6,FDIFF_1:29
      .= (tan.x+cot.x)*diff(sin,x)+sin.x*diff(tan+cot,x)
    by A4,A7,VALUED_1:def 1
      .= (tan.x+cot.x) * cos.x +sin.x * diff(tan+cot,x) by SIN_COS:69
      .=(tan.x+cot.x) * cos.x +sin.x * ((tan+cot)`|Z).x by A5,A7,FDIFF_1:def 8
      .=(tan.x+cot.x) * cos.x +sin.x * (1/(cos.x)^2-1/(sin.x)^2) by A4,A7,Th6;
    hence thesis;
  end;
  hence thesis by A1,A5,A6,FDIFF_1:29;
end;

::f.x=cos.x*(tan.x+cot.x)

theorem
  Z c= dom (cos(#)(tan+cot)) implies cos(#)(tan+cot) is_differentiable_on Z
  & for x st x in Z holds ((cos(#)(tan+cot))`|Z).x
  =-sin.x*(tan.x+cot.x)+cos.x*(1/(cos.x)^2-1/(sin.x)^2)
proof
  assume
A1: Z c= dom (cos(#)(tan+cot));
  then
A2: Z c= dom (tan+cot) /\ dom cos by VALUED_1:def 4;
  then
A3: Z c=dom cos by XBOOLE_1:18;
A4: Z c= dom (tan+cot) by A2,XBOOLE_1:18;
  then
A5: tan+cot is_differentiable_on Z & for x st x in Z holds ((tan+cot)`|Z ).x
  =1/(cos.x)^2-1/(sin.x)^2 by Th6;
  for x st x in Z holds cos is_differentiable_in x by SIN_COS:68;
  then
A6: cos is_differentiable_on Z by A3,FDIFF_1:16;
  for x st x in Z holds (cos(#)(tan+cot)`|Z).x
  =-sin.x*(tan.x+cot.x)+cos.x*(1/(cos.x)^2-1/(sin.x)^2)
  proof
    let x;
    assume
A7: x in Z;
    then (cos(#)(tan+cot)`|Z).x
    = ((tan+cot).x)*diff(cos,x) + cos.x*diff(tan+cot,x) by A1,A5,A6,FDIFF_1:29
      .= (tan.x+cot.x)*diff(cos,x) + cos.x*diff(tan+cot,x)
    by A4,A7,VALUED_1:def 1
      .= (tan.x+cot.x) * (-sin.x) + cos.x * diff(tan+cot,x) by SIN_COS:68
      .=(tan.x+cot.x) * (-sin.x) + cos.x * ((tan+cot)`|Z).x
    by A5,A7,FDIFF_1:def 8
      .=(tan.x+cot.x) * (-sin.x) +cos.x * (1/(cos.x)^2-1/(sin.x)^2)
    by A4,A7,Th6;
    hence thesis;
  end;
  hence thesis by A1,A5,A6,FDIFF_1:29;
end;

:: f.x=sin.x*(tan.x-cot.x)

theorem
  Z c= dom (sin(#)(tan-cot)) implies sin(#)(tan-cot) is_differentiable_on Z
  & for x st x in Z holds ((sin(#)(tan-cot))`|Z).x
  =cos.x*(tan.x-cot.x)+sin.x*(1/(cos.x)^2+1/(sin.x)^2)
proof
  assume
A1: Z c= dom (sin(#)(tan-cot));
  then
A2: Z c= dom (tan-cot) /\ dom sin by VALUED_1:def 4;
  then
A3: Z c= dom sin by XBOOLE_1:18;
A4: Z c= dom (tan-cot) by A2,XBOOLE_1:18;
  then
A5: tan-cot is_differentiable_on Z & for x st x in Z holds ((tan-cot)`|Z ).x
  =1/(cos.x)^2+1/(sin.x)^2 by Th5;
  for x st x in Z holds sin is_differentiable_in x by SIN_COS:69;
  then
A6: sin is_differentiable_on Z by A3,FDIFF_1:16;
  for x st x in Z holds (sin(#)(tan-cot)`|Z).x
  =cos.x*(tan.x-cot.x)+sin.x*(1/(cos.x)^2+1/(sin.x)^2)
  proof
    let x;
    assume
A7: x in Z;
    then (sin(#)(tan-cot)`|Z).x
    = ((tan-cot).x)*diff(sin,x)+sin.x*diff(tan-cot,x) by A1,A5,A6,FDIFF_1:29
      .= (tan.x-cot.x)*diff(sin,x)+sin.x*diff(tan-cot,x) by A4,A7,VALUED_1:13
      .= (tan.x-cot.x) * cos.x +sin.x * diff(tan-cot,x) by SIN_COS:69
      .=(tan.x-cot.x) * cos.x +sin.x * ((tan-cot)`|Z).x by A5,A7,FDIFF_1:def 8
      .=(tan.x-cot.x) * cos.x +sin.x * (1/(cos.x)^2+1/(sin.x)^2) by A4,A7,Th5;
    hence thesis;
  end;
  hence thesis by A1,A5,A6,FDIFF_1:29;
end;

:: f.x=cos.x*(tan.x-cot.x)

theorem
  Z c= dom (cos(#)(tan-cot)) implies cos(#)(tan-cot) is_differentiable_on Z
  & for x st x in Z holds ((cos(#)(tan-cot))`|Z).x
  =-sin.x*(tan.x-cot.x)+cos.x*(1/(cos.x)^2+1/(sin.x)^2)
proof
  assume
A1: Z c= dom (cos(#)(tan-cot));
  then
A2: Z c= dom (tan-cot) /\ dom cos by VALUED_1:def 4;
  then
A3: Z c=dom cos by XBOOLE_1:18;
A4: Z c= dom (tan-cot) by A2,XBOOLE_1:18;
  then
A5: tan-cot is_differentiable_on Z & for x st x in Z holds ((tan-cot)`|Z ).x
  =1/(cos.x)^2+1/(sin.x)^2 by Th5;
  for x st x in Z holds cos is_differentiable_in x by SIN_COS:68;
  then
A6: cos is_differentiable_on Z by A3,FDIFF_1:16;
  for x st x in Z holds (cos(#)(tan-cot)`|Z).x
  =-sin.x*(tan.x-cot.x)+cos.x*(1/(cos.x)^2+1/(sin.x)^2)
  proof
    let x;
    assume
A7: x in Z;
    then (cos(#)(tan-cot)`|Z).x
    = ((tan-cot).x)*diff(cos,x)+cos.x*diff(tan-cot,x) by A1,A5,A6,FDIFF_1:29
      .= (tan.x-cot.x)*diff(cos,x)+cos.x*diff(tan-cot,x) by A4,A7,VALUED_1:13
      .= (tan.x-cot.x) *(-sin.x)+cos.x * diff(tan-cot,x) by SIN_COS:68
      .=(tan.x-cot.x) * (-sin.x)+cos.x * ((tan-cot)`|Z).x
    by A5,A7,FDIFF_1:def 8
      .=(tan.x-cot.x) * (-sin.x)+cos.x * (1/(cos.x)^2+1/(sin.x)^2)
    by A4,A7,Th5;
    hence thesis;
  end;
  hence thesis by A1,A5,A6,FDIFF_1:29;
end;

::f.x=exp_R.x*(tan.x + cot.x)

theorem
  Z c= dom (exp_R(#)(tan+cot)) implies exp_R(#)(tan+cot) is_differentiable_on
  Z & for x st x in Z holds ((exp_R(#)(tan+cot))`|Z).x
  =exp_R.x*(tan.x+cot.x)+exp_R.x*(1/(cos.x)^2-1/(sin.x)^2)
proof
  assume
A1: Z c= dom (exp_R(#)(tan+cot));
  then Z c= dom (tan+cot) /\ dom exp_R by VALUED_1:def 4;
  then
A2: Z c= dom (tan+cot) by XBOOLE_1:18;
  then
A3: tan+cot is_differentiable_on Z & for x st x in Z holds ((tan+cot)`|Z ).x
  =1/(cos.x)^2-1/(sin.x)^2 by Th6;
A4: exp_R is_differentiable_on Z by FDIFF_1:34,TAYLOR_1:16;
  for x st x in Z holds (exp_R(#)(tan+cot)`|Z).x
  =exp_R.x*(tan.x+cot.x)+exp_R.x*(1/(cos.x)^2-1/(sin.x)^2)
  proof
    let x;
    assume
A5: x in Z;
    then (exp_R(#)(tan+cot)`|Z).x
    = ((tan+cot).x)*diff(exp_R,x)+exp_R.x*diff(tan+cot,x)
    by A1,A3,A4,FDIFF_1:29
      .= (tan.x+cot.x)*diff(exp_R,x)+exp_R.x*diff(tan+cot,x)
    by A2,A5,VALUED_1:def 1
      .=exp_R.x*(tan.x+cot.x)+exp_R.x*diff(tan+cot,x) by TAYLOR_1:16
      .=exp_R.x*(tan.x+cot.x)+exp_R.x*((tan+cot)`|Z).x by A3,A5,FDIFF_1:def 8
      .=exp_R.x*(tan.x+cot.x)+exp_R.x*(1/(cos.x)^2-1/(sin.x)^2) by A2,A5,Th6;
    hence thesis;
  end;
  hence thesis by A1,A3,A4,FDIFF_1:29;
end;

::f.x=exp_R.x*(tan.x - cot.x)

theorem
  Z c= dom (exp_R(#)(tan-cot)) implies exp_R(#)(tan-cot) is_differentiable_on
  Z & for x st x in Z holds ((exp_R(#)(tan-cot))`|Z).x
  =exp_R.x*(tan.x-cot.x)+exp_R.x*(1/(cos.x)^2+1/(sin.x)^2)
proof
  assume
A1: Z c= dom (exp_R(#)(tan-cot));
  then Z c= dom (tan-cot) /\ dom exp_R by VALUED_1:def 4;
  then
A2: Z c= dom (tan-cot) by XBOOLE_1:18;
  then
A3: tan-cot is_differentiable_on Z & for x st x in Z holds ((tan-cot)`|Z ).x
  =1/(cos.x)^2+1/(sin.x)^2 by Th5;
A4: exp_R is_differentiable_on Z by FDIFF_1:34,TAYLOR_1:16;
  for x st x in Z holds (exp_R(#)(tan-cot)`|Z).x
  =exp_R.x*(tan.x-cot.x)+exp_R.x*(1/(cos.x)^2+1/(sin.x)^2)
  proof
    let x;
    assume
A5: x in Z;
    then (exp_R(#)(tan-cot)`|Z).x
    = ((tan-cot).x)*diff(exp_R,x)+exp_R.x*diff(tan-cot,x)
    by A1,A3,A4,FDIFF_1:29
      .=(tan.x-cot.x)*diff(exp_R,x)+exp_R.x*diff(tan-cot,x)
    by A2,A5,VALUED_1:13
      .=exp_R.x*(tan.x-cot.x)+exp_R.x*diff(tan-cot,x) by TAYLOR_1:16
      .=exp_R.x*(tan.x-cot.x)+exp_R.x*((tan-cot)`|Z).x by A3,A5,FDIFF_1:def 8
      .=exp_R.x*(tan.x-cot.x)+exp_R.x*(1/(cos.x)^2+1/(sin.x)^2) by A2,A5,Th5;
    hence thesis;
  end;
  hence thesis by A1,A3,A4,FDIFF_1:29;
end;

::f.x=sin.x*(sin.x+cos.x)

theorem
  Z c= dom (sin(#)(sin+cos)) implies sin(#)(sin+cos) is_differentiable_on Z
  & for x st x in Z holds ((sin(#)(sin+cos))`|Z).x
  =(cos.x)^2+2*sin.x*cos.x-(sin.x)^2
proof
  assume
A1: Z c= dom (sin(#)(sin+cos));
  then
A2: Z c= dom (sin+cos) /\ dom sin by VALUED_1:def 4;
  then
A3: Z c= dom sin by XBOOLE_1:18;
A4: Z c= dom (sin+cos) by A2,XBOOLE_1:18;
  then
A5: sin+cos is_differentiable_on Z &
  for x st x in Z holds ((sin+cos)`|Z).x =cos.x-sin.x by FDIFF_7:38;
  for x st x in Z holds sin is_differentiable_in x by SIN_COS:69;
  then
A6: sin is_differentiable_on Z by A3,FDIFF_1:16;
  for x st x in Z holds ((sin(#)(sin+cos))`|Z).x
  =(cos.x)^2+2*sin.x*cos.x-(sin.x)^2
  proof
    let x;
    assume
A7: x in Z;
    then ((sin(#)(sin+cos))`|Z).x
    =((sin+cos).x)*diff(sin,x) + (sin.x)*diff((sin+cos),x)
    by A1,A5,A6,FDIFF_1:29
      .=(sin.x+cos.x)*diff(sin,x) + (sin.x)*diff((sin+cos),x) by VALUED_1:1
      .=(sin.x+cos.x)*cos.x + (sin.x)*diff((sin+cos),x) by SIN_COS:69
      .=(sin.x+cos.x)*cos.x + (sin.x)*((sin+cos)`|Z).x by A5,A7,FDIFF_1:def 8
      .=(sin.x+cos.x)*cos.x + (sin.x)*(cos.x-sin.x) by A4,A7,FDIFF_7:38;
    hence thesis;
  end;
  hence thesis by A1,A5,A6,FDIFF_1:29;
end;

::f.x=sin.x*(sin.x-cos.x)

theorem
  Z c= dom (sin(#)(sin-cos)) implies sin(#)(sin-cos) is_differentiable_on Z
  & for x st x in Z holds ((sin(#)(sin-cos))`|Z).x
  =(sin.x)^2+2*sin.x*cos.x-(cos.x)^2
proof
  assume
A1: Z c= dom (sin(#)(sin-cos));
  then
A2: Z c= dom (sin-cos) /\ dom sin by VALUED_1:def 4;
  then
A3: Z c= dom sin by XBOOLE_1:18;
A4: Z c= dom (sin-cos) by A2,XBOOLE_1:18;
  then
A5: sin-cos is_differentiable_on Z &
  for x st x in Z holds ((sin-cos)`|Z).x =cos.x+sin.x by FDIFF_7:39;
  for x st x in Z holds sin is_differentiable_in x by SIN_COS:69;
  then
A6: sin is_differentiable_on Z by A3,FDIFF_1:16;
  for x st x in Z holds ((sin(#)(sin-cos))`|Z).x
  =(sin.x)^2+2*sin.x*cos.x-(cos.x)^2
  proof
    let x;
    assume
A7: x in Z;
    then ((sin(#)(sin-cos))`|Z).x
    =((sin-cos).x)*diff(sin,x) + (sin.x)*diff((sin-cos),x)
    by A1,A5,A6,FDIFF_1:29
      .=(sin.x-cos.x)*diff(sin,x) + (sin.x)*diff((sin-cos),x)
    by A4,A7,VALUED_1:13
      .=(sin.x-cos.x)*cos.x + (sin.x)*diff((sin-cos),x) by SIN_COS:69
      .=(sin.x-cos.x)*cos.x + (sin.x)*((sin-cos)`|Z).x by A5,A7,FDIFF_1:def 8
      .=(sin.x-cos.x)*cos.x + (sin.x)*(cos.x+sin.x) by A4,A7,FDIFF_7:39;
    hence thesis;
  end;
  hence thesis by A1,A5,A6,FDIFF_1:29;
end;

:: f.x=cos.x*(sin.x-cos.x)

theorem
  Z c= dom (cos(#)(sin-cos)) implies cos(#)(sin-cos) is_differentiable_on Z
  & for x st x in Z holds ((cos(#)(sin-cos))`|Z).x
  =(cos.x)^2+2*sin.x*cos.x-(sin.x)^2
proof
  assume
A1: Z c= dom (cos(#)(sin-cos));
  then
A2: Z c= dom (sin-cos) /\ dom cos by VALUED_1:def 4;
  then
A3: Z c= dom cos by XBOOLE_1:18;
A4: Z c= dom (sin-cos) by A2,XBOOLE_1:18;
  then
A5: sin-cos is_differentiable_on Z &
  for x st x in Z holds ((sin-cos)`|Z).x =cos.x+sin.x by FDIFF_7:39;
  for x st x in Z holds cos is_differentiable_in x by SIN_COS:68;
  then
A6: cos is_differentiable_on Z by A3,FDIFF_1:16;
  for x st x in Z holds ((cos(#)(sin-cos))`|Z).x
  =(cos.x)^2+2*sin.x*cos.x-(sin.x)^2
  proof
    let x;
    assume
A7: x in Z;
    then ((cos(#)(sin-cos))`|Z).x
    =((sin-cos).x)*diff(cos,x) + (cos.x)*diff((sin-cos),x)
    by A1,A5,A6,FDIFF_1:29
      .=(sin.x-cos.x)*diff(cos,x) + (cos.x)*diff((sin-cos),x)
    by A4,A7,VALUED_1:13
      .=(sin.x-cos.x)*(-sin.x) + (cos.x)*diff((sin-cos),x) by SIN_COS:68
      .=(sin.x-cos.x)*(-sin.x) + (cos.x)*((sin-cos)`|Z).x
    by A5,A7,FDIFF_1:def 8
      .=(sin.x-cos.x)*(-sin.x) + (cos.x)*(cos.x+sin.x) by A4,A7,FDIFF_7:39;
    hence thesis;
  end;
  hence thesis by A1,A5,A6,FDIFF_1:29;
end;

:: f.x=cos.x*(sin.x+cos.x)

theorem
  Z c= dom (cos(#)(sin+cos)) implies cos(#)(sin+cos) is_differentiable_on Z
  & for x st x in Z holds ((cos(#)(sin+cos))`|Z).x
  =(cos.x)^2-2*sin.x*cos.x-(sin.x)^2
proof
  assume
A1: Z c= dom (cos(#)(sin+cos));
  then
A2: Z c= dom (sin+cos) /\ dom cos by VALUED_1:def 4;
  then
A3: Z c= dom cos by XBOOLE_1:18;
A4: Z c= dom (sin+cos) by A2,XBOOLE_1:18;
  then
A5: sin+cos is_differentiable_on Z &
  for x st x in Z holds ((sin+cos)`|Z).x =cos.x-sin.x by FDIFF_7:38;
  for x st x in Z holds cos is_differentiable_in x by SIN_COS:68;
  then
A6: cos is_differentiable_on Z by A3,FDIFF_1:16;
  for x st x in Z holds ((cos(#)(sin+cos))`|Z).x
  =(cos.x)^2-2*sin.x*cos.x-(sin.x)^2
  proof
    let x;
    assume
A7: x in Z;
    then ((cos(#)(sin+cos))`|Z).x
    =((sin+cos).x)*diff(cos,x) + (cos.x)*diff((sin+cos),x)
    by A1,A5,A6,FDIFF_1:29
      .=(sin.x+cos.x)*diff(cos,x) + (cos.x)*diff((sin+cos),x) by VALUED_1:1
      .=(sin.x+cos.x)*(-sin.x) + (cos.x)*diff((sin+cos),x) by SIN_COS:68
      .=(sin.x+cos.x)*(-sin.x) +(cos.x)*((sin+cos)`|Z).x
    by A5,A7,FDIFF_1:def 8
      .=(sin.x+cos.x)*(-sin.x) + (cos.x)*(cos.x-sin.x) by A4,A7,FDIFF_7:38;
    hence thesis;
  end;
  hence thesis by A1,A5,A6,FDIFF_1:29;
end;

::f.x=sin.(tan.x+cot.x)

theorem
  Z c= dom (sin*(tan+cot)) implies sin*(tan+cot) is_differentiable_on Z &
  for x st x in Z holds (sin*(tan+cot)`|Z).x =
  cos.(tan.x+cot.x)*(1/(cos.x)^2-1/(sin.x)^2)
proof
  assume that
A1: Z c= dom (sin*(tan+cot));
  dom (sin*(tan+cot)) c= dom (tan+cot) by RELAT_1:44;
  then
A2: Z c=dom(tan+cot) by A1,XBOOLE_1:1;
  then
A3: tan + cot is_differentiable_on Z by Th6;
A4: for x st x in Z holds sin*(tan + cot) is_differentiable_in x
  proof
    let x;
    assume x in Z;
    then
A5: (tan + cot) is_differentiable_in x by A3,FDIFF_1:16;
    sin is_differentiable_in (tan+cot).x by SIN_COS:69;
    hence sin*(tan + cot) is_differentiable_in x by A5,FDIFF_2:13;
  end;
  then
A6: sin*(tan + cot) is_differentiable_on Z by A1,FDIFF_1:16;
  for x st x in Z holds (sin*(tan+cot)`|Z).x =
  cos.(tan.x+cot.x)*(1/(cos.x)^2-1/(sin.x)^2)
  proof
    let x;
    assume
A7: x in Z;
    then
A8: tan + cot is_differentiable_in x by A3,FDIFF_1:16;
    sin is_differentiable_in (tan+cot).x by SIN_COS:69;
    then diff(sin*(tan + cot),x)
    = diff(sin, (tan+cot).x)*diff((tan+cot),x) by A8,FDIFF_2:13
      .=cos.((tan+cot).x)*diff((tan+cot),x) by SIN_COS:69
      .=cos.((tan+cot).x)*((tan+cot)`|Z).x by A3,A7,FDIFF_1:def 8
      .=cos.((tan+cot).x)*(1/(cos.x)^2-1/(sin.x)^2) by A2,A7,Th6
      .=cos.(tan.x+cot.x)*(1/(cos.x)^2-1/(sin.x)^2) by A2,A7,VALUED_1:def 1;
    hence thesis by A6,A7,FDIFF_1:def 8;
  end;
  hence thesis by A1,A4,FDIFF_1:16;
end;

::f.x=sin.(tan.x-cot.x)

theorem
  Z c= dom (sin*(tan-cot)) implies sin*(tan-cot) is_differentiable_on Z &
  for x st x in Z holds (sin*(tan-cot)`|Z).x =
  cos.(tan.x-cot.x)*(1/(cos.x)^2+1/(sin.x)^2)
proof
  assume that
A1: Z c= dom (sin*(tan-cot));
  dom (sin*(tan-cot)) c= dom (tan-cot) by RELAT_1:44;
  then
A2: Z c=dom(tan-cot) by A1,XBOOLE_1:1;
  then
A3: tan - cot is_differentiable_on Z by Th5;
A4: for x st x in Z holds sin*(tan - cot) is_differentiable_in x
  proof
    let x;
    assume x in Z;
    then
A5: (tan - cot) is_differentiable_in x by A3,FDIFF_1:16;
    sin is_differentiable_in (tan-cot).x by SIN_COS:69;
    hence sin*(tan - cot) is_differentiable_in x by A5,FDIFF_2:13;
  end;
  then
A6: sin*(tan - cot) is_differentiable_on Z by A1,FDIFF_1:16;
  for x st x in Z holds (sin*(tan-cot)`|Z).x =
  cos.(tan.x-cot.x)*(1/(cos.x)^2+1/(sin.x)^2)
  proof
    let x;
    assume
A7: x in Z;
    then
A8: tan - cot is_differentiable_in x by A3,FDIFF_1:16;
    sin is_differentiable_in (tan-cot).x by SIN_COS:69;
    then diff(sin*(tan -cot),x)
    = diff(sin, (tan-cot).x)*diff((tan-cot),x) by A8,FDIFF_2:13
      .=cos.((tan-cot).x)*diff((tan-cot),x) by SIN_COS:69
      .=cos.((tan-cot).x)*((tan-cot)`|Z).x by A3,A7,FDIFF_1:def 8
      .=cos.((tan-cot).x)*(1/(cos.x)^2+1/(sin.x)^2) by A2,A7,Th5
      .=cos.(tan.x-cot.x)*(1/(cos.x)^2+1/(sin.x)^2) by A2,A7,VALUED_1:13;
    hence thesis by A6,A7,FDIFF_1:def 8;
  end;
  hence thesis by A1,A4,FDIFF_1:16;
end;

::f.x=cos.(tan.x-cot.x)

theorem
  Z c= dom (cos*(tan-cot)) implies cos*(tan-cot) is_differentiable_on Z &
  for x st x in Z holds (cos*(tan-cot)`|Z).x =
  -sin.(tan.x-cot.x)*(1/(cos.x)^2+1/(sin.x)^2)
proof
  assume that
A1: Z c= dom (cos*(tan-cot));
  dom (cos*(tan-cot)) c= dom (tan-cot) by RELAT_1:44;
  then
A2: Z c=dom(tan-cot) by A1,XBOOLE_1:1;
  then
A3: tan - cot is_differentiable_on Z by Th5;
A4: for x st x in Z holds cos*(tan - cot) is_differentiable_in x
  proof
    let x;
    assume x in Z;
    then
A5: (tan - cot) is_differentiable_in x by A3,FDIFF_1:16;
    cos is_differentiable_in (tan-cot).x by SIN_COS:68;
    hence cos*(tan - cot) is_differentiable_in x by A5,FDIFF_2:13;
  end;
  then
A6: cos*(tan - cot) is_differentiable_on Z by A1,FDIFF_1:16;
  for x st x in Z holds (cos*(tan-cot)`|Z).x =
  -sin.(tan.x-cot.x)*(1/(cos.x)^2+1/(sin.x)^2)
  proof
    let x;
    assume
A7: x in Z;
    then
A8: tan - cot is_differentiable_in x by A3,FDIFF_1:16;
    cos is_differentiable_in (tan-cot).x by SIN_COS:68;
    then diff(cos*(tan -cot),x)
    = diff(cos, (tan-cot).x)*diff((tan-cot),x) by A8,FDIFF_2:13
      .=(-sin.((tan-cot).x))*diff((tan-cot),x) by SIN_COS:68
      .=(-sin.((tan-cot).x))*((tan-cot)`|Z).x by A3,A7,FDIFF_1:def 8
      .=(-sin.((tan-cot).x))*(1/(cos.x)^2+1/(sin.x)^2) by A2,A7,Th5
      .=(-sin.(tan.x-cot.x))*(1/(cos.x)^2+1/(sin.x)^2) by A2,A7,VALUED_1:13;
    hence thesis by A6,A7,FDIFF_1:def 8;
  end;
  hence thesis by A1,A4,FDIFF_1:16;
end;

::f.x=cos.(tan.x+cot.x)

theorem
  Z c= dom (cos*(tan+cot)) implies cos*(tan+cot) is_differentiable_on Z &
  for x st x in Z holds (cos*(tan+cot)`|Z).x =
  -sin.(tan.x+cot.x)*(1/(cos.x)^2-1/(sin.x)^2)
proof
  assume that
A1: Z c= dom (cos*(tan+cot));
  dom (cos*(tan+cot)) c= dom (tan+cot) by RELAT_1:44;
  then
A2: Z c=dom(tan+cot) by A1,XBOOLE_1:1;
  then
A3: tan + cot is_differentiable_on Z by Th6;
A4: for x st x in Z holds cos*(tan + cot) is_differentiable_in x
  proof
    let x;
    assume x in Z;
    then
A5: (tan + cot) is_differentiable_in x by A3,FDIFF_1:16;
    cos is_differentiable_in (tan+cot).x by SIN_COS:68;
    hence cos*(tan + cot) is_differentiable_in x by A5,FDIFF_2:13;
  end;
  then
A6: cos*(tan + cot) is_differentiable_on Z by A1,FDIFF_1:16;
  for x st x in Z holds (cos*(tan+cot)`|Z).x =
  -sin.(tan.x+cot.x)*(1/(cos.x)^2-1/(sin.x)^2)
  proof
    let x;
    assume
A7: x in Z;
    then
A8: tan + cot is_differentiable_in x by A3,FDIFF_1:16;
    cos is_differentiable_in (tan+cot).x by SIN_COS:68;
    then diff(cos*(tan +cot),x)
    = diff(cos, (tan+cot).x)*diff((tan+cot),x) by A8,FDIFF_2:13
      .=(-sin.((tan+cot).x))*diff((tan+cot),x) by SIN_COS:68
      .=(-sin.((tan+cot).x))*((tan+cot)`|Z).x by A3,A7,FDIFF_1:def 8
      .=(-sin.((tan+cot).x))*(1/(cos.x)^2-1/(sin.x)^2) by A2,A7,Th6
      .=(-sin.(tan.x+cot.x))*(1/(cos.x)^2-1/(sin.x)^2)
    by A2,A7,VALUED_1:def 1;
    hence thesis by A6,A7,FDIFF_1:def 8;
  end;
  hence thesis by A1,A4,FDIFF_1:16;
end;

::f.x=exp_R.(tan.x + cot.x)

theorem
  Z c= dom (exp_R*(tan+cot)) implies exp_R*(tan+cot) is_differentiable_on Z &
  for x st x in Z holds (exp_R*(tan+cot)`|Z).x =
  exp_R.(tan.x+cot.x)*(1/(cos.x)^2-1/(sin.x)^2)
proof
  assume that
A1: Z c= dom (exp_R*(tan+cot));
  dom (exp_R*(tan+cot)) c= dom (tan+cot) by RELAT_1:44;
  then
A2: Z c=dom(tan+cot) by A1,XBOOLE_1:1;
  then
A3: tan + cot is_differentiable_on Z by Th6;
A4: for x st x in Z holds exp_R*(tan + cot) is_differentiable_in x
  proof
    let x;
    assume x in Z;
    then
A5: (tan + cot) is_differentiable_in x by A3,FDIFF_1:16;
    exp_R is_differentiable_in (tan+cot).x by SIN_COS:70;
    hence exp_R*(tan + cot) is_differentiable_in x by A5,FDIFF_2:13;
  end;
  then
A6: exp_R*(tan + cot) is_differentiable_on Z by A1,FDIFF_1:16;
  for x st x in Z holds (exp_R*(tan+cot)`|Z).x =
  exp_R.(tan.x+cot.x)*(1/(cos.x)^2-1/(sin.x)^2)
  proof
    let x;
    assume
A7: x in Z;
    then
A8: tan + cot is_differentiable_in x by A3,FDIFF_1:16;
    exp_R is_differentiable_in (tan+cot).x by SIN_COS:70;
    then diff(exp_R*(tan +cot),x)
    = diff(exp_R, (tan+cot).x)*diff((tan+cot),x) by A8,FDIFF_2:13
      .=exp_R.((tan+cot).x)*diff((tan+cot),x) by SIN_COS:70
      .=exp_R.((tan+cot).x)*((tan+cot)`|Z).x by A3,A7,FDIFF_1:def 8
      .=exp_R.((tan+cot).x)*(1/(cos.x)^2-1/(sin.x)^2) by A2,A7,Th6
      .=exp_R.(tan.x+cot.x)*(1/(cos.x)^2-1/(sin.x)^2) by A2,A7,VALUED_1:def 1;
    hence thesis by A6,A7,FDIFF_1:def 8;
  end;
  hence thesis by A1,A4,FDIFF_1:16;
end;

::f.x=exp_R.(tan.x - cot.x)

theorem
  Z c= dom (exp_R*(tan-cot)) implies exp_R*(tan-cot) is_differentiable_on Z &
  for x st x in Z holds (exp_R*(tan-cot)`|Z).x =
  exp_R.(tan.x-cot.x)*(1/(cos.x)^2+1/(sin.x)^2)
proof
  assume that
A1: Z c= dom (exp_R*(tan-cot));
  dom (exp_R*(tan-cot)) c= dom (tan-cot) by RELAT_1:44;
  then
A2: Z c=dom(tan-cot) by A1,XBOOLE_1:1;
  then
A3: tan - cot is_differentiable_on Z by Th5;
A4: for x st x in Z holds exp_R*(tan - cot) is_differentiable_in x
  proof
    let x;
    assume x in Z;
    then
A5: (tan - cot) is_differentiable_in x by A3,FDIFF_1:16;
    exp_R is_differentiable_in (tan-cot).x by SIN_COS:70;
    hence exp_R*(tan - cot) is_differentiable_in x by A5,FDIFF_2:13;
  end;
  then
A6: exp_R*(tan - cot) is_differentiable_on Z by A1,FDIFF_1:16;
  for x st x in Z holds (exp_R*(tan-cot)`|Z).x =
  exp_R.(tan.x-cot.x)*(1/(cos.x)^2+1/(sin.x)^2)
  proof
    let x;
    assume
A7: x in Z;
    then
A8: tan - cot is_differentiable_in x by A3,FDIFF_1:16;
    exp_R is_differentiable_in (tan-cot).x by SIN_COS:70;
    then diff(exp_R*(tan -cot),x)
    = diff(exp_R, (tan-cot).x)*diff((tan-cot),x) by A8,FDIFF_2:13
      .=exp_R.((tan-cot).x)*diff((tan-cot),x) by SIN_COS:70
      .=exp_R.((tan-cot).x)*((tan-cot)`|Z).x by A3,A7,FDIFF_1:def 8
      .=exp_R.((tan-cot).x)*(1/(cos.x)^2+1/(sin.x)^2) by A2,A7,Th5
      .=exp_R.(tan.x-cot.x)*(1/(cos.x)^2+1/(sin.x)^2) by A2,A7,VALUED_1:13;
    hence thesis by A6,A7,FDIFF_1:def 8;
  end;
  hence thesis by A1,A4,FDIFF_1:16;
end;

::f.x=(tan.x-cot.x)/exp_.x

theorem
  Z c= dom ((tan-cot)/exp_R) implies (tan-cot)/exp_R is_differentiable_on Z &
  for x st x in Z holds (((tan-cot)/exp_R)`|Z).x =
  (1/(cos.x)^2+1/(sin.x)^2-tan.x+cot.x)/exp_R.x
proof
  assume Z c= dom ((tan-cot)/exp_R);
  then Z c= dom (tan-cot) /\ (dom exp_R \ (exp_R)"{0}) by RFUNCT_1:def 4;
  then
A1: Z c= dom (tan-cot) by XBOOLE_1:18;
  then
A2: tan-cot is_differentiable_on Z &
  for x st x in Z holds ((tan-cot)`|Z).x =1/(cos.x)^2+1/(sin.x)^2 by Th5;
A3: exp_R is_differentiable_on Z by FDIFF_1:34,TAYLOR_1:16;
A4: for x st x in Z holds exp_R.x<>0 by SIN_COS:59;
  then
A5: (tan-cot)/exp_R is_differentiable_on Z by A2,A3,FDIFF_2:21;
  for x st x in Z holds (((tan-cot)/exp_R)`|Z).x
  =(1/(cos.x)^2+1/(sin.x)^2-tan.x+cot.x)/exp_R.x
  proof
    let x;
    assume
A6: x in Z;
A7: exp_R is_differentiable_in x by SIN_COS:70;
A8: tan-cot is_differentiable_in x by A2,A6,FDIFF_1:16;
A9: (tan-cot).x=tan.x-cot.x by A1,A6,VALUED_1:13;
A10: exp_R.x <>0 by SIN_COS:59;
    then diff((tan-cot)/exp_R,x)
    =(diff(tan-cot,x) *exp_R.x -diff(exp_R,x) *(tan-cot).x)/(exp_R.x)^2
    by A7,A8,FDIFF_2:14
      .=(((tan-cot)`|Z).x *exp_R.x-diff(exp_R,x) *(tan-cot).x)/(exp_R.x)^2
    by A2,A6,FDIFF_1:def 8
      .=((1/(cos.x)^2+1/(sin.x)^2)*exp_R.x-diff(exp_R,x)*(tan-cot).x)
    /(exp_R.x)^2 by A1,A6,Th5
      .=((1/(cos.x)^2+1/(sin.x)^2)*exp_R.x-exp_R.x*(tan.x-cot.x))
    /(exp_R.x*exp_R.x) by A9,SIN_COS:70
      .=(1/(cos.x)^2+1/(sin.x)^2-(tan.x-cot.x))*
    (exp_R.x/((exp_R.x)*(exp_R.x)))
      .=(1/(cos.x)^2+1/(sin.x)^2-(tan.x-cot.x))*
    ((exp_R.x)/(exp_R.x)/(exp_R.x)) by XCMPLX_1:79
      .=(1/(cos.x)^2+1/(sin.x)^2-(tan.x-cot.x))*(1/exp_R.x) by A10,XCMPLX_1:60
      .=(1/(cos.x)^2+1/(sin.x)^2-(tan.x-cot.x))/exp_R.x;
    hence thesis by A5,A6,FDIFF_1:def 8;
  end;
  hence thesis by A2,A3,A4,FDIFF_2:21;
end;

::f.x=(tan.x+cot.x)/exp_.x

theorem
  Z c= dom ((tan+cot)/exp_R) implies (tan+cot)/exp_R is_differentiable_on Z &
  for x st x in Z holds (((tan+cot)/exp_R)`|Z).x =
  (1/(cos.x)^2-1/(sin.x)^2-tan.x-cot.x)/exp_R.x
proof
  assume Z c= dom ((tan+cot)/exp_R);
  then Z c= dom (tan+cot) /\ (dom exp_R \ (exp_R)"{0}) by RFUNCT_1:def 4;
  then
A1: Z c= dom (tan+cot) by XBOOLE_1:18;
  then
A2: tan+cot is_differentiable_on Z &
  for x st x in Z holds ((tan+cot)`|Z).x =1/(cos.x)^2-1/(sin.x)^2 by Th6;
A3: exp_R is_differentiable_on Z by FDIFF_1:34,TAYLOR_1:16;
A4: for x st x in Z holds exp_R.x<>0 by SIN_COS:59;
  then
A5: (tan+cot)/exp_R is_differentiable_on Z by A2,A3,FDIFF_2:21;
  for x st x in Z holds (((tan+cot)/exp_R)`|Z).x
  =(1/(cos.x)^2-1/(sin.x)^2-tan.x-cot.x)/exp_R.x
  proof
    let x;
    assume
A6: x in Z;
A7: exp_R is_differentiable_in x by SIN_COS:70;
A8: tan+cot is_differentiable_in x by A2,A6,FDIFF_1:16;
A9: (tan+cot).x=tan.x+cot.x by A1,A6,VALUED_1:def 1;
A10: exp_R.x <>0 by SIN_COS:59;
    then diff((tan+cot)/exp_R,x)
    =(diff(tan+cot,x) *exp_R.x -diff(exp_R,x) *(tan+cot).x)/(exp_R.x)^2
    by A7,A8,FDIFF_2:14
      .=(((tan+cot)`|Z).x *exp_R.x-diff(exp_R,x) *(tan+cot).x)/(exp_R.x)^2
    by A2,A6,FDIFF_1:def 8
      .=((1/(cos.x)^2-1/(sin.x)^2)*exp_R.x-diff(exp_R,x)*(tan+cot).x)
    /(exp_R.x)^2 by A1,A6,Th6
      .=((1/(cos.x)^2-1/(sin.x)^2)*exp_R.x-exp_R.x*(tan.x+cot.x))
    /(exp_R.x*exp_R.x) by A9,SIN_COS:70
      .=(1/(cos.x)^2-1/(sin.x)^2-(tan.x+cot.x))*
    (exp_R.x/((exp_R.x)*(exp_R.x)))
      .=(1/(cos.x)^2-1/(sin.x)^2-(tan.x+cot.x))*
    ((exp_R.x)/(exp_R.x)/(exp_R.x)) by XCMPLX_1:79
      .=(1/(cos.x)^2-1/(sin.x)^2-(tan.x+cot.x))*(1/exp_R.x) by A10,XCMPLX_1:60
      .=(1/(cos.x)^2-1/(sin.x)^2-(tan.x+cot.x))/exp_R.x;
    hence thesis by A5,A6,FDIFF_1:def 8;
  end;
  hence thesis by A2,A3,A4,FDIFF_2:21;
end;

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

theorem
  Z c= dom (sin*sec) implies sin*sec is_differentiable_on Z &
  for x st x in Z holds ((sin*sec)`|Z).x = cos.(sec.x)* sin.x/(cos.x)^2
proof
  assume
A1: Z c= dom (sin*sec);
  dom (sin*sec) c= dom sec by RELAT_1:44;
  then
A2: Z c= dom sec by A1,XBOOLE_1:1;
A3: for x st x in Z holds sin*sec is_differentiable_in x
  proof
    let x;
    assume x in Z;
    then cos.x<>0 by A2,RFUNCT_1:13;
    then
A4: sec is_differentiable_in x by FDIFF_9:1;
    sin is_differentiable_in sec.x by SIN_COS:69;
    hence sin*sec is_differentiable_in x by A4,FDIFF_2:13;
  end;
  then
A5: sin*sec is_differentiable_on Z by A1,FDIFF_1:16;
  for x st x in Z holds ((sin*sec)`|Z).x = cos.(sec.x)* sin.x/(cos.x)^2
  proof
    let x;
    assume
A6: x in Z;
    then
A7: cos.x <>0 by A2,RFUNCT_1:13;
    then
A8: sec is_differentiable_in x by FDIFF_9:1;
    sin is_differentiable_in sec.x by SIN_COS:69;
    then diff(sin*sec,x) = diff(sin,sec.x)*diff(sec,x) by A8,FDIFF_2:13
      .= cos(sec.x)*diff(sec,x) by SIN_COS:69
      .= cos(sec.x)* (sin.x/(cos.x)^2) by A7,FDIFF_9:1
      .=cos.(sec.x)* sin.x/(cos.x)^2;
    hence thesis by A5,A6,FDIFF_1:def 8;
  end;
  hence thesis by A1,A3,FDIFF_1:16;
end;

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

theorem
  Z c= dom (cos*sec) implies cos*sec is_differentiable_on Z &
  for x st x in Z holds ((cos*sec)`|Z).x = -sin.(sec.x)* sin.x/(cos.x)^2
proof
  assume
A1: Z c= dom (cos*sec);
  dom (cos*sec) c= dom sec by RELAT_1:44;
  then
A2: Z c= dom sec by A1,XBOOLE_1:1;
A3: for x st x in Z holds cos*sec is_differentiable_in x
  proof
    let x;
    assume x in Z;
    then cos.x<>0 by A2,RFUNCT_1:13;
    then
A4: sec is_differentiable_in x by FDIFF_9:1;
    cos is_differentiable_in sec.x by SIN_COS:68;
    hence cos*sec is_differentiable_in x by A4,FDIFF_2:13;
  end;
  then
A5: cos*sec is_differentiable_on Z by A1,FDIFF_1:16;
  for x st x in Z holds ((cos*sec)`|Z).x = -sin.(sec.x)* sin.x/(cos.x)^2
  proof
    let x;
    assume
A6: x in Z;
    then
A7: cos.x <>0 by A2,RFUNCT_1:13;
    then
A8: sec is_differentiable_in x by FDIFF_9:1;
    cos is_differentiable_in sec.x by SIN_COS:68;
    then diff(cos*sec,x) = diff(cos,sec.x)*diff(sec,x) by A8,FDIFF_2:13
      .= (-sin(sec.x))*diff(sec,x) by SIN_COS:68
      .= (-sin(sec.x))* (sin.x/(cos.x)^2) by A7,FDIFF_9:1
      .=-sin.(sec.x)* sin.x/(cos.x)^2;
    hence thesis by A5,A6,FDIFF_1:def 8;
  end;
  hence thesis by A1,A3,FDIFF_1:16;
end;

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

theorem
  Z c= dom (sin*cosec) implies sin*cosec is_differentiable_on Z &
  for x st x in Z holds ((sin*cosec)`|Z).x = -cos.(cosec.x)*cos.x/(sin.x)^2
proof
  assume
A1: Z c= dom (sin*cosec);
  dom (sin*cosec) c= dom cosec by RELAT_1:44;
  then
A2: Z c= dom cosec by A1,XBOOLE_1:1;
A3: for x st x in Z holds sin*cosec is_differentiable_in x
  proof
    let x;
    assume x in Z;
    then sin.x<>0 by A2,RFUNCT_1:13;
    then
A4: cosec is_differentiable_in x by FDIFF_9:2;
    sin is_differentiable_in cosec.x by SIN_COS:69;
    hence sin*cosec is_differentiable_in x by A4,FDIFF_2:13;
  end;
  then
A5: sin*cosec is_differentiable_on Z by A1,FDIFF_1:16;
  for x st x in Z holds ((sin*cosec)`|Z).x = -cos.(cosec.x)*cos.x/(sin.x)^2
  proof
    let x;
    assume
A6: x in Z;
    then
A7: sin.x <>0 by A2,RFUNCT_1:13;
    then
A8: cosec is_differentiable_in x by FDIFF_9:2;
    sin is_differentiable_in cosec.x by SIN_COS:69;
    then diff(sin*cosec,x) = diff(sin,cosec.x)*diff(cosec,x) by A8,FDIFF_2:13
      .= cos(cosec.x)*diff(cosec,x) by SIN_COS:69
      .= cos(cosec.x)* (-cos.x/(sin.x)^2) by A7,FDIFF_9:2
      .=-cos.(cosec.x)*cos.x/(sin.x)^2;
    hence thesis by A5,A6,FDIFF_1:def 8;
  end;
  hence thesis by A1,A3,FDIFF_1:16;
end;

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

theorem
  Z c= dom (cos*cosec) implies cos*cosec is_differentiable_on Z &
  for x st x in Z holds ((cos*cosec)`|Z).x = sin.(cosec.x)*cos.x/(sin.x)^2
proof
  assume
A1: Z c= dom (cos*cosec);
  dom (cos*cosec) c= dom cosec by RELAT_1:44;
  then
A2: Z c= dom cosec by A1,XBOOLE_1:1;
A3: for x st x in Z holds cos*cosec is_differentiable_in x
  proof
    let x;
    assume x in Z;
    then sin.x<>0 by A2,RFUNCT_1:13;
    then
A4: cosec is_differentiable_in x by FDIFF_9:2;
    cos is_differentiable_in cosec.x by SIN_COS:68;
    hence cos*cosec is_differentiable_in x by A4,FDIFF_2:13;
  end;
  then
A5: cos*cosec is_differentiable_on Z by A1,FDIFF_1:16;
  for x st x in Z holds ((cos*cosec)`|Z).x = sin.(cosec.x)*cos.x/(sin.x)^2
  proof
    let x;
    assume
A6: x in Z;
    then
A7: sin.x <>0 by A2,RFUNCT_1:13;
    then
A8: cosec is_differentiable_in x by FDIFF_9:2;
    cos is_differentiable_in cosec.x by SIN_COS:68;
    then diff(cos*cosec,x) = diff(cos,cosec.x)*diff(cosec,x) by A8,FDIFF_2:13
      .= (-sin(cosec.x))*diff(cosec,x) by SIN_COS:68
      .= (-sin(cosec.x))* (-cos.x/(sin.x)^2) by A7,FDIFF_9:2;
    hence thesis by A5,A6,FDIFF_1:def 8;
  end;
  hence thesis by A1,A3,FDIFF_1:16;
end;