:: Several Higher Differentiation Formulas of Special Functions
::  by Junjie Zhao , Xiquan Liang and Li Yan
:: 
:: Received March 18, 2008
:: Copyright (c) 2008 Association of Mizar Users

environ

 vocabularies PRE_TOPC, BOOLE, FUNCT_1, ARYTM, ARYTM_1, ARYTM_3, RELAT_1,
      ABSVALUE, QC_LANG1, PARTFUN1, SEQ_1, TAYLOR_2, RCOMP_1, SIN_COS, GROUP_1,
      TAYLOR_1, MATRIX_2, SQUARE_1, FDIFF_1, PREPOWER, FINSEQ_1, NEWTON,
      SIN_COS4;
 notations SUBSET_1, PARTFUN1, RCOMP_1, XXREAL_0, NUMBERS, COMPLEX1, FUNCT_2,
      REAL_1, NAT_1, VALUED_1, SEQ_1, TAYLOR_2, FDIFF_1, SEQFUNC, NEWTON,
      SIN_COS, TAYLOR_1, ABIAN, XBOOLE_0, TARSKI, PREPOWER, BINARITH, RFUNCT_1,
      SQUARE_1, RELSET_1;
 constructors REAL_1, NAT_1, RCOMP_1, LIMFUNC1, TAYLOR_2, FDIFF_1, SIN_COS,
      ABIAN, TAYLOR_1, RFUNCT_1, SQUARE_1, PREPOWER, BINARITH, PARTFUN2, SEQ_1,
      VALUED_1, BINOP_2;
 registrations RELSET_1, NUMBERS, XXREAL_0, NAT_1, MEMBERED, VALUED_0, RCOMP_1,
      XBOOLE_0, FUNCT_1, INT_1, ORDINAL1, FUNCT_2;
 requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
 definitions TAYLOR_1, SEQ_1, VALUED_1, FDIFF_1, TARSKI;
 theorems RFUNCT_1, XBOOLE_0, NEWTON, XCMPLX_1, FUNCT_1, XBOOLE_1, ABSVALUE,
      PARTFUN1, RELAT_1, RCOMP_1, SIN_COS, NAT_1, FDIFF_1, FDIFF_2, TAYLOR_1,
      SIN_COS2, XREAL_1, ABIAN, XXREAL_0, TAYLOR_2, INT_1, WSIERP_1, SQUARE_1,
      FUNCT_2, TARSKI, XCMPLX_0, BINARITH, VALUED_1, PREPOWER, ZFMISC_1,
      FDIFF_7, FDIFF_8, FDIFF_4, XXREAL_1;
 schemes NAT_1;

begin

 reserve x,c,r,a,x0,p for Real;
 reserve n,i,j,s,m for Element of NAT;
 reserve Z for open Subset of REAL;
 reserve f,f1,f2 for PartFunc of REAL,REAL;
 reserve k for Nat;

theorem LemX:
  for f being Function of REAL, REAL holds
    dom (f | Z) = Z
proof
  let f be Function of REAL, REAL;
A1: dom f = REAL by FUNCT_2:def 1;
  thus dom (f|Z) = dom f /\ Z by FUNCT_1:68
    .= Z by XBOOLE_1:28,A1;
end;

theorem ThB6:
  (-f1)(#)(-f2)=f1(#)f2
proof
A1:  dom(-f1) = dom f1 by VALUED_1:def 5;
A2:  dom(-f2) = dom f2 by VALUED_1:def 5;
A3:  dom ((-f1)(#)(-f2)) = dom f1/\dom f2 by A1,A2,VALUED_1:def 4
     .=dom(f1(#)f2) by VALUED_1:def 4;
     for x st x in dom(f1(#)f2) holds ((-f1)(#)(-f2)).x=(f1(#)f2).x
   proof
     let x;
     assume
A5:   x in dom(f1(#)f2);
A6:   dom f1/\dom f2 c= dom f1 by XBOOLE_1:17;
      dom(f1(#)f2) c= dom f1 by A6,VALUED_1:def 4;then
A7:   x in dom f1 by A5;
A8:   x in dom((-1)(#)f1) by A7,VALUED_1:def 5;
B2:   dom(f1(#)f2) = dom f2/\dom f1 by VALUED_1:def 4;
      dom(f2(#)f1) c= dom f2 by B2,XBOOLE_1:17;then
A9:   x in dom f2 by A5;
A10:  x in dom((-1)(#)f2) by A9,VALUED_1:def 5;
      ((-f1)(#)(-f2)).x =(-f1).x*(-f2).x by VALUED_1:def 4,A5,A3
       .=(-1)*f1.x*((-1)(#)f2).x by VALUED_1:def 5,A8
       .=(-1)*f1.x*((-1)*f2.x) by VALUED_1:def 5,A10
       .=f1.x*f2.x;
     hence thesis by VALUED_1:def 4,A5;
   end;
 hence thesis by PARTFUN1:34,A3;
end;

theorem Th36:
  n>=1 implies dom(( #Z n)^)=REAL\{0} & ( #Z n)"{0}={0}
proof
  assume A1:n >= 1;
A0: ( #Z n)"{0} = {0}
  proof
   for x be set st x in {0} holds x in ( #Z n)"{0}
  proof let x be set;
    assume x in {0};
    then A2:x = 0 by TARSKI:def 1;
    {0} c= REAL by ZFMISC_1:37;then
A3: {0} c= dom( #Z n) by FUNCT_2:def 1;
A4:  0 in {0} by TARSKI:def 1;
     ( #Z n).0 = 0 #Z n by TAYLOR_1:def 1
             .=0|^n by PREPOWER:46
             .=0 by NEWTON:16,A1;
     hence x in ( #Z n)"{0} by A2,FUNCT_1:def 13,A4,A3;
    end;
   then A6: {0} c= ( #Z n)"{0} by TARSKI:def 3;
for x be set st x in ( #Z n)"{0} holds x in {0}
    proof let x be set;
     assume A7: x in ( #Z n)"{0}; then
     reconsider x as Element of REAL;
    ( #Z n).x in {0} by FUNCT_1:def 13,A7;then
    ( #Z n).x = 0 by TARSKI:def 1;then
      x #Z n = 0 by TAYLOR_1:def 1;then
     x |^ n = 0 by PREPOWER:46;then
     x = 0 by PREPOWER:12;
   hence thesis by TARSKI:def 1;
  end;
   then ( #Z n)"{0} c= {0} by TARSKI:def 3;
  hence thesis by A6,XBOOLE_0:def 10;
  end;
  then dom(( #Z n)^) = dom ( #Z n) \ {0} by RFUNCT_1:def 8
                    .= REAL \ {0} by FUNCT_2:def 1;
 hence thesis by A0;
end;

Lm2: ].0,r.[ c= REAL\{0}
proof
   let x0 be set;
   assume
A1: x0 in ].0,r.[; then
    x0 <> 0 by XXREAL_1:4;then
    not x0 in {0} by TARSKI:def 1;
   hence thesis by A1,XBOOLE_0:def 4;
end;

theorem
  (r*p)(#)(( #Z n)^)=r(#)(p(#)(( #Z n)^))
proof
A1:  dom ((r*p) (#) (( #Z n)^))
       = dom((( #Z n)^)) by VALUED_1:def 5
      .= dom (p(#)(( #Z n)^)) by VALUED_1:def 5
      .= dom (r(#)(p(#)(( #Z n)^))) by VALUED_1:def 5;
     now let c be set; assume A2: c in dom ((r*p)(#)(( #Z n)^));then
A3:  c in dom (p(#)(( #Z n)^)) by A1,VALUED_1:def 5;
  thus ((r*p)(#)(( #Z n)^)).c
         = r*p * (( #Z n)^).c by A2,VALUED_1:def 5
        .= r*(p * (( #Z n)^).c)
        .= r * (p(#)(( #Z n)^)).c by A3,VALUED_1:def 5
        .= (r(#)(p(#)(( #Z n)^))).c by A1,A2,VALUED_1:def 5;
    end;
 hence thesis by A1,FUNCT_1:9;
end;

theorem ThB2:
  for n,m be Element of REAL holds n(#)f1+m(#)f1=(n+m)(#)f1
proof
  let n,m be Element of REAL;
B1: dom(n(#)f1+m(#)f1)
        = dom (n(#)f1)/\dom (m(#)f1) by VALUED_1:def 1
       .= dom f1/\dom (m(#)f1)by VALUED_1:def 5
       .= dom f1/\dom f1 by VALUED_1:def 5
       .=dom f1;
B2:  dom(n(#)f1+m(#)f1) = dom((n+m)(#)f1) by B1,VALUED_1:def 5;
    for x st x in dom f1 holds (n(#)f1+m(#)f1).x=((n+m)(#)f1).x
    proof
      let x;
      assume
A2:   x in dom f1;
B4:   x in dom(n(#)f1) by A2,VALUED_1:def 5;
B5:   x in dom(m(#)f1) by A2,VALUED_1:def 5;
A4:   (n(#)f1+m(#)f1).x
         =(n(#)f1).x+(m(#)f1).x by VALUED_1:def 1, A2,B1
         .=n*f1.x +(m(#)f1).x by VALUED_1:def 5,B4
         .=n*f1.x +m*f1.x by VALUED_1:def 5,B5;
      x in dom((n+m)(#)f1) by A2,VALUED_1:def 5;then
      ((n+m)(#)f1).x = (n+m)*f1.x by VALUED_1:def 5
        .=n*f1.x +m*f1.x;
    hence thesis by A4;
   end;
 hence thesis by PARTFUN1:34,B1,B2;
end;

theorem ThB1:
  f|Z is_differentiable_on Z implies f is_differentiable_on Z
proof
   assume
A:   f|Z is_differentiable_on Z;
A1:  Z c= dom (f|Z) by FDIFF_1:16,A;
     dom (f|Z) c= dom f by RELAT_1:89;then
A2:  Z c= dom f by A1,XBOOLE_1:1;
     for x st x in Z holds f|Z is_differentiable_in x by A,FDIFF_1:16;
   hence thesis by A2,FDIFF_1:def 7;
end;

theorem ThB19:
  n>=1 & f1 is_differentiable_on n,Z implies f1 is_differentiable_on Z
proof
  assume that
A1:  n>=1 and
A2:  f1 is_differentiable_on n,Z;
A:   1-1<=n-1 by A1,XREAL_1:11;
A3:  diff(f1,Z).0 is_differentiable_on Z by TAYLOR_1:def 6,A,A2;
     f1|Z is_differentiable_on Z by A3,TAYLOR_1:def 5;
   hence thesis by ThB1;
end;

theorem Th18:
  #Z n is_differentiable_on REAL
proof
A1: dom( #Z n) = REAL by FUNCT_2:def 1;
    for x be Real st x in REAL holds
    ( #Z n)|REAL is_differentiable_in x
    proof
      let x be Real;
      assume x in REAL;
      #Z n is_differentiable_in x by TAYLOR_1:2;
      hence thesis by A1,RELAT_1:97;
    end;
    hence thesis by A1,FDIFF_1:def 7;
end;

:: 1 f.x = sin.x
theorem
  x in Z implies (diff(sin,Z).2).x = -sin.x
proof
   assume
A1: x in Z;
A2: cos is_differentiable_on Z by FDIFF_1:34,SIN_COS:72;
A3: sin is_differentiable_on Z by FDIFF_1:34,SIN_COS:73;
    (diff(sin,Z).(2*1)).x = (diff(sin,Z).(1 +1) ).x
         .=(diff(sin,Z).(1+0)`|Z).x by TAYLOR_1:def 5
         .=((diff(sin,Z).0 `|Z)`|Z).x by TAYLOR_1:def 5
         .=((sin | Z`|Z)`|Z).x by TAYLOR_1:def 5
         .=((sin `| Z)`|Z).x by FDIFF_2:16,A3
         .=((cos | Z)`|Z).x by TAYLOR_2:17
         .=(cos `| Z).x by FDIFF_2:16,A2
         .=diff(cos,x) by FDIFF_1:def 8,A2,A1
         .=-sin.x by SIN_COS:68;
    hence thesis;
end;

theorem
  x in Z implies (diff(sin,Z).3).x = (-cos).x
proof
  assume x in Z; then
A2: x in dom (cos|Z) by TAYLOR_2:17;
   dom ((-cos)|Z) = dom (-cos) /\ Z by RELAT_1:90
     .= dom cos /\ Z by VALUED_1:8
     .= dom (cos|Z) by RELAT_1:90
     .= dom (-(cos|Z)) by VALUED_1:8;then
A5: x in dom ((-cos)|Z) by A2,VALUED_1:8;
    (diff(sin,Z).3).x = (diff(sin,Z).(2*1+1)).x
           .= (((-1) |^ 1) (#) (cos | Z)).x by TAYLOR_2:19
           .=((-1)(#)(cos | Z)).x by NEWTON:10
           .=((-cos)|Z).x by RFUNCT_1:65
           .=(-cos).x by FUNCT_1:70,A5;
  hence thesis;
end;

theorem Th3:
  x in Z implies (diff(sin,Z).n).x = sin.(x + n*PI/2)
proof
  assume
A1:  x in Z;
     dom(((-1)(#) sin)|Z) = dom((-1)(#) sin)/\ Z by FUNCT_1:68
            .= dom(sin) /\ Z by VALUED_1:def 5
           .= Z by XBOOLE_1:28,SIN_COS:27;then
A2:  Z c= dom((-1)(#) sin) by RELAT_1:89;
     dom(((-1)(#) cos)|Z) = dom((-1)(#) cos)/\ Z by FUNCT_1:68
          .= dom(cos) /\ Z by VALUED_1:def 5
          .= Z by XBOOLE_1:28,SIN_COS:27;then
A3:  Z c= dom((-1)(#) cos) by RELAT_1:89;
A4:  sin is_differentiable_on Z by FDIFF_1:34,SIN_COS:73;then
AA:     (-1)(#)sin is_differentiable_on Z by FDIFF_2:19;
A6:  cos is_differentiable_on Z by FDIFF_1:34,SIN_COS:72;then
AAA:     (-1)(#)cos is_differentiable_on Z by FDIFF_2:19;
 per cases;
  suppose n>0;then
     0<0+n;then
     1<=n by NAT_1:19;then
      reconsider i=n-1 as Element of NAT by INT_1:18;
   now per cases;
     suppose i is even;then
        consider j be Element of NAT such that
A8:       i = 2*j by ABIAN:def 2;
       per cases;
     suppose j is even;
     then consider m be Element of NAT such that
A9:    j = 2*m by ABIAN:def 2;
      (diff(sin,Z).(i+1)).x
           = (diff(sin,Z).(2*j) `| Z).x by A8,TAYLOR_1:def 5
           .=((-1) |^ j (#) sin | Z`| Z).x by TAYLOR_2:19
           .=( 1 |^ (2*m) (#) sin | Z`| Z).x by WSIERP_1:3,A9
           .= (1 (#) sin | Z`| Z).x by NEWTON:15
           .=(sin | Z`| Z).x by RFUNCT_1:33
           .=(sin`| Z).x by FDIFF_2:16,A4
           .=diff(sin,x) by FDIFF_1:def 8,A4,A1
           .=cos.x by SIN_COS:69
           .=cos.(x+(2*PI*m)) by SIN_COS2:11
           .=sin.(x+((i/2)*PI)+PI/2) by SIN_COS:83,A8,A9
           .=sin.(x + n*PI/2);
           hence thesis;
           end;
      suppose j is odd;
         then consider s be Element of NAT such that
A11:      j = 2*s+1 by ABIAN:9;
       (diff(sin,Z).(i+1)).x
           = (diff(sin,Z).(2*j) `| Z).x by A8,TAYLOR_1:def 5
           .=((-1) |^ (2*s+1) (#) sin | Z`| Z).x by A11,TAYLOR_2:19
           .=(((-1) |^ (2*s)*(-1)) (#) sin | Z`| Z).x by NEWTON:11
           .=((1|^ (2*s)*(-1)) (#) sin | Z`| Z).x by WSIERP_1:3
           .=((1*(-1)) (#) sin | Z`| Z).x by NEWTON:15
           .=((-sin)| Z`| Z).x by RFUNCT_1:65
           .=(((-1) (#) sin)`| Z).x by FDIFF_2:16,AA
           .=(-1)*diff(sin,x) by FDIFF_1:28,A4,A1,A2
           .=(-1)*(cos.x) by SIN_COS:69
           .=-cos.x
           .=cos.(x+PI) by SIN_COS:83
           .=cos.(x+PI+(2*PI*s)) by SIN_COS2:11
           .=sin.(x+((i/2)*PI)+PI/2) by SIN_COS:83,A8,A11
           .=sin.(x + n*PI/2);
           hence thesis;
            end;
          end;
    suppose i is odd;then
     consider j be Element of NAT such that
A13:   i = 2*j +1 by ABIAN:9;
     per cases;
     suppose j is even;
      then consider m be Element of NAT such that
A14:  j = 2*m by ABIAN:def 2;
     (diff(sin,Z).(i+1)).x
         = (diff(sin,Z).(2*j+1) `| Z).x by A13,TAYLOR_1:def 5
        .=((-1) |^ (2*m) (#) cos | Z`| Z).x by A14,TAYLOR_2:19
        .=( 1 |^ (2*m) (#) cos | Z`| Z).x by WSIERP_1:3
        .= (1 (#) cos | Z`| Z).x by NEWTON:15
        .=(cos | Z`| Z).x by RFUNCT_1:33
        .=(cos`| Z).x by FDIFF_2:16,A6
        .=diff(cos,x) by FDIFF_1:def 8,A6,A1
        .=-sin.x by SIN_COS:68
        .=sin.(x+PI) by SIN_COS:83
        .=sin.(x+PI+(2*PI*m)) by SIN_COS2:10
        .=sin.(x+(((i-1)/2)*PI)+PI) by A13,A14
        .=sin.(x + n*PI/2);
       hence thesis;
      end;
     suppose j is odd;
      then consider s be Element of NAT such that
 A16: j = 2*s+1 by ABIAN:9;
      (diff(sin,Z).(i+1)).x
            = (diff(sin,Z).(2*j+1) `| Z).x by A13,TAYLOR_1:def 5
            .=((-1) |^ j (#) cos | Z`| Z).x by TAYLOR_2:19
            .=(((-1) |^ (2*s)*(-1)) (#) cos | Z`| Z).x by NEWTON:11, A16
            .=((1|^ (2*s)*(-1)) (#) cos | Z`| Z).x by WSIERP_1:3
            .=((1*(-1)) (#) cos |Z`| Z).x by NEWTON:15
            .=((-cos)| Z`| Z).x by RFUNCT_1:65
            .=(((-1) (#) cos)`|Z).x by FDIFF_2:16,AAA
            .=(-1)*diff(cos,x) by FDIFF_1:28,A6,A1,A3
            .=(-1)*(-sin.x) by SIN_COS:68
            .=sin.(x+2*PI*s) by SIN_COS2:10
            .=sin.(x+(((i-3)/2)*PI)+2*PI) by SIN_COS:83,A13,A16
           .=sin.(x + n*PI/2);
           hence thesis;
           end;
       end;
     end;
    hence thesis;
   end;
  suppose A18: n=0;
   (diff(sin,Z).n).x = (sin|Z).x by TAYLOR_1:def 5,A18
          .=sin.(x+n*PI/2) by A18,A1,FUNCT_1:72;
   hence thesis;
  end;
end;

:: 2 f.x = cos.x
theorem
  x in Z implies (diff(cos,Z).2).x = -cos.x
proof
 assume
A1: x in Z;
A2: cos is_differentiable_on Z by FDIFF_1:34,SIN_COS:72;
A3: sin is_differentiable_on Z by FDIFF_1:34,SIN_COS:73;then
 AA:    (-1)(#)sin is_differentiable_on Z by FDIFF_2:19;
    dom(((-1)(#) sin)|Z) = dom((-1)(#) sin)/\ Z by FUNCT_1:68
       .= dom(sin) /\ Z by VALUED_1:def 5
       .= Z by XBOOLE_1:28,SIN_COS:27;then
A5: Z c= dom((-1)(#) sin) by RELAT_1:89;
   (diff(cos,Z).2).x = (diff(cos,Z).(1 +1) ).x
      .=(diff(cos,Z).(1+0)`|Z).x by TAYLOR_1:def 5
      .=((diff(cos,Z).0 `|Z)`|Z).x by TAYLOR_1:def 5
      .=((cos | Z`|Z)`|Z).x by TAYLOR_1:def 5
      .=((cos `| Z)`|Z).x by FDIFF_2:16,A2
      .=(((-sin) | Z)`|Z).x by TAYLOR_2:17
      .=(((-1) (#) sin)`| Z).x by FDIFF_2:16,AA
      .=(-1)*diff(sin,x) by FDIFF_1:28,A1,A3,A5
      .=(-1)*(cos.x) by SIN_COS:69
      .=-cos.x;
   hence thesis;
end;

theorem
  x in Z implies (diff(cos,Z).3).x = sin.x
proof
  assume
A1: x in Z;
A2: x in dom (sin|Z) by A1,TAYLOR_2:17;
    (diff(cos,Z).3).x = (diff(cos,Z).(2*1+1)).x
       .= (((-1) |^ (1+1)) (#) (sin | Z)).x by TAYLOR_2:19
       .=(((1|^2)(#)sin| Z)).x by WSIERP_1:2
       .=(((1*1)(#)sin| Z)).x by WSIERP_1:2
       .=((sin)|Z).x by RFUNCT_1:33
       .=(sin).x by FUNCT_1:70,A2;
  hence thesis;
end;

theorem Th6:
  x in Z implies (diff(cos,Z).n).x = cos.(x + n*PI/2)
  proof
     assume
A1:  x in Z;
     dom(((-1)(#) cos)|Z) =dom((-1)(#) cos)/\ Z by FUNCT_1:68
          .= dom(cos) /\ Z by VALUED_1:def 5
         .= Z by XBOOLE_1:28,SIN_COS:27;then
A2:  Z c= dom((-1)(#) cos) by RELAT_1:89;
     dom(((-1)(#) sin)|Z) = dom((-1)(#) sin)/\ Z by FUNCT_1:68
          .= dom(sin) /\ Z by VALUED_1:def 5
         .= Z by XBOOLE_1:28,SIN_COS:27;then
A3:  Z c= dom((-1)(#) sin) by RELAT_1:89;
A4:  cos is_differentiable_on Z by FDIFF_1:34,SIN_COS:72;then
AAA: (-1)(#)cos is_differentiable_on Z by FDIFF_2:19;
A6:  sin is_differentiable_on Z by FDIFF_1:34,SIN_COS:73;then
 AA: (-1)(#)sin is_differentiable_on Z by FDIFF_2:19;
  per cases;
     suppose n>0;then
     0<0+n;then
     1<=n by NAT_1:19;then
     reconsider i=n-1 as Element of NAT by INT_1:18;
      now per cases;
        suppose i is even;then
        consider j be Element of NAT such that
A8:   i = 2*j by ABIAN:def 2;
       per cases;
        suppose j is even;
         then consider m be Element of NAT such that
A9:     j = 2*m by ABIAN:def 2;
        (diff(cos,Z).(i+1)).x
           = (diff(cos,Z).(2*j) `| Z).x by A8,TAYLOR_1:def 5
           .=((-1) |^ (2*m) (#) cos | Z`| Z).x by A9,TAYLOR_2:19
           .=( 1 |^ (2*m) (#) cos | Z`| Z).x by WSIERP_1:3
           .= (1 (#) cos | Z`| Z).x by NEWTON:15
           .=(cos | Z`| Z).x by RFUNCT_1:33
           .=(cos`| Z).x by FDIFF_2:16,A4
           .=diff(cos,x) by FDIFF_1:def 8,A4,A1
           .=-sin.x by SIN_COS:68
           .=cos.(x+PI/2) by SIN_COS:83
           .=cos.(x+PI/2+(2*PI*m)) by SIN_COS2:11
           .=cos.(x+PI/2+((i/2)*PI)) by A8,A9
           .=cos.(x+n*PI/2);
           hence thesis;
           end;
          suppose j is odd;
             then consider s be Element of NAT such that
          A11: j = 2*s+1 by ABIAN:9;
    (diff(cos,Z).(i+1)).x
         = (diff(cos,Z).(2*j) `| Z).x by A8,TAYLOR_1:def 5
        .=((-1) |^ (2*s+1) (#) cos | Z`| Z).x by A11,TAYLOR_2:19
           .=(((-1) |^ (2*s)*(-1)) (#) cos | Z`| Z).x by NEWTON:11
           .=((1|^ (2*s)*(-1)) (#) cos | Z`| Z).x by WSIERP_1:3
           .=((1*(-1)) (#) cos | Z`| Z).x by NEWTON:15
           .=((-cos)| Z`| Z).x by RFUNCT_1:65
           .=(((-1) (#) cos)`| Z).x by FDIFF_2:16,AAA
           .=(-1)*diff(cos,x) by FDIFF_1:28,A4,A1,A2
           .=(-1)*(-sin.x) by SIN_COS:68
           .=sin.(x+(2*PI*s)) by SIN_COS2:10
           .=sin.(x+((i/2-1)*PI)+2*PI) by SIN_COS:83,A8,A11
           .=cos.(PI/2-(x+(i/2+1)*PI)) by SIN_COS:83
           .=cos.(-(PI/2-(x+(i/2+1)*PI))) by SIN_COS:33
           .=cos.(x+n*PI/2);
           hence thesis;
           end;
          end;
    suppose i is odd;
         then consider j be Element of NAT such that
          A13: i = 2*j +1 by ABIAN:9;
           per cases;
       suppose j is even; then consider m be Element of NAT such that
          A14: j = 2*m by ABIAN:def 2;
     (diff(cos,Z).(i+1)).x
           = (diff(cos,Z).(2*j+1) `| Z).x by A13,TAYLOR_1:def 5
          .=((-1) |^ (2*m+1) (#) sin | Z`| Z).x by A14,TAYLOR_2:19
           .=(((-1) |^ (2*m)*(-1)) (#) sin | Z`| Z).x by NEWTON:11
           .=((1|^ (2*m)*(-1)) (#) sin | Z`| Z).x by WSIERP_1:3
           .=((1*(-1)) (#) sin | Z`| Z).x by NEWTON:15
           .=((-sin)| Z`| Z).x by RFUNCT_1:65
           .=(((-1) (#) sin)`| Z).x by FDIFF_2:16,AA
           .=(-1)*diff(sin,x) by FDIFF_1:28,A6,A1,A3
           .=(-1)*(cos.x) by SIN_COS:69
           .=-cos.x
           .=cos.(x+PI) by SIN_COS:83
           .=cos.(x+PI+2*PI*m) by SIN_COS2:11
           .=cos.(x + (i+1)*PI/2) by A13,A14
           .=cos.(x+n*PI/2);
           hence thesis;
           end;
           suppose j is odd;then consider s be Element of NAT such that
          A16: j = 2*s+1 by ABIAN:9;
       (diff(cos,Z).(i+1)).x
           = (diff(cos,Z).(2*j+1) `| Z).x by A13,TAYLOR_1:def 5
          .=((-1) |^ (j+1) (#) sin | Z`| Z).x by TAYLOR_2:19
          .=(1|^ (2*(s+1)) (#) sin |Z`| Z).x by WSIERP_1:3, A16
          .=(1 (#) sin | Z`| Z).x by NEWTON:15
          .=( sin | Z`| Z).x by RFUNCT_1:33
          .=(sin`|Z).x by FDIFF_2:16,A6
         .=diff(sin,x) by FDIFF_1:def 8,A1,A6
         .=cos.x by SIN_COS:69
         .=cos.(x+(2*PI*s)) by SIN_COS2:11
         .=cos.(x+(((i-1)/2-1)*PI)+2*PI) by SIN_COS:83, A13,A16
         .=cos.(x+n*PI/2);
        hence thesis;
           end;
     end;
   end;
  hence thesis;
end;
 suppose A18: n=0;
   (diff(cos,Z).n).x =(cos|Z).x by TAYLOR_1:def 5,A18
          .=cos.(x+n*PI/2) by A18,A1,FUNCT_1:72;
   hence thesis;
 end;
end;

theorem Th7:
  f1 is_differentiable_on n,Z & f2 is_differentiable_on n,Z
    implies diff(f1+f2,Z).n = diff(f1,Z).n + diff(f2,Z).n
proof
  defpred P[Nat] means
     f1 is_differentiable_on $1,Z &
    f2 is_differentiable_on $1,Z
    implies diff(f1+f2,Z).$1 = diff(f1,Z).$1 + diff(f2,Z).$1;
A1: P[0]
    proof
      assume f1 is_differentiable_on 0,Z &
      f2 is_differentiable_on 0,Z;
      diff(f1+f2,Z).0 = (f1+f2)|Z by TAYLOR_1:def 5
         .=f1|Z + f2|Z by RFUNCT_1:60
         .=diff(f1,Z).0 + f2|Z by TAYLOR_1:def 5
         .=diff(f1,Z).0 + diff(f2,Z).0 by TAYLOR_1:def 5;
      hence thesis;
      end;
A2:   for k be Element of NAT st P[k] holds P[k+1]
    proof
      let k be Element of NAT such that
A3:   P[k];
     assume
A4: f1 is_differentiable_on (k+1),Z & f2 is_differentiable_on (k+1),Z;
AA:  k<k+1 by NAT_1:19;
     k<= (k+1)-1;then
A8:  diff(f1,Z).k is_differentiable_on Z &
     diff(f2,Z).k is_differentiable_on Z by TAYLOR_1:def 6,A4;
     diff(f1+f2,Z).(k+1) = ((diff(f1,Z).k)+(diff(f2,Z).k))`|Z
                                by A3,AA,TAYLOR_1:23,A4,TAYLOR_1:def 5
        .= (diff(f1,Z).k)`|Z + (diff(f2,Z).k)`|Z by A8,FDIFF_2:17
        .= diff(f1,Z).(k+1) + (diff(f2,Z).k)`|Z by TAYLOR_1:def 5
        .= diff(f1,Z).(k+1) + diff(f2,Z).(k+1)  by TAYLOR_1:def 5;
  hence thesis;
 end;
   for k be Element of NAT holds P[k] from NAT_1:sch 1(A1,A2);
    hence thesis;
end;

theorem Th8:
  f1 is_differentiable_on n,Z & f2 is_differentiable_on n,Z
    implies diff(f1-f2,Z).n = diff(f1,Z).n - diff(f2,Z).n
proof
  defpred P[Element of NAT] means
    f1 is_differentiable_on $1,Z & f2 is_differentiable_on $1,Z
    implies diff(f1-f2,Z).$1 = diff(f1,Z).$1 - diff(f2,Z).$1;
A1: P[0]
    proof
      assume f1 is_differentiable_on 0,Z & f2 is_differentiable_on 0,Z;
      diff(f1-f2,Z).0 = (f1-f2)|Z by TAYLOR_1:def 5
        .=f1|Z - f2|Z by RFUNCT_1:63
        .=diff(f1,Z).0 - f2|Z by TAYLOR_1:def 5
        .=diff(f1,Z).0 - diff(f2,Z).0 by TAYLOR_1:def 5;
      hence thesis;
      end;
A2: for k be Element of NAT st P[k] holds P[k+1]
  proof
    let k be Element of NAT such that
A3:  P[k];
     assume A4: f1 is_differentiable_on (k+1),Z &
     f2 is_differentiable_on (k+1),Z;
 AA:    k<k+1 by NAT_1:19;
     k<= (k+1)-1;then
A8:  diff(f1,Z).k is_differentiable_on Z &
     diff(f2,Z).k is_differentiable_on Z by TAYLOR_1:def 6,A4;
     diff(f1-f2,Z).(k+1)
          = ((diff(f1,Z).k)-(diff(f2,Z).k))`|Z
                                 by A3,TAYLOR_1:23,A4,AA,TAYLOR_1:def 5
          .= (diff(f1,Z).k)`|Z - (diff(f2,Z).k)`|Z by A8,FDIFF_2:18
          .= diff(f1,Z).(k+1) - (diff(f2,Z).k)`|Z by TAYLOR_1:def 5
          .= diff(f1,Z).(k+1) - diff(f2,Z).(k+1)  by TAYLOR_1:def 5;
    hence thesis;
  end;
   for k be Element of NAT holds P[k] from NAT_1:sch 1(A1,A2);
    hence thesis;
end;

theorem Th9:
  f1 is_differentiable_on n,Z & f2 is_differentiable_on n,Z & i<=n
     implies diff(f1+f2,Z).i = diff(f1,Z).i + diff(f2,Z).i
proof
    assume that
A1: f1 is_differentiable_on n,Z and
A2:  f2 is_differentiable_on n,Z;
    assume
A3: i<=n;
A4: f1 is_differentiable_on i, Z by TAYLOR_1:23,A1,A3;
    f2 is_differentiable_on i, Z by TAYLOR_1:23,A2,A3;
  hence thesis by Th7,A4;
end;

theorem Th10:
  f1 is_differentiable_on n,Z & f2 is_differentiable_on n,Z & i<=n
     implies diff(f1-f2,Z).i = diff(f1,Z).i - diff(f2,Z).i
proof
  assume that
A1:  f1 is_differentiable_on n,Z and
A2:  f2 is_differentiable_on n,Z;
     assume
A3:   i<=n;
A4:   f1 is_differentiable_on i, Z by TAYLOR_1:23,A1,A3;
      f2 is_differentiable_on i, Z by TAYLOR_1:23,A2,A3;
  hence thesis by Th8,A4;
end;

theorem
  f1 is_differentiable_on n,Z & f2 is_differentiable_on n,Z
    implies f1+f2 is_differentiable_on n,Z
proof
assume that
A1:  f1 is_differentiable_on n,Z and
A2:  f2 is_differentiable_on n,Z;
    now let i be Element of NAT such that
A3:    i <= n-1;
A4:   diff(f1,Z).i is_differentiable_on Z by TAYLOR_1:def 6,A3,A1;
A5:   diff(f2,Z).i is_differentiable_on Z by TAYLOR_1:def 6,A2,A3;
      i <= n by WSIERP_1:23,A3;then
A6:   diff(f1+f2,Z).i = diff(f1,Z).i + diff(f2,Z).i by Th9,A1,A2;
     Z c= dom (diff(f1,Z).i) & Z c= dom (diff(f2,Z).i) by FDIFF_1:def 7,A4,A5;
     then Z c= dom (diff(f1,Z).i) /\ dom (diff(f2,Z).i) by XBOOLE_1:19;
     then Z c= dom(diff(f1,Z).i + diff(f2,Z).i) by VALUED_1:def 1;
      hence diff(f1+f2,Z).i is_differentiable_on Z by FDIFF_1:26,A5,A4,A6;
    end;
  hence f1+f2 is_differentiable_on n,Z by TAYLOR_1:def 6;
end;

theorem
  f1 is_differentiable_on n,Z & f2 is_differentiable_on n,Z
    implies f1-f2 is_differentiable_on n,Z
proof
assume A1:  f1 is_differentiable_on n,Z & f2 is_differentiable_on n,Z;
    now let i be Element of NAT such that
A3:   i <= n-1;
A4:   diff(f1,Z).i is_differentiable_on Z by TAYLOR_1:def 6,A3,A1;
A5:   diff(f2,Z).i is_differentiable_on Z by TAYLOR_1:def 6,A1,A3;
      i <= n by WSIERP_1:23,A3;then
A6:   diff(f1-f2,Z).i = diff(f1,Z).i - diff(f2,Z).i by Th10,A1;
      Z c= dom (diff(f1,Z).i) & Z c= dom (diff(f2,Z).i) by FDIFF_1:def 7,A4,A5;
      then Z c= dom (diff(f1,Z).i) /\ dom (diff(f2,Z).i) by XBOOLE_1:19;
      then Z c= dom(diff(f1,Z).i - diff(f2,Z).i) by VALUED_1:12;
     hence diff(f1-f2,Z).i is_differentiable_on Z by FDIFF_1:27,A5,A4,A6;
    end;
  hence f1-f2 is_differentiable_on n,Z by TAYLOR_1:def 6;
end;

theorem Th13:
  f is_differentiable_on n,Z
    implies diff(r(#)f,Z).n = r(#)diff(f,Z).n
proof
  defpred P[Element of NAT] means
     f is_differentiable_on $1,Z
     implies diff(r(#)f,Z).$1 = r(#)diff(f,Z).$1;
A1: P[0] proof
    assume f is_differentiable_on 0,Z;
    diff(r(#)f,Z).0 = (r(#)f)|Z by TAYLOR_1:def 5
         .=r(#)f|Z by RFUNCT_1:65
        .=r(#)diff(f,Z).0  by TAYLOR_1:def 5;
     hence thesis;
    end;
A2: for k be Element of NAT st P[k] holds P[k+1]
     proof let k be Element of NAT;assume
A3:   P[k];
      assume
A4:    f is_differentiable_on (k+1),Z;
 AA:      k<k+1 by NAT_1:19;
       k<= (k+1)-1;then
A6:    diff(f,Z).k is_differentiable_on Z by TAYLOR_1:def 6,A4;
       diff(r(#)f,Z).(k+1)
          = (r(#)diff(f,Z).k) `| Z by A3,AA,TAYLOR_1:23,A4,TAYLOR_1:def 5
          .= r (#) (diff(f,Z).k `| Z) by FDIFF_2:19,A6
          .= r(#) diff(f,Z).(k+1) by TAYLOR_1:def 5;
      hence thesis;
     end;
   for k be Element of NAT holds P[k] from NAT_1:sch 1(A1,A2);
  hence thesis;
end;

theorem Th14:
  f is_differentiable_on n,Z
    implies r(#)f is_differentiable_on n,Z
proof
  assume
A1: f is_differentiable_on n,Z;
   now let i be Element of NAT such that
A2:   i <= n-1;
a3:   i <= n by WSIERP_1:23,A2;
      diff(f,Z).i is_differentiable_on Z by TAYLOR_1:def 6,A2,A1;then
     r(#) diff(f,Z).i is_differentiable_on Z by FDIFF_2:19;
    hence diff(r(#)f,Z).i is_differentiable_on Z by Th13,a3,TAYLOR_1:23,A1;
   end;
  hence r(#)f is_differentiable_on n,Z by TAYLOR_1:def 6;
end;

theorem
  f is_differentiable_on Z implies diff(f,Z).1 = f`|Z
proof
  assume
A1:  f is_differentiable_on Z;
A2:  dom(diff(f,Z).1) = dom(diff(f,Z).(1+0))
      .= dom((diff(f,Z).0)`|Z) by TAYLOR_1:def 5
      .= dom(f|Z`|Z) by TAYLOR_1:def 5
      .= dom(f`|Z) by A1,FDIFF_2:16
      .= Z by FDIFF_1:def 8,A1;
A3:  dom(f`|Z) = Z by FDIFF_1:def 8,A1;
     for x st x in Z holds (diff(f,Z).1).x = (f`|Z).x
    proof
      let x;
      assume x in Z;
      (diff(f,Z).1).x =(diff(f,Z).(1+0)).x
          .=((diff(f,Z).0)`|Z).x by TAYLOR_1:def 5
          .=(f|Z`|Z).x by TAYLOR_1:def 5
          .=(f`|Z).x by A1, FDIFF_2:16;
      hence thesis;
    end;
  hence thesis by PARTFUN1:34,A2,A3;
end;

theorem
  n>=1 & f1 is_differentiable_on n,Z implies diff(f1,Z).1=f1`|Z
proof
  assume that
A1:  n>=1 and
A2:  f1 is_differentiable_on n,Z;
A3:  f1 is_differentiable_on Z by ThB19,A1,A2;
     diff(f1,Z).1 = diff(f1,Z).(1+0)
       .=diff(f1,Z).0`|Z by TAYLOR_1:def 5
       .=f1|Z`|Z by TAYLOR_1:def 5
       .=f1`|Z by FDIFF_2:16,A3;
  hence thesis;
end;

theorem
  x in Z implies (diff(r(#)sin,Z).n).x = r*sin.(x + n*PI/2)
proof
  assume
A1:  x in Z;
A2:  sin is_differentiable_on n, Z by TAYLOR_2:21;
  per cases;
     suppose n>0;then
     0<0+n;then
     1<=n by NAT_1:19;then
     reconsider i=n-1 as Element of NAT by INT_1:18;
A5:  diff(sin,Z ).i is_differentiable_on Z by TAYLOR_1:def 6,A2;
  dom (diff(sin,Z ).n) = dom (diff(sin,Z ).(i+1))
        .= dom((diff(sin,Z ).i)`|Z ) by TAYLOR_1:def 5
        .= Z by FDIFF_1:def 8,A5;then
A8:  x in dom (r (#) diff(sin,Z).n) by A1, VALUED_1:def 5;
    (diff(r(#)sin,Z ).n).x
        = (r (#) diff(sin,Z ).n).x by Th13,A2
       .= r* (diff(sin,Z ).n).x by VALUED_1:def 5,A8
       .= r* (sin.(x + n*PI/2)) by Th3,A1;
  hence thesis;
end;
     suppose A9: n=0;
A10:  dom(r(#) (sin|Z )) = dom(sin|Z) by VALUED_1:def 5
         .= Z by LemX;
     (diff(r(#)sin,Z ).n).x = (r (#) diff(sin,Z ).0).x by A9,Th13,A2
       .=(r (#) (sin|Z)).x by TAYLOR_1:def 5
       .=r*(sin|Z).x by VALUED_1:def 5,A10,A1
       .=r* (sin.(x + n*PI/2)) by A9,FUNCT_1:72,A1;
   hence thesis;
  end;
end;

theorem
  x in Z implies (diff(r(#)cos,Z).n).x = r*cos.(x + n*PI/2)
proof
  assume
A1:  x in Z;
A2:  cos is_differentiable_on n, Z by TAYLOR_2:21;
  per cases;
     suppose n>0;then
     0<0+n;then
     1<=n by NAT_1:19;then
     reconsider i=n-1 as Element of NAT by INT_1:18;
A5:  diff(cos,Z ).i is_differentiable_on Z by TAYLOR_1:def 6,A2;
   dom (diff(cos,Z ).n) = dom(diff(cos,Z ).(i+1))
          .= dom((diff(cos,Z ).i)`|Z ) by TAYLOR_1:def 5
         .= Z by FDIFF_1:def 8,A5;then
A8:  x in dom (r (#) diff(cos,Z).n) by A1,VALUED_1:def 5;
    (diff(r(#)cos,Z ).n).x
            = (r (#) diff(cos,Z).n).x by Th13,A2
          .= r* (diff(cos,Z).n).x by VALUED_1:def 5,A8
         .= r* (cos.(x + n*PI/2)) by Th6,A1;
  hence thesis;
end;
   suppose A9: n=0;
A10:  dom(r(#) (cos|Z )) = dom(cos|Z) by VALUED_1:def 5
         .= Z by LemX;
      (diff(r(#)cos,Z ).n).x=(r (#) diff(cos,Z ).0).x by A9,Th13,A2
        .=(r (#) (cos|Z)).x by TAYLOR_1:def 5
        .=r*(cos|Z).x by VALUED_1:def 5,A10,A1
        .=r* (cos.(x + n*PI/2)) by A9,FUNCT_1:72,A1;
   hence thesis;
  end;
end;

theorem
  x in Z implies (diff(r(#)exp_R,Z).n).x = r*exp_R.x
proof
  assume
A1:  x in Z;
A2:  exp_R is_differentiable_on n,Z by TAYLOR_2:10;
  per cases;
     suppose n>0;then
     0<0+n;then
     1<=n by NAT_1:19;then
     reconsider i=n-1 as Element of NAT by INT_1:18;
A5:  diff(exp_R,Z).i is_differentiable_on Z by TAYLOR_1:def 6,A2;
  dom (diff(exp_R,Z).n) = dom (diff(exp_R,Z).(i+1))
        .= dom((diff(exp_R,Z).i)`|Z) by TAYLOR_1:def 5
        .= Z by FDIFF_1:def 8,A5;then
A8:  x in dom (r (#) diff(exp_R,Z).n) by A1,VALUED_1:def 5;
    (diff(r(#)exp_R,Z).n).x
           = (r (#) diff(exp_R,Z).n).x by Th13,TAYLOR_2:10
          .= r*(diff(exp_R,Z).n).x by VALUED_1:def 5,A8
          .= r*exp_R.x by TAYLOR_2:7,A1;
  hence thesis;
 end;
    suppose A9: n=0;
A10:   dom(r(#) (exp_R|Z )) = dom(exp_R|Z ) by VALUED_1:def 5
           .= Z by LemX;
      (diff(r(#)exp_R,Z).n).x
           = (r (#) diff(exp_R,Z).0).x by A9,Th13,TAYLOR_2:10
          .= (r (#) exp_R|Z).x by TAYLOR_1:def 5
        .= r* ( exp_R|Z).x by VALUED_1:def 5,A10,A1
        .= r*exp_R.x by FUNCT_1:72,A1;
   hence thesis;
 end;
end;

theorem Th19:
  #Z n `| Z = (n(#) #Z (n-1)) | Z
proof
A3:  #Z n is_differentiable_on Z by Th18,FDIFF_1:34;then
A4:  dom (( #Z n )`| Z) = Z by FDIFF_1:def 8;
A6:  dom (n (#) #Z (n-1) ) = dom ( #Z (n-1) ) by VALUED_1:def 5;
A7:  dom (n (#) #Z (n-1) ) = REAL by A6,FUNCT_2:def 1; then
     n (#) #Z (n-1) is Function of REAL, REAL by FUNCT_2:130; then
A8:  dom ((n (#) #Z (n-1)) | Z) = Z by LemX;
     for x be Real st x in Z holds
         (( #Z n ) `| Z ).x = ((n (#) #Z (n-1) )| Z).x
   proof
    let x be Real such that
    A10: x in Z;
     (( #Z n ) `| Z).x = diff(( #Z n ),x) by FDIFF_1:def 8,A3,A10
           .= n *  x #Z (n-1) by TAYLOR_1:2
           .=n*( #Z (n-1) ).x by TAYLOR_1:def 1
           .=(n (#) #Z (n-1)).x by VALUED_1:def 5,A7
           .=((n (#) #Z (n-1)) | Z).x by FUNCT_1:70,A8,A10;
    hence thesis;
  end;
 hence thesis by A4,A8,PARTFUN1:34;
end;

theorem Th20:
  x <> 0 implies ( #Z n)^ is_differentiable_in x &
    diff(( #Z n)^,x) = -(n * x #Z (n-1))/(x #Z n)^2
proof
  assume
A1:   x<>0;
A2:   ( #Z n).x = x #Z n by TAYLOR_1:def 1;
A3:   x #Z n = x|^n by PREPOWER:46;
A5:   ( #Z n).x <>0 by A2,A3,PREPOWER:12,A1;
A6:   #Z n is_differentiable_in x by TAYLOR_1:2;
      diff(( #Z n)^,x)
          = - diff( #Z n,x)/(( #Z n).x)^2 by A5,FDIFF_2:15,A6
         .= -(n * x #Z (n-1))/( #Z n.x)^2 by TAYLOR_1:2
         .= -(n * x #Z (n-1))/(x #Z n)^2 by TAYLOR_1:def 1;
  hence thesis by A5,FDIFF_2:15,A6;
end;

theorem Th21:
  n>=1 implies diff( #Z n,Z).2 = (n*(n-1)(#) #Z (n-2))|Z
proof
  assume
A1: n>=1;
   reconsider m = n-1 as Element of NAT by INT_1:18,A1;
A3:  #Z n is_differentiable_on Z by Th18,FDIFF_1:34;
A4:  #Z m is_differentiable_on Z by Th18,FDIFF_1:34;then
A5:  (m+1)(#) #Z m is_differentiable_on Z by FDIFF_2:19;
    diff( #Z n,Z).2 = diff( #Z n, Z).(1+1)
             .= (diff( #Z n, Z ).(1+0))`|Z by TAYLOR_1:def 5
             .= (diff( #Z n, Z ).0 `|Z)`|Z by TAYLOR_1:def 5
             .= (( #Z n |Z) `|Z)`|Z by TAYLOR_1:def 5
             .= ( #Z n `|Z)`|Z by FDIFF_2:16,A3
             .= (((m+1)(#) #Z ((m+1)-1))| Z)`|Z by Th19
             .= ((m+1)(#) #Z m )`|Z by FDIFF_2:16,A5
             .=(m+1) (#) ( #Z m`|Z) by FDIFF_2:19,A4
             .=(m+1) (#) ((m (#) #Z (m-1))|Z) by Th19
             .=((m+1)(#)(m (#) #Z (m-1) )) |Z by RFUNCT_1:65
             .=(n*(n-1)(#) #Z (n-2))|Z by RFUNCT_1:29;
   hence thesis;
end;

theorem
  n>=2 implies diff( #Z n,Z).3 = (n*(n-1)*(n-2)(#) #Z (n-3))|Z
proof
  assume
A1:  2<=n;
A2:  2+(-1)<=n+0 by XREAL_1:9,A1;
     reconsider m = n-2 as Element of NAT by INT_1:18,A1;
A3:  #Z m is_differentiable_on Z by Th18,FDIFF_1:34;then
A4:  (m+2)*(m+1)(#) #Z m is_differentiable_on Z by FDIFF_2:19;
     diff( #Z n,Z).3
        = diff( #Z n,Z).(2+1)
       .= diff( #Z n,Z).2 `|Z by TAYLOR_1:def 5
       .= ((n*(n-1)(#) #Z (n-2))|Z) `|Z by Th21,A2
       .= ((m+2)*(m+1)(#) #Z m) `|Z by FDIFF_2:16,A4
       .= (m+2)*(m+1)(#)( #Z m`|Z ) by FDIFF_2:19,A3
       .= (m+2)*(m+1)(#)(( m(#) #Z(m-1))|Z) by Th19
       .=(n*(n-1)(#)((n-2)(#) #Z (n-3))) |Z by RFUNCT_1:65
       .=(n*(n-1)*(n-2)(#) #Z (n-3)) |Z by RFUNCT_1:29;
  hence thesis;
end;

Lm1:  n>1 implies (m!)/(n!)*n = (m!)/((n-'1)!)
proof
     assume
A1:  n>1; then
A2:  n-1=n-'1 by BINARITH:50;
A3:  n=n-'1+1 by A2;
     (m!)/(n!)*n = (m!)/((n-'1)!*n)*n by NEWTON:21,A3
       .= (m!)/((n-'1)!) by XCMPLX_1:93,A1;
     hence thesis;
end;

theorem Th23:
  n>m implies diff( #Z n,Z).m = ((n choose m)*(m!)(#) #Z (n-m)) |Z
proof
   defpred P[Nat] means n>$1
      implies diff( #Z n,Z).$1
               = (((n choose $1)*($1!))(#) #Z (n-$1)) | Z;
A1: P[0]
     proof
      assume n>0;
      diff( #Z n,Z).0 = #Z n | Z by TAYLOR_1:def 5
        .=((1*1)(#) #Z n )| Z by RFUNCT_1:33
        .=(((n choose 0)*(0!))(#) #Z (n-0))| Z by NEWTON:18,NEWTON:29;
      hence thesis;
    end;
A5: for k st P[k] holds P[k+1]
     proof let k such that
A6:   P[k];
      assume
A7:    n>(k+1);
A8:   (k+1)+(-1)<=n+0 by XREAL_1:9,A7;then
      reconsider l=n-k as Element of NAT by INT_1:18;
A10:  #Z (l) is_differentiable_on Z by FDIFF_1:34,Th18;then
A11:  (n choose k)*(k!)(#) #Z (l) is_differentiable_on Z by FDIFF_2:19;
A12:  (k!)>0 by NEWTON:23;
A13:  n-k>(k+1)-k by XREAL_1:11,A7;
A14:  ((k+1)!)>0 by NEWTON:23;
      reconsider s=n-(k+1) as Element of NAT by INT_1:18,A7;
      l>=(k+1)-k by XREAL_1:11,A7;then
A15:  l-'1=n-k-1 by BINARITH:50;
 AA:  0+k<1+k by XREAL_1:8;
      diff( #Z n,Z).(k+1)
       =((((n choose k)*(k!))(#) #Z (l)) | Z) `| Z
                                    by A6,AA,A7,XXREAL_0:2,TAYLOR_1:def 5
       .=(((n choose k)*(k!))(#) #Z (l))`| Z by A11,FDIFF_2:16
       .=(n choose k)*(k!)(#) ( #Z (l) `| Z) by FDIFF_2:19,A10
       .=((n choose k)*(k!))(#) (((l)(#) #Z ((l)-1)) | Z) by Th19
       .=(((n choose k)*(k!))(#) ((l)(#) #Z (l-1)))| Z by RFUNCT_1:65
       .=(((n choose k)*(k!)*(l))(#) #Z (l-1))| Z by RFUNCT_1:29
       .=(((n!)/((k!) * (l!))*(k!)*(n-k))(#) #Z (l-1))| Z by A8,NEWTON:def 3
       .=(((n!)/ (l!)*l)(#) #Z (l-1))| Z by XCMPLX_1:93,A12
       .=(((n!)/ ((l-'1)!))(#) #Z (l-1))| Z by Lm1,A13
       .=(((n!)/ (((s)!)*((k+1)!)))*((k+1)!)(#) #Z (n-k-1))| Z
                                                 by A15,XCMPLX_1:93,A14
       .=((n choose (k+1))*((k+1)!)(#) #Z (n-(k+1)))| Z by NEWTON:def 3,A7;
    hence thesis;
  end;
   for k holds P[k] from NAT_1:sch 2 (A1,A5);
    hence thesis;
  end;

theorem
  f is_differentiable_on n,Z implies
    diff(-f,Z).n = -diff(f,Z).n & -f is_differentiable_on n,Z
proof
   assume
A1: f is_differentiable_on n,Z;
A2: diff(-f,Z).n = (-1)(#) diff(f,Z).n by A1,Th13
        .= -diff(f,Z).n;
     -f = (-1)(#)f;
   hence thesis by A2,Th14,A1;
end;

theorem
  x0 in Z implies
    Taylor(sin,Z,x0,x).n = sin.(x0+n*PI/2)*(x-x0)|^ n / (n!) &
    Taylor(cos,Z,x0,x).n = cos.(x0+n*PI/2)*(x-x0)|^ n / (n!)
proof
  assume
A1:  x0 in Z;
A2:  Taylor(sin,Z,x0,x).n
          =(diff(sin,Z).n).x0 *(x-x0)|^ n / (n!) by TAYLOR_1:def 7
        .=sin.(x0+n*PI/2)*(x-x0)|^ n / (n!) by Th3,A1;
       Taylor(cos,Z,x0,x).n
           =(diff(cos,Z).n).x0 *(x-x0)|^ n / (n!) by TAYLOR_1:def 7
         .=cos.(x0+n*PI/2)*(x-x0)|^ n / (n!) by Th6,A1;
    hence thesis by A2;
end;

theorem
  r>0 implies Maclaurin(sin,].-r,r.[,x).n = sin.(n*PI/2)*x|^ n / (n!) &
     Maclaurin(cos,].-r,r.[,x).n = cos.(n*PI/2)*x|^ n / (n!)
proof
 assume
A1: r>0;
    abs(0-0)=0 by ABSVALUE:7;then
A3: 0 in ].0-r,0+r.[ by A1,RCOMP_1:8;
A4: Maclaurin(sin,].-r,r.[,x).n
         =Taylor(sin,].-r,r.[,0,x).n by TAYLOR_2:def 1
        .=(diff(sin,].-r,r.[).n).0 *(x-0)|^ n / (n!) by TAYLOR_1:def 7
        .=sin.(0+n*PI/2)*x|^ n / (n!) by Th3,A3;
    Maclaurin(cos,].-r,r.[,x).n
         =Taylor(cos,].-r,r.[,0,x).n by TAYLOR_2:def 1
        .=(diff(cos,].-r,r.[).n).0 *(x-0)|^ n / (n!) by TAYLOR_1:def 7
        .=cos.(0+n*PI/2)*x|^ n / (n!) by Th6,A3;
    hence thesis by A4;
end;

theorem Th27:
  n>m & x in Z implies
    (diff( #Z n,Z).m).x = (n choose m)*(m!)*x #Z (n-m)
proof
  assume
A1:  n>m & x in Z;
A2:  dom( #Z (n-m))=REAL by FUNCT_2:def 1;
A3:  dom((n choose m)*(m!)(#) #Z (n-m))= REAL by A2,VALUED_1:def 5;
A5:    dom(((n choose m)*(m!)(#) #Z (n-m))|Z) = REAL /\ Z by A3,RELAT_1:90
        .= Z by XBOOLE_1:28;
     (diff( #Z n,Z).m).x
        =(((n choose m)*(m!)(#) #Z (n-m))| Z).x by Th23,A1
       .= ((n choose m)*(m!)(#) #Z (n-m)).x by A5,A1,FUNCT_1:70
       .=(n choose m)*(m!)*( #Z (n-m)).x by VALUED_1:def 5,A3
       .=(n choose m)*(m!)*x #Z (n-m) by TAYLOR_1:def 1;
 hence thesis;
end;

theorem Th28:
  x in Z implies (diff( #Z m,Z).m).x = m!
proof
   assume
A1:  x in Z;
  per cases;
     suppose m>0;then
     0<0+m;then
     1<=m by NAT_1:19;then
      reconsider n=m-1 as Element of NAT by INT_1:18;
A3:    0+n<n+1 by XREAL_1:8;
     reconsider l=(n+1)-n as Element of NAT;
A4:  n!<>0 by NEWTON:23;
A6:  #Z 1 is_differentiable_on Z by FDIFF_1:34,Th18;then
A7:  ((n+1)!)(#) #Z 1 is_differentiable_on Z by FDIFF_2:19;
     Z c= dom( #Z 1) by FDIFF_1:def 7,A6;then
A8:  Z c= dom (((n+1)!)(#) #Z 1) by VALUED_1:def 5;
     (diff( #Z m,Z).m).x
        =(diff( #Z (n+1),Z).n`| Z).x by TAYLOR_1:def 5
       .=(((((n+1) choose n)*(n!)(#) #Z ((n+1)-n)) | Z )`| Z).x by Th23,A3
       .=((((((n+1)!)/((n!)*1))*(n!)(#) #Z ((n+1)-n))|Z )`|Z).x
                                                  by NEWTON:19,NEWTON:def 3,A3
       .=(((((n+1)!)/1(#) #Z 1 )|Z )`| Z).x by XCMPLX_1:93,A4
       .=((((n+1)!)(#) #Z 1)`| Z).x  by A7,FDIFF_2:16
       .=((n+1)!)*diff( #Z 1,x) by FDIFF_1:28,A8,A1,A6
       .=((n+1)!)*(1*x #Z (1-1)) by TAYLOR_1:2
       .=((n+1)!)*1 by PREPOWER:44
       .=m!;
    hence thesis;
  end;
  suppose A9: m=0;then
   (diff( #Z m,Z).m).x = ( #Z 0|Z).x by TAYLOR_1:def 5
      .= ( #Z 0).x by A1,FUNCT_1:72
      .=x #Z 0 by TAYLOR_1:def 1
      .=m! by A9,NEWTON:18,PREPOWER:44;
     hence thesis;
   end;
  end;

theorem Th29:
  #Z n is_differentiable_on n,Z
proof
  let i be Element of NAT;
  assume
A1:  i <= n-1;
     reconsider i as Element of NAT;
     dom( #Z (n-i))=REAL by FUNCT_2:def 1;then
A3:  dom((n choose i)*(i!)(#) #Z (n-i))= REAL by VALUED_1:def 5;
  -1+n<0+n by XREAL_1:8;then
A7:  i<n by A1,XXREAL_0:2;
A8:   dom(diff( #Z n,Z).i)
           = dom(((n choose i)*(i!)(#) #Z (n-i)) | Z) by Th23,A7
          .= REAL /\ Z by A3,RELAT_1:90
          .= Z by XBOOLE_1:28;
      for x be Real st x in Z holds
      diff( #Z n,Z).i | Z is_differentiable_in x
   proof
     let x be Real such that
A10:   x in Z;
       i+0 <= (n-1)+1 by XREAL_1:10,A1;then
       reconsider m = n-i as Element of NAT by INT_1:18;
A12:    diff( #Z n,Z).i | Z
            =(((n choose i)*(i!))(#) #Z m) | Z | Z by Th23,A7
           .=(((n choose i)*(i!))(#) #Z m) |Z by FUNCT_1:82
          .=((n choose i)*(i!))(#) #Z m | Z by RFUNCT_1:65;
        #Z m is_differentiable_on Z by Th18,FDIFF_1:34;then
        #Z m | Z is_differentiable_in x by FDIFF_1:def 7,A10;
          hence thesis by FDIFF_1:23,A12;
         end;
  hence thesis by FDIFF_1:def 7,A8;
end;

theorem
  x in Z & n>m implies (diff(a(#) #Z n,Z).m).x
                                 = a*(n choose m)*(m!)*x #Z (n-m)
proof
 assume that
A1:  x in Z and
A2:  n>m;
A3:  #Z n is_differentiable_on m, Z by A2,TAYLOR_1:23,Th29;
     dom( #Z (n-m))=REAL by FUNCT_2:def 1;then
A5:  dom((n choose m)*(m!)(#) #Z (n-m))= REAL by VALUED_1:def 5;
A9:    dom(diff( #Z n,Z).m)
           = dom(((n choose m)*(m!)(#) #Z (n-m)) | Z) by Th23,A2
          .= REAL /\ Z by A5,RELAT_1:90
          .= Z by XBOOLE_1:28;
A10:  dom(a(#)diff( #Z n,Z).m)
         =dom(diff( #Z n,Z).m) by VALUED_1:def 5;
     (diff(a(#) #Z n,Z).m).x
         = (a(#)diff( #Z n,Z).m).x by Th13,A3
        .= a*(diff( #Z n,Z).m).x by A9,A1,A10,VALUED_1:def 5
        .= a*((n choose m)*(m!)*x #Z (n-m)) by A1,A2,Th27;
hence thesis;
end;

theorem
  x in Z implies (diff(a(#) #Z n,Z).n).x = a*(n!)
proof
  assume
A1:  x in Z;
   per cases;
     suppose n>0;then
     0<0+n;then
     1<=n by NAT_1:19;then
      reconsider  m=n-1 as Element of NAT by INT_1:18;
     #Z n is_differentiable_on n, Z by Th29;then
A4:  (diff( #Z n,Z).m) is_differentiable_on Z by TAYLOR_1:def 6;
A6:  dom(diff( #Z n,Z).n)
          = dom(diff( #Z n,Z).(m+1))
         .= dom( (diff( #Z n,Z).m)`| Z) by TAYLOR_1:def 5
         .=Z by FDIFF_1:def 8,A4;
A7:  dom(a(#)diff( #Z n,Z).n) = dom(diff( #Z n,Z).n) by VALUED_1:def 5;
     (diff(a(#) #Z n,Z).n).x
         = (a(#)diff( #Z n,Z).n).x by Th13,Th29
        .=a*(diff( #Z n,Z).n).x by VALUED_1:def 5,A6,A1,A7
        .=a*(n!) by Th28,A1;
   hence thesis;
end;
    suppose A9:n=0;
      dom( #Z 0)=REAL by FUNCT_2:def 1;then
A12:   dom(a(#) #Z 0)=REAL by VALUED_1:def 5;
       (diff(a(#) #Z n,Z).n).x
         =(a(#)diff( #Z 0,Z).0).x by A9,Th13,Th29
         .=(a(#) #Z 0|Z).x by TAYLOR_1:def 5
         .=((a(#) #Z 0)|Z).x by RFUNCT_1:65
         .=(a(#) #Z 0).x by FUNCT_1:72,A1
         .=a*( #Z 0).x by VALUED_1:def 5,A12
         .=a*x #Z 0 by TAYLOR_1:def 1
         .=a*(n!) by A9,NEWTON:18,PREPOWER:44;
      hence thesis;
   end;
end;

theorem Th31:
  x0 in Z & n>m implies
    Taylor( #Z n,Z,x0,x).m = (n choose m)*x0 #Z (n-m) *(x-x0)|^ m &
    Taylor( #Z n,Z,x0,x).n = (x-x0)|^ n
proof
   assume that
A1:   x0 in Z and
A2:   n>m;
A3:   m!<>0 by NEWTON:23;
A4:   n!<>0 by NEWTON:23;
A5:   Taylor( #Z n,Z,x0,x).m
         = (diff( #Z n,Z).m).x0*(x-x0)|^ m / (m!) by TAYLOR_1:def 7
        .= (n choose m)*(m!)*x0 #Z (n-m)*(x-x0)|^ m / (m!) by Th27,A2,A1
        .=(n choose m)*(x0 #Z (n-m)*(x-x0)|^ m)*(m!)/ (m!)
        .= (n choose m)*x0 #Z (n-m)*(x-x0)|^ m by A3,XCMPLX_1:90;
       Taylor( #Z n,Z,x0,x).n
         =(diff( #Z n ,Z).n).x0*(x-x0)|^ n / (n!) by TAYLOR_1:def 7
         .=(x-x0)|^ n*(n!)/ (n!) by Th28,A1
        .=(x-x0)|^ n by A4,XCMPLX_1:90;
    hence thesis by A5;
end;

theorem
  for n,m be Element of NAT,r,x be Real st n>m & r>0
     holds Maclaurin( #Z n,].-r,r.[,x).m = 0 &
           Maclaurin( #Z n,].-r,r.[,x).n = x|^ n
proof
   let n,m be Element of NAT;
   let r,x be Real;
   assume that
A1:   n>m and
A2:   r>0;
      abs(0-0)=0 by ABSVALUE:7;then
A3:      0 in ].0-r,0+r.[ by A2,RCOMP_1:8;
      reconsider s = n-m as Element of NAT by INT_1:18,A1;
 A4:     n-m>m-m by XREAL_1:11,A1;
A5:   Maclaurin( #Z n,].-r,r.[,x).m
         =Taylor( #Z n,].-r,r.[,0,x).m by TAYLOR_2:def 1
        .=(n choose m)*0 #Z (n-m)*(x-0)|^ m by Th31,A1,A3
        .=(n choose m)*(0|^s)*x|^ m by PREPOWER:46
        .=(n choose m)*0*x|^ m by NEWTON:103,A4
        .=0;
      Maclaurin( #Z n,].-r,r.[,x).n
          =Taylor( #Z n,].-r,r.[,0,x).n by TAYLOR_2:def 1
         .=(x-0)|^ n by Th31,A1,A3
         .=x|^ n;
 hence thesis by A5;
end;

theorem Th34:
  ( #Z n)^ is_differentiable_on ].0,r.[
proof
A2: for x0 st x0 in ].0,r.[ holds #Z n.x0 <> 0
    proof
      let x0;
      assume
A3:   x0 in ].0,r.[;
A4:   x0 <> 0 by XXREAL_1:4,A3;
      #Z n.x0 = x0 #Z n by TAYLOR_1:def 1;
      hence thesis by PREPOWER:48,A4;
     end;
    #Z n is_differentiable_on ].0,r.[ by FDIFF_1:34,Th18;
  hence thesis by FDIFF_2:22,A2;
end;

theorem
  x0 in ].0,r.[ implies
    ((( #Z n)^)`|].0,r.[).x0 =- n/( #Z (n+1)).x0
proof
    assume
A2: x0 in ].0,r.[;
A3: ( #Z n)^ is_differentiable_on ].0,r.[ by Th34;
A5: x0 <> 0 by XXREAL_1:4,A2;
  per cases;
     suppose n>0;then
     0<0+n;then
     n>=1 by NAT_1:19;then
     reconsider i=n-1 as Element of NAT by INT_1:18;
     x0 #Z i<>0 by PREPOWER:48,A5;then
A8: x0|^i<>0 by PREPOWER:46;
    ((( #Z n)^)`|].0,r.[ ).x0
        = diff(( #Z n)^,x0) by A3,FDIFF_1:def 8,A2
       .=- (n* x0 #Z i) /( x0 #Z n)^2 by Th20,A5
       .=- (n* x0 #Z i) /(x0 |^n)^2 by PREPOWER:46
       .= - (n* x0|^i) /( x0 |^n)^2 by PREPOWER:46
       .= - (n* x0|^i) /(( x0 |^(i+1))*( x0 |^(i+1))) by SQUARE_1:def 3
       .=- (n* x0|^i) /(( x0 |^(i+1))*( x0 |^1*x0 |^i)) by NEWTON:13
       .=- (n* x0|^i) /(( x0 |^(i+1)* x0 |^1)*x0 |^i)
       .=- (n* x0|^i) /( x0 |^(i+1+1)*x0 |^i) by NEWTON:13
       .=- n/x0 |^(i+2) by XCMPLX_1:92,A8
       .=- n/x0 #Z (i+2) by PREPOWER:46
       .=- n/( #Z (n+1)).x0 by TAYLOR_1:def 1;
      hence thesis;
   end;
   suppose A9: n=0;
      ((( #Z n)^)`|].0,r.[ ).x0 = diff(( #Z n)^,x0) by A3,FDIFF_1:def 8,A2
        .=- (0* x0 #Z (n-1)) /( x0 #Z n)^2 by A9,Th20,A5
        .=- n/( #Z (n+1)).x0 by A9;
      hence thesis;
   end;
end;

theorem ThA:
  x <>0 implies ( #Z 1)^ is_differentiable_in x &
     diff(( #Z 1)^,x) = -1/(x #Z 1)^2
proof
  assume
A1:   x<>0;
A2:   ( #Z 1).x = x #Z 1 by TAYLOR_1:def 1;
     x #Z 1 = x|^1 by PREPOWER:46;then
A5:   ( #Z 1).x <>0 by A2,PREPOWER:12,A1;
A6:   #Z 1 is_differentiable_in x by TAYLOR_1:2;
       diff(( #Z 1)^,x)
          = - diff( #Z 1,x)/(( #Z 1).x)^2 by A5,FDIFF_2:15,A6
         .= -(1 * x #Z (1-1))/(( #Z 1).x)^2 by TAYLOR_1:2
         .=-(1 * x #Z 0)/(x #Z 1)^2 by TAYLOR_1:def 1
         .=-1/(x #Z 1)^2 by PREPOWER:44;
  hence thesis by A6,A5,FDIFF_2:15;
end;

theorem
  ].0,r.[ c= dom((( #Z 2)^)) implies
    (( #Z 1)^)`|].0,r.[ = ((-1)(#)(( #Z 2)^))|].0,r.[
proof
   assume
A2: ].0,r.[ c=dom((( #Z 2)^));
     ( #Z 1)^ is_differentiable_on ].0,r.[ by Th34; then
A4:  dom((( #Z 1)^)`|].0,r.[) = ].0,r.[ by FDIFF_1:def 8;
A5:  dom(((-1)(#)(( #Z (1+1))^))|].0,r.[)
        = dom(((-1)(#)(( #Z 2)^)))/\].0,r.[ by FUNCT_1:68
        .=dom((( #Z 2)^))/\].0,r.[ by VALUED_1:def 5
        .=].0,r.[ by XBOOLE_1:28,A2;
  for x0 st x0 in ].0,r.[ holds
     ((( #Z 1)^)`|].0,r.[ ).x0 =(((-1)(#)(( #Z 2)^))|].0,r.[).x0
   proof
     let x0;assume
A8:   x0 in ].0,r.[;
A9:   ( #Z 1)^ is_differentiable_on ].0,r.[ by Th34;
A11:   x0 <> 0 by XXREAL_1:4,A8;
A13:   dom((-1)(#)(( #Z 2)^))=dom((( #Z (1+1))^)) by VALUED_1:def 5;
      ((( #Z 1)^)`|].0,r.[ ).x0
           = diff(( #Z 1)^,x0) by A9,FDIFF_1:def 8,A8
          .=-1/(x0 #Z 1)^2 by ThA,A11
           .=-1/(x0 |^1)^2 by PREPOWER:46
          .= - (1* 1) /(( x0 |^1)*( x0 |^1)) by SQUARE_1:def 3
          .=- 1/(x0|^(1+1)) by NEWTON:13
          .=- 1/x0 #Z 2 by PREPOWER:46
          .=- 1/( #Z 2).x0 by TAYLOR_1:def 1
          .=-1*(( #Z 2).x0)" by XCMPLX_0:def 9
          .=-1*(( #Z 2)^).x0 by RFUNCT_1:def 8,A8,A2
          .=(-1)*(( #Z 2)^).x0
          .=((-1)(#)(( #Z 2)^)).x0 by VALUED_1:def 5,A8,A2,A13
          .=(((-1)(#)(( #Z 2)^))|].0,r.[).x0 by FUNCT_1:72,A8;
     hence thesis;
  end;
 hence thesis by PARTFUN1:34,A5,A4;
end;

theorem ThB:
  x <> 0 implies ( #Z 2)^ is_differentiable_in x &
    diff(( #Z 2)^,x) = -(2 * x #Z 1)/(x #Z 2)^2
proof
  assume
A1: x<>0;
A2: ( #Z 2).x = x #Z 2 by TAYLOR_1:def 1;
     x #Z 2 = x|^2 by PREPOWER:46;then
A5:   ( #Z 2).x <>0 by A2,PREPOWER:12,A1;
A6:   #Z 2 is_differentiable_in x by TAYLOR_1:2;
       diff(( #Z 2)^,x)
          = - diff( #Z 2,x)/(( #Z 2).x)^2 by A5,FDIFF_2:15,A6
         .= -(2 * x #Z (2-1))/(( #Z 2).x)^2 by TAYLOR_1:2
         .= -(2 * x #Z 1)/(x #Z 2)^2 by TAYLOR_1:def 1;
  hence thesis by A6,A5,FDIFF_2:15;
end;

theorem
  ].0,r.[ c= dom((( #Z 3)^)) implies
    (( #Z 2)^)`|].0,r.[ = ((-2)(#)(( #Z 3)^))|].0,r.[
proof
   assume
A2: ].0,r.[ c= dom((( #Z 3)^));
     ( #Z 2)^ is_differentiable_on ].0,r.[ by Th34;then
A4:  dom((( #Z 2)^)`|].0,r.[) = ].0,r.[ by FDIFF_1:def 8;
A5:  dom(((-2)(#)(( #Z 3)^))|].0,r.[)
        = dom(((-2)(#)(( #Z 3)^)))/\].0,r.[ by FUNCT_1:68
        .=dom((( #Z 3)^))/\].0,r.[ by VALUED_1:def 5
        .=].0,r.[ by XBOOLE_1:28,A2;
  for x0 st x0 in ].0,r.[ holds
     ((( #Z 2)^)`|].0,r.[ ).x0 =(((-2)(#)(( #Z 3)^))|].0,r.[).x0
   proof
     let x0;assume
A8:   x0 in ].0,r.[;
A9:   ( #Z 2)^ is_differentiable_on ].0,r.[ by Th34;
A11:   x0 <> 0 by XXREAL_1:4,A8;
A13:   dom((-2)(#)(( #Z 3)^))=dom((( #Z 3)^)) by VALUED_1:def 5;
      reconsider i=2-1 as Element of NAT;
A16:   x0 #Z i<>0 by PREPOWER:48,A11;
A17:   x0|^i<>0 by A16,PREPOWER:46;
      ((( #Z 2)^)`|].0,r.[ ).x0
         = diff(( #Z 2)^,x0) by A9,FDIFF_1:def 8,A8
        .= - (2* x0 #Z 1) /( x0 #Z 2)^2 by ThB,A11
        .=- (2* x0 #Z 1) /(x0 |^2)^2 by PREPOWER:46
        .= - (2* x0|^1) /( x0 |^2)^2 by PREPOWER:46
        .=- (2* x0|^1) /(( x0 |^2)*( x0 |^(1+1))) by SQUARE_1:def 3
        .=- (2* x0|^1) /(( x0 |^2)*( x0 |^1*x0 |^1)) by NEWTON:13
        .=- (2* x0|^1) /(( x0 |^(2)* x0 |^1)*x0 |^1)
        .=- (2* x0|^1) /( x0 |^(2+1)*x0 |^1) by NEWTON:13
        .=- 2/x0 |^(1+2) by XCMPLX_1:92,A17
        .=- 2/x0 #Z 3 by PREPOWER:46
        .=- 2/( #Z 3).x0 by TAYLOR_1:def 1
        .=-2*(( #Z 3).x0)" by XCMPLX_0:def 9
        .=-2*(( #Z 3)^).x0 by RFUNCT_1:def 8,A8,A2
        .=(-2)*(( #Z 3)^).x0
        .=((-2)(#)(( #Z 3)^)).x0 by VALUED_1:def 5,A8,A2,A13
        .=(((-2)(#)(( #Z 3)^))|].0,r.[).x0 by FUNCT_1:72,A8;
     hence thesis;
  end;
 hence thesis by PARTFUN1:34,A5,A4;
end;

theorem Th37:
  n>=1 implies (( #Z n)^)`|].0,r.[ = ((-n)(#)(( #Z (n+1))^))|].0,r.[
proof
   assume
A1: n>=1;
A3: n+1>=1+0 by XREAL_1:9;
    ].0,r.[ c= REAL\{0} by Lm2;then
A4: ].0,r.[ c=dom((( #Z (n+1))^)) by Th36,A3;
    ( #Z n)^ is_differentiable_on ].0,r.[ by Th34; then
A5: dom((( #Z n)^)`|].0,r.[) = ].0,r.[ by FDIFF_1:def 8;
A6: dom(((-n)(#)(( #Z (n+1))^))|].0,r.[)
        = dom(((-n)(#)(( #Z (n+1))^)))/\].0,r.[ by FUNCT_1:68
        .=dom((( #Z (n+1))^))/\].0,r.[ by VALUED_1:def 5
        .=].0,r.[ by XBOOLE_1:28,A4;
    for x0 st x0 in ].0,r.[ holds
     ((( #Z n)^)`|].0,r.[ ).x0 =(((-n)(#)(( #Z (n+1))^))|].0,r.[).x0
   proof
     let x0;assume
A9:   x0 in ].0,r.[;
A10:   ( #Z n)^ is_differentiable_on ].0,r.[ by Th34;
A12:   x0 <> 0 by XXREAL_1:4,A9;
A14:   dom((-n)(#)(( #Z (n+1))^))
             =dom((( #Z (n+1))^)) by VALUED_1:def 5;
A15:   n+1>=1+0 by XREAL_1:9;
       ].0,r.[ c= REAL\{0} by Lm2;then
A17:   ].0,r.[ c=dom((( #Z (n+1))^)) by Th36,A15;
       reconsider i=n-1 as Element of NAT by INT_1:18,A1;
A18:   x0 #Z i<>0 by PREPOWER:48,A12;
A19:   x0|^i<>0 by PREPOWER:46, A18;
       ((( #Z n)^)`|].0,r.[ ).x0
         = diff(( #Z n)^,x0) by A10,FDIFF_1:def 8,A9
        .= - (n* x0 #Z (n-1)) /( x0 #Z n)^2 by Th20,A12
        .=- (n* x0 #Z i) /(x0 |^n)^2 by PREPOWER:46
        .= - (n* x0|^i) /( x0 |^n)^2 by PREPOWER:46
        .=- (n* x0|^i) /(( x0 |^n)*( x0 |^n)) by SQUARE_1:def 3
        .=- (n* x0|^i) /(( x0 |^(i+1))*( x0 |^1*x0 |^i)) by NEWTON:13
        .=- (n* x0|^i) /(( x0 |^(i+1)* x0 |^1)*x0 |^i)
        .=- (n* x0|^i) /( x0 |^(i+1+1)*x0 |^i) by NEWTON:13
        .=- n/x0 |^(i+2) by XCMPLX_1:92,A19
        .=- n/x0 #Z (i+2) by PREPOWER:46
        .=- n/( #Z (i+2)).x0 by TAYLOR_1:def 1
        .=-n*(( #Z (n+1)).x0)" by XCMPLX_0:def 9
        .=-n*(( #Z (n+1))^).x0 by RFUNCT_1:def 8,A9,A17
        .=(-n)*(( #Z (n+1))^).x0
        .=((-n)(#)(( #Z (n+1))^)).x0 by VALUED_1:def 5,A9,A14,A17
        .=(((-n)(#)(( #Z (n+1))^))|].0,r.[).x0 by FUNCT_1:72,A9;
     hence thesis;
  end;
 hence thesis by PARTFUN1:34,A5,A6;
end;

theorem ThB3:
  f1 is_differentiable_on 2,Z & f2 is_differentiable_on 2,Z implies
     diff(f1(#)f2,Z).2 =
       (diff(f1,Z).2)(#)f2 + 2(#)((f1`|Z)(#)(f2`|Z))+ f1(#)(diff(f2,Z).2)
proof
   assume that
A1:  f1 is_differentiable_on 2,Z and
A2:  f2 is_differentiable_on 2,Z;
A3:  0<= 2-1;then
A4:  diff(f1,Z).0 is_differentiable_on Z by TAYLOR_1:def 6,A1;
     f1|Z is_differentiable_on Z by A4,TAYLOR_1:def 5;then
A6:  f1 is_differentiable_on Z by ThB1;
A7:  diff(f2,Z).0 is_differentiable_on Z by TAYLOR_1:def 6,A2,A3;
     f2|Z is_differentiable_on Z by A7,TAYLOR_1:def 5;then
A8:  f2 is_differentiable_on Z by ThB1;then
A9:  f1(#)f2 is_differentiable_on Z by FDIFF_2:20,A6;
A10: 1<=2-1;
A12: diff(f1,Z).1 = diff(f1,Z).(1+0)
      .= diff(f1,Z).0`|Z by TAYLOR_1:def 5
      .=(f1|Z)`|Z by TAYLOR_1:def 5
      .=f1`|Z by A6,FDIFF_2:16;
A13:  f1`|Z is_differentiable_on Z by TAYLOR_1:def 6,A1,A12,A10;then
B1:   (f1`|Z)(#)f2 is_differentiable_on Z by FDIFF_2:20,A8;
A15: diff(f2,Z).1 = diff(f2,Z).(1+0)
      .= diff(f2,Z).0`|Z by TAYLOR_1:def 5
      .=(f2|Z)`|Z by TAYLOR_1:def 5
      .=f2`|Z by A8,FDIFF_2:16;
A16:  f2`|Z is_differentiable_on Z by TAYLOR_1:def 6,A2,A10,A15;then
A17:  f1(#)(f2`|Z) is_differentiable_on Z by FDIFF_2:20,A6;
A18:  diff(f1,Z).2 = diff(f1,Z).(1+1)
       .= diff(f1,Z).(1+0)`|Z by TAYLOR_1:def 5
       .=(diff(f1,Z).0`|Z)`|Z by TAYLOR_1:def 5
       .=((f1|Z)`|Z)`|Z by TAYLOR_1:def 5
       .=(f1`|Z)`|Z by FDIFF_2:16,A6;
A19:  diff(f2,Z).2 = diff(f2,Z).(1+1)
       .= diff(f2,Z).(1+0)`|Z by TAYLOR_1:def 5
       .=(diff(f2,Z).0`|Z)`|Z by TAYLOR_1:def 5
       .=((f2|Z)`|Z)`|Z by TAYLOR_1:def 5
       .=(f2`|Z)`|Z by FDIFF_2:16,A8;
      diff(f1(#)f2,Z).2 =diff(f1(#)f2,Z).(1+1)
       .=diff(f1(#)f2,Z).(1+0)`|Z by TAYLOR_1:def 5
       .=(diff(f1(#)f2,Z).0`|Z)`|Z by TAYLOR_1:def 5
       .=(((f1(#)f2)|Z)`|Z)`|Z by TAYLOR_1:def 5
       .=((f1(#)f2)`|Z)`|Z by FDIFF_2:16,A9
       .=((f1`|Z)(#)f2 + f1(#)(f2`|Z))`|Z by FDIFF_2:20,A8,A6
       .=((f1`|Z)(#)f2)`|Z+(f1(#)(f2`|Z))`|Z by FDIFF_2:17,A17,B1
       .=(((f1`|Z)`|Z)(#)f2 + (f1`|Z)(#)(f2`|Z))+(f1(#)(f2`|Z))`|Z
                                              by FDIFF_2:20,A13,A8
       .=((diff(f1,Z).2)(#)f2 + (f1`|Z)(#)(f2`|Z))+
                ((f1`|Z)(#)(f2`|Z) + f1(#)(diff(f2,Z).2))
                             by A18,A19,FDIFF_2:20,A6,A16
       .=(((diff(f1,Z).2)(#)f2 + ((f1`|Z)(#)(f2`|Z))+
         (f1`|Z)(#)(f2`|Z))) + f1(#)(diff(f2,Z).2) by RFUNCT_1:19
       .=(diff(f1,Z).2)(#)f2 + ((f1`|Z)(#)(f2`|Z)+
         (f1`|Z)(#)(f2`|Z)) + f1(#)(diff(f2,Z).2) by RFUNCT_1:19
       .=(diff(f1,Z).2)(#)f2 + (1(#)((f1`|Z)(#)(f2`|Z))+
         ((f1`|Z)(#)(f2`|Z))) + f1(#)(diff(f2,Z).2) by RFUNCT_1:33
       .=(diff(f1,Z).2)(#)f2 + (1(#)((f1`|Z)(#)(f2`|Z))+
         1(#)((f1`|Z)(#)(f2`|Z))) + f1(#)(diff(f2,Z).2) by RFUNCT_1:33
       .=((diff(f1,Z).2)(#)f2 + ((1+1)(#)((f1`|Z)(#)(f2`|Z)))
          + f1(#)(diff(f2,Z).2)) by ThB2
       .=((diff(f1,Z).2)(#)f2 + (2(#)((f1`|Z)(#)(f2`|Z)))
          + f1(#)(diff(f2,Z).2));
   hence thesis;
end;

theorem
  Z c= dom ln & Z c= dom((( #Z 1)^))
    implies ln`| Z = (( #Z 1)^)| Z
proof
assume that
A1:  Z c= dom ln and
A:   Z c= dom((( #Z 1)^));
AA:  dom ((( #Z 1)^)| Z) = dom((( #Z 1)^))/\Z by FUNCT_1:68
       .=Z by XBOOLE_1:28,A;
     ln is_differentiable_on Z by A1,TAYLOR_1:18,FDIFF_1:34;then
B:   dom ((( #Z 1)^)| Z) = dom (ln`| Z) by AA,FDIFF_1:def 8;
     for x0 st x0 in dom((( #Z 1)^)|Z)
           holds (ln`| Z).x0 = ((( #Z 1)^)| Z).x0
      proof
        let x0;
        assume
A3:  x0 in dom((( #Z 1)^)|Z);
A5:  ln is_differentiable_on Z by A1,TAYLOR_1:18,FDIFF_1:34;
       (ln`| Z).x0 = diff(ln,x0) by FDIFF_1:def 8,AA,A3,A5
         .=1/x0 by TAYLOR_1:18,A1,AA,A3
         .=1/(x0 #Z 1) by PREPOWER:45
         .=1/(( #Z 1).x0) by TAYLOR_1:def 1
         .=1*(( #Z 1).x0)"by XCMPLX_0:def 9
         .= 1*(( #Z 1)^).x0 by RFUNCT_1:def 8,A,AA,A3
        .= ((( #Z 1)^)|Z).x0 by AA,A3,FUNCT_1:72;
      hence thesis;
     end;
hence thesis by PARTFUN1:34,B;
end;

theorem
  n>=1 & x0 in ].0,r.[
    implies (diff((( #Z n)^),].0,r.[).2).x0 = n*(n+1)*((( #Z (n+2))^).x0)
proof
   assume that
A1:  n>=1 and
A2:  x0 in ].0,r.[;
A3:  ( #Z n)^ is_differentiable_on ].0,r.[ by Th34;
     reconsider m =-n as Element of REAL;
A:   (( #Z (n+1))^) is_differentiable_on ].0,r.[ by Th34;then
A4:  m(#)(( #Z (n+1))^) is_differentiable_on ].0,r.[ by FDIFF_2:19;
A5:  n+1>=1+0 by XREAL_1:9;
A6:  dom((m )(#)(( #Z (n+1))^))=dom((( #Z (n+1))^)) by VALUED_1:def 5;
B:   ].0,r.[ c= REAL\{0} by Lm2;then
A7:  ].0,r.[ c= dom((-n)(#)(( #Z (n+1))^)) by A6,Th36,A5;
     n+1+1>=1+0 by XREAL_1:9;then
A8:  ].0,r.[ c=dom((( #Z (n+2))^)) by Th36,B;
A9:  dom((-(n+1))(#)((( #Z (n+2))^)|].0,r.[))
      =dom((( #Z (n+2))^)|].0,r.[) by VALUED_1:def 5
      .=dom((( #Z (n+2))^))/\ ].0,r.[ by FUNCT_1:68
      .=].0,r.[ by A8,XBOOLE_1:28;
      (diff((( #Z n)^),].0,r.[).2).x0
         =(diff((( #Z n)^),].0,r.[).(1+1)).x0
        .=((diff((( #Z n)^),].0,r.[).(1+0))`|].0,r.[).x0 by TAYLOR_1:def 5
        .=(((diff((( #Z n)^),].0,r.[).0)`|].0,r.[)`|].0,r.[).x0
                                                     by TAYLOR_1:def 5
        .=(((((( #Z n)^)|].0,r.[))`|].0,r.[)`|].0,r.[).x0 by TAYLOR_1:def 5
        .=((((( #Z n)^))`|].0,r.[)`|].0,r.[).x0 by FDIFF_2:16,A3
        .= ((((m )(#)(( #Z (n+1))^))|].0,r.[)`|].0,r.[).x0 by Th37,A1
        .=(((m )(#)(( #Z (n+1))^))`|].0,r.[).x0 by FDIFF_2:16,A4
        .=(m )*diff((( #Z (n+1))^),x0) by FDIFF_1:28,A2,A,A7
        .=(m )*((( #Z (n+1))^)`|].0,r.[).x0 by FDIFF_1:def 8,A2,A
        .=(m )*(((-(n+1))(#)(( #Z ((n+1)+1))^))|].0,r.[).x0 by Th37,A5
        .=(m )*((-(n+1))(#)(((( #Z (n+2))^))|].0,r.[)).x0 by RFUNCT_1:65
        .=(m)*((-(n+1))*(((( #Z (n+2))^)|].0,r.[).x0 ))
           by VALUED_1:def 5,A9,A2
        .=n*(n+1)*((( #Z (n+2))^)|].0,r.[).x0
        .=n*(n+1)*((( #Z (n+2))^).x0) by A2,FUNCT_1:72;
     hence thesis;
  end;

theorem
  diff(sin(#)sin,Z).2 = 2(#)((cos(#)cos)|Z) +(-2)(#)((sin(#) sin)|Z)
proof
A2:  sin is_differentiable_on 2,Z by TAYLOR_2:21;
     diff(sin(#)sin,Z).2
        =(diff(sin,Z).(2*1))(#)sin + 2(#)((sin`|Z)(#)(sin`|Z))
          +sin(#)(diff(sin,Z).(2*1)) by ThB3,A2
        .=((-1) |^ 1 (#) sin | Z)(#)sin + 2(#)((sin`|Z)(#)(sin`|Z))
          +sin(#)(diff(sin,Z).(2*1))by TAYLOR_2:19
        .=((-1) |^ 1 (#) sin | Z)(#)sin + 2(#)((sin`|Z)(#)(sin`|Z))
          +sin(#)((-1) |^ 1 (#) sin | Z) by TAYLOR_2:19
        .=((-1) |^ 1 (#) sin | Z)(#)sin + 2(#)((sin`|Z)(#)(sin`|Z))
          +sin(#)((-1)(#) sin | Z)by NEWTON:10
        .=((-1)(#) sin | Z)(#)sin + 2(#)((sin`|Z)(#)(sin`|Z))
          +sin(#)((-1)(#) sin | Z) by NEWTON:10
        .=2(#)((sin`|Z)(#)(sin`|Z)) + (sin(#)((-1)(#) sin | Z)
          +sin(#)((-1)(#) sin | Z)) by RFUNCT_1:19
        .=2(#)((sin`|Z)(#)(sin`|Z)) + (1(#)(sin(#)((-1)(#) sin | Z))
          +sin(#)((-1)(#) sin | Z)) by RFUNCT_1:33
        .=2(#)((sin`|Z)(#)(sin`|Z)) + (1(#)(sin(#)((-1)(#) sin | Z))
          +1(#)(sin(#)((-1)(#) sin | Z))) by RFUNCT_1:33
        .=2(#)((sin`|Z)(#)(sin`|Z)) +((1+1)(#)(sin(#)((-1)(#) sin | Z)))
                                                                       by ThB2
        .=2(#)((cos|Z)(#)(sin`|Z))+2(#)(sin(#)((-1)(#) sin | Z)) by TAYLOR_2:17
        .=2(#)((cos|Z)(#)(cos|Z)) +2(#)(sin(#)((-1)(#) sin | Z)) by TAYLOR_2:17
        .=2(#)((cos(#)cos)|Z) +2(#)(((-1)(#) sin | Z)(#)sin) by RFUNCT_1:61
        .=2(#)((cos(#)cos)|Z) +2(#)((-1)(#)(sin | Z(#) sin)) by RFUNCT_1:24
        .=2(#)((cos(#)cos)|Z) +2(#)((-1)(#)((sin(#) sin)|Z)) by RFUNCT_1:61
        .=2(#)((cos(#)cos)|Z) +(2*(-1))(#)((sin(#) sin)|Z) by RFUNCT_1:29
        .=2(#)((cos(#)cos)|Z) +(-2)(#)((sin(#) sin)|Z);
      hence thesis;
end;

theorem
  diff(cos(#)cos,Z).2 =2(#)((sin(#) sin)|Z) +(-2)(#)((cos(#)cos)|Z)
proof
A2:  cos is_differentiable_on 2,Z by TAYLOR_2:21;
     diff(cos(#)cos,Z).2
         =(diff(cos,Z).(2*1))(#)cos + 2(#)((cos`|Z)(#)(cos`|Z))
          +cos(#)(diff(cos,Z).(2*1)) by ThB3,A2
        .=((-1) |^ 1 (#) cos | Z)(#)cos + 2(#)((cos`|Z)(#)(cos`|Z))
          +cos(#)(diff(cos,Z).(2*1))by TAYLOR_2:19
        .=((-1) |^ 1 (#) cos | Z)(#)cos + 2(#)((cos`|Z)(#)(cos`|Z))
          +cos(#)((-1) |^ 1 (#) cos | Z) by TAYLOR_2:19
        .=((-1) |^ 1 (#) cos | Z)(#)cos + 2(#)((cos`|Z)(#)(cos`|Z))
          +cos(#)((-1)(#) cos | Z)by NEWTON:10
        .=((-1)(#) cos | Z)(#)cos + 2(#)((cos`|Z)(#)(cos`|Z))
          +cos(#)((-1)(#) cos | Z) by NEWTON:10
        .=2(#)((cos`|Z)(#)(cos`|Z)) + (cos(#)((-1)(#) cos | Z)
          +cos(#)((-1)(#) cos | Z)) by RFUNCT_1:19
        .=2(#)((cos`|Z)(#)(cos`|Z)) + (1(#)(cos(#)((-1)(#) cos | Z))
          +cos(#)((-1)(#) cos | Z)) by RFUNCT_1:33
        .=2(#)((cos`|Z)(#)(cos`|Z)) + (1(#)(cos(#)((-1)(#) cos | Z))
          +1(#)(cos(#)((-1)(#) cos | Z))) by RFUNCT_1:33
        .=2(#)((cos`|Z)(#)(cos`|Z)) +(1+1)(#)(cos(#)((-1)(#) cos | Z)) by ThB2
        .=2(#)(((-sin)|Z)(#)(cos`|Z))+2(#)(cos(#)((-1)(#) cos | Z))
                                                             by TAYLOR_2:17
        .=2(#)(((-sin)|Z)(#)((-sin)|Z)) + 2(#)(cos(#)((-1)(#) cos | Z))
                                                                by TAYLOR_2:17
        .=2(#)(((-sin)(#)(-sin))|Z) +2(#)(((-1)(#)cos|Z)(#)cos) by RFUNCT_1:61
        .=2(#)(((-sin)(#)(-sin))|Z) +2(#)((-1)(#)(cos|Z(#)cos)) by RFUNCT_1:24
        .=2(#)(((-sin)(#)(-sin))|Z) +(2*(-1))(#)(cos|Z(#)cos) by RFUNCT_1:29
        .=2(#)(((-sin)(#)(-sin))|Z) +(-2)(#)((cos(#)cos)|Z) by RFUNCT_1:61
        .=2(#)((sin(#)sin)|Z) +(-2)(#)((cos(#)cos)|Z) by ThB6;
  hence thesis;
end;

theorem
  diff(sin(#)cos,Z).2 = 4(#)((-sin)(#)cos)|Z
proof
A2:  cos is_differentiable_on 2,Z by TAYLOR_2:21;
A3:  sin is_differentiable_on 2,Z by TAYLOR_2:21;
     diff(sin(#)cos,Z).2
        =(diff(sin,Z).(2*1))(#)cos+2(#)((sin`|Z) (#) (cos`|Z))
                                + sin(#)(diff(cos,Z).(2*1))  by ThB3,A2,A3
       .=((-1) |^ 1(#)sin | Z)(#)cos + 2(#)((sin`|Z)(#)(cos`|Z))
                                + sin(#)(diff(cos,Z).(2*1)) by TAYLOR_2:19
       .=((-1) |^ 1(#)sin | Z)(#)cos + 2(#)((sin`|Z)(#)(cos`|Z))
                                + sin(#)((-1) |^ 1(#)cos | Z) by TAYLOR_2:19
       .=((-1)(#)sin | Z)(#)cos + 2(#)((sin`|Z)(#)(cos`|Z))
                                + sin(#)((-1) |^ 1(#)cos | Z) by NEWTON:10
       .=((-1)(#)sin | Z)(#)cos + 2(#)((sin`|Z)(#)(cos`|Z))
                                + sin(#)((-1)(#)cos | Z) by NEWTON:10
       .=((-1)(#)sin | Z)(#)cos + 2(#)((cos|Z)(#)(cos`|Z))
                                + sin(#)((-1)(#)cos | Z) by TAYLOR_2:17
       .=((-1)(#)sin | Z)(#)cos + 2(#)((cos|Z)(#)((-sin) | Z))
                                + sin(#)((-1)(#)cos | Z) by TAYLOR_2:17
       .=(((-1)(#)sin) | Z)(#)cos + 2(#)((cos|Z)(#)((-sin) | Z))
                                + sin(#)((-1)(#)cos | Z) by RFUNCT_1:65
       .=(((-1)(#)sin) | Z)(#)cos + 2(#)((cos|Z)(#)((-sin) | Z))
                                + sin(#)(((-1)(#)cos) | Z) by RFUNCT_1:65
       .=((-sin)(#)cos)| Z + 2(#)((cos|Z)(#)((-sin) | Z))
                                + sin(#)((-cos) | Z) by RFUNCT_1:61
       .=((-sin)(#)cos)| Z + 2(#)((cos|Z)(#)((-sin) | Z))
                                + (sin(#)(-cos)) | Z by RFUNCT_1:61
       .=((-sin)(#)cos)| Z + 2(#)((-sin)(#)cos)|Z
                                + (sin(#)(-cos)) | Z by RFUNCT_1:61
       .=((-sin)(#)cos)| Z + 2(#)((-sin)(#)cos)|Z
                                + ((-1)(#)(sin(#)cos)) | Z by RFUNCT_1:25
       .=((-sin)(#)cos)| Z + 2(#)((-sin)(#)cos)|Z
                                + (((-1)(#)sin)(#)cos) | Z by RFUNCT_1:24
       .=1(#)((-sin)(#)cos)| Z + 2(#)((-sin)(#)cos)|Z
                                + ((-sin)(#)cos)| Z by RFUNCT_1:33
       .=1(#)((-sin)(#)cos)| Z + 2(#)((-sin)(#)cos)|Z
                                + 1(#)((-sin)(#)cos)| Z by RFUNCT_1:33
      .=(1+2)(#)((-sin)(#)cos)|Z+ 1(#)((-sin)(#)cos)| Z by ThB2
      .=(3+1)(#)((-sin)(#)cos)|Z by ThB2
      .=4(#)((-sin)(#)cos)|Z;
 hence thesis;
end;

theorem ThB10:
  Z c= dom tan implies tan is_differentiable_on Z &
    tan`|Z = ((cos^)(#)(cos^))|Z
proof
   assume
A1: Z c= dom tan;
A2:   for x st x in Z holds tan is_differentiable_in x
    proof
     let x;assume
A3:   x in Z;
A4:   sin is_differentiable_in x by SIN_COS:69;
A5:   cos is_differentiable_in x by SIN_COS:68;
     cos.x <> 0 by FDIFF_8:1,A1,A3;
     hence thesis by SIN_COS:def 30,A4,A5,FDIFF_2:14;
    end;then
A7:   tan is_differentiable_on Z by A1,FDIFF_1:16;then
B1:   dom (tan`|Z)=Z by FDIFF_1:def 8;
      set f1 = cos^;
AA:   dom(tan)=dom(sin(#)f1) by RFUNCT_1:47,SIN_COS:def 30
         .=dom sin /\ dom f1 by VALUED_1:def 4;
c1:   dom sin /\ dom f1 c=dom f1 by XBOOLE_1:17;then
C1:   Z c=dom f1 by A1,XBOOLE_1:1,AA;
C2:   dom((cos^)(#)(cos^)) = dom (cos^) /\ dom (cos^) by VALUED_1:def 4
       .= dom (cos^);
C3:   dom(((cos^)(#)(cos^))|Z) = dom (cos^) /\ Z by C2,RELAT_1:90
        .=Z by c1,XBOOLE_1:28,A1,XBOOLE_1:1,AA;
    for x st x in dom (tan`|Z) holds ((tan)`|Z).x = (((cos^)(#)(cos^))|Z).x
    proof
      let x;
      assume
B4:   x in dom (tan`|Z);
A8:   x in Z by B4,FDIFF_1:def 8,A7;
A12:  cos.x <> 0 by FDIFF_8:1, A1,A8;
      ((tan)`|Z).x
        =diff(sin/cos, x) by SIN_COS:def 30,FDIFF_1:def 8,A7,A8
        .=1/(cos.x)^2 by FDIFF_7:46,A12
        .=1/(cos.x*cos.x) by SQUARE_1:def 3
        .=(1/cos.x)*(1/cos.x) by XCMPLX_1:103
        .=1*(cos.x)"*(1/cos.x) by XCMPLX_0:def 9
        .=cos^.x*(1/cos.x) by RFUNCT_1:def 8,A8,C1
        .=cos^.x*(1*(cos.x)") by XCMPLX_0:def 9
        .=cos^.x * f1.x by RFUNCT_1:def 8,A8,C1
        .=(cos^(#)f1).x by A8,C1,C2,VALUED_1:def 4
        .=((f1(#)f1)|Z).x by A8,FUNCT_1:72;
     hence thesis;
    end;
 hence thesis by PARTFUN1:34,B1,C3,A1,FDIFF_1:16,A2;
end;

theorem ThB11:
  Z c= dom tan implies cos^ is_differentiable_on Z &
    (cos^)`|Z = ((cos^)(#)tan)|Z
proof
  assume
A1:  Z c= dom tan;
A13:  for x st x in Z holds cos.x<>0 by FDIFF_8:1,A1;then
A15:  cos^ is_differentiable_on Z by FDIFF_4:39;
C5:   dom((cos^)`|Z)= Z by FDIFF_1:def 8,A15;
 AA:    dom(tan) = dom(sin(#)(cos^)) by RFUNCT_1:47,SIN_COS:def 30
        .=dom sin /\ dom(cos^) by VALUED_1:def 4;
      dom sin /\ dom (cos^) c=dom (cos^) by XBOOLE_1:17;then
B4:   Z c=dom (cos^) by A1,XBOOLE_1:1,AA;
C7:   dom(((cos^)(#)tan)|Z) = dom((cos^)(#)tan)/\Z by RELAT_1:90
       .=(dom(cos^)/\dom tan)/\Z by VALUED_1:def 4
       .=Z by XBOOLE_1:28,B4,XBOOLE_1:19,A1;
    for x st x in Z holds ((cos^)`|Z).x=(((cos^)(#)tan)|Z).x
   proof
     let x;
       assume
A18:   x in Z;
D1:    dom((cos^)(#)sin) = dom tan by SIN_COS:def 30,RFUNCT_1:47;then
      dom(((cos^)(#)sin)(#)(cos^))
        =dom(tan)/\dom(cos^) by VALUED_1:def 4;then
 A23:      Z c= dom(((cos^)(#)sin)(#)(cos^)) by XBOOLE_1:19,B4,A1;
       ((cos^)`|Z).x =sin.x/(cos.x)^2 by A18,A13,FDIFF_4:39
        .=sin.x/((cos.x)*(cos.x)) by SQUARE_1:def 3
        .=1/(cos.x)*(sin.x/(cos.x)) by XCMPLX_1:104
        .=1/cos.x*sin.x*(1/cos.x) by XCMPLX_1:100
        .=1/cos.x*sin.x*(1*(cos.x)") by XCMPLX_0:def 9
        .=(1*(cos.x)")*sin.x*(1*(cos.x)") by XCMPLX_0:def 9
        .=(cos^).x*sin.x*(1*(cos.x)") by RFUNCT_1:def 8,A18,B4
        .=(cos^).x*sin.x*(cos^.x) by RFUNCT_1:def 8,A18,B4
        .=((cos^) (#)sin).x*(cos^.x) by VALUED_1:def 4,A18,A1,D1
        .=(((cos^)(#)sin)(#)(cos^)).x by VALUED_1:def 4,A18,A23
        .=((((cos^)(#)sin)(#)(cos^))|Z).x by A18,FUNCT_1:72
        .=(((cos^)(#)tan)|Z).x by SIN_COS:def 30,RFUNCT_1:47;
      hence thesis;
     end;
   hence thesis by PARTFUN1:34,C7,C5,FDIFF_4:39,A13;
  end;

theorem
  Z c= dom tan implies diff(tan,Z).2=2(#)((tan(#)(cos^)(#)(cos^))|Z)
proof
  assume
A1:  Z c= dom tan;
A7:   tan is_differentiable_on Z by A1,ThB10;
A15:  cos^ is_differentiable_on Z by ThB11,A1;then
A16:  ((cos^)(#)(cos^)) is_differentiable_on Z by FDIFF_2:20;
     diff(tan,Z).2 = diff(tan,Z).(1+1)
      .=diff(tan,Z).(1+0)`|Z by TAYLOR_1:def 5
      .=(diff(tan,Z).0`|Z)`|Z by TAYLOR_1:def 5
      .=tan|Z`|Z`|Z by TAYLOR_1:def 5
      .=tan`|Z`|Z by FDIFF_2:16,A7
      .=(((cos^)(#)(cos^))|Z)`|Z by ThB10,A1
      .=((cos^)(#)(cos^))`|Z by A16,FDIFF_2:16
      .=(((cos^)`|Z)(#)(cos^)) + ((cos^)`|Z)(#)(cos^)  by FDIFF_2:20,A15
      .=1(#)(((cos^)`|Z)(#)(cos^))+ ((cos^)`|Z)(#)(cos^) by RFUNCT_1:33
      .=1(#)(((cos^)`|Z)(#)(cos^)) + 1(#)(((cos^)`|Z)(#)(cos^)) by RFUNCT_1:33
      .=(1+1)(#)(((cos^)`|Z)(#)(cos^)) by ThB2
      .=2(#)((((cos^)(#)tan)|Z)(#)(cos^)) by ThB11,A1
      .=2(#)((tan(#)(cos^)(#)(cos^))|Z) by RFUNCT_1:61;
  hence thesis;
end;

theorem ThB14:
  Z c= dom cot implies cot is_differentiable_on Z &
    cot`|Z = ((-1)(#)((sin^)(#)(sin^)))|Z
proof
  assume
A1:   Z c= dom cot;
 A2:    for x st x in Z holds cot is_differentiable_in x
     proof
       let x;
       assume
A3:    x in Z;
A4:    sin is_differentiable_in x by SIN_COS:69;
A5:    cos is_differentiable_in x by SIN_COS:68;
       sin.x <> 0 by A1,FDIFF_8:2,A3;
      hence thesis by A4,A5,FDIFF_2:14,SIN_COS:def 31;
     end;then
A6:    cot is_differentiable_on Z by A1,FDIFF_1:16;then
A7:    dom (cot`|Z) = Z by FDIFF_1:def 8;
AA:    dom(cot) = dom(cos(#)(sin^)) by RFUNCT_1:47, SIN_COS:def 31
         .=dom(cos)/\dom(sin^) by VALUED_1:def 4;
AA1:      dom(cos)/\dom(sin^)c=dom(sin^) by XBOOLE_1:17;then
A9:      Z c=dom(sin^) by XBOOLE_1:1,A1,AA;
A10:      dom(((-1)(#)((sin^)(#)(sin^)))|Z)
          =dom((-1)(#)((sin^)(#)(sin^))) /\ Z by RELAT_1:90
         .= dom((sin^)(#)(sin^)) /\ Z by VALUED_1:def 5
         .=dom(sin^)/\ dom(sin^)/\Z by VALUED_1:def 4
         .=Z by AA1,XBOOLE_1:28,XBOOLE_1:1,A1,AA;
     for x st x in dom (cot`|Z) holds ((cot)`|Z).x
       =(((-1)(#)((sin^)(#)(sin^)))|Z).x
    proof
       let x;
       assume
A11:   x in dom (cot`|Z);
A:     x in Z by FDIFF_1:def 8,A11,A6;then
A12:   sin.x<>0 by FDIFF_8:2,A1;
      dom((sin^)(#)(sin^)) = (dom(sin^)/\dom(sin^)) by VALUED_1:def 4
        .=dom(sin^);then
 AA2:    Z c= dom((sin^)(#)(sin^)) by XBOOLE_1:1,A1,AA,AA1;then
A14:  x in dom((sin^)(#)(sin^)) by A;
A15:  x in dom((-1)(#)((sin^)(#)(sin^))) by A14,VALUED_1:def 5;
      ((cot)`|Z).x
       =diff(cos/sin, x) by SIN_COS:def 31,A,FDIFF_1:def 8,A6
       .=-1/(sin.x)^2 by FDIFF_7:47,A12
       .=-1/(sin.x*sin.x) by SQUARE_1:def 3
       .=(-1)*(1/(sin.x*sin.x))
       .=(-1)*((1/sin.x)*(1/sin.x)) by XCMPLX_1:103
       .=(-1)*((1*(sin.x)")*(1/sin.x)) by XCMPLX_0:def 9
       .=(-1)*((sin^.x)*(1/sin.x)) by RFUNCT_1:def 8,A,A9
       .=(-1)*((sin^.x)*(1*(sin.x)")) by XCMPLX_0:def 9
       .=(-1)*((sin^.x)*(sin^.x)) by RFUNCT_1:def 8,A,A9
       .=(-1)*(((sin^)(#)(sin^)).x)  by VALUED_1:def 4,AA2,A
       .=((-1)(#)((sin^)(#)(sin^))).x by VALUED_1:def 5,A15
       .=(((-1)(#)((sin^)(#)(sin^)))|Z).x by A,FUNCT_1:72;
     hence thesis;
   end;
 hence thesis by A7,A10,PARTFUN1:34,A1,FDIFF_1:16,A2;
end;

theorem ThB15:
  Z c= dom cot implies sin^ is_differentiable_on Z &
    (sin^)`|Z = (-(sin^)(#)cot)|Z
proof
  assume
A1:  Z c= dom cot;
A2:  for x st x in Z holds sin.x<>0 by FDIFF_8:2,A1;then
A4:  sin^ is_differentiable_on Z by FDIFF_4:40;then
A5:  dom((sin^)`|Z)=Z by FDIFF_1:def 8;
A7:   dom(cot) = dom(cos(#)(sin^)) by RFUNCT_1:47,SIN_COS:def 31
       .=dom(cos)/\dom(sin^) by VALUED_1:def 4;
       dom(cos)/\dom(sin^) c= dom(sin^) by XBOOLE_1:17;then
A9:    Z c=dom(sin^) by XBOOLE_1:1,A7,A1;
A11:  dom((-(sin^)(#)cot)|Z)=dom((-1)(#)((sin^)(#)cot))/\Z by RELAT_1:90
        .=dom((sin^)(#)cot)/\Z by VALUED_1:def 5
        .=dom(sin^)/\dom cot/\Z by VALUED_1:def 4
        .=Z by XBOOLE_1:28,A9,XBOOLE_1:19,A1;
    for x st x in dom((sin^)`|Z) holds ((sin^)`|Z).x=((-(sin^)(#)cot)|Z).x
   proof
      let x;
      assume
B1:     x in dom((sin^)`|Z);
A12:    x in Z by B1,A4,FDIFF_1:def 8;
A14:    Z c= dom(cos(#)(sin^)) by A1,A7, VALUED_1:def 4;
        dom ((sin^)(#)(cos(#)(sin^)))
           =dom (sin^)/\dom(cos(#)(sin^)) by VALUED_1:def 4;then
A16:        Z c=dom ((sin^)(#)(cos(#)(sin^))) by A14,A9,XBOOLE_1:19;
AAA:       dom((-1)(#)((sin^)(#)cot))
          =dom((sin^)(#)(cos/sin)) by SIN_COS:def 31, VALUED_1:def 5
          .=dom((sin^)(#)(cos(#)(sin^))) by RFUNCT_1:47;
         ((sin^)`|Z).x = -cos.x/(sin.x)^2 by FDIFF_4:40,A2,A12
         .= -(1*cos.x)/(sin.x*sin.x) by SQUARE_1:def 3
         .= -(1/sin.x)*(cos.x/sin.x) by XCMPLX_1:77
         .= -(1/sin.x)*(cos.x*(1/sin.x)) by XCMPLX_1:100
         .= -(1*(sin.x)")*(cos.x*(1/sin.x)) by XCMPLX_0:def 9
         .= -(sin.x)"*(cos.x*(1*(sin.x)")) by XCMPLX_0:def 9
         .= -(sin^.x)*(cos.x*(sin.x)") by RFUNCT_1:def 8,A9,A12
         .= -(sin^.x)*(cos.x*(sin^.x)) by RFUNCT_1:def 8,A9,A12
         .= -(sin^.x)*(cos(#)(sin^)).x by VALUED_1:def 4,A12,A14
         .= -((sin^)(#)(cos(#)(sin^))).x by VALUED_1:def 4,A16,A12
         .= -((sin^)(#)cot).x by SIN_COS:def 31,RFUNCT_1:47
         .=(-1)*((sin^)(#)cot).x
         .=((-1)(#)((sin^)(#)cot)).x by VALUED_1:def 5,A16,A12,AAA
         .= ((-(sin^)(#)cot)|Z).x by A12,FUNCT_1:72;
    hence thesis;
   end;
  hence thesis by PARTFUN1:34,A2,FDIFF_4:40,A5,A11;
end;

theorem
  Z c= dom cot implies diff(cot,Z).2=2(#)(cot(#)(sin^)(#)(sin^))|Z
proof
  assume
A1:  Z c= dom cot;
A2:  cot is_differentiable_on Z by A1,ThB14;
A3:  sin^ is_differentiable_on Z by ThB15,A1;then
A:   ((sin^)(#)(sin^)) is_differentiable_on Z by FDIFF_2:20;then
A4:  ((-1)(#)((sin^)(#)(sin^))) is_differentiable_on Z by FDIFF_2:19;
     diff(cot,Z).2 =diff(cot,Z).(1+1)
      .=diff(cot,Z).(1+0)`|Z by TAYLOR_1:def 5
      .=(diff(cot,Z).0`|Z)`|Z by TAYLOR_1:def 5
      .=cot|Z`|Z`|Z by TAYLOR_1:def 5
      .=cot`|Z`|Z by FDIFF_2:16,A2
      .=(((-1)(#)((sin^)(#)(sin^)))|Z)`|Z by ThB14,A1
      .=((-1)(#)((sin^)(#)(sin^)))`|Z by FDIFF_2:16,A4
      .=(-1)(#)(((sin^)(#)(sin^))`|Z) by FDIFF_2:19,A
      .=(-1)(#)(((sin^)`|Z)(#)(sin^) + ((sin^)`|Z)(#)(sin^)) by FDIFF_2:20,A3
      .=(-1)(#)(1(#)(((sin^)`|Z)(#)(sin^)) + ((sin^)`|Z)(#)(sin^))
                                                              by RFUNCT_1:33
      .=(-1)(#)(1(#)(((sin^)`|Z)(#)(sin^)) +1(#)(((sin^)`|Z)(#)(sin^)))
                                                              by RFUNCT_1:33
      .=(-1)(#)((1+1)(#)(((sin^)`|Z)(#)(sin^))) by ThB2
      .=(-1)(#)(2(#)(((-(sin^)(#)cot)|Z)(#)(sin^))) by ThB15,A1
      .=((-1)*2)(#)(((-(sin^)(#)cot)|Z)(#)(sin^)) by RFUNCT_1:29
      .=((-1)*2)(#)((((-(sin^)(#)cot))(#)(sin^)))|Z by RFUNCT_1:61
      .=(((-1)*2)(#)((((-(sin^)(#)cot))(#)(sin^))))|Z by RFUNCT_1:65
      .=((-2)(#)(-(sin^)(#)cot)(#)(sin^))|Z by RFUNCT_1:24
      .=((((-2)*(-1))(#)((sin^)(#)cot))(#)(sin^))|Z by RFUNCT_1:29
      .=(2(#)(((sin^)(#)cot)(#)(sin^)))|Z by RFUNCT_1:24
      .=2(#)(cot(#)(sin^)(#)(sin^))|Z by RFUNCT_1:65;
     hence thesis;
end;

theorem
  diff(exp_R(#)sin,Z).2 = 2(#)((exp_R(#)cos)|Z)
proof
A2: sin is_differentiable_on 2,Z by TAYLOR_2:21;
A3:  exp_R is_differentiable_on 2,Z by TAYLOR_2:10;
A4:  dom(0(#)((exp_R(#)sin)|Z))
       = dom ((exp_R(#)sin)|Z) by VALUED_1:def 5
      .=dom(exp_R(#)sin)/\Z by RELAT_1:90
      .=REAL/\REAL/\Z by SIN_COS:27,SIN_COS:51,VALUED_1:def 4
      .=Z by XBOOLE_1:28;
A5:   dom(2(#)((exp_R(#)cos)|Z)) =dom((exp_R(#)cos)|Z) by VALUED_1:def 5
       .=dom(exp_R(#)cos)/\Z by RELAT_1:90
       .=REAL/\REAL/\Z by SIN_COS:27,SIN_COS:51,VALUED_1:def 4
       .=Z by XBOOLE_1:28;
A6:    dom(0(#)((exp_R(#)sin)|Z)+ 2(#)((exp_R(#)cos)|Z))
        =Z/\Z by A5,A4,VALUED_1:def 1
        .=Z;
A7:     exp_R is_differentiable_on Z by FDIFF_1:34,TAYLOR_1:16;
A8:     sin is_differentiable_on Z  by FDIFF_1:34,SIN_COS:73;then
A9:     exp_R(#)sin is_differentiable_on Z by FDIFF_2:20,A7;
       exp_R|Z is_differentiable_on Z by FDIFF_2:16,A7;then
A11:   exp_R|Z(#)sin is_differentiable_on Z by FDIFF_2:20,A8;
        cos is_differentiable_on Z by FDIFF_1:34,SIN_COS:72;then
        cos|Z is_differentiable_on Z by FDIFF_2:16;then
      exp_R(#)(cos|Z) is_differentiable_on Z by FDIFF_2:20,A7;then
A16: exp_R|Z(#)sin+exp_R(#)(cos|Z) is_differentiable_on Z by A11,FDIFF_2:17;
A17:  dom (diff(exp_R(#)sin,Z).2)
        = dom (diff(exp_R(#)sin,Z).(1+1))
       .=dom ((diff(exp_R(#)sin,Z).(1+0))`|Z) by TAYLOR_1:def 5
       .=dom (((diff(exp_R(#)sin,Z).0)`|Z)`|Z) by TAYLOR_1:def 5
       .=dom ((((exp_R(#)sin)|Z)`|Z)`|Z) by TAYLOR_1:def 5
       .=dom (((exp_R(#)sin)`|Z)`|Z) by A9,FDIFF_2:16
       .=dom (((exp_R`|Z)(#)sin+exp_R(#)(sin`|Z))`|Z) by FDIFF_2:20,A7,A8
       .=dom (((exp_R|Z)(#)sin+exp_R(#)(sin`|Z))`|Z) by TAYLOR_2:5
       .=dom (((exp_R|Z)(#)sin+exp_R(#)(cos|Z))`|Z) by TAYLOR_2:17
       .=Z by FDIFF_1:def 8,A16;
      for x st x in dom(diff(exp_R(#)sin,Z).2) holds
          (diff(exp_R(#)sin,Z).2).x = (2(#)((exp_R(#)cos)|Z)).x
   proof
     let x;
     assume
B1:  x in dom(diff(exp_R(#)sin,Z).2);
      (diff(exp_R(#)sin,Z).2).x
        =((diff(exp_R,Z).2)(#)sin + 2(#)((exp_R`|Z)(#)(sin`|Z))
                                + exp_R(#)(diff(sin,Z).2)).x by ThB3,A2,A3
       .=(exp_R|Z(#)sin+2(#)((exp_R`|Z)(#)(sin`|Z))+exp_R(#)(diff(sin,Z).2)).x
                                                                by TAYLOR_2:6
       .=(exp_R|Z(#)sin+2(#)((exp_R|Z)(#)(sin`|Z))+exp_R(#)(diff(sin,Z).2)).x
                                                                by TAYLOR_2:5
       .=(exp_R|Z(#)sin+2(#)((exp_R|Z)(#)(cos|Z))
                         +exp_R(#)(diff(sin,Z).(2*1))).x  by TAYLOR_2:17
       .=(exp_R|Z(#)sin+2(#)((exp_R|Z)(#)(cos|Z))+exp_R(#)((-1)|^1(#)sin|Z)).x
                                                               by TAYLOR_2:19
       .=(exp_R|Z(#)sin+2(#)((exp_R|Z)(#)(cos|Z))+exp_R(#)((-1)(#)sin|Z)).x
                                                               by NEWTON:10
       .=((exp_R(#)sin)|Z+2(#)((exp_R|Z)(#)(cos|Z))+exp_R(#)((-1)(#)sin|Z)).x
                                                               by RFUNCT_1:61
       .=((exp_R(#)sin)|Z+ 2(#)((exp_R(#)cos)|Z)+exp_R(#)((-1)(#)sin|Z)).x
                                                               by RFUNCT_1:61
       .=(((exp_R(#)sin)|Z+(exp_R(#)((-1)(#)sin|Z))+2(#)((exp_R(#)cos)|Z))).x
                                                by RFUNCT_1:19
       .=(((exp_R(#)sin)|Z+((-1)(#)(exp_R(#)sin|Z))+2(#)((exp_R(#)cos)|Z))).x
                                                                by RFUNCT_1:25
       .=((exp_R(#)sin)|Z+((-1)(#)((exp_R(#)sin)|Z))+2(#)((exp_R(#)cos)|Z)).x
                                                                by RFUNCT_1:61
       .=(1(#)((exp_R(#)sin)|Z)+(-1)(#)((exp_R(#)sin)|Z)
                                       +2(#)((exp_R(#)cos)|Z)).x by RFUNCT_1:33
       .=((1+(-1))(#)((exp_R(#)sin)|Z)+ 2(#)((exp_R(#)cos)|Z)).x by ThB2
       .=(0(#)((exp_R(#)sin)|Z)).x+ (2(#)((exp_R(#)cos)|Z)).x
                                                by VALUED_1:def 1,A6,A17,B1
       .=0*((exp_R(#)sin)|Z).x+ (2(#)((exp_R(#)cos)|Z)).x
                                                by VALUED_1:def 5,A4,A17,B1
       .=(2(#)((exp_R(#)cos)|Z)).x;
    hence thesis;
   end;
  hence thesis by PARTFUN1:34,A5,A17;
end;

theorem
  diff(exp_R(#)cos,Z).2 = 2(#)((exp_R(#)-sin)|Z)
proof
A2: cos is_differentiable_on 2,Z by TAYLOR_2:21;
A3:  exp_R is_differentiable_on 2,Z by TAYLOR_2:10;
A4:  dom(0(#)((exp_R(#)cos)|Z))
       = dom ((exp_R(#)cos)|Z) by VALUED_1:def 5
      .=dom(exp_R(#)cos)/\Z by RELAT_1:90
      .=REAL/\REAL/\Z by SIN_COS:27,SIN_COS:51,VALUED_1:def 4
      .=Z by XBOOLE_1:28;
A5: dom(2(#)((exp_R(#)-sin)|Z))
      =dom((exp_R(#)-sin)|Z) by VALUED_1:def 5
     .=dom(exp_R(#)-sin)/\Z by RELAT_1:90
     .=dom(exp_R)/\dom(-sin)/\Z by VALUED_1:def 4
     .=REAL/\REAL/\Z by SIN_COS:27,SIN_COS:51,VALUED_1:def 5
     .=Z by XBOOLE_1:28;
A6:  dom(0(#)((exp_R(#)cos)|Z)+ 2(#)((exp_R(#)-sin)|Z))
      =Z/\Z by A5,A4,VALUED_1:def 1
      .=Z;
 A7:     exp_R is_differentiable_on Z by FDIFF_1:34,TAYLOR_1:16;
 A8:     cos is_differentiable_on Z  by FDIFF_1:34,SIN_COS:72;then
A9:     exp_R(#)cos is_differentiable_on Z by FDIFF_2:20,A7;
      exp_R|Z is_differentiable_on Z by FDIFF_2:16,A7;then
A11:   exp_R|Z(#)cos is_differentiable_on Z by FDIFF_2:20,A8;
        sin is_differentiable_on Z by FDIFF_1:34,SIN_COS:73;then
        sin|Z is_differentiable_on Z by FDIFF_2:16;then
      (-1)(#)(sin|Z) is_differentiable_on Z by FDIFF_2:19;then
      exp_R(#)((-1)(#)(sin|Z)) is_differentiable_on Z by FDIFF_2:20,A7;then
A16: exp_R|Z(#)cos+exp_R(#)((-1)(#)(sin|Z)) is_differentiable_on Z
                                                     by A11,FDIFF_2:17;
A17:  dom (diff(exp_R(#)cos,Z).2) = dom (diff(exp_R(#)cos,Z).(1+1))
       .=dom ((diff(exp_R(#)cos,Z).(1+0))`|Z) by TAYLOR_1:def 5
       .=dom (((diff(exp_R(#)cos,Z).0)`|Z)`|Z) by TAYLOR_1:def 5
       .=dom ((((exp_R(#)cos)|Z)`|Z)`|Z) by TAYLOR_1:def 5
       .=dom (((exp_R(#)cos)`|Z)`|Z) by A9,FDIFF_2:16
       .=dom (((exp_R`|Z)(#)cos+exp_R(#)(cos`|Z))`|Z) by FDIFF_2:20,A7,A8
       .=dom (((exp_R|Z)(#)cos+exp_R(#)(cos`|Z))`|Z) by TAYLOR_2:5
       .=dom (((exp_R|Z)(#)cos+exp_R(#)((-sin)|Z))`|Z) by TAYLOR_2:17
       .=dom (((exp_R|Z)(#)cos+exp_R(#)((-1)(#)(sin|Z)))`|Z) by RFUNCT_1:65
       .=Z by FDIFF_1:def 8,A16;
      for x st x in dom ( diff(exp_R(#)cos,Z).2) holds
      (diff(exp_R(#)cos,Z).2).x = (2(#)((exp_R(#)-sin)|Z)).x
  proof
    let x;
    assume
  B1: x in dom ( diff(exp_R(#)cos,Z).2);
      (diff(exp_R(#)cos,Z).2).x
        =((diff(exp_R,Z).2)(#)cos + 2(#)((exp_R`|Z)(#)(cos`|Z))
                                + exp_R(#)(diff(cos,Z).2)).x by ThB3,A2,A3
       .=(exp_R|Z(#)cos+2(#)((exp_R`|Z)(#)(cos`|Z))+exp_R(#)(diff(cos,Z).2)).x
                                                                by TAYLOR_2:6
       .=(exp_R|Z(#)cos+2(#)((exp_R|Z)(#)(cos`|Z))+exp_R(#)(diff(cos,Z).2)).x
                                                                by TAYLOR_2:5
  .=(exp_R|Z(#)cos+2(#)((exp_R|Z)(#)((-sin)|Z))+exp_R(#)(diff(cos,Z).(2*1))).x
                                                               by TAYLOR_2:17
    .=(exp_R|Z(#)cos+2(#)((exp_R|Z)(#)(-sin|Z))+exp_R(#)(diff(cos,Z).(2*1))).x
                                                              by RFUNCT_1:62
       .=(exp_R|Z(#)cos+2(#)((exp_R|Z)(#)(-sin|Z))+exp_R(#)((-1)|^1(#)cos|Z)).x
                                                               by TAYLOR_2:19
       .=(exp_R|Z(#)cos+2(#)((exp_R|Z)(#)(-sin|Z))+exp_R(#)((-1)(#)cos|Z)).x
                                                               by NEWTON:10
       .=((exp_R(#)cos)|Z+2(#)((exp_R|Z)(#)(-sin|Z))+exp_R(#)((-1)(#)cos|Z)).x
                                                               by RFUNCT_1:61
       .=((exp_R(#)cos)|Z+2(#)((exp_R|Z)(#)(-sin)|Z)+exp_R(#)((-1)(#)cos|Z)).x
                                                               by RFUNCT_1:62
       .=((exp_R(#)cos)|Z+ 2(#)((exp_R(#)(-sin))|Z)+exp_R(#)((-1)(#)cos|Z)).x
                                                               by RFUNCT_1:61
       .=(((exp_R(#)cos)|Z+(exp_R(#)((-1)(#)cos|Z))+2(#)((exp_R(#)-sin)|Z))).x
                                          by RFUNCT_1:19
       .=(((exp_R(#)cos)|Z+((-1)(#)(exp_R(#)cos|Z))+2(#)((exp_R(#)-sin)|Z))).x
                                                                by RFUNCT_1:25
       .=((exp_R(#)cos)|Z+((-1)(#)((exp_R(#)cos)|Z))+2(#)((exp_R(#)-sin)|Z)).x
                                                                by RFUNCT_1:61
    .=(1(#)((exp_R(#)cos)|Z)+(-1)(#)((exp_R(#)cos)|Z)+2(#)((exp_R(#)-sin)|Z)).x
                                                            by RFUNCT_1:33
       .=((1+(-1))(#)((exp_R(#)cos)|Z)+ 2(#)((exp_R(#)-sin)|Z)).x by ThB2
       .=(0(#)((exp_R(#)cos)|Z)).x+(2(#)((exp_R(#)-sin)|Z)).x
                                                by VALUED_1:def 1,A6,B1,A17
       .=0*((exp_R(#)cos)|Z).x+(2(#)((exp_R(#)-sin)|Z)).x
                                                by VALUED_1:def 5,A4,B1,A17
       .=(2(#)((exp_R(#)-sin)|Z)).x;
      hence thesis;
     end;
    hence thesis by PARTFUN1:34,A17,A5;
end;

Lm1:
 f is_differentiable_on Z implies (f`|Z)`|Z=diff(f,Z).2
proof
  assume
A1:  f is_differentiable_on Z;
   (f`|Z)`|Z =(f|Z`|Z)`|Z by A1,FDIFF_2:16
    .=(diff(f,Z).0`|Z)`|Z by TAYLOR_1:def 5
    .=(diff(f,Z).(0+1))`|Z by TAYLOR_1:def 5
    .=diff(f,Z).(1+1) by TAYLOR_1:def 5;
 hence thesis;
end;

theorem Th21:
  f1 is_differentiable_on 3,Z &
  f2 is_differentiable_on 3,Z implies diff(f1(#)f2,Z).3
   =(diff(f1,Z).3)(#)f2 + (3(#)(diff(f1,Z).2(#)(f2`|Z))
      +3(#)((f1`|Z)(#)diff(f2,Z).2))+ f1(#)(diff(f2,Z).3)
proof
    assume that
A1:   f1 is_differentiable_on 3,Z and
A2:   f2 is_differentiable_on 3,Z;
A3:   f1 is_differentiable_on 2,Z by A1,TAYLOR_1:23;
A4:   f1 is_differentiable_on Z by A1,ThB19;
A5:   f2 is_differentiable_on 2,Z by A2,TAYLOR_1:23;
A6:   f2 is_differentiable_on Z by ThB19,A2;
A7:   2 <=3-1;then
A8:   diff(f1,Z).2 is_differentiable_on Z by TAYLOR_1:def 6,A1;then
A9:   (diff(f1,Z).2)(#)f2 is_differentiable_on Z by FDIFF_2:20,A6;
A10:  diff(f2,Z).2 is_differentiable_on Z by TAYLOR_1:def 6,A2,A7;then
A11:  f1(#)(diff(f2,Z).2) is_differentiable_on Z by FDIFF_2:20,A4;
A12:  1<= 3-1;
      diff(f1,Z).1 =diff(f1,Z).(1+0)
        .= diff(f1,Z).0`|Z by TAYLOR_1:def 5
        .=f1|Z`|Z by TAYLOR_1:def 5
        .=f1`|Z by FDIFF_2:16,A4;then
A14:  f1`|Z is_differentiable_on Z by TAYLOR_1:def 6,A1,A12;
      diff(f2,Z).1 =diff(f2,Z).(1+0)
        .= diff(f2,Z).0`|Z by TAYLOR_1:def 5
        .=f2|Z`|Z by TAYLOR_1:def 5
        .=f2`|Z by FDIFF_2:16,A6;then
A16:  f2`|Z is_differentiable_on Z by TAYLOR_1:def 6,A2,A12;then
A17:  (f1`|Z)(#)(f2`|Z) is_differentiable_on Z by FDIFF_2:20,A14;then
A18:  2(#)((f1`|Z)(#)(f2`|Z)) is_differentiable_on Z by FDIFF_2:19;then
A19:  (diff(f1,Z).2)(#)f2 + 2(#)((f1`|Z)(#)(f2`|Z))
                              is_differentiable_on Z by FDIFF_2:17,A9;
     set g1 =diff(f1,Z).2;
     set g2=diff(f2,Z).2;
    diff(f1(#)f2,Z).3 =diff(f1(#)f2,Z).(2+1)
      .=(diff(f1(#)f2,Z).2)`|Z by TAYLOR_1:def 5
      .=((diff(f1,Z).2)(#)f2 + 2(#)((f1`|Z)(#)(f2`|Z))+ f1(#)(diff(f2,Z).2))`|Z
                                                           by ThB3,A3,A5
    .=((diff(f1,Z).2)(#)f2+2(#)((f1`|Z)(#)(f2`|Z)))`|Z+(f1(#)(diff(f2,Z).2))`|Z
                                                         by FDIFF_2:17,A19,A11
      .=((diff(f1,Z).2)(#)f2)`|Z+(2(#)((f1`|Z)(#)(f2`|Z)))`|Z
                                 +(f1(#)(diff(f2,Z).2))`|Z by FDIFF_2:17,A9,A18
      .=((diff(f1,Z).2)(#)f2)`|Z+2(#)((((f1`|Z)(#)(f2`|Z)))`|Z)
                                 +(f1(#)(diff(f2,Z).2))`|Z by FDIFF_2:19,A17
      .=((diff(f1,Z).2)`|Z)(#)f2 + (diff(f1,Z).2)(#)(f2`|Z)
                     +2(#)((((f1`|Z)(#)(f2`|Z)))`|Z)+(f1(#)(diff(f2,Z).2))`|Z
                                                           by FDIFF_2:20,A8,A6
      .=((diff(f1,Z).2)`|Z)(#)f2 + (diff(f1,Z).2)(#)(f2`|Z)
                   +2(#)((((f1`|Z)(#)(f2`|Z)))`|Z)+((f1`|Z)(#)(diff(f2,Z).2)
                               + f1(#)((diff(f2,Z).2)`|Z)) by FDIFF_2:20,A4,A10
      .=(diff(f1,Z).(2+1))(#)f2 + (diff(f1,Z).2)(#)(f2`|Z)
                   +2(#)((((f1`|Z)(#)(f2`|Z)))`|Z)+((f1`|Z)(#)(diff(f2,Z).2)
                               + f1(#)((diff(f2,Z).2)`|Z)) by TAYLOR_1:def 5
     .=(diff(f1,Z).3)(#)f2 + (diff(f1,Z).2)(#)(f2`|Z)
                   +2(#)((((f1`|Z)(#)(f2`|Z)))`|Z)+((f1`|Z)(#)(diff(f2,Z).2)
                              + f1(#)(diff(f2,Z).(2+1))) by TAYLOR_1:def 5
     .=(diff(f1,Z).3)(#)f2 + (diff(f1,Z).2)(#)(f2`|Z)
        +2(#)(((f1`|Z)`|Z)(#)(f2`|Z) + (f1`|Z)(#)((f2`|Z)`|Z))
        +((f1`|Z)(#)(diff(f2,Z).2)+ f1(#)(diff(f2,Z).3))
          by FDIFF_2:20,A14,A16
     .=(diff(f1,Z).3)(#)f2 + (diff(f1,Z).2)(#)(f2`|Z)
        +2(#)(diff(f1,Z).2(#)(f2`|Z) + (f1`|Z)(#)((f2`|Z)`|Z))
        +((f1`|Z)(#)(diff(f2,Z).2)+ f1(#)(diff(f2,Z).3)) by Lm1,A1,ThB19
     .=(diff(f1,Z).3)(#)f2 + (diff(f1,Z).2)(#)(f2`|Z)
        +2(#)(diff(f1,Z).2(#)(f2`|Z) + (f1`|Z)(#)diff(f2,Z).2)
        +((f1`|Z)(#)(diff(f2,Z).2)+ f1(#)(diff(f2,Z).3)) by Lm1,ThB19,A2
     .=(diff(f1,Z).3)(#)f2 + 1(#)(diff(f1,Z).2)(#)(f2`|Z)
        +2(#)(diff(f1,Z).2(#)(f2`|Z) + (f1`|Z)(#)diff(f2,Z).2)
        +((f1`|Z)(#)(diff(f2,Z).2)+ f1(#)(diff(f2,Z).3)) by RFUNCT_1:33
    .=(diff(f1,Z).3)(#)f2 + 1(#)(diff(f1,Z).2)(#)(f2`|Z)
        +(2(#)(diff(f1,Z).2(#)(f2`|Z)) +2(#)((f1`|Z)(#)diff(f2,Z).2))
        +((f1`|Z)(#)(diff(f2,Z).2)+ f1(#)(diff(f2,Z).3)) by RFUNCT_1:28
    .=(diff(f1,Z).3)(#)f2 +(1(#)(diff(f1,Z).2)(#)(f2`|Z)
        +(2(#)(diff(f1,Z).2(#)(f2`|Z)) +2(#)((f1`|Z)(#)diff(f2,Z).2)))
        +((f1`|Z)(#)(diff(f2,Z).2)+ f1(#)(diff(f2,Z).3)) by RFUNCT_1:19
    .=(diff(f1,Z).3)(#)f2 + (((1(#)(diff(f1,Z).2)(#)(f2`|Z)
        +2(#)(diff(f1,Z).2(#)(f2`|Z)))) +2(#)((f1`|Z)(#)diff(f2,Z).2))
        +((f1`|Z)(#)(diff(f2,Z).2)+ f1(#)(diff(f2,Z).3)) by RFUNCT_1:19
    .=(diff(f1,Z).3)(#)f2 + ((((1(#)(g1(#)(f2`|Z))+2(#)(g1(#)(f2`|Z)))))
        +2(#)((f1`|Z)(#)g2))+((f1`|Z)(#)g2+ f1(#)(diff(f2,Z).3))
                                                          by RFUNCT_1:24
    .=(diff(f1,Z).3)(#)f2 + (((((1+2)(#)(g1(#)(f2`|Z)))))
       +2(#)((f1`|Z)(#)g2))+((f1`|Z)(#)g2+ f1(#)(diff(f2,Z).3)) by ThB2
    .=(diff(f1,Z).3)(#)f2 + (((3(#)(g1(#)(f2`|Z)))+2(#)((f1`|Z)(#)g2))
                +((f1`|Z)(#)g2+ f1(#)(diff(f2,Z).3))) by RFUNCT_1:19
    .=(diff(f1,Z).3)(#)f2 + ((3(#)(g1(#)(f2`|Z)))+(2(#)((f1`|Z)(#)g2)
        +((f1`|Z)(#)g2+ f1(#)(diff(f2,Z).3)))) by RFUNCT_1:19
    .=(diff(f1,Z).3)(#)f2 + ((3(#)(g1(#)(f2`|Z)))+((2(#)((f1`|Z)(#)g2)
        +(f1`|Z)(#)g2)+ f1(#)(diff(f2,Z).3)))  by RFUNCT_1:19
    .=(diff(f1,Z).3)(#)f2 + ((3(#)(g1(#)(f2`|Z)))+((2(#)((f1`|Z)(#)g2)
        +1(#)((f1`|Z)(#)g2))+ f1(#)(diff(f2,Z).3)))  by RFUNCT_1:33
    .=(diff(f1,Z).3)(#)f2+((3(#)(g1(#)(f2`|Z)))+(((2+1)(#)((f1`|Z)(#)g2))
                + f1(#)(diff(f2,Z).3))) by ThB2
    .=(diff(f1,Z).3)(#)f2 + (3(#)(g1(#)(f2`|Z))+3(#)((f1`|Z)(#)g2)
              + f1(#)(diff(f2,Z).3)) by RFUNCT_1:19
    .=(diff(f1,Z).3)(#)f2 + (3(#)(g1(#)(f2`|Z))+3(#)((f1`|Z)(#)g2))
         + f1(#)(diff(f2,Z).3) by RFUNCT_1:19;
  hence thesis;
end;

theorem
  diff(sin(#)sin,Z).3=(-8)(#)((cos(#)sin)|Z)
proof
A1: sin is_differentiable_on 3,Z by TAYLOR_2:21;
    diff(sin(#)sin,Z).3
     =(diff(sin,Z).(2*1+1))(#)sin + (3(#)(diff(sin,Z).(2*1)(#)(sin`|Z))
      +3(#)((sin`|Z)(#)diff(sin,Z).(2*1)))+ sin(#)(diff(sin,Z).(2*1+1))
                                                            by Th21,A1
     .=((-1) |^ 1 (#) cos | Z)(#)sin + (3(#)(diff(sin,Z).(2*1)(#)(sin`|Z))
      +3(#)((sin`|Z)(#)diff(sin,Z).(2*1)))+ sin(#)(diff(sin,Z).(2*1+1))
                                                              by TAYLOR_2:19
     .=((-1) |^ 1 (#) cos | Z)(#)sin + (3(#)(diff(sin,Z).(2*1)(#)(sin`|Z))
      +3(#)((sin`|Z)(#)diff(sin,Z).(2*1)))+ sin(#)((-1) |^ 1 (#) cos | Z)
                                                              by TAYLOR_2:19
     .=((-1) |^ 1 (#) cos | Z)(#)sin + (3(#)((-1) |^ 1 (#) sin |Z(#)(sin`|Z))
      +3(#)((sin`|Z)(#)diff(sin,Z).(2*1)))+ sin(#)((-1) |^ 1 (#) cos | Z)
                                                              by TAYLOR_2:19
     .=((-1) |^ 1 (#) cos | Z)(#)sin + (3(#)((-1) |^ 1 (#) sin |Z(#)(sin`|Z))
      +3(#)((sin`|Z)(#)((-1) |^ 1 (#) sin | Z)))+ sin(#)((-1) |^ 1 (#) cos | Z)
                                                              by TAYLOR_2:19
     .=((-1)(#) cos | Z)(#)sin + (3(#)((-1) |^ 1 (#) sin |Z(#)(sin`|Z))
      +3(#)((sin`|Z)(#)((-1)|^1(#)sin|Z)))+sin(#)((-1)|^1(#)cos|Z) by NEWTON:10
     .=((-1)(#) cos | Z)(#)sin + (3(#)((-1)(#) sin |Z(#)(sin`|Z))
      +3(#)((sin`|Z)(#)((-1)|^1(#)sin|Z)))+sin(#)((-1)|^1(#)cos|Z) by NEWTON:10
     .=((-1)(#) cos | Z)(#)sin + (3(#)((-1)(#) sin |Z(#)(sin`|Z))
      +3(#)((sin`|Z)(#)((-1)(#)sin|Z)))+sin(#)((-1)|^1(#)cos|Z) by NEWTON:10
     .=((-1)(#) cos | Z)(#)sin + (3(#)((-1)(#) sin |Z(#)(sin`|Z))
      +3(#)((sin`|Z)(#)((-1)(#) sin|Z)))+ sin(#)((-1)(#) cos | Z) by NEWTON:10
     .=((-1)(#) cos | Z)(#)sin + (3(#)((-1)(#) sin |Z(#)(cos|Z))
      +3(#)((sin`|Z)(#)((-1)(#) sin|Z)))+ sin(#)((-1)(#)cos|Z) by TAYLOR_2:17
     .=((-1)(#) cos | Z)(#)sin + ((3(#)((-1)(#) sin |Z(#)(cos|Z))
      +3(#)((cos|Z)(#)((-1)(#) sin|Z))))+ sin(#)((-1)(#) cos|Z) by TAYLOR_2:17
     .=((-1)(#) cos | Z)(#)sin +((3+3)(#)((cos|Z)(#)((-1)(#) sin|Z)))
                                              +sin(#)((-1)(#) cos|Z) by ThB2
     .=(6(#)((cos|Z)(#)((-1)(#) sin|Z))) +(((-1)(#) cos | Z)(#)sin
                              +((-1)(#) cos | Z)(#)sin)  by RFUNCT_1:19
     .=(6(#)((cos|Z)(#)((-1)(#) sin|Z))) +(1(#)(((-1)(#) (cos | Z))(#)sin)
                              +((-1)(#) cos | Z)(#)sin)  by RFUNCT_1:33
     .=(6(#)((cos|Z)(#)((-1)(#) sin|Z))) +(1(#)(((-1)(#) (cos | Z))(#)sin)
                              +1(#)(((-1)(#) cos | Z)(#)sin)) by RFUNCT_1:33
     .=(6(#)((cos|Z)(#)((-1)(#)sin|Z)))+((1+1)(#)(((-1)(#)(cos|Z))(#)sin))
                                                                    by ThB2
     .=(6(#)((-1)(#)((cos|Z)(#)sin|Z)))+(2(#)(((-1)(#)(cos|Z))(#)sin))
                                                                by RFUNCT_1:25
     .=6(#)((-1)(#)((cos(#)sin)|Z))+2(#)(((-1)(#)(cos|Z))(#)sin) by RFUNCT_1:61
     .=6(#)((-1)(#)((cos(#)sin)|Z))+2(#)((-1)(#)((cos|Z)(#)sin)) by RFUNCT_1:24
     .=6(#)((-1)(#)((cos(#)sin)|Z))+2(#)((-1)(#)((cos(#)sin)|Z)) by RFUNCT_1:61
     .=(6+2)(#)((-1)(#)((cos(#)sin)|Z)) by ThB2
     .=(8*(-1))(#)((cos(#)sin)|Z) by RFUNCT_1:29
     .=(-8)(#)((cos(#)sin)|Z);
   hence thesis;
end;

theorem
  f is_differentiable_on 2,Z implies
    diff(f(#)f,Z).2=2(#)(f(#)(diff(f,Z).2))+2(#)((f`|Z)(#)(f`|Z))
proof
   assume
A1:  f is_differentiable_on 2,Z;
     diff(f(#)f,Z).2
      =(diff(f,Z).2)(#)f+(2(#)((f`|Z)(#)(f`|Z))+f(#)(diff(f,Z).2)) by ThB3,A1
      .=((diff(f,Z).2)(#)f+ f(#)(diff(f,Z).2)) + 2(#)((f`|Z)(#)(f`|Z))
                                                     by RFUNCT_1:19
      .=1(#)(f(#)(diff(f,Z).2))+ f(#)(diff(f,Z).2) + 2(#)((f`|Z)(#)(f`|Z))
                                                            by RFUNCT_1:33
      .=1(#)(f(#)(diff(f,Z).2))+1(#)(f(#)(diff(f,Z).2))+2(#)((f`|Z)(#)(f`|Z))
                                                             by RFUNCT_1:33
      .=(1+1)(#)(f(#)(diff(f,Z).2))+2(#)((f`|Z)(#)(f`|Z)) by ThB2
      .=2(#)(f(#)(diff(f,Z).2))+2(#)((f`|Z)(#)(f`|Z));
   hence thesis;
end;

theorem
  f is_differentiable_on 2,Z & (for x0 st x0 in Z holds f.x0 <> 0)
    implies diff(f^,Z).2=(f/f)(#)((2(#)(f`|Z)(#)(f`|Z)-diff(f,Z).2(#)f)
              /(f(#)(f(#)f)))
proof
   assume that
A1:  f is_differentiable_on 2,Z and
A2:  for x0 st x0 in Z holds f.x0 <> 0;
A3:  f is_differentiable_on Z by ThB19,A1;then
A4:  f^ is_differentiable_on Z by FDIFF_2:22,A2;
A:   1<=2-1;
A5:  diff(f,Z).1 = diff(f,Z).(1+0)
      .=diff(f,Z).0`|Z by TAYLOR_1:def 5
      .=f|Z`|Z by TAYLOR_1:def 5
      .=f`|Z by FDIFF_2:16,A3;
A6:  f`|Z is_differentiable_on Z by A5,A1,TAYLOR_1:def 6,A;
A7:  (f(#)f) is_differentiable_on Z by FDIFF_2:20,A3;
A8:  for x0 st x0 in Z holds (f(#)f).x0 <> 0
    proof
      let x0;
      assume
A9:   x0 in Z;
A10:  Z c= dom f by A3,FDIFF_1:def 7;
      dom(f(#)f) = dom f/\dom f by VALUED_1:def 4
       .=dom f;then
A12:  (f(#)f).x0 =f.x0*f.x0 by VALUED_1:def 4,A9,A10;
      f.x0 <>0 by A9,A2;
      hence thesis by A12,XCMPLX_1:6;
   end;
A13: (f`|Z)/ (f (#) f) is_differentiable_on Z by A8,A7,A6,FDIFF_2:21;
  set f1=(f`|Z);
  set f2=(f (#) f);
     diff(f^,Z).2 =diff(f^,Z).(1+1)
      .=diff(f^,Z).(1+0)`|Z by TAYLOR_1:def 5
      .=(diff(f^,Z).0)`|Z`|Z by TAYLOR_1:def 5
      .=f^|Z`|Z`|Z by TAYLOR_1:def 5
      .=f^`|Z`|Z by FDIFF_2:16,A4
      .=(- (f`|Z)/ (f (#) f))`|Z by FDIFF_2:22,A3,A2
      .=(-1)(#)(((f`|Z)/ (f (#) f))`|Z) by FDIFF_2:19,A13
    .=(-1)(#)((((f`|Z)`|Z)(#)(f(#)f)-(f(#)f)`|Z(#)(f`|Z))/((f(#)f)(#)(f(#)f)))
                               by FDIFF_2:21,A8,A7,A6
.=(-1)(#)(((diff(f,Z).2)(#)(f(#)f)-((f(#)f)`|Z)(#)(f`|Z))/((f(#)f)(#)(f(#)f)))
                                                    by Lm1,ThB19,A1
    .=(-1)(#)(((diff(f,Z).2)(#)(f(#)f)-((f`|Z)(#)f + f(#)(f`|Z))(#)(f`|Z))
              /((f(#)f)(#)(f(#)f))) by FDIFF_2:20,A3
    .=(-1)(#)(((diff(f,Z).2)(#)(f(#)f)-(f(#)((f`|Z)+(f`|Z)))(#)(f`|Z))
              /((f(#)f)(#)(f(#)f))) by RFUNCT_1:23
    .=(-1)(#)(((diff(f,Z).2)(#)(f(#)f)-(f(#)(1(#)(f`|Z)+(f`|Z)))(#)(f`|Z))
              /((f(#)f)(#)(f(#)f))) by RFUNCT_1:33
    .=(-1)(#)(((diff(f,Z).2)(#)(f(#)f)-(f(#)(1(#)(f`|Z)+1(#)(f`|Z)))(#)(f`|Z))
              /((f(#)f)(#)(f(#)f))) by RFUNCT_1:33
    .=(-1)(#)(((diff(f,Z).2)(#)(f(#)f)-(f(#)((1+1)(#)(f`|Z)))(#)(f`|Z))
              /((f(#)f)(#)(f(#)f))) by ThB2
    .=(-1)(#)((f(#)((diff(f,Z).2)(#)f)-(f(#)((2(#)(f`|Z)))(#)(f`|Z)))
              /((f(#)f)(#)(f(#)f))) by RFUNCT_1:21
    .=((-1)(#)((f(#)((diff(f,Z).2)(#)f)-(f(#)((2(#)(f`|Z)))(#)(f`|Z))))
              /((f(#)f)(#)(f(#)f))) by RFUNCT_1:48
    .=((((f(#)((2(#)(f`|Z)))(#)(f`|Z))-(f(#)((diff(f,Z).2)(#)f))))
              /((f(#)f)(#)(f(#)f))) by RFUNCT_1:31
    .=((f(#)((2(#)(f`|Z))(#)(f`|Z)))-(f(#)((diff(f,Z).2)(#)f)))
              /((f(#)f)(#)(f(#)f)) by RFUNCT_1:21
    .=(f(#)(((2(#)(f`|Z))(#)(f`|Z))-((diff(f,Z).2)(#)f)))
              /(f(#)f(#)(f(#)f)) by RFUNCT_1:27
    .=(f(#)(((2(#)(f`|Z))(#)(f`|Z))-((diff(f,Z).2)(#)f)))
              /(f(#)(f(#)(f(#)f))) by RFUNCT_1:21
    .=(f/f)(#)((2(#)(f`|Z)(#)(f`|Z)-diff(f,Z).2(#)f)
              /(f(#)(f(#)f))) by RFUNCT_1:50;
 hence thesis;
end;

theorem
  diff(exp_R(#)sin,Z).3=(2(#)(exp_R(#)((-sin)+cos)))|Z
proof
A2:sin is_differentiable_on 3,Z by TAYLOR_2:21;
A3:  exp_R is_differentiable_on 3,Z by TAYLOR_2:10;
   diff(exp_R(#)sin,Z).3
     =(diff(exp_R,Z).3)(#)sin + (3(#)(diff(exp_R,Z).2(#)(sin`|Z))
      +3(#)((exp_R`|Z)(#)diff(sin,Z).2))+ exp_R(#)(diff(sin,Z).3) by Th21,A2,A3
    .=(exp_R|Z)(#)sin + (3(#)(diff(exp_R,Z).2(#)(sin`|Z))
      +3(#)((exp_R`|Z)(#)diff(sin,Z).2))+ exp_R(#)(diff(sin,Z).3)
                                                             by TAYLOR_2:6
    .=(exp_R|Z)(#)sin + (3(#)(exp_R|Z(#)(sin`|Z))
      +3(#)((exp_R`|Z)(#)diff(sin,Z).2))+exp_R(#)(diff(sin,Z).3)
                                                             by TAYLOR_2:6
    .=(exp_R|Z)(#)sin + (3(#)(exp_R|Z(#)(sin`|Z))
      +3(#)((exp_R|Z)(#)diff(sin,Z).2))+exp_R(#)(diff(sin,Z).3) by TAYLOR_2:5
    .=(exp_R|Z)(#)sin + (3(#)(exp_R|Z(#)(cos|Z))
      +3(#)((exp_R|Z)(#)diff(sin,Z).(2*1)))+ exp_R(#)(diff(sin,Z).(2*1+1))
                                                                 by TAYLOR_2:17
    .=(exp_R|Z)(#)sin + (3(#)(exp_R|Z(#)(cos|Z))
      +3(#)((exp_R|Z)(#)((-1)|^1(#)sin|Z)))+ exp_R(#)(diff(sin,Z).(2*1+1))
                                                                 by TAYLOR_2:19
    .=(exp_R|Z)(#)sin + (3(#)(exp_R|Z(#)(cos|Z))
      +3(#)((exp_R|Z)(#)((-1)|^1(#)sin|Z)))+ exp_R(#)((-1) |^ 1(#)cos |Z )
                                                                 by TAYLOR_2:19
    .=(exp_R|Z)(#)sin + (3(#)(exp_R|Z(#)(cos|Z))
      +3(#)((exp_R|Z)(#)((-1)(#)sin|Z)))+exp_R(#)((-1)|^1(#)cos |Z)
                                                                by NEWTON:10
    .=exp_R|Z(#)sin + (3(#)(exp_R|Z(#)(cos|Z))
      +3(#)((exp_R|Z)(#)((-1)(#)sin|Z)))+exp_R(#)((-1)(#)cos|Z) by NEWTON:10
    .=(exp_R(#)sin)|Z+(3(#)(exp_R|Z(#)(cos|Z))
      +3(#)((exp_R|Z)(#)((-1)(#)sin|Z)))+exp_R(#)((-1)(#)cos|Z) by RFUNCT_1:61
    .=(exp_R(#)sin)|Z+(3(#)((exp_R(#)cos)|Z)
      +3(#)((exp_R|Z)(#)((-1)(#)sin|Z)))+exp_R(#)((-1)(#)cos|Z) by RFUNCT_1:61
    .=(exp_R(#)sin)|Z+(3(#)((exp_R(#)cos)|Z)
      +3(#)((-1)(#)((exp_R|Z)(#)sin|Z)))+exp_R(#)((-1)(#)cos|Z) by RFUNCT_1:25
    .=(exp_R(#)sin)|Z+(3(#)((exp_R(#)cos)|Z)
      +(3*(-1))(#)((exp_R|Z)(#)sin|Z))+exp_R(#)((-1)(#)cos|Z) by RFUNCT_1:29
    .=(exp_R(#)sin)|Z+(3(#)((exp_R(#)cos)|Z)
      +(-3)(#)((exp_R(#)sin)|Z))+exp_R(#)((-1)(#)cos|Z) by RFUNCT_1:61
    .=(exp_R(#)sin)|Z+(3(#)((exp_R(#)cos)|Z)
      +(-3)(#)((exp_R(#)sin)|Z))+(-1)(#)(exp_R(#)cos|Z) by RFUNCT_1:25
    .=(exp_R(#)sin)|Z+(3(#)((exp_R(#)cos)|Z)
      +(-3)(#)((exp_R(#)sin)|Z))+(-1)(#)((exp_R(#)cos)|Z) by RFUNCT_1:61
    .=(exp_R(#)sin)|Z+3(#)((exp_R(#)cos)|Z)
      +(-3)(#)((exp_R(#)sin)|Z)+(-1)(#)((exp_R(#)cos)|Z) by RFUNCT_1:19
    .=3(#)((exp_R(#)cos)|Z)+1(#)((exp_R(#)sin)|Z)
      +(-3)(#)((exp_R(#)sin)|Z)+(-1)(#)((exp_R(#)cos)|Z) by RFUNCT_1:33
    .=3(#)((exp_R(#)cos)|Z)+(1(#)((exp_R(#)sin)|Z)
      +(-3)(#)((exp_R(#)sin)|Z))+(-1)(#)((exp_R(#)cos)|Z) by RFUNCT_1:19
    .=3(#)((exp_R(#)cos)|Z)+((1+(-3))(#)((exp_R(#)sin)|Z))
                                      +(-1)(#)((exp_R(#)cos)|Z) by ThB2
    .=((-2)(#)((exp_R(#)sin)|Z))+(3(#)((exp_R(#)cos)|Z)
                             +(-1)(#)((exp_R(#)cos)|Z)) by RFUNCT_1:19
    .=((-2)(#)((exp_R(#)sin)|Z))+((3+(-1))(#)((exp_R(#)cos)|Z)) by ThB2
    .=((-2)(#)(exp_R(#)sin))|Z+2(#)((exp_R(#)cos)|Z) by RFUNCT_1:65
    .=((-2)(#)(exp_R(#)sin))|Z+(2(#)(exp_R(#)cos))|Z by RFUNCT_1:65
    .=((2*(-1))(#)(exp_R(#)sin)+2(#)(exp_R(#)cos))|Z by RFUNCT_1:60
    .=(2(#)((-1)(#)(exp_R(#)sin))+2(#)(exp_R(#)cos))|Z by RFUNCT_1:29
    .=(2(#)(((-1)(#)(exp_R(#)sin))+(exp_R(#)cos)))|Z by RFUNCT_1:28
    .=(2(#)((exp_R(#)((-1)(#)sin))+(exp_R(#)cos)))|Z by RFUNCT_1:25
    .=(2(#)(exp_R(#)((-sin)+cos)))|Z by RFUNCT_1:23;
  hence thesis;
end;