hfdiff_1.miz

    begin

    reserve x,r,a,x0,p for Real;

    reserve n,i,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 :: HFDIFF_1:1



     Th1: for f be 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 RELAT_1: 61

      .= Z by A1, XBOOLE_1: 28;

    end;

    theorem :: HFDIFF_1:2



     Th2: (( - f1) (#) ( - f2)) = (f1 (#) f2)

    proof

      ( dom ( - f1)) = ( dom f1) & ( dom ( - f2)) = ( dom f2) by VALUED_1:def 5;



      then

       A1: ( dom (( - f1) (#) ( - f2))) = (( dom f1) /\ ( dom f2)) by VALUED_1:def 4

      .= ( dom (f1 (#) f2)) by VALUED_1:def 4;

      for x be Element of REAL st x in ( dom (f1 (#) f2)) holds ((( - f1) (#) ( - f2)) . x) = ((f1 (#) f2) . x)

      proof

        let x be Element of REAL ;

        assume

         A2: x in ( dom (f1 (#) f2));

        ( dom (f1 (#) f2)) = (( dom f2) /\ ( dom f1)) by VALUED_1:def 4;

        then ( dom (f2 (#) f1)) c= ( dom f2) by XBOOLE_1: 17;

        then x in ( dom f2) by A2;

        then

         A3: x in ( dom (( - 1) (#) f2)) by VALUED_1:def 5;

        (( dom f1) /\ ( dom f2)) c= ( dom f1) by XBOOLE_1: 17;

        then ( dom (f1 (#) f2)) c= ( dom f1) by VALUED_1:def 4;

        then x in ( dom f1) by A2;

        then

         A4: x in ( dom (( - 1) (#) f1)) by VALUED_1:def 5;

        ((( - f1) (#) ( - f2)) . x) = ((( - f1) . x) * (( - f2) . x)) by A1, A2, VALUED_1:def 4

        .= ((( - 1) * (f1 . x)) * ((( - 1) (#) f2) . x)) by A4, VALUED_1:def 5

        .= ((( - 1) * (f1 . x)) * (( - 1) * (f2 . x))) by A3, VALUED_1:def 5

        .= ((f1 . x) * (f2 . x));

        hence thesis by A2, VALUED_1:def 4;

      end;

      hence thesis by A1, PARTFUN1: 5;

    end;

    theorem :: HFDIFF_1:3



     Th3: n >= 1 implies ( dom (( #Z n) ^ )) = ( REAL \ { 0 }) & (( #Z n) " { 0 }) = { 0 }

    proof

      assume

       A1: n >= 1;



       A2: (( #Z n) " { 0 }) = { 0 }

      proof

        thus (( #Z n) " { 0 }) c= { 0 }

        proof

          let x be object;

          assume

           A3: x in (( #Z n) " { 0 });

          then

          reconsider x as Element of REAL ;

          (( #Z n) . x) in { 0 } by A3, FUNCT_1:def 7;

          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: 36;

          then x = 0 by PREPOWER: 5;

          hence thesis by TARSKI:def 1;

        end;

        let x be object;



         A4: 0 in { 0 } by TARSKI:def 1;

        assume x in { 0 };

        then

         A5: x = 0 by TARSKI:def 1;

         {( In ( 0 , REAL ))} c= REAL by ZFMISC_1: 31;

        then

         A6: { 0 } c= ( dom ( #Z n)) by FUNCT_2:def 1;

        (( #Z n) . 0 ) = ( 0 #Z n) by TAYLOR_1:def 1

        .= ( 0 |^ n) by PREPOWER: 36

        .= 0 by A1, NEWTON: 11;

        hence thesis by A5, A6, A4, FUNCT_1:def 7;

      end;



      then ( dom (( #Z n) ^ )) = (( dom ( #Z n)) \ { 0 }) by RFUNCT_1:def 2

      .= ( REAL \ { 0 }) by FUNCT_2:def 1;

      hence thesis by A2;

    end;

    theorem :: HFDIFF_1:4

    ((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 object;

        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: 2;

    end;

    theorem :: HFDIFF_1:5



     Th5: for n,m be Real holds ((n (#) f1) + (m (#) f1)) = ((n + m) (#) f1)

    proof

      let n,m be Real;



       A1: ( 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);



       A2: for x be Element of REAL st x in ( dom f1) holds (((n (#) f1) + (m (#) f1)) . x) = (((n + m) (#) f1) . x)

      proof

        let x be Element of REAL ;

        assume

         A3: x in ( dom f1);

        then

         A4: x in ( dom (n (#) f1)) by VALUED_1:def 5;

        x in ( dom ((n + m) (#) f1)) by A3, VALUED_1:def 5;



        then

         A5: (((n + m) (#) f1) . x) = ((n + m) * (f1 . x)) by VALUED_1:def 5

        .= ((n * (f1 . x)) + (m * (f1 . x)));



         A6: x in ( dom (m (#) f1)) by A3, VALUED_1:def 5;

        (((n (#) f1) + (m (#) f1)) . x) = (((n (#) f1) . x) + ((m (#) f1) . x)) by A1, A3, VALUED_1:def 1

        .= ((n * (f1 . x)) + ((m (#) f1) . x)) by A4, VALUED_1:def 5

        .= ((n * (f1 . x)) + (m * (f1 . x))) by A6, VALUED_1:def 5;

        hence thesis by A5;

      end;

      ( dom ((n (#) f1) + (m (#) f1))) = ( dom ((n + m) (#) f1)) by A1, VALUED_1:def 5;

      hence thesis by A1, A2, PARTFUN1: 5;

    end;

    theorem :: HFDIFF_1:6



     Th6: (f | Z) is_differentiable_on Z implies f is_differentiable_on Z

    proof



       A1: ( dom (f | Z)) c= ( dom f) by RELAT_1: 60;

      assume

       A2: (f | Z) is_differentiable_on Z;

      then

       A3: for x st x in Z holds (f | Z) is_differentiable_in x by FDIFF_1: 9;

      Z c= ( dom (f | Z)) by A2, FDIFF_1: 9;

      then Z c= ( dom f) by A1;

      hence thesis by A3, FDIFF_1:def 6;

    end;

    theorem :: HFDIFF_1:7



     Th7: 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);

      (1 - 1) <= (n - 1) by A1, XREAL_1: 9;

      then (( diff (f1,Z)) . 0 ) is_differentiable_on Z by A2;

      then (f1 | Z) is_differentiable_on Z by TAYLOR_1:def 5;

      hence thesis by Th6;

    end;

    theorem :: HFDIFF_1:8



     Th8: ( #Z n) is_differentiable_on REAL

    proof



       A1: ( dom ( #Z n)) = REAL by FUNCT_2:def 1;

      for x st x in REAL holds (( #Z n) | REAL ) is_differentiable_in x

      proof

        let x;

        assume x in REAL ;

        ( #Z n) is_differentiable_in x by TAYLOR_1: 2;

        hence thesis by A1, RELAT_1: 68;

      end;

      hence thesis by A1, FDIFF_1:def 6;

    end;

    theorem :: HFDIFF_1:9

    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: 26, SIN_COS: 67;



       A3: sin is_differentiable_on Z by FDIFF_1: 26, SIN_COS: 68;

      ((( 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 A3, FDIFF_2: 16

      .= ((( cos | Z) `| Z) . x) by TAYLOR_2: 17

      .= (( cos `| Z) . x) by A2, FDIFF_2: 16

      .= ( diff ( cos ,x)) by A1, A2, FDIFF_1:def 7

      .= ( - ( sin . x)) by SIN_COS: 63;

      hence thesis;

    end;

    theorem :: HFDIFF_1:10

    x in Z implies ((( diff ( sin ,Z)) . 3) . x) = (( - cos ) . x)

    proof

      assume x in Z;

      then

       A1: x in ( dom ( cos | Z)) by TAYLOR_2: 17;

      ( dom (( - cos ) | Z)) = (( dom ( - cos )) /\ Z) by RELAT_1: 61

      .= (( dom cos ) /\ Z) by VALUED_1: 8

      .= ( dom ( cos | Z)) by RELAT_1: 61

      .= ( dom ( - ( cos | Z))) by VALUED_1: 8;

      then

       A2: x in ( dom (( - cos ) | Z)) by A1, 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)

      .= ((( - cos ) | Z) . x) by RFUNCT_1: 49

      .= (( - cos ) . x) by A2, FUNCT_1: 47;

      hence thesis;

    end;

    theorem :: HFDIFF_1:11



     Th11: x in Z implies ((( diff ( sin ,Z)) . n) . x) = ( sin . (x + ((n * PI ) / 2)))

    proof

      assume

       A1: x in Z;

      ( dom ((( - 1) (#) cos ) | Z)) = (( dom (( - 1) (#) cos )) /\ Z) by RELAT_1: 61

      .= (( dom cos ) /\ Z) by VALUED_1:def 5

      .= Z by SIN_COS: 24, XBOOLE_1: 28;

      then

       A2: Z c= ( dom (( - 1) (#) cos )) by RELAT_1: 60;

      ( dom ((( - 1) (#) sin ) | Z)) = (( dom (( - 1) (#) sin )) /\ Z) by RELAT_1: 61

      .= (( dom sin ) /\ Z) by VALUED_1:def 5

      .= Z by SIN_COS: 24, XBOOLE_1: 28;

      then

       A3: Z c= ( dom (( - 1) (#) sin )) by RELAT_1: 60;



       A4: sin is_differentiable_on Z by FDIFF_1: 26, SIN_COS: 68;

      then

       A5: (( - 1) (#) sin ) is_differentiable_on Z by FDIFF_2: 19;



       A6: cos is_differentiable_on Z by FDIFF_1: 26, SIN_COS: 67;

      then

       A7: (( - 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: 5;

        now

          per cases ;

            suppose i is even;

            then

            consider j be Nat such that

             A8: i = (2 * j) by ABIAN:def 2;

            per cases ;

              suppose j is even;

              then

              consider m be 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 A9, WSIERP_1: 2

              .= (((1 (#) ( sin | Z)) `| Z) . x)

              .= ((( sin | Z) `| Z) . x) by RFUNCT_1: 21

              .= (( sin `| Z) . x) by A4, FDIFF_2: 16

              .= ( diff ( sin ,x)) by A1, A4, FDIFF_1:def 7

              .= ( cos . x) by SIN_COS: 64

              .= ( cos . (x + ((2 * PI ) * m))) by SIN_COS2: 11

              .= ( sin . ((x + ((i / 2) * PI )) + ( PI / 2))) by A8, A9, SIN_COS: 78

              .= ( sin . (x + ((n * PI ) / 2)));

              hence thesis;

            end;

              suppose j is odd;

              then

              consider s be Nat such that

               A10: 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 A10, TAYLOR_2: 19

              .= (((((( - 1) |^ (2 * s)) * ( - 1)) (#) ( sin | Z)) `| Z) . x) by NEWTON: 6

              .= (((((1 |^ (2 * s)) * ( - 1)) (#) ( sin | Z)) `| Z) . x) by WSIERP_1: 2

              .= ((((1 * ( - 1)) (#) ( sin | Z)) `| Z) . x)

              .= (((( - sin ) | Z) `| Z) . x) by RFUNCT_1: 49

              .= (((( - 1) (#) sin ) `| Z) . x) by A5, FDIFF_2: 16

              .= (( - 1) * ( diff ( sin ,x))) by A1, A3, A4, FDIFF_1: 20

              .= (( - 1) * ( cos . x)) by SIN_COS: 64

              .= ( - ( cos . x))

              .= ( cos . (x + PI )) by SIN_COS: 78

              .= ( cos . ((x + PI ) + ((2 * PI ) * s))) by SIN_COS2: 11

              .= ( sin . ((x + ((i / 2) * PI )) + ( PI / 2))) by A8, A10, SIN_COS: 78

              .= ( sin . (x + ((n * PI ) / 2)));

              hence thesis;

            end;

          end;

            suppose i is odd;

            then

            consider j be Nat such that

             A11: i = ((2 * j) + 1) by ABIAN: 9;

            per cases ;

              suppose j is even;

              then

              consider m be Nat such that

               A12: j = (2 * m) by ABIAN:def 2;

              ((( diff ( sin ,Z)) . (i + 1)) . x) = (((( diff ( sin ,Z)) . ((2 * j) + 1)) `| Z) . x) by A11, TAYLOR_1:def 5

              .= ((((( - 1) |^ (2 * m)) (#) ( cos | Z)) `| Z) . x) by A12, TAYLOR_2: 19

              .= ((((1 |^ (2 * m)) (#) ( cos | Z)) `| Z) . x) by WSIERP_1: 2

              .= (((1 (#) ( cos | Z)) `| Z) . x)

              .= ((( cos | Z) `| Z) . x) by RFUNCT_1: 21

              .= (( cos `| Z) . x) by A6, FDIFF_2: 16

              .= ( diff ( cos ,x)) by A1, A6, FDIFF_1:def 7

              .= ( - ( sin . x)) by SIN_COS: 63

              .= ( sin . (x + PI )) by SIN_COS: 78

              .= ( sin . ((x + PI ) + ((2 * PI ) * m))) by SIN_COS2: 10

              .= ( sin . ((x + (((i - 1) / 2) * PI )) + PI )) by A11, A12

              .= ( sin . (x + ((n * PI ) / 2)));

              hence thesis;

            end;

              suppose j is odd;

              then

              consider s be Nat such that

               A13: j = ((2 * s) + 1) by ABIAN: 9;

              ((( diff ( sin ,Z)) . (i + 1)) . x) = (((( diff ( sin ,Z)) . ((2 * j) + 1)) `| Z) . x) by A11, TAYLOR_1:def 5

              .= ((((( - 1) |^ j) (#) ( cos | Z)) `| Z) . x) by TAYLOR_2: 19

              .= (((((( - 1) |^ (2 * s)) * ( - 1)) (#) ( cos | Z)) `| Z) . x) by A13, NEWTON: 6

              .= (((((1 |^ (2 * s)) * ( - 1)) (#) ( cos | Z)) `| Z) . x) by WSIERP_1: 2

              .= ((((1 * ( - 1)) (#) ( cos | Z)) `| Z) . x)

              .= (((( - cos ) | Z) `| Z) . x) by RFUNCT_1: 49

              .= (((( - 1) (#) cos ) `| Z) . x) by A7, FDIFF_2: 16

              .= (( - 1) * ( diff ( cos ,x))) by A1, A2, A6, FDIFF_1: 20

              .= (( - 1) * ( - ( sin . x))) by SIN_COS: 63

              .= ( sin . (x + ((2 * PI ) * s))) by SIN_COS2: 10

              .= ( sin . ((x + (((i - 3) / 2) * PI )) + (2 * PI ))) by A11, A13, SIN_COS: 78

              .= ( sin . (x + ((n * PI ) / 2)));

              hence thesis;

            end;

          end;

        end;

        hence thesis;

      end;

        suppose

         A14: n = 0 ;



        then ((( diff ( sin ,Z)) . n) . x) = (( sin | Z) . x) by TAYLOR_1:def 5

        .= ( sin . (x + ((n * PI ) / 2))) by A1, A14, FUNCT_1: 49;

        hence thesis;

      end;

    end;

    theorem :: HFDIFF_1:12

    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: 26, SIN_COS: 67;

      ( dom ((( - 1) (#) sin ) | Z)) = (( dom (( - 1) (#) sin )) /\ Z) by RELAT_1: 61

      .= (( dom sin ) /\ Z) by VALUED_1:def 5

      .= Z by SIN_COS: 24, XBOOLE_1: 28;

      then

       A3: Z c= ( dom (( - 1) (#) sin )) by RELAT_1: 60;



       A4: sin is_differentiable_on Z by FDIFF_1: 26, SIN_COS: 68;

      then

       A5: (( - 1) (#) sin ) is_differentiable_on Z by FDIFF_2: 19;

      ((( 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 A2, FDIFF_2: 16

      .= (((( - sin ) | Z) `| Z) . x) by TAYLOR_2: 17

      .= (((( - 1) (#) sin ) `| Z) . x) by A5, FDIFF_2: 16

      .= (( - 1) * ( diff ( sin ,x))) by A1, A4, A3, FDIFF_1: 20

      .= (( - 1) * ( cos . x)) by SIN_COS: 64

      .= ( - ( cos . x));

      hence thesis;

    end;

    theorem :: HFDIFF_1:13

    x in Z implies ((( diff ( cos ,Z)) . 3) . x) = ( sin . x)

    proof

      assume x in Z;

      then

       A1: x in ( dom ( sin | Z)) by 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: 1

      .= (((1 * 1) (#) ( sin | Z)) . x)

      .= (( sin | Z) . x) by RFUNCT_1: 21

      .= ( sin . x) by A1, FUNCT_1: 47;

      hence thesis;

    end;

    theorem :: HFDIFF_1:14



     Th14: x in Z implies ((( diff ( cos ,Z)) . n) . x) = ( cos . (x + ((n * PI ) / 2)))

    proof

      assume

       A1: x in Z;

      ( dom ((( - 1) (#) sin ) | Z)) = (( dom (( - 1) (#) sin )) /\ Z) by RELAT_1: 61

      .= (( dom sin ) /\ Z) by VALUED_1:def 5

      .= Z by SIN_COS: 24, XBOOLE_1: 28;

      then

       A2: Z c= ( dom (( - 1) (#) sin )) by RELAT_1: 60;

      ( dom ((( - 1) (#) cos ) | Z)) = (( dom (( - 1) (#) cos )) /\ Z) by RELAT_1: 61

      .= (( dom cos ) /\ Z) by VALUED_1:def 5

      .= Z by SIN_COS: 24, XBOOLE_1: 28;

      then

       A3: Z c= ( dom (( - 1) (#) cos )) by RELAT_1: 60;



       A4: cos is_differentiable_on Z by FDIFF_1: 26, SIN_COS: 67;

      then

       A5: (( - 1) (#) cos ) is_differentiable_on Z by FDIFF_2: 19;



       A6: sin is_differentiable_on Z by FDIFF_1: 26, SIN_COS: 68;

      then

       A7: (( - 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: 5;

        now

          per cases ;

            suppose i is even;

            then

            consider j be Nat such that

             A8: i = (2 * j) by ABIAN:def 2;

            per cases ;

              suppose j is even;

              then

              consider m be 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: 2

              .= (((1 (#) ( cos | Z)) `| Z) . x)

              .= ((( cos | Z) `| Z) . x) by RFUNCT_1: 21

              .= (( cos `| Z) . x) by A4, FDIFF_2: 16

              .= ( diff ( cos ,x)) by A1, A4, FDIFF_1:def 7

              .= ( - ( sin . x)) by SIN_COS: 63

              .= ( cos . (x + ( PI / 2))) by SIN_COS: 78

              .= ( 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 Nat such that

               A10: 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 A10, TAYLOR_2: 19

              .= (((((( - 1) |^ (2 * s)) * ( - 1)) (#) ( cos | Z)) `| Z) . x) by NEWTON: 6

              .= (((((1 |^ (2 * s)) * ( - 1)) (#) ( cos | Z)) `| Z) . x) by WSIERP_1: 2

              .= ((((1 * ( - 1)) (#) ( cos | Z)) `| Z) . x)

              .= (((( - cos ) | Z) `| Z) . x) by RFUNCT_1: 49

              .= (((( - 1) (#) cos ) `| Z) . x) by A5, FDIFF_2: 16

              .= (( - 1) * ( diff ( cos ,x))) by A1, A3, A4, FDIFF_1: 20

              .= (( - 1) * ( - ( sin . x))) by SIN_COS: 63

              .= ( sin . (x + ((2 * PI ) * s))) by SIN_COS2: 10

              .= ( sin . ((x + (((i / 2) - 1) * PI )) + (2 * PI ))) by A8, A10, SIN_COS: 78

              .= ( cos . (( PI / 2) - (x + (((i / 2) + 1) * PI )))) by SIN_COS: 78

              .= ( cos . ( - (( PI / 2) - (x + (((i / 2) + 1) * PI ))))) by SIN_COS: 30

              .= ( cos . (x + ((n * PI ) / 2)));

              hence thesis;

            end;

          end;

            suppose i is odd;

            then

            consider j be Nat such that

             A11: i = ((2 * j) + 1) by ABIAN: 9;

            per cases ;

              suppose j is even;

              then

              consider m be Nat such that

               A12: j = (2 * m) by ABIAN:def 2;

              ((( diff ( cos ,Z)) . (i + 1)) . x) = (((( diff ( cos ,Z)) . ((2 * j) + 1)) `| Z) . x) by A11, TAYLOR_1:def 5

              .= ((((( - 1) |^ ((2 * m) + 1)) (#) ( sin | Z)) `| Z) . x) by A12, TAYLOR_2: 19

              .= (((((( - 1) |^ (2 * m)) * ( - 1)) (#) ( sin | Z)) `| Z) . x) by NEWTON: 6

              .= (((((1 |^ (2 * m)) * ( - 1)) (#) ( sin | Z)) `| Z) . x) by WSIERP_1: 2

              .= ((((1 * ( - 1)) (#) ( sin | Z)) `| Z) . x)

              .= (((( - sin ) | Z) `| Z) . x) by RFUNCT_1: 49

              .= (((( - 1) (#) sin ) `| Z) . x) by A7, FDIFF_2: 16

              .= (( - 1) * ( diff ( sin ,x))) by A1, A2, A6, FDIFF_1: 20

              .= (( - 1) * ( cos . x)) by SIN_COS: 64

              .= ( - ( cos . x))

              .= ( cos . (x + PI )) by SIN_COS: 78

              .= ( cos . ((x + PI ) + ((2 * PI ) * m))) by SIN_COS2: 11

              .= ( cos . (x + (((i + 1) * PI ) / 2))) by A11, A12

              .= ( cos . (x + ((n * PI ) / 2)));

              hence thesis;

            end;

              suppose j is odd;

              then

              consider s be Nat such that

               A13: j = ((2 * s) + 1) by ABIAN: 9;

              ((( diff ( cos ,Z)) . (i + 1)) . x) = (((( diff ( cos ,Z)) . ((2 * j) + 1)) `| Z) . x) by A11, TAYLOR_1:def 5

              .= ((((( - 1) |^ (j + 1)) (#) ( sin | Z)) `| Z) . x) by TAYLOR_2: 19

              .= ((((1 |^ (2 * (s + 1))) (#) ( sin | Z)) `| Z) . x) by A13, WSIERP_1: 2

              .= (((1 (#) ( sin | Z)) `| Z) . x)

              .= ((( sin | Z) `| Z) . x) by RFUNCT_1: 21

              .= (( sin `| Z) . x) by A6, FDIFF_2: 16

              .= ( diff ( sin ,x)) by A1, A6, FDIFF_1:def 7

              .= ( cos . x) by SIN_COS: 64

              .= ( cos . (x + ((2 * PI ) * s))) by SIN_COS2: 11

              .= ( cos . ((x + ((((i - 1) / 2) - 1) * PI )) + (2 * PI ))) by A11, A13, SIN_COS: 78

              .= ( cos . (x + ((n * PI ) / 2)));

              hence thesis;

            end;

          end;

        end;

        hence thesis;

      end;

        suppose

         A14: n = 0 ;



        then ((( diff ( cos ,Z)) . n) . x) = (( cos | Z) . x) by TAYLOR_1:def 5

        .= ( cos . (x + ((n * PI ) / 2))) by A1, A14, FUNCT_1: 49;

        hence thesis;

      end;

    end;

    theorem :: HFDIFF_1:15



     Th15: 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: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat such that

         A2: P[k];

        assume

         A3: f1 is_differentiable_on ((k + 1),Z) & f2 is_differentiable_on ((k + 1),Z);



         A4: (( diff (f1,Z)) . k) is_differentiable_on Z & (( diff (f2,Z)) . k) is_differentiable_on Z by A3;

        k < (k + 1) by NAT_1: 19;



        then (( diff ((f1 + f2),Z)) . (k + 1)) = (((( diff (f1,Z)) . k) + (( diff (f2,Z)) . k)) `| Z) by A2, A3, TAYLOR_1: 23, TAYLOR_1:def 5

        .= (((( diff (f1,Z)) . k) `| Z) + ((( diff (f2,Z)) . k) `| Z)) by A4, 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;



       A5: P[ 0 ]

      proof

        assume that f1 is_differentiable_on ( 0 ,Z) and 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: 44

        .= ((( 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;

      for k be Nat holds P[k] from NAT_1:sch 2( A5, A1);

      hence thesis;

    end;

    theorem :: HFDIFF_1:16



     Th16: 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: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat such that

         A2: P[k];

        assume

         A3: f1 is_differentiable_on ((k + 1),Z) & f2 is_differentiable_on ((k + 1),Z);



         A4: (( diff (f1,Z)) . k) is_differentiable_on Z & (( diff (f2,Z)) . k) is_differentiable_on Z by A3;

        k < (k + 1) by NAT_1: 19;



        then (( diff ((f1 - f2),Z)) . (k + 1)) = (((( diff (f1,Z)) . k) - (( diff (f2,Z)) . k)) `| Z) by A2, A3, TAYLOR_1: 23, TAYLOR_1:def 5

        .= (((( diff (f1,Z)) . k) `| Z) - ((( diff (f2,Z)) . k) `| Z)) by A4, 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;



       A5: P[ 0 ]

      proof

        assume that f1 is_differentiable_on ( 0 ,Z) and 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: 47

        .= ((( 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;

      for k be Nat holds P[k] from NAT_1:sch 2( A5, A1);

      hence thesis;

    end;

    theorem :: HFDIFF_1:17



     Th17: 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

       A1: f1 is_differentiable_on (n,Z) & f2 is_differentiable_on (n,Z);

      assume i <= n;

      then f1 is_differentiable_on (i,Z) & f2 is_differentiable_on (i,Z) by A1, TAYLOR_1: 23;

      hence thesis by Th15;

    end;

    theorem :: HFDIFF_1:18



     Th18: 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

       A1: f1 is_differentiable_on (n,Z) & f2 is_differentiable_on (n,Z);

      assume i <= n;

      then f1 is_differentiable_on (i,Z) & f2 is_differentiable_on (i,Z) by A1, TAYLOR_1: 23;

      hence thesis by Th16;

    end;

    theorem :: HFDIFF_1:19

    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 Nat such that

         A3: i <= (n - 1);



         A4: i in NAT by ORDINAL1:def 12;



         A5: (( diff (f2,Z)) . i) is_differentiable_on Z by A2, A3;

        then

         A6: Z c= ( dom (( diff (f2,Z)) . i)) by FDIFF_1:def 6;

        i <= n by A3, WSIERP_1: 18;

        then

         A7: (( diff ((f1 + f2),Z)) . i) = ((( diff (f1,Z)) . i) + (( diff (f2,Z)) . i)) by A1, A2, Th17, A4;



         A8: (( diff (f1,Z)) . i) is_differentiable_on Z by A1, A3;

        then Z c= ( dom (( diff (f1,Z)) . i)) by FDIFF_1:def 6;

        then Z c= (( dom (( diff (f1,Z)) . i)) /\ ( dom (( diff (f2,Z)) . i))) by A6, 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 A8, A5, A7, FDIFF_1: 18;

      end;

      hence thesis;

    end;

    theorem :: HFDIFF_1:20

    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 Nat such that

         A3: i <= (n - 1);



         A4: i in NAT by ORDINAL1:def 12;



         A5: (( diff (f2,Z)) . i) is_differentiable_on Z by A2, A3;

        then

         A6: Z c= ( dom (( diff (f2,Z)) . i)) by FDIFF_1:def 6;

        i <= n by A3, WSIERP_1: 18;

        then

         A7: (( diff ((f1 - f2),Z)) . i) = ((( diff (f1,Z)) . i) - (( diff (f2,Z)) . i)) by A1, A2, Th18, A4;



         A8: (( diff (f1,Z)) . i) is_differentiable_on Z by A1, A3;

        then Z c= ( dom (( diff (f1,Z)) . i)) by FDIFF_1:def 6;

        then Z c= (( dom (( diff (f1,Z)) . i)) /\ ( dom (( diff (f2,Z)) . i))) by A6, 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 A8, A5, A7, FDIFF_1: 19;

      end;

      hence thesis;

    end;

    theorem :: HFDIFF_1:21



     Th21: f is_differentiable_on (n,Z) implies (( diff ((r (#) f),Z)) . n) = (r (#) (( diff (f,Z)) . n))

    proof

      defpred P[ Nat] means f is_differentiable_on ($1,Z) implies (( diff ((r (#) f),Z)) . $1) = (r (#) (( diff (f,Z)) . $1));



       A1: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat;

        assume

         A2: P[k];

        assume

         A3: f is_differentiable_on ((k + 1),Z);



         A4: (( diff (f,Z)) . k) is_differentiable_on Z by A3;

        k < (k + 1) by NAT_1: 19;



        then (( diff ((r (#) f),Z)) . (k + 1)) = ((r (#) (( diff (f,Z)) . k)) `| Z) by A2, A3, TAYLOR_1: 23, TAYLOR_1:def 5

        .= (r (#) ((( diff (f,Z)) . k) `| Z)) by A4, FDIFF_2: 19

        .= (r (#) (( diff (f,Z)) . (k + 1))) by TAYLOR_1:def 5;

        hence thesis;

      end;



       A5: 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: 49

        .= (r (#) (( diff (f,Z)) . 0 )) by TAYLOR_1:def 5;

        hence thesis;

      end;

      for k be Nat holds P[k] from NAT_1:sch 2( A5, A1);

      hence thesis;

    end;

    theorem :: HFDIFF_1:22



     Th22: 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 Nat such that

         A2: i <= (n - 1);



         A3: i in NAT by ORDINAL1:def 12;

        (( diff (f,Z)) . i) is_differentiable_on Z by A1, A2;

        then

         A4: (r (#) (( diff (f,Z)) . i)) is_differentiable_on Z by FDIFF_2: 19;

        i <= n by A2, WSIERP_1: 18;

        hence (( diff ((r (#) f),Z)) . i) is_differentiable_on Z by A1, A4, Th21, TAYLOR_1: 23, A3;

      end;

      hence thesis;

    end;

    theorem :: HFDIFF_1:23

    f is_differentiable_on Z implies (( diff (f,Z)) . 1) = (f `| Z)

    proof

      assume

       A1: f is_differentiable_on Z;

      then

       A2: ( dom (f `| Z)) = Z by FDIFF_1:def 7;



       A3: for x be Element of REAL st x in Z holds ((( diff (f,Z)) . 1) . x) = ((f `| Z) . x)

      proof

        let x be Element of REAL ;

        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;

      ( 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 A1, FDIFF_1:def 7;

      hence thesis by A2, A3, PARTFUN1: 5;

    end;

    theorem :: HFDIFF_1:24

    n >= 1 & f1 is_differentiable_on (n,Z) implies (( diff (f1,Z)) . 1) = (f1 `| Z)

    proof

      assume n >= 1 & f1 is_differentiable_on (n,Z);

      then

       A1: f1 is_differentiable_on Z by Th7;

      (( 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 A1, FDIFF_2: 16;

      hence thesis;

    end;

    theorem :: HFDIFF_1:25

    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: 5;



         A3: (( diff ( sin ,Z)) . i) is_differentiable_on Z by 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 A3, FDIFF_1:def 7;

        then

         A4: 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 A2, Th21

        .= (r * ((( diff ( sin ,Z)) . n) . x)) by A4, VALUED_1:def 5

        .= (r * ( sin . (x + ((n * PI ) / 2)))) by A1, Th11;

        hence thesis;

      end;

        suppose

         A5: n = 0 ;



         A6: ( dom (r (#) ( sin | Z))) = ( dom ( sin | Z)) by VALUED_1:def 5

        .= Z by Th1;

        ((( diff ((r (#) sin ),Z)) . n) . x) = ((r (#) (( diff ( sin ,Z)) . 0 )) . x) by A2, A5, Th21

        .= ((r (#) ( sin | Z)) . x) by TAYLOR_1:def 5

        .= (r * (( sin | Z) . x)) by A1, A6, VALUED_1:def 5

        .= (r * ( sin . (x + ((n * PI ) / 2)))) by A1, A5, FUNCT_1: 49;

        hence thesis;

      end;

    end;

    theorem :: HFDIFF_1:26

    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: 5;



         A3: (( diff ( cos ,Z)) . i) is_differentiable_on Z by 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 A3, FDIFF_1:def 7;

        then

         A4: 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 A2, Th21

        .= (r * ((( diff ( cos ,Z)) . n) . x)) by A4, VALUED_1:def 5

        .= (r * ( cos . (x + ((n * PI ) / 2)))) by A1, Th14;

        hence thesis;

      end;

        suppose

         A5: n = 0 ;



         A6: ( dom (r (#) ( cos | Z))) = ( dom ( cos | Z)) by VALUED_1:def 5

        .= Z by Th1;

        ((( diff ((r (#) cos ),Z)) . n) . x) = ((r (#) (( diff ( cos ,Z)) . 0 )) . x) by A2, A5, Th21

        .= ((r (#) ( cos | Z)) . x) by TAYLOR_1:def 5

        .= (r * (( cos | Z) . x)) by A1, A6, VALUED_1:def 5

        .= (r * ( cos . (x + ((n * PI ) / 2)))) by A1, A5, FUNCT_1: 49;

        hence thesis;

      end;

    end;

    theorem :: HFDIFF_1:27

    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: 5;



         A3: (( diff ( exp_R ,Z)) . i) is_differentiable_on Z by 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 A3, FDIFF_1:def 7;

        then

         A4: 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 Th21, TAYLOR_2: 10

        .= (r * ((( diff ( exp_R ,Z)) . n) . x)) by A4, VALUED_1:def 5

        .= (r * ( exp_R . x)) by A1, TAYLOR_2: 7;

        hence thesis;

      end;

        suppose

         A5: n = 0 ;



         A6: ( dom (r (#) ( exp_R | Z))) = ( dom ( exp_R | Z)) by VALUED_1:def 5

        .= Z by Th1;

        ((( diff ((r (#) exp_R ),Z)) . n) . x) = ((r (#) (( diff ( exp_R ,Z)) . 0 )) . x) by A5, Th21, TAYLOR_2: 10

        .= ((r (#) ( exp_R | Z)) . x) by TAYLOR_1:def 5

        .= (r * (( exp_R | Z) . x)) by A1, A6, VALUED_1:def 5

        .= (r * ( exp_R . x)) by A1, FUNCT_1: 49;

        hence thesis;

      end;

    end;

    theorem :: HFDIFF_1:28



     Th28: (( #Z n) `| Z) = ((n (#) ( #Z (n - 1))) | Z)

    proof

      ( dom (n (#) ( #Z (n - 1)))) = ( dom ( #Z (n - 1))) by VALUED_1:def 5;

      then

       A1: ( dom (n (#) ( #Z (n - 1)))) = REAL by FUNCT_2:def 1;

      then (n (#) ( #Z (n - 1))) is Function of REAL , REAL by FUNCT_2: 67;

      then

       A2: ( dom ((n (#) ( #Z (n - 1))) | Z)) = Z by Th1;



       A3: ( #Z n) is_differentiable_on Z by Th8, FDIFF_1: 26;



       A4: for x be Element of REAL st x in Z holds ((( #Z n) `| Z) . x) = (((n (#) ( #Z (n - 1))) | Z) . x)

      proof

        let x be Element of REAL such that

         A5: x in Z;

        ((( #Z n) `| Z) . x) = ( diff (( #Z n),x)) by A3, A5, FDIFF_1:def 7

        .= (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 A1, VALUED_1:def 5

        .= (((n (#) ( #Z (n - 1))) | Z) . x) by A2, A5, FUNCT_1: 47;

        hence thesis;

      end;

      ( dom (( #Z n) `| Z)) = Z by A3, FDIFF_1:def 7;

      hence thesis by A2, A4, PARTFUN1: 5;

    end;

    theorem :: HFDIFF_1:29



     Th29: x <> 0 implies (( #Z n) ^ ) is_differentiable_in x & ( diff ((( #Z n) ^ ),x)) = ( - ((n * (x #Z (n - 1))) / ((x #Z n) ^2 )))

    proof



       A1: (( #Z n) . x) = (x #Z n) & (x #Z n) = (x |^ n) by PREPOWER: 36, TAYLOR_1:def 1;

      assume x <> 0 ;

      then

       A2: (( #Z n) . x) <> 0 by A1, PREPOWER: 5;



       A3: ( #Z n) is_differentiable_in x by TAYLOR_1: 2;



      then ( diff ((( #Z n) ^ ),x)) = ( - (( diff (( #Z n),x)) / ((( #Z n) . x) ^2 ))) by A2, FDIFF_2: 15

      .= ( - ((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 A2, A3, FDIFF_2: 15;

    end;

    theorem :: HFDIFF_1:30



     Th30: n >= 1 implies (( diff (( #Z n),Z)) . 2) = (((n * (n - 1)) (#) ( #Z (n - 2))) | Z)

    proof

      assume n >= 1;

      then

      reconsider m = (n - 1) as Element of NAT by INT_1: 5;



       A1: ( #Z n) is_differentiable_on Z by Th8, FDIFF_1: 26;



       A2: ( #Z m) is_differentiable_on Z by Th8, FDIFF_1: 26;

      then

       A3: ((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 A1, FDIFF_2: 16

      .= ((((m + 1) (#) ( #Z ((m + 1) - 1))) | Z) `| Z) by Th28

      .= (((m + 1) (#) ( #Z m)) `| Z) by A3, FDIFF_2: 16

      .= ((m + 1) (#) (( #Z m) `| Z)) by A2, FDIFF_2: 19

      .= ((m + 1) (#) ((m (#) ( #Z (m - 1))) | Z)) by Th28

      .= (((m + 1) (#) (m (#) ( #Z (m - 1)))) | Z) by RFUNCT_1: 49

      .= (((n * (n - 1)) (#) ( #Z (n - 2))) | Z) by RFUNCT_1: 17;

      hence thesis;

    end;

    theorem :: HFDIFF_1:31

    n >= 2 implies (( diff (( #Z n),Z)) . 3) = ((((n * (n - 1)) * (n - 2)) (#) ( #Z (n - 3))) | Z)

    proof

      assume

       A1: 2 <= n;

      then

       A2: (2 + ( - 1)) <= (n + 0 ) by XREAL_1: 7;

      reconsider m = (n - 2) as Element of NAT by A1, INT_1: 5;



       A3: ( #Z m) is_differentiable_on Z by Th8, FDIFF_1: 26;

      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 A2, Th30

      .= ((((m + 2) * (m + 1)) (#) ( #Z m)) `| Z) by A4, FDIFF_2: 16

      .= (((m + 2) * (m + 1)) (#) (( #Z m) `| Z)) by A3, FDIFF_2: 19

      .= (((m + 2) * (m + 1)) (#) ((m (#) ( #Z (m - 1))) | Z)) by Th28

      .= (((n * (n - 1)) (#) ((n - 2) (#) ( #Z (n - 3)))) | Z) by RFUNCT_1: 49

      .= ((((n * (n - 1)) * (n - 2)) (#) ( #Z (n - 3))) | Z) by RFUNCT_1: 17;

      hence thesis;

    end;



     Lm1: n > 1 implies (((m ! ) / (n ! )) * n) = ((m ! ) / ((n -' 1) ! ))

    proof

      assume

       A1: n > 1;

      then (n - 1) = (n -' 1) by XREAL_1: 233;

      then n = ((n -' 1) + 1);



      then (((m ! ) / (n ! )) * n) = (((m ! ) / (((n -' 1) ! ) * n)) * n) by NEWTON: 15

      .= ((m ! ) / ((n -' 1) ! )) by A1, XCMPLX_1: 92;

      hence thesis;

    end;

    theorem :: HFDIFF_1:32



     Th32: 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: for k st P[k] holds P[(k + 1)]

      proof

        let k such that

         A2: P[k];

        assume

         A3: n > (k + 1);

        then

         A4: (n - k) > ((k + 1) - k) by XREAL_1: 9;



         A5: ((k + 1) + ( - 1)) <= (n + 0 ) by A3, XREAL_1: 7;

        then

        reconsider l = (n - k) as Element of NAT by INT_1: 5;

        l >= ((k + 1) - k) by A3, XREAL_1: 9;

        then

         A6: ((k + 1) ! ) > 0 & (l -' 1) = ((n - k) - 1) by XREAL_1: 233;

        reconsider s = (n - (k + 1)) as Element of NAT by A3, INT_1: 5;



         A7: ( #Z l) is_differentiable_on Z by Th8, FDIFF_1: 26;

        then

         A8: (((n choose k) * (k ! )) (#) ( #Z l)) is_differentiable_on Z by FDIFF_2: 19;

        ( 0 + k) < (1 + k) by XREAL_1: 6;



        then (( diff (( #Z n),Z)) . (k + 1)) = (((((n choose k) * (k ! )) (#) ( #Z l)) | Z) `| Z) by A2, A3, TAYLOR_1:def 5, XXREAL_0: 2

        .= ((((n choose k) * (k ! )) (#) ( #Z l)) `| Z) by A8, FDIFF_2: 16

        .= (((n choose k) * (k ! )) (#) (( #Z l) `| Z)) by A7, FDIFF_2: 19

        .= (((n choose k) * (k ! )) (#) ((l (#) ( #Z (l - 1))) | Z)) by Th28

        .= ((((n choose k) * (k ! )) (#) (l (#) ( #Z (l - 1)))) | Z) by RFUNCT_1: 49

        .= (((((n choose k) * (k ! )) * l) (#) ( #Z (l - 1))) | Z) by RFUNCT_1: 17

        .= ((((((n ! ) / ((k ! ) * (l ! ))) * (k ! )) * (n - k)) (#) ( #Z (l - 1))) | Z) by A5, NEWTON:def 3

        .= (((((n ! ) / (l ! )) * l) (#) ( #Z (l - 1))) | Z) by XCMPLX_1: 92

        .= ((((n ! ) / ((l -' 1) ! )) (#) ( #Z (l - 1))) | Z) by A4, Lm1

        .= (((((n ! ) / ((s ! ) * ((k + 1) ! ))) * ((k + 1) ! )) (#) ( #Z ((n - k) - 1))) | Z) by A6, XCMPLX_1: 92

        .= ((((n choose (k + 1)) * ((k + 1) ! )) (#) ( #Z (n - (k + 1)))) | Z) by A3, NEWTON:def 3;

        hence thesis;

      end;



       A9: 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: 21

        .= ((((n choose 0 ) * ( 0 ! )) (#) ( #Z (n - 0 ))) | Z) by NEWTON: 12, NEWTON: 19;

        hence thesis;

      end;

      for k holds P[k] from NAT_1:sch 2( A9, A1);

      hence thesis;

    end;

    theorem :: HFDIFF_1:33

    f is_differentiable_on (n,Z) implies (( diff (( - f),Z)) . n) = ( - (( diff (f,Z)) . n)) & ( - f) is_differentiable_on (n,Z) by Th21, Th22;

    theorem :: HFDIFF_1:34

    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 ( 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 A1, Th14;

      (( 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 A1, Th11;

      hence thesis by A2;

    end;

    theorem :: HFDIFF_1:35

    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



       A1: |.( 0 - 0 ).| = 0 by ABSVALUE: 2;

      assume r > 0 ;

      then

       A2: 0 in ].( 0 - r), ( 0 + r).[ by A1, RCOMP_1: 1;



       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 A2, Th14;

      (( 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 A2, Th11;

      hence thesis by A3;

    end;

    theorem :: HFDIFF_1:36



     Th36: n > m & x in Z implies ((( diff (( #Z n),Z)) . m) . x) = (((n choose m) * (m ! )) * (x #Z (n - m)))

    proof

      assume that

       A1: n > m and

       A2: x in Z;

      ( dom ( #Z (n - m))) = REAL by FUNCT_2:def 1;

      then

       A3: ( dom (((n choose m) * (m ! )) (#) ( #Z (n - m)))) = REAL by VALUED_1:def 5;



      then

       A4: ( dom ((((n choose m) * (m ! )) (#) ( #Z (n - m))) | Z)) = ( REAL /\ Z) by RELAT_1: 61

      .= Z by XBOOLE_1: 28;

      reconsider xx = x as Element of REAL by XREAL_0:def 1;

      ((( diff (( #Z n),Z)) . m) . x) = (((((n choose m) * (m ! )) (#) ( #Z (n - m))) | Z) . x) by A1, Th32

      .= ((((n choose m) * (m ! )) (#) ( #Z (n - m))) . x) by A2, A4, FUNCT_1: 47

      .= (((n choose m) * (m ! )) * (( #Z (n - m)) . xx)) by A3, VALUED_1:def 5

      .= (((n choose m) * (m ! )) * (x #Z (n - m))) by TAYLOR_1:def 1;

      hence thesis;

    end;

    theorem :: HFDIFF_1:37



     Th37: 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: 5;



         A2: ( 0 + n) < (n + 1) by XREAL_1: 6;



         A3: ( #Z 1) is_differentiable_on Z by Th8, FDIFF_1: 26;

        then

         A4: (((n + 1) ! ) (#) ( #Z 1)) is_differentiable_on Z by FDIFF_2: 19;

        Z c= ( dom ( #Z 1)) by A3, FDIFF_1:def 6;

        then

         A5: 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 A2, Th32

        .= ((((((((n + 1) ! ) / ((n ! ) * 1)) * (n ! )) (#) ( #Z ((n + 1) - n))) | Z) `| Z) . x) by A2, NEWTON: 13, NEWTON:def 3

        .= (((((((n + 1) ! ) / 1) (#) ( #Z 1)) | Z) `| Z) . x) by XCMPLX_1: 92

        .= (((((n + 1) ! ) (#) ( #Z 1)) `| Z) . x) by A4, FDIFF_2: 16

        .= (((n + 1) ! ) * ( diff (( #Z 1),x))) by A1, A3, A5, FDIFF_1: 20

        .= (((n + 1) ! ) * (1 * (x #Z (1 - 1)))) by TAYLOR_1: 2

        .= (((n + 1) ! ) * 1) by PREPOWER: 34

        .= (m ! );

        hence thesis;

      end;

        suppose

         A6: 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: 49

        .= (x #Z 0 ) by TAYLOR_1:def 1

        .= (m ! ) by A6, NEWTON: 12, PREPOWER: 34;

        hence thesis;

      end;

    end;

    theorem :: HFDIFF_1:38



     Th38: ( #Z n) is_differentiable_on (n,Z)

    proof

      let i be Nat;

      assume

       A1: i <= (n - 1);

      reconsider i as Element of NAT by ORDINAL1:def 12;

      (( - 1) + n) < ( 0 + n) by XREAL_1: 6;

      then

       A2: i < n by A1, XXREAL_0: 2;



       A3: for x be Real st x in Z holds ((( diff (( #Z n),Z)) . i) | Z) is_differentiable_in x

      proof

        (i + 0 ) <= ((n - 1) + 1) by A1, XREAL_1: 8;

        then

        reconsider m = (n - i) as Element of NAT by INT_1: 5;



         A4: ( #Z m) is_differentiable_on Z by Th8, FDIFF_1: 26;

        let x be Real;

        assume x in Z;

        then

         A5: (( #Z m) | Z) is_differentiable_in x by A4, FDIFF_1:def 6;

        ((( diff (( #Z n),Z)) . i) | Z) = (((((n choose i) * (i ! )) (#) ( #Z m)) | Z) | Z) by A2, Th32

        .= ((((n choose i) * (i ! )) (#) ( #Z m)) | Z) by FUNCT_1: 51

        .= (((n choose i) * (i ! )) (#) (( #Z m) | Z)) by RFUNCT_1: 49;

        hence thesis by A5, FDIFF_1: 15;

      end;

      ( dom ( #Z (n - i))) = REAL by FUNCT_2:def 1;

      then

       A6: ( dom (((n choose i) * (i ! )) (#) ( #Z (n - i)))) = REAL by VALUED_1:def 5;

      ( dom (( diff (( #Z n),Z)) . i)) = ( dom ((((n choose i) * (i ! )) (#) ( #Z (n - i))) | Z)) by A2, Th32

      .= ( REAL /\ Z) by A6, RELAT_1: 61

      .= Z by XBOOLE_1: 28;

      hence thesis by A3, FDIFF_1:def 6;

    end;

    theorem :: HFDIFF_1:39

    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;

      ( dom ( #Z (n - m))) = REAL by FUNCT_2:def 1;

      then

       A3: ( dom (((n choose m) * (m ! )) (#) ( #Z (n - m)))) = REAL by VALUED_1:def 5;



       A4: ( dom (( diff (( #Z n),Z)) . m)) = ( dom ((((n choose m) * (m ! )) (#) ( #Z (n - m))) | Z)) by A2, Th32

      .= ( REAL /\ Z) by A3, RELAT_1: 61

      .= Z by XBOOLE_1: 28;



       A5: ( dom (a (#) (( diff (( #Z n),Z)) . m))) = ( dom (( diff (( #Z n),Z)) . m)) by VALUED_1:def 5;

      ( #Z n) is_differentiable_on (m,Z) by A2, Th38, TAYLOR_1: 23;



      then ((( diff ((a (#) ( #Z n)),Z)) . m) . x) = ((a (#) (( diff (( #Z n),Z)) . m)) . x) by Th21

      .= (a * ((( diff (( #Z n),Z)) . m) . x)) by A1, A4, A5, VALUED_1:def 5

      .= (a * (((n choose m) * (m ! )) * (x #Z (n - m)))) by A1, A2, Th36;

      hence thesis;

    end;

    theorem :: HFDIFF_1:40

    x in Z implies ((( diff ((a (#) ( #Z n)),Z)) . n) . x) = (a * (n ! ))

    proof

      assume

       A1: x in Z;

      reconsider xx = x as Element of REAL by XREAL_0:def 1;

      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: 5;



         A2: ( dom (a (#) (( diff (( #Z n),Z)) . n))) = ( dom (( diff (( #Z n),Z)) . n)) by VALUED_1:def 5;

        ( #Z n) is_differentiable_on (n,Z) by Th38;

        then

         A3: (( diff (( #Z n),Z)) . m) is_differentiable_on Z;



         A4: ( 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 A3, FDIFF_1:def 7;

        ((( diff ((a (#) ( #Z n)),Z)) . n) . x) = ((a (#) (( diff (( #Z n),Z)) . n)) . x) by Th21, Th38

        .= (a * ((( diff (( #Z n),Z)) . n) . x)) by A1, A4, A2, VALUED_1:def 5

        .= (a * (n ! )) by A1, Th37;

        hence thesis;

      end;

        suppose

         A5: n = 0 ;

        ( dom ( #Z 0 )) = REAL by FUNCT_2:def 1;

        then

         A6: ( 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 A5, Th21, Th38

        .= ((a (#) (( #Z 0 ) | Z)) . x) by TAYLOR_1:def 5

        .= (((a (#) ( #Z 0 )) | Z) . x) by RFUNCT_1: 49

        .= ((a (#) ( #Z 0 )) . x) by A1, FUNCT_1: 49

        .= (a * (( #Z 0 ) . xx)) by A6, VALUED_1:def 5

        .= (a * (x #Z 0 )) by TAYLOR_1:def 1

        .= (a * (n ! )) by A5, NEWTON: 12, PREPOWER: 34;

        hence thesis;

      end;

    end;

    theorem :: HFDIFF_1:41



     Th41: 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: (( 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 A1, Th37

      .= ((x - x0) |^ n) by XCMPLX_1: 89;

      (( 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 A1, A2, Th36

      .= ((((n choose m) * ((x0 #Z (n - m)) * ((x - x0) |^ m))) * (m ! )) / (m ! ))

      .= (((n choose m) * (x0 #Z (n - m))) * ((x - x0) |^ m)) by XCMPLX_1: 89;

      hence thesis by A3;

    end;

    theorem :: HFDIFF_1:42

    for n,m be Element of NAT , r,x be Element of 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 Element of REAL ;

      assume that

       A1: n > m and

       A2: r > 0 ;

       |.( 0 - 0 ).| = 0 by ABSVALUE: 2;

      then

       A3: 0 in ].( 0 - r), ( 0 + r).[ by A2, RCOMP_1: 1;

      reconsider s = (n - m) as Element of NAT by A1, INT_1: 5;



       A4: (n - m) > (m - m) by A1, XREAL_1: 9;



       A5: (( Maclaurin (( #Z n), ].( - r), r.[,x)) . n) = (( Taylor (( #Z n), ].( - r), r.[, 0 ,x)) . n) by TAYLOR_2:def 1

      .= ((x - 0 ) |^ n) by A1, A3, Th41

      .= (x |^ n);

      (( 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 A1, A3, Th41

      .= (((n choose m) * ( 0 |^ s)) * (x |^ m)) by PREPOWER: 36

      .= (((n choose m) * 0 ) * (x |^ m)) by A4, NEWTON: 84

      .= 0 ;

      hence thesis by A5;

    end;

    theorem :: HFDIFF_1:43



     Th43: not 0 in Z implies (( #Z n) ^ ) is_differentiable_on Z

    proof

      assume

       A1: not 0 in Z;



       A2: for x0 st x0 in Z holds (( #Z n) . x0) <> 0

      proof

        let x0;



         A3: (( #Z n) . x0) = (x0 #Z n) by TAYLOR_1:def 1;

        assume x0 in Z;

        hence thesis by A1, A3, PREPOWER: 38;

      end;

      ( #Z n) is_differentiable_on Z by Th8, FDIFF_1: 26;

      hence thesis by A2, FDIFF_2: 22;

    end;

    theorem :: HFDIFF_1:44

     not 0 in Z & x0 in Z implies (((( #Z n) ^ ) `| Z) . x0) = ( - (n / (( #Z (n + 1)) . x0)))

    proof

      assume that

       A1: not 0 in Z and

       A2: x0 in Z;



       A3: (( #Z n) ^ ) is_differentiable_on Z by A1, Th43;

      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: 5;

        (x0 #Z i) <> 0 by A1, A2, PREPOWER: 38;

        then

         A4: (x0 |^ i) <> 0 by PREPOWER: 36;

        (((( #Z n) ^ ) `| Z) . x0) = ( diff ((( #Z n) ^ ),x0)) by A2, A3, FDIFF_1:def 7

        .= ( - ((n * (x0 #Z i)) / ((x0 #Z n) ^2 ))) by A1, A2, Th29

        .= ( - ((n * (x0 #Z i)) / ((x0 |^ n) ^2 ))) by PREPOWER: 36

        .= ( - ((n * (x0 |^ i)) / ((x0 |^ n) ^2 ))) by PREPOWER: 36

        .= ( - ((n * (x0 |^ i)) / ((x0 |^ (i + 1)) * ((x0 |^ 1) * (x0 |^ i))))) by NEWTON: 8

        .= ( - ((n * (x0 |^ i)) / (((x0 |^ (i + 1)) * (x0 |^ 1)) * (x0 |^ i))))

        .= ( - ((n * (x0 |^ i)) / ((x0 |^ ((i + 1) + 1)) * (x0 |^ i)))) by NEWTON: 8

        .= ( - (n / (x0 |^ (i + 2)))) by A4, XCMPLX_1: 91

        .= ( - (n / (x0 #Z (i + 2)))) by PREPOWER: 36

        .= ( - (n / (( #Z (n + 1)) . x0))) by TAYLOR_1:def 1;

        hence thesis;

      end;

        suppose

         A5: n = 0 ;

        (((( #Z n) ^ ) `| Z) . x0) = ( diff ((( #Z n) ^ ),x0)) by A2, A3, FDIFF_1:def 7

        .= ( - (( 0 * (x0 #Z (n - 1))) / ((x0 #Z n) ^2 ))) by A1, A2, A5, Th29

        .= ( - (n / (( #Z (n + 1)) . x0))) by A5;

        hence thesis;

      end;

    end;



     Lm2: ( #Z 1) = ( id REAL )

    proof

      for x be Element of REAL holds (( #Z 1) . x) = (( id REAL ) . x)

      proof

        let x be Element of REAL ;

        (( #Z 1) . x) = (x #Z 1) by TAYLOR_1:def 1

        .= x by PREPOWER: 35

        .= (( id REAL ) . x);

        hence thesis;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: HFDIFF_1:45



     Th45: x <> 0 implies (( id REAL ) ^ ) is_differentiable_in x & ( diff ((( id REAL ) ^ ),x)) = ( - (1 / (x ^2 )))

    proof

      set f = ( id REAL );

      assume

       A1: x <> 0 ;

      reconsider xx = x as Element of REAL by XREAL_0:def 1;

      (f . x) = (x #Z 1) & (x #Z 1) = (x |^ 1) by Lm2, PREPOWER: 36, TAYLOR_1:def 1;

      then

       A2: (f . x) <> 0 by A1;



       A3: f is_differentiable_in x by Lm2, TAYLOR_1: 2;



      then ( diff ((f ^ ),x)) = ( - (( diff (f,x)) / ((f . x) ^2 ))) by A2, FDIFF_2: 15

      .= ( - ((1 * (x #Z (1 - 1))) / ((f . xx) ^2 ))) by Lm2, TAYLOR_1: 2

      .= ( - ((1 * (x #Z 0 )) / (x ^2 )))

      .= ( - (1 / (x ^2 ))) by PREPOWER: 34;

      hence thesis by A2, A3, FDIFF_2: 15;

    end;

    theorem :: HFDIFF_1:46

     not 0 in Z implies ((( id REAL ) ^ ) `| Z) = ((( - 1) (#) (( #Z 2) ^ )) | Z)

    proof

      assume

       A1: not 0 in Z;

      then (( id REAL ) ^ ) is_differentiable_on Z by Lm2, Th43;

      then

       A2: ( dom ((( id REAL ) ^ ) `| Z)) = Z by FDIFF_1:def 7;



       A3: ( dom (( #Z 2) ^ )) = ( REAL \ { 0 }) by Th3;

      then

       A4: Z c= ( dom (( #Z 2) ^ )) by A1, ZFMISC_1: 34;



       A5: for x0 be Element of REAL st x0 in Z holds (((( id REAL ) ^ ) `| Z) . x0) = (((( - 1) (#) (( #Z 2) ^ )) | Z) . x0)

      proof



         A6: ( dom (( - 1) (#) (( #Z 2) ^ ))) = ( dom (( #Z (1 + 1)) ^ )) by VALUED_1:def 5;

        let x0 be Element of REAL ;

        assume

         A7: x0 in Z;

        (( id REAL ) ^ ) is_differentiable_on Z by A1, Lm2, Th43;



        then (((( id REAL ) ^ ) `| Z) . x0) = ( diff ((( id REAL ) ^ ),x0)) by A7, FDIFF_1:def 7

        .= ( - (1 / (x0 ^2 ))) by A1, A7, Th45

        .= ( - (1 / (x0 |^ (1 + 1)))) by NEWTON: 81

        .= ( - (1 / (x0 #Z 2))) by PREPOWER: 36

        .= ( - (1 / (( #Z 2) . x0))) by TAYLOR_1:def 1

        .= ( - (1 * ((( #Z 2) . x0) " ))) by XCMPLX_0:def 9

        .= ( - (1 * ((( #Z 2) ^ ) . x0))) by A4, A7, RFUNCT_1:def 2

        .= (( - 1) * ((( #Z 2) ^ ) . x0))

        .= ((( - 1) (#) (( #Z 2) ^ )) . x0) by A4, A7, A6, VALUED_1:def 5

        .= (((( - 1) (#) (( #Z 2) ^ )) | Z) . x0) by A7, FUNCT_1: 49;

        hence thesis;

      end;

      ( dom ((( - 1) (#) (( #Z (1 + 1)) ^ )) | Z)) = (( dom (( - 1) (#) (( #Z 2) ^ ))) /\ Z) by RELAT_1: 61

      .= (( dom (( #Z 2) ^ )) /\ Z) by VALUED_1:def 5

      .= Z by A1, A3, XBOOLE_1: 28, ZFMISC_1: 34;

      hence thesis by A2, A5, PARTFUN1: 5;

    end;

    theorem :: HFDIFF_1:47



     Th47: x <> 0 implies (( #Z 2) ^ ) is_differentiable_in x & ( diff ((( #Z 2) ^ ),x)) = ( - ((2 * x) / ((x #Z 2) ^2 )))

    proof



       A1: (( #Z 2) . x) = (x #Z 2) & (x #Z 2) = (x |^ 2) by PREPOWER: 36, TAYLOR_1:def 1;

      assume x <> 0 ;

      then

       A2: (( #Z 2) . x) <> 0 by A1, PREPOWER: 5;



       A3: ( #Z 2) is_differentiable_in x by TAYLOR_1: 2;



      then ( diff ((( #Z 2) ^ ),x)) = ( - (( diff (( #Z 2),x)) / ((( #Z 2) . x) ^2 ))) by A2, FDIFF_2: 15

      .= ( - ((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

      .= ( - ((2 * x) / ((x #Z 2) ^2 ))) by PREPOWER: 35;

      hence thesis by A2, A3, FDIFF_2: 15;

    end;

    theorem :: HFDIFF_1:48

     not 0 in Z implies ((( #Z 2) ^ ) `| Z) = ((( - 2) (#) (( #Z 3) ^ )) | Z)

    proof

      assume

       A1: not 0 in Z;

      then (( #Z 2) ^ ) is_differentiable_on Z by Th43;

      then

       A2: ( dom ((( #Z 2) ^ ) `| Z)) = Z by FDIFF_1:def 7;

      Z c= ( REAL \ { 0 }) by A1, ZFMISC_1: 34;

      then

       A3: Z c= ( dom (( #Z 3) ^ )) by Th3;



       A4: for x0 be Element of REAL st x0 in Z holds (((( #Z 2) ^ ) `| Z) . x0) = (((( - 2) (#) (( #Z 3) ^ )) | Z) . x0)

      proof

        reconsider i = (2 - 1) as Element of NAT ;

        let x0 be Element of REAL ;



         A5: ( dom (( - 2) (#) (( #Z 3) ^ ))) = ( dom (( #Z 3) ^ )) by VALUED_1:def 5;

        assume

         A6: x0 in Z;

        then (x0 #Z i) <> 0 by A1, PREPOWER: 38;

        then

         A7: (x0 |^ i) <> 0 by PREPOWER: 36;

        (( #Z 2) ^ ) is_differentiable_on Z by A1, Th43;



        then (((( #Z 2) ^ ) `| Z) . x0) = ( diff ((( #Z 2) ^ ),x0)) by A6, FDIFF_1:def 7

        .= ( - ((2 * x0) / ((x0 #Z 2) ^2 ))) by A1, A6, Th47

        .= ( - ((2 * (x0 #Z 1)) / ((x0 #Z 2) ^2 ))) by PREPOWER: 35

        .= ( - ((2 * (x0 #Z 1)) / ((x0 |^ 2) ^2 ))) by PREPOWER: 36

        .= ( - ((2 * (x0 |^ 1)) / ((x0 |^ 2) * (x0 |^ (1 + 1))))) by PREPOWER: 36

        .= ( - ((2 * (x0 |^ 1)) / ((x0 |^ 2) * ((x0 |^ 1) * (x0 |^ 1))))) by NEWTON: 8

        .= ( - ((2 * (x0 |^ 1)) / (((x0 |^ 2) * (x0 |^ 1)) * (x0 |^ 1))))

        .= ( - ((2 * (x0 |^ 1)) / ((x0 |^ (2 + 1)) * (x0 |^ 1)))) by NEWTON: 8

        .= ( - (2 / (x0 |^ (1 + 2)))) by A7, XCMPLX_1: 91

        .= ( - (2 / (x0 #Z 3))) by PREPOWER: 36

        .= ( - (2 / (( #Z 3) . x0))) by TAYLOR_1:def 1

        .= ( - (2 * ((( #Z 3) . x0) " ))) by XCMPLX_0:def 9

        .= ( - (2 * ((( #Z 3) ^ ) . x0))) by A3, A6, RFUNCT_1:def 2

        .= (( - 2) * ((( #Z 3) ^ ) . x0))

        .= ((( - 2) (#) (( #Z 3) ^ )) . x0) by A3, A6, A5, VALUED_1:def 5

        .= (((( - 2) (#) (( #Z 3) ^ )) | Z) . x0) by A6, FUNCT_1: 49;

        hence thesis;

      end;

      ( dom ((( - 2) (#) (( #Z 3) ^ )) | Z)) = (( dom (( - 2) (#) (( #Z 3) ^ ))) /\ Z) by RELAT_1: 61

      .= (( dom (( #Z 3) ^ )) /\ Z) by VALUED_1:def 5

      .= Z by A3, XBOOLE_1: 28;

      hence thesis by A2, A4, PARTFUN1: 5;

    end;

    theorem :: HFDIFF_1:49



     Th49: not 0 in Z & n >= 1 implies ((( #Z n) ^ ) `| Z) = ((( - n) (#) (( #Z (n + 1)) ^ )) | Z)

    proof

      assume that

       A1: not 0 in Z and

       A2: n >= 1;

      (n + 1) >= (1 + 0 ) & Z c= ( REAL \ { 0 }) by A1, XREAL_1: 7, ZFMISC_1: 34;

      then

       A3: Z c= ( dom (( #Z (n + 1)) ^ )) by Th3;



       A4: for x0 be Element of REAL st x0 in Z holds (((( #Z n) ^ ) `| Z) . x0) = (((( - n) (#) (( #Z (n + 1)) ^ )) | Z) . x0)

      proof

        (n + 1) >= (1 + 0 ) & Z c= ( REAL \ { 0 }) by A1, XREAL_1: 7, ZFMISC_1: 34;

        then

         A5: Z c= ( dom (( #Z (n + 1)) ^ )) by Th3;

        reconsider i = (n - 1) as Element of NAT by A2, INT_1: 5;

        let x0 be Element of REAL ;



         A6: ( dom (( - n) (#) (( #Z (n + 1)) ^ ))) = ( dom (( #Z (n + 1)) ^ )) by VALUED_1:def 5;

        assume

         A7: x0 in Z;

        then (x0 #Z i) <> 0 by A1, PREPOWER: 38;

        then

         A8: (x0 |^ i) <> 0 by PREPOWER: 36;

        (( #Z n) ^ ) is_differentiable_on Z by A1, Th43;



        then (((( #Z n) ^ ) `| Z) . x0) = ( diff ((( #Z n) ^ ),x0)) by A7, FDIFF_1:def 7

        .= ( - ((n * (x0 #Z (n - 1))) / ((x0 #Z n) ^2 ))) by A1, A7, Th29

        .= ( - ((n * (x0 #Z i)) / ((x0 |^ n) ^2 ))) by PREPOWER: 36

        .= ( - ((n * (x0 |^ i)) / ((x0 |^ n) ^2 ))) by PREPOWER: 36

        .= ( - ((n * (x0 |^ i)) / ((x0 |^ (i + 1)) * ((x0 |^ 1) * (x0 |^ i))))) by NEWTON: 8

        .= ( - ((n * (x0 |^ i)) / (((x0 |^ (i + 1)) * (x0 |^ 1)) * (x0 |^ i))))

        .= ( - ((n * (x0 |^ i)) / ((x0 |^ ((i + 1) + 1)) * (x0 |^ i)))) by NEWTON: 8

        .= ( - (n / (x0 |^ (i + 2)))) by A8, XCMPLX_1: 91

        .= ( - (n / (x0 #Z (i + 2)))) by PREPOWER: 36

        .= ( - (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 A7, A5, RFUNCT_1:def 2

        .= (( - n) * ((( #Z (n + 1)) ^ ) . x0))

        .= ((( - n) (#) (( #Z (n + 1)) ^ )) . x0) by A7, A6, A5, VALUED_1:def 5

        .= (((( - n) (#) (( #Z (n + 1)) ^ )) | Z) . x0) by A7, FUNCT_1: 49;

        hence thesis;

      end;

      (( #Z n) ^ ) is_differentiable_on Z by A1, Th43;

      then

       A9: ( dom ((( #Z n) ^ ) `| Z)) = Z by FDIFF_1:def 7;

      ( dom ((( - n) (#) (( #Z (n + 1)) ^ )) | Z)) = (( dom (( - n) (#) (( #Z (n + 1)) ^ ))) /\ Z) by RELAT_1: 61

      .= (( dom (( #Z (n + 1)) ^ )) /\ Z) by VALUED_1:def 5

      .= Z by A3, XBOOLE_1: 28;

      hence thesis by A9, A4, PARTFUN1: 5;

    end;

    theorem :: HFDIFF_1:50



     Th50: 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);

      (( diff (f1,Z)) . 0 ) is_differentiable_on Z by A1;

      then (f1 | Z) is_differentiable_on Z by TAYLOR_1:def 5;

      then

       A3: f1 is_differentiable_on Z by Th6;



       A4: (( 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 A3, FDIFF_2: 16;

      (( diff (f2,Z)) . 0 ) is_differentiable_on Z by A2;

      then (f2 | Z) is_differentiable_on Z by TAYLOR_1:def 5;

      then

       A5: f2 is_differentiable_on Z by Th6;

      then

       A6: (f1 (#) f2) is_differentiable_on Z by A3, FDIFF_2: 20;

      (( 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 A5, FDIFF_2: 16;

      then

       A7: (f2 `| Z) is_differentiable_on Z by A2;

      then

       A8: (f1 (#) (f2 `| Z)) is_differentiable_on Z by A3, FDIFF_2: 20;

      (( 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 A3, FDIFF_2: 16;

      then

       A9: (f1 `| Z) is_differentiable_on Z by A1;

      then

       A10: ((f1 `| Z) (#) f2) is_differentiable_on Z by A5, FDIFF_2: 20;



       A11: (( 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 A5, FDIFF_2: 16;

      (( 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 A6, FDIFF_2: 16

      .= ((((f1 `| Z) (#) f2) + (f1 (#) (f2 `| Z))) `| Z) by A3, A5, FDIFF_2: 20

      .= ((((f1 `| Z) (#) f2) `| Z) + ((f1 (#) (f2 `| Z)) `| Z)) by A10, A8, FDIFF_2: 17

      .= (((((f1 `| Z) `| Z) (#) f2) + ((f1 `| Z) (#) (f2 `| Z))) + ((f1 (#) (f2 `| Z)) `| Z)) by A5, A9, FDIFF_2: 20

      .= ((((( diff (f1,Z)) . 2) (#) f2) + ((f1 `| Z) (#) (f2 `| Z))) + (((f1 `| Z) (#) (f2 `| Z)) + (f1 (#) (( diff (f2,Z)) . 2)))) by A3, A7, A4, A11, FDIFF_2: 20

      .= (((((( diff (f1,Z)) . 2) (#) f2) + ((f1 `| Z) (#) (f2 `| Z))) + ((f1 `| Z) (#) (f2 `| Z))) + (f1 (#) (( diff (f2,Z)) . 2))) by RFUNCT_1: 8

      .= ((((( diff (f1,Z)) . 2) (#) f2) + (((f1 `| Z) (#) (f2 `| Z)) + ((f1 `| Z) (#) (f2 `| Z)))) + (f1 (#) (( diff (f2,Z)) . 2))) by RFUNCT_1: 8

      .= ((((( diff (f1,Z)) . 2) (#) f2) + ((1 (#) ((f1 `| Z) (#) (f2 `| Z))) + ((f1 `| Z) (#) (f2 `| Z)))) + (f1 (#) (( diff (f2,Z)) . 2))) by RFUNCT_1: 21

      .= ((((( diff (f1,Z)) . 2) (#) f2) + ((1 (#) ((f1 `| Z) (#) (f2 `| Z))) + (1 (#) ((f1 `| Z) (#) (f2 `| Z))))) + (f1 (#) (( diff (f2,Z)) . 2))) by RFUNCT_1: 21

      .= ((((( diff (f1,Z)) . 2) (#) f2) + ((1 + 1) (#) ((f1 `| Z) (#) (f2 `| Z)))) + (f1 (#) (( diff (f2,Z)) . 2))) by Th5

      .= ((((( diff (f1,Z)) . 2) (#) f2) + (2 (#) ((f1 `| Z) (#) (f2 `| Z)))) + (f1 (#) (( diff (f2,Z)) . 2)));

      hence thesis;

    end;

    theorem :: HFDIFF_1:51

    Z c= ( dom ln ) & Z c= ( dom (( id REAL ) ^ )) implies ( ln `| Z) = ((( id REAL ) ^ ) | Z)

    proof

      assume that

       A1: Z c= ( dom ln ) and

       A2: Z c= ( dom (( id REAL ) ^ ));



       A3: ( dom ((( id REAL ) ^ ) | Z)) = (( dom (( id REAL ) ^ )) /\ Z) by RELAT_1: 61

      .= Z by A2, XBOOLE_1: 28;



       A4: for x0 be Element of REAL st x0 in ( dom ((( id REAL ) ^ ) | Z)) holds (( ln `| Z) . x0) = (((( id REAL ) ^ ) | Z) . x0)

      proof

        let x0 be Element of REAL ;

        assume

         A5: x0 in ( dom ((( id REAL ) ^ ) | Z));

         ln is_differentiable_on Z by A1, FDIFF_1: 26, TAYLOR_1: 18;



        then (( ln `| Z) . x0) = ( diff ( ln ,x0)) by A3, A5, FDIFF_1:def 7

        .= (1 / x0) by A1, A3, A5, TAYLOR_1: 18

        .= (1 / (( id REAL ) . x0))

        .= (1 * ((( id REAL ) . x0) " )) by XCMPLX_0:def 9

        .= (1 * ((( id REAL ) ^ ) . x0)) by A2, A3, A5, RFUNCT_1:def 2

        .= (((( id REAL ) ^ ) | Z) . x0) by A3, A5, FUNCT_1: 49;

        hence thesis;

      end;

       ln is_differentiable_on Z by A1, FDIFF_1: 26, TAYLOR_1: 18;

      then ( dom ((( id REAL ) ^ ) | Z)) = ( dom ( ln `| Z)) by A3, FDIFF_1:def 7;

      hence thesis by A4, PARTFUN1: 5;

    end;

    theorem :: HFDIFF_1:52

    n >= 1 & x0 in Z & not 0 in Z implies ((( diff ((( #Z n) ^ ),Z)) . 2) . x0) = ((n * (n + 1)) * ((( #Z (n + 2)) ^ ) . x0))

    proof

      assume that

       A1: n >= 1 and

       A2: x0 in Z and

       A3: not 0 in Z;



       A4: Z c= ( REAL \ { 0 }) by A3, ZFMISC_1: 34;

      ((n + 1) + 1) >= (1 + 0 ) by XREAL_1: 7;

      then

       A5: Z c= ( dom (( #Z (n + 2)) ^ )) by A4, Th3;



       A6: ( dom (( - (n + 1)) (#) ((( #Z (n + 2)) ^ ) | Z))) = ( dom ((( #Z (n + 2)) ^ ) | Z)) by VALUED_1:def 5

      .= (( dom (( #Z (n + 2)) ^ )) /\ Z) by RELAT_1: 61

      .= Z by A5, XBOOLE_1: 28;



       A7: (( #Z n) ^ ) is_differentiable_on Z by A3, Th43;



       A8: (n + 1) >= (1 + 0 ) by XREAL_1: 7;

      reconsider m = ( - n) as Element of REAL by XREAL_0:def 1;



       A9: (( #Z (n + 1)) ^ ) is_differentiable_on Z by A3, Th43;

      then

       A10: (m (#) (( #Z (n + 1)) ^ )) is_differentiable_on Z by FDIFF_2: 19;

      ( dom (m (#) (( #Z (n + 1)) ^ ))) = ( dom (( #Z (n + 1)) ^ )) by VALUED_1:def 5;

      then

       A11: Z c= ( dom (( - n) (#) (( #Z (n + 1)) ^ ))) by A8, A4, Th3;

      ((( diff ((( #Z n) ^ ),Z)) . 2) . x0) = ((( diff ((( #Z n) ^ ),Z)) . (1 + 1)) . x0)

      .= (((( diff ((( #Z n) ^ ),Z)) . (1 + 0 )) `| Z) . x0) by TAYLOR_1:def 5

      .= ((((( diff ((( #Z n) ^ ),Z)) . 0 ) `| Z) `| Z) . x0) by TAYLOR_1:def 5

      .= (((((( #Z n) ^ ) | Z) `| Z) `| Z) . x0) by TAYLOR_1:def 5

      .= ((((( #Z n) ^ ) `| Z) `| Z) . x0) by A7, FDIFF_2: 16

      .= ((((m (#) (( #Z (n + 1)) ^ )) | Z) `| Z) . x0) by A1, A3, Th49

      .= (((m (#) (( #Z (n + 1)) ^ )) `| Z) . x0) by A10, FDIFF_2: 16

      .= (m * ( diff ((( #Z (n + 1)) ^ ),x0))) by A2, A9, A11, FDIFF_1: 20

      .= (m * (((( #Z (n + 1)) ^ ) `| Z) . x0)) by A2, A9, FDIFF_1:def 7

      .= (m * (((( - (n + 1)) (#) (( #Z ((n + 1) + 1)) ^ )) | Z) . x0)) by A3, A8, Th49

      .= (m * ((( - (n + 1)) (#) ((( #Z (n + 2)) ^ ) | Z)) . x0)) by RFUNCT_1: 49

      .= (m * (( - (n + 1)) * (((( #Z (n + 2)) ^ ) | Z) . x0))) by A2, A6, VALUED_1:def 5

      .= ((n * (n + 1)) * (((( #Z (n + 2)) ^ ) | Z) . x0))

      .= ((n * (n + 1)) * ((( #Z (n + 2)) ^ ) . x0)) by A2, FUNCT_1: 49;

      hence thesis;

    end;

    theorem :: HFDIFF_1:53

    (( diff (( sin ^2 ),Z)) . 2) = ((2 (#) (( cos ^2 ) | Z)) + (( - 2) (#) (( sin ^2 ) | Z)))

    proof

       sin is_differentiable_on (2,Z) by TAYLOR_2: 21;



      then (( diff (( sin ^2 ),Z)) . 2) = ((((( diff ( sin ,Z)) . (2 * 1)) (#) sin ) + (2 (#) (( sin `| Z) (#) ( sin `| Z)))) + ( sin (#) (( diff ( sin ,Z)) . (2 * 1)))) by Th50

      .= (((((( - 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))))

      .= ((((( - 1) (#) ( sin | Z)) (#) sin ) + (2 (#) (( sin `| Z) (#) ( sin `| Z)))) + ( sin (#) (( - 1) (#) ( sin | Z))))

      .= ((2 (#) (( sin `| Z) (#) ( sin `| Z))) + (( sin (#) (( - 1) (#) ( sin | Z))) + ( sin (#) (( - 1) (#) ( sin | Z))))) by RFUNCT_1: 8

      .= ((2 (#) (( sin `| Z) (#) ( sin `| Z))) + ((1 (#) ( sin (#) (( - 1) (#) ( sin | Z)))) + ( sin (#) (( - 1) (#) ( sin | Z))))) by RFUNCT_1: 21

      .= ((2 (#) (( sin `| Z) (#) ( sin `| Z))) + ((1 (#) ( sin (#) (( - 1) (#) ( sin | Z)))) + (1 (#) ( sin (#) (( - 1) (#) ( sin | Z)))))) by RFUNCT_1: 21

      .= ((2 (#) (( sin `| Z) (#) ( sin `| Z))) + ((1 + 1) (#) ( sin (#) (( - 1) (#) ( sin | Z))))) by Th5

      .= ((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: 45

      .= ((2 (#) (( cos (#) cos ) | Z)) + (2 (#) (( - 1) (#) (( sin | Z) (#) sin )))) by RFUNCT_1: 12

      .= ((2 (#) (( cos (#) cos ) | Z)) + (2 (#) (( - 1) (#) (( sin (#) sin ) | Z)))) by RFUNCT_1: 45

      .= ((2 (#) (( cos (#) cos ) | Z)) + ((2 * ( - 1)) (#) (( sin (#) sin ) | Z))) by RFUNCT_1: 17

      .= ((2 (#) (( cos (#) cos ) | Z)) + (( - 2) (#) (( sin (#) sin ) | Z)))

      .= ((2 (#) (( cos ^2 ) | Z)) + (( - 2) (#) (( sin ^2 ) | Z)));

      hence thesis;

    end;

    theorem :: HFDIFF_1:54

    (( diff (( cos ^2 ),Z)) . 2) = ((2 (#) (( sin ^2 ) | Z)) + (( - 2) (#) (( cos ^2 ) | Z)))

    proof

       cos is_differentiable_on (2,Z) by TAYLOR_2: 21;



      then (( diff (( cos ^2 ),Z)) . 2) = ((((( diff ( cos ,Z)) . (2 * 1)) (#) cos ) + (2 (#) (( cos `| Z) (#) ( cos `| Z)))) + ( cos (#) (( diff ( cos ,Z)) . (2 * 1)))) by Th50

      .= (((((( - 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))))

      .= ((((( - 1) (#) ( cos | Z)) (#) cos ) + (2 (#) (( cos `| Z) (#) ( cos `| Z)))) + ( cos (#) (( - 1) (#) ( cos | Z))))

      .= ((2 (#) (( cos `| Z) (#) ( cos `| Z))) + (( cos (#) (( - 1) (#) ( cos | Z))) + ( cos (#) (( - 1) (#) ( cos | Z))))) by RFUNCT_1: 8

      .= ((2 (#) (( cos `| Z) (#) ( cos `| Z))) + ((1 (#) ( cos (#) (( - 1) (#) ( cos | Z)))) + ( cos (#) (( - 1) (#) ( cos | Z))))) by RFUNCT_1: 21

      .= ((2 (#) (( cos `| Z) (#) ( cos `| Z))) + ((1 (#) ( cos (#) (( - 1) (#) ( cos | Z)))) + (1 (#) ( cos (#) (( - 1) (#) ( cos | Z)))))) by RFUNCT_1: 21

      .= ((2 (#) (( cos `| Z) (#) ( cos `| Z))) + ((1 + 1) (#) ( cos (#) (( - 1) (#) ( cos | Z))))) by Th5

      .= ((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: 45

      .= ((2 (#) ((( - sin ) (#) ( - sin )) | Z)) + (2 (#) (( - 1) (#) (( cos | Z) (#) cos )))) by RFUNCT_1: 12

      .= ((2 (#) ((( - sin ) (#) ( - sin )) | Z)) + ((2 * ( - 1)) (#) (( cos | Z) (#) cos ))) by RFUNCT_1: 17

      .= ((2 (#) ((( - sin ) (#) ( - sin )) | Z)) + (( - 2) (#) (( cos (#) cos ) | Z))) by RFUNCT_1: 45

      .= ((2 (#) (( sin (#) sin ) | Z)) + (( - 2) (#) (( cos (#) cos ) | Z))) by Th2;

      hence thesis;

    end;

    theorem :: HFDIFF_1:55

    (( diff (( sin (#) cos ),Z)) . 2) = (4 (#) ((( - sin ) (#) cos ) | Z))

    proof

       cos is_differentiable_on (2,Z) & sin is_differentiable_on (2,Z) by TAYLOR_2: 21;



      then (( diff (( sin (#) cos ),Z)) . 2) = ((((( diff ( sin ,Z)) . (2 * 1)) (#) cos ) + (2 (#) (( sin `| Z) (#) ( cos `| Z)))) + ( sin (#) (( diff ( cos ,Z)) . (2 * 1)))) by Th50

      .= (((((( - 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))))

      .= ((((( - 1) (#) ( sin | Z)) (#) cos ) + (2 (#) (( sin `| Z) (#) ( cos `| Z)))) + ( sin (#) (( - 1) (#) ( cos | Z))))

      .= ((((( - 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: 49

      .= (((((( - 1) (#) sin ) | Z) (#) cos ) + (2 (#) (( cos | Z) (#) (( - sin ) | Z)))) + ( sin (#) ((( - 1) (#) cos ) | Z))) by RFUNCT_1: 49

      .= ((((( - sin ) (#) cos ) | Z) + (2 (#) (( cos | Z) (#) (( - sin ) | Z)))) + ( sin (#) (( - cos ) | Z))) by RFUNCT_1: 45

      .= ((((( - sin ) (#) cos ) | Z) + (2 (#) (( cos | Z) (#) (( - sin ) | Z)))) + (( sin (#) ( - cos )) | Z)) by RFUNCT_1: 45

      .= ((((( - sin ) (#) cos ) | Z) + (2 (#) ((( - sin ) (#) cos ) | Z))) + (( sin (#) ( - cos )) | Z)) by RFUNCT_1: 45

      .= ((((( - sin ) (#) cos ) | Z) + (2 (#) ((( - sin ) (#) cos ) | Z))) + ((( - 1) (#) ( sin (#) cos )) | Z)) by RFUNCT_1: 13

      .= ((((( - sin ) (#) cos ) | Z) + (2 (#) ((( - sin ) (#) cos ) | Z))) + (((( - 1) (#) sin ) (#) cos ) | Z)) by RFUNCT_1: 12

      .= (((1 (#) ((( - sin ) (#) cos ) | Z)) + (2 (#) ((( - sin ) (#) cos ) | Z))) + ((( - sin ) (#) cos ) | Z)) by RFUNCT_1: 21

      .= (((1 (#) ((( - sin ) (#) cos ) | Z)) + (2 (#) ((( - sin ) (#) cos ) | Z))) + (1 (#) ((( - sin ) (#) cos ) | Z))) by RFUNCT_1: 21

      .= (((1 + 2) (#) ((( - sin ) (#) cos ) | Z)) + (1 (#) ((( - sin ) (#) cos ) | Z))) by Th5

      .= ((3 + 1) (#) ((( - sin ) (#) cos ) | Z)) by Th5

      .= (4 (#) ((( - sin ) (#) cos ) | Z));

      hence thesis;

    end;

    theorem :: HFDIFF_1:56



     Th56: Z c= ( dom tan ) implies tan is_differentiable_on Z & ( tan `| Z) = ((( cos ^ ) ^2 ) | Z)

    proof

      set f1 = ( cos ^ );

      assume

       A1: Z c= ( dom tan );



       A2: (( dom sin ) /\ ( dom f1)) c= ( dom f1) by XBOOLE_1: 17;



       A3: ( dom tan ) = ( dom ( sin (#) f1)) by RFUNCT_1: 31, SIN_COS:def 26

      .= (( dom sin ) /\ ( dom f1)) by VALUED_1:def 4;

      then

       A4: Z c= ( dom f1) by A1, A2;



       A5: ( dom (( cos ^ ) (#) ( cos ^ ))) = (( dom ( cos ^ )) /\ ( dom ( cos ^ ))) by VALUED_1:def 4

      .= ( dom ( cos ^ ));



      then

       A6: ( dom ((( cos ^ ) (#) ( cos ^ )) | Z)) = (( dom ( cos ^ )) /\ Z) by RELAT_1: 61

      .= Z by A1, A3, A2, XBOOLE_1: 1, XBOOLE_1: 28;



       A7: for x st x in Z holds tan is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then

         A8: ( cos . x) <> 0 by A1, FDIFF_8: 1;

         sin is_differentiable_in x & cos is_differentiable_in x by SIN_COS: 63, SIN_COS: 64;

        hence thesis by A8, FDIFF_2: 14, SIN_COS:def 26;

      end;

      then

       A9: tan is_differentiable_on Z by A1, FDIFF_1: 9;



       A10: for x be Element of REAL st x in ( dom ( tan `| Z)) holds (( tan `| Z) . x) = (((( cos ^ ) (#) ( cos ^ )) | Z) . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom ( tan `| Z));

        then

         A11: x in Z by A9, FDIFF_1:def 7;

        then

         A12: ( cos . x) <> 0 by A1, FDIFF_8: 1;

        (( tan `| Z) . x) = ( diff (( sin / cos ),x)) by A9, A11, FDIFF_1:def 7, SIN_COS:def 26

        .= (1 / (( cos . x) ^2 )) by A12, FDIFF_7: 46

        .= ((1 / ( cos . x)) * (1 / ( cos . x))) by XCMPLX_1: 102

        .= ((1 * (( cos . x) " )) * (1 / ( cos . x))) by XCMPLX_0:def 9

        .= ((( cos ^ ) . x) * (1 / ( cos . x))) by A4, A11, RFUNCT_1:def 2

        .= ((( cos ^ ) . x) * (1 * (( cos . x) " ))) by XCMPLX_0:def 9

        .= ((( cos ^ ) . x) * (f1 . x)) by A4, A11, RFUNCT_1:def 2

        .= ((( cos ^ ) (#) f1) . x) by A4, A5, A11, VALUED_1:def 4

        .= (((f1 (#) f1) | Z) . x) by A11, FUNCT_1: 49;

        hence thesis;

      end;

      ( dom ( tan `| Z)) = Z by A9, FDIFF_1:def 7;

      hence thesis by A1, A7, A6, A10, FDIFF_1: 9, PARTFUN1: 5;

    end;

    theorem :: HFDIFF_1:57



     Th57: Z c= ( dom tan ) implies ( cos ^ ) is_differentiable_on Z & (( cos ^ ) `| Z) = ((( cos ^ ) (#) tan ) | Z)

    proof



       A1: (( dom sin ) /\ ( dom ( cos ^ ))) c= ( dom ( cos ^ )) by XBOOLE_1: 17;

      assume

       A2: Z c= ( dom tan );

      then

       A3: for x st x in Z holds ( cos . x) <> 0 by FDIFF_8: 1;

      then ( cos ^ ) is_differentiable_on Z by FDIFF_4: 39;

      then

       A4: ( dom (( cos ^ ) `| Z)) = Z by FDIFF_1:def 7;

      ( dom tan ) = ( dom ( sin (#) ( cos ^ ))) by RFUNCT_1: 31, SIN_COS:def 26

      .= (( dom sin ) /\ ( dom ( cos ^ ))) by VALUED_1:def 4;

      then

       A5: Z c= ( dom ( cos ^ )) by A2, A1;



       A6: for x be Element of REAL st x in Z holds ((( cos ^ ) `| Z) . x) = (((( cos ^ ) (#) tan ) | Z) . x)

      proof

        let x be Element of REAL ;



         A7: ( dom (( cos ^ ) (#) sin )) = ( dom tan ) by RFUNCT_1: 31, SIN_COS:def 26;

        then ( dom ((( cos ^ ) (#) sin ) (#) ( cos ^ ))) = (( dom tan ) /\ ( dom ( cos ^ ))) by VALUED_1:def 4;

        then

         A8: Z c= ( dom ((( cos ^ ) (#) sin ) (#) ( cos ^ ))) by A2, A5, XBOOLE_1: 19;

        assume

         A9: x in Z;



        then ((( cos ^ ) `| Z) . x) = (( sin . x) / (( cos . x) ^2 )) by A3, FDIFF_4: 39

        .= ((1 / ( cos . x)) * (( sin . x) / ( cos . x))) by XCMPLX_1: 103

        .= (((1 / ( cos . x)) * ( sin . x)) * (1 / ( cos . x))) by XCMPLX_1: 99

        .= (((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 A5, A9, RFUNCT_1:def 2

        .= (((( cos ^ ) . x) * ( sin . x)) * (( cos ^ ) . x)) by A5, A9, RFUNCT_1:def 2

        .= (((( cos ^ ) (#) sin ) . x) * (( cos ^ ) . x)) by A2, A9, A7, VALUED_1:def 4

        .= (((( cos ^ ) (#) sin ) (#) ( cos ^ )) . x) by A9, A8, VALUED_1:def 4

        .= ((((( cos ^ ) (#) sin ) (#) ( cos ^ )) | Z) . x) by A9, FUNCT_1: 49

        .= (((( cos ^ ) (#) tan ) | Z) . x) by RFUNCT_1: 31, SIN_COS:def 26;

        hence thesis;

      end;

      ( dom ((( cos ^ ) (#) tan ) | Z)) = (( dom (( cos ^ ) (#) tan )) /\ Z) by RELAT_1: 61

      .= ((( dom ( cos ^ )) /\ ( dom tan )) /\ Z) by VALUED_1:def 4

      .= Z by A2, A5, XBOOLE_1: 19, XBOOLE_1: 28;

      hence thesis by A3, A4, A6, FDIFF_4: 39, PARTFUN1: 5;

    end;

    theorem :: HFDIFF_1:58

    Z c= ( dom tan ) implies (( diff ( tan ,Z)) . 2) = (2 (#) ((( tan (#) ( cos ^ )) (#) ( cos ^ )) | Z))

    proof

      assume

       A1: Z c= ( dom tan );

      then

       A2: tan is_differentiable_on Z by Th56;



       A3: ( cos ^ ) is_differentiable_on Z by A1, Th57;

      then

       A4: (( 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 A2, FDIFF_2: 16

      .= (((( cos ^ ) ^2 ) | Z) `| Z) by A1, Th56

      .= ((( cos ^ ) (#) ( cos ^ )) `| Z) by A4, FDIFF_2: 16

      .= (((( cos ^ ) `| Z) (#) ( cos ^ )) + ((( cos ^ ) `| Z) (#) ( cos ^ ))) by A3, FDIFF_2: 20

      .= ((1 (#) ((( cos ^ ) `| Z) (#) ( cos ^ ))) + ((( cos ^ ) `| Z) (#) ( cos ^ ))) by RFUNCT_1: 21

      .= ((1 (#) ((( cos ^ ) `| Z) (#) ( cos ^ ))) + (1 (#) ((( cos ^ ) `| Z) (#) ( cos ^ )))) by RFUNCT_1: 21

      .= ((1 + 1) (#) ((( cos ^ ) `| Z) (#) ( cos ^ ))) by Th5

      .= (2 (#) (((( cos ^ ) (#) tan ) | Z) (#) ( cos ^ ))) by A1, Th57

      .= (2 (#) ((( tan (#) ( cos ^ )) (#) ( cos ^ )) | Z)) by RFUNCT_1: 45;

      hence thesis;

    end;

    theorem :: HFDIFF_1:59



     Th59: Z c= ( dom cot ) implies cot is_differentiable_on Z & ( cot `| Z) = ((( - 1) (#) (( sin ^ ) ^2 )) | Z)

    proof



       A1: (( dom cos ) /\ ( dom ( sin ^ ))) c= ( dom ( sin ^ )) by XBOOLE_1: 17;

      assume

       A2: Z c= ( dom cot );



       A3: for x st x in Z holds cot is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then

         A4: ( sin . x) <> 0 by A2, FDIFF_8: 2;

         sin is_differentiable_in x & cos is_differentiable_in x by SIN_COS: 63, SIN_COS: 64;

        hence thesis by A4, FDIFF_2: 14, SIN_COS:def 27;

      end;

      then

       A5: cot is_differentiable_on Z by A2, FDIFF_1: 9;



       A6: ( dom cot ) = ( dom ( cos (#) ( sin ^ ))) by RFUNCT_1: 31, SIN_COS:def 27

      .= (( dom cos ) /\ ( dom ( sin ^ ))) by VALUED_1:def 4;

      then

       A7: Z c= ( dom ( sin ^ )) by A2, A1;



       A8: for x be Element of REAL st x in ( dom ( cot `| Z)) holds (( cot `| Z) . x) = (((( - 1) (#) (( sin ^ ) (#) ( sin ^ ))) | Z) . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom ( cot `| Z));

        then

         A9: x in Z by A5, FDIFF_1:def 7;

        then

         A10: ( sin . x) <> 0 by A2, FDIFF_8: 2;

        ( dom (( sin ^ ) (#) ( sin ^ ))) = (( dom ( sin ^ )) /\ ( dom ( sin ^ ))) by VALUED_1:def 4

        .= ( dom ( sin ^ ));

        then

         A11: Z c= ( dom (( sin ^ ) (#) ( sin ^ ))) by A2, A6, A1;

        then x in ( dom (( sin ^ ) (#) ( sin ^ ))) by A9;

        then

         A12: x in ( dom (( - 1) (#) (( sin ^ ) (#) ( sin ^ )))) by VALUED_1:def 5;

        (( cot `| Z) . x) = ( diff (( cos / sin ),x)) by A5, A9, FDIFF_1:def 7, SIN_COS:def 27

        .= ( - (1 / (( sin . x) ^2 ))) by A10, FDIFF_7: 47

        .= (( - 1) * (1 / (( sin . x) * ( sin . x))))

        .= (( - 1) * ((1 / ( sin . x)) * (1 / ( sin . x)))) by XCMPLX_1: 102

        .= (( - 1) * ((1 * (( sin . x) " )) * (1 / ( sin . x)))) by XCMPLX_0:def 9

        .= (( - 1) * ((( sin ^ ) . x) * (1 / ( sin . x)))) by A7, A9, RFUNCT_1:def 2

        .= (( - 1) * ((( sin ^ ) . x) * (1 * (( sin . x) " )))) by XCMPLX_0:def 9

        .= (( - 1) * ((( sin ^ ) . x) * (( sin ^ ) . x))) by A7, A9, RFUNCT_1:def 2

        .= (( - 1) * ((( sin ^ ) (#) ( sin ^ )) . x)) by A9, A11, VALUED_1:def 4

        .= ((( - 1) (#) (( sin ^ ) (#) ( sin ^ ))) . x) by A12, VALUED_1:def 5

        .= (((( - 1) (#) (( sin ^ ) (#) ( sin ^ ))) | Z) . x) by A9, FUNCT_1: 49;

        hence thesis;

      end;



       A13: ( dom ((( - 1) (#) (( sin ^ ) (#) ( sin ^ ))) | Z)) = (( dom (( - 1) (#) (( sin ^ ) ^2 ))) /\ Z) by RELAT_1: 61

      .= (( dom (( sin ^ ) ^2 )) /\ Z) by VALUED_1:def 5

      .= ((( dom ( sin ^ )) /\ ( dom ( sin ^ ))) /\ Z) by VALUED_1:def 4

      .= Z by A2, A6, A1, XBOOLE_1: 1, XBOOLE_1: 28;

      ( dom ( cot `| Z)) = Z by A5, FDIFF_1:def 7;

      hence thesis by A2, A3, A13, A8, FDIFF_1: 9, PARTFUN1: 5;

    end;

    theorem :: HFDIFF_1:60



     Th60: Z c= ( dom cot ) implies ( sin ^ ) is_differentiable_on Z & (( sin ^ ) `| Z) = (( - (( sin ^ ) (#) cot )) | Z)

    proof



       A1: ( dom cot ) = ( dom ( cos (#) ( sin ^ ))) by RFUNCT_1: 31, SIN_COS:def 27

      .= (( dom cos ) /\ ( dom ( sin ^ ))) by VALUED_1:def 4;

      assume

       A2: Z c= ( dom cot );

      (( dom cos ) /\ ( dom ( sin ^ ))) c= ( dom ( sin ^ )) by XBOOLE_1: 17;

      then

       A3: Z c= ( dom ( sin ^ )) by A2, A1;



       A4: for x st x in Z holds ( sin . x) <> 0 by A2, FDIFF_8: 2;

      then

       A5: ( sin ^ ) is_differentiable_on Z by FDIFF_4: 40;



       A6: for x be Element of REAL st x in ( dom (( sin ^ ) `| Z)) holds ((( sin ^ ) `| Z) . x) = ((( - (( sin ^ ) (#) cot )) | Z) . x)

      proof

        let x be Element of REAL ;



         A7: ( dom (( - 1) (#) (( sin ^ ) (#) cot ))) = ( dom (( sin ^ ) (#) ( cos / sin ))) by SIN_COS:def 27, VALUED_1:def 5

        .= ( dom (( sin ^ ) (#) ( cos (#) ( sin ^ )))) by RFUNCT_1: 31;



         A8: Z c= ( dom ( cos (#) ( sin ^ ))) by A2, A1, VALUED_1:def 4;

        ( dom (( sin ^ ) (#) ( cos (#) ( sin ^ )))) = (( dom ( sin ^ )) /\ ( dom ( cos (#) ( sin ^ )))) by VALUED_1:def 4;

        then

         A9: Z c= ( dom (( sin ^ ) (#) ( cos (#) ( sin ^ )))) by A3, A8, XBOOLE_1: 19;

        assume x in ( dom (( sin ^ ) `| Z));

        then

         A10: x in Z by A5, FDIFF_1:def 7;



        then ((( sin ^ ) `| Z) . x) = ( - (( cos . x) / (( sin . x) ^2 ))) by A4, FDIFF_4: 40

        .= ( - ((1 * ( cos . x)) / (( sin . x) * ( sin . x))))

        .= ( - ((1 / ( sin . x)) * (( cos . x) / ( sin . x)))) by XCMPLX_1: 76

        .= ( - ((1 / ( sin . x)) * (( cos . x) * (1 / ( sin . x))))) by XCMPLX_1: 99

        .= ( - ((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 A3, A10, RFUNCT_1:def 2

        .= ( - ((( sin ^ ) . x) * (( cos . x) * (( sin ^ ) . x)))) by A3, A10, RFUNCT_1:def 2

        .= ( - ((( sin ^ ) . x) * (( cos (#) ( sin ^ )) . x))) by A10, A8, VALUED_1:def 4

        .= ( - ((( sin ^ ) (#) ( cos (#) ( sin ^ ))) . x)) by A10, A9, VALUED_1:def 4

        .= ( - ((( sin ^ ) (#) cot ) . x)) by RFUNCT_1: 31, SIN_COS:def 27

        .= (( - 1) * ((( sin ^ ) (#) cot ) . x))

        .= ((( - 1) (#) (( sin ^ ) (#) cot )) . x) by A10, A9, A7, VALUED_1:def 5

        .= ((( - (( sin ^ ) (#) cot )) | Z) . x) by A10, FUNCT_1: 49;

        hence thesis;

      end;



       A11: ( dom (( - (( sin ^ ) (#) cot )) | Z)) = (( dom (( - 1) (#) (( sin ^ ) (#) cot ))) /\ Z) by RELAT_1: 61

      .= (( dom (( sin ^ ) (#) cot )) /\ Z) by VALUED_1:def 5

      .= ((( dom ( sin ^ )) /\ ( dom cot )) /\ Z) by VALUED_1:def 4

      .= Z by A2, A3, XBOOLE_1: 19, XBOOLE_1: 28;

      ( dom (( sin ^ ) `| Z)) = Z by A5, FDIFF_1:def 7;

      hence thesis by A4, A11, A6, FDIFF_4: 40, PARTFUN1: 5;

    end;

    theorem :: HFDIFF_1:61

    Z c= ( dom cot ) implies (( diff ( cot ,Z)) . 2) = (2 (#) ((( cot (#) ( sin ^ )) (#) ( sin ^ )) | Z))

    proof

      assume

       A1: Z c= ( dom cot );

      then

       A2: cot is_differentiable_on Z by Th59;



       A3: ( sin ^ ) is_differentiable_on Z by A1, Th60;

      then

       A4: (( sin ^ ) (#) ( sin ^ )) is_differentiable_on Z by FDIFF_2: 20;

      then

       A5: (( - 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 A2, FDIFF_2: 16

      .= (((( - 1) (#) (( sin ^ ) (#) ( sin ^ ))) | Z) `| Z) by A1, Th59

      .= ((( - 1) (#) (( sin ^ ) (#) ( sin ^ ))) `| Z) by A5, FDIFF_2: 16

      .= (( - 1) (#) ((( sin ^ ) (#) ( sin ^ )) `| Z)) by A4, FDIFF_2: 19

      .= (( - 1) (#) (((( sin ^ ) `| Z) (#) ( sin ^ )) + ((( sin ^ ) `| Z) (#) ( sin ^ )))) by A3, FDIFF_2: 20

      .= (( - 1) (#) ((1 (#) ((( sin ^ ) `| Z) (#) ( sin ^ ))) + ((( sin ^ ) `| Z) (#) ( sin ^ )))) by RFUNCT_1: 21

      .= (( - 1) (#) ((1 (#) ((( sin ^ ) `| Z) (#) ( sin ^ ))) + (1 (#) ((( sin ^ ) `| Z) (#) ( sin ^ ))))) by RFUNCT_1: 21

      .= (( - 1) (#) ((1 + 1) (#) ((( sin ^ ) `| Z) (#) ( sin ^ )))) by Th5

      .= (( - 1) (#) (2 (#) ((( - (( sin ^ ) (#) cot )) | Z) (#) ( sin ^ )))) by A1, Th60

      .= ((( - 1) * 2) (#) ((( - (( sin ^ ) (#) cot )) | Z) (#) ( sin ^ ))) by RFUNCT_1: 17

      .= ((( - 1) * 2) (#) ((( - (( sin ^ ) (#) cot )) (#) ( sin ^ )) | Z)) by RFUNCT_1: 45

      .= (((( - 1) * 2) (#) (( - (( sin ^ ) (#) cot )) (#) ( sin ^ ))) | Z) by RFUNCT_1: 49

      .= (((( - 2) (#) ( - (( sin ^ ) (#) cot ))) (#) ( sin ^ )) | Z) by RFUNCT_1: 12

      .= ((((( - 2) * ( - 1)) (#) (( sin ^ ) (#) cot )) (#) ( sin ^ )) | Z) by RFUNCT_1: 17

      .= ((2 (#) ((( sin ^ ) (#) cot ) (#) ( sin ^ ))) | Z) by RFUNCT_1: 12

      .= (2 (#) ((( cot (#) ( sin ^ )) (#) ( sin ^ )) | Z)) by RFUNCT_1: 49;

      hence thesis;

    end;

    theorem :: HFDIFF_1:62

    (( diff (( exp_R (#) sin ),Z)) . 2) = (2 (#) (( exp_R (#) cos ) | Z))

    proof



       A1: sin is_differentiable_on (2,Z) & exp_R is_differentiable_on (2,Z) by TAYLOR_2: 10, TAYLOR_2: 21;



       A2: ( dom (2 (#) (( exp_R (#) cos ) | Z))) = ( dom (( exp_R (#) cos ) | Z)) by VALUED_1:def 5

      .= (( dom ( exp_R (#) cos )) /\ Z) by RELAT_1: 61

      .= (( REAL /\ REAL ) /\ Z) by SIN_COS: 24, SIN_COS: 47, VALUED_1:def 4

      .= Z by XBOOLE_1: 28;



       A3: exp_R is_differentiable_on Z by FDIFF_1: 26, TAYLOR_1: 16;

       cos is_differentiable_on Z by FDIFF_1: 26, SIN_COS: 67;

      then ( cos | Z) is_differentiable_on Z by FDIFF_2: 16;

      then

       A4: ( exp_R (#) ( cos | Z)) is_differentiable_on Z by A3, FDIFF_2: 20;



       A5: sin is_differentiable_on Z by FDIFF_1: 26, SIN_COS: 68;

      then

       A6: ( exp_R (#) sin ) is_differentiable_on Z by A3, FDIFF_2: 20;

      ( exp_R | Z) is_differentiable_on Z by A3, FDIFF_2: 16;

      then (( exp_R | Z) (#) sin ) is_differentiable_on Z by A5, FDIFF_2: 20;

      then

       A7: ((( exp_R | Z) (#) sin ) + ( exp_R (#) ( cos | Z))) is_differentiable_on Z by A4, FDIFF_2: 17;



       A8: ( 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 A6, FDIFF_2: 16

      .= ( dom (((( exp_R `| Z) (#) sin ) + ( exp_R (#) ( sin `| Z))) `| Z)) by A3, A5, FDIFF_2: 20

      .= ( 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 A7, FDIFF_1:def 7;



       A9: ( dom ( 0 (#) (( exp_R (#) sin ) | Z))) = ( dom (( exp_R (#) sin ) | Z)) by VALUED_1:def 5

      .= (( dom ( exp_R (#) sin )) /\ Z) by RELAT_1: 61

      .= (( REAL /\ REAL ) /\ Z) by SIN_COS: 24, SIN_COS: 47, VALUED_1:def 4

      .= Z by XBOOLE_1: 28;



      then

       A10: ( dom (( 0 (#) (( exp_R (#) sin ) | Z)) + (2 (#) (( exp_R (#) cos ) | Z)))) = (Z /\ Z) by A2, VALUED_1:def 1

      .= Z;

      for x be Element of REAL 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 be Element of REAL ;

        assume

         A11: 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 A1, Th50

        .= ((((( 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)

        .= ((((( exp_R (#) sin ) | Z) + (2 (#) (( exp_R | Z) (#) ( cos | Z)))) + ( exp_R (#) (( - 1) (#) ( sin | Z)))) . x) by RFUNCT_1: 45

        .= ((((( exp_R (#) sin ) | Z) + (2 (#) (( exp_R (#) cos ) | Z))) + ( exp_R (#) (( - 1) (#) ( sin | Z)))) . x) by RFUNCT_1: 45

        .= ((((( exp_R (#) sin ) | Z) + ( exp_R (#) (( - 1) (#) ( sin | Z)))) + (2 (#) (( exp_R (#) cos ) | Z))) . x) by RFUNCT_1: 8

        .= ((((( exp_R (#) sin ) | Z) + (( - 1) (#) ( exp_R (#) ( sin | Z)))) + (2 (#) (( exp_R (#) cos ) | Z))) . x) by RFUNCT_1: 13

        .= ((((( exp_R (#) sin ) | Z) + (( - 1) (#) (( exp_R (#) sin ) | Z))) + (2 (#) (( exp_R (#) cos ) | Z))) . x) by RFUNCT_1: 45

        .= ((((1 (#) (( exp_R (#) sin ) | Z)) + (( - 1) (#) (( exp_R (#) sin ) | Z))) + (2 (#) (( exp_R (#) cos ) | Z))) . x) by RFUNCT_1: 21

        .= ((((1 + ( - 1)) (#) (( exp_R (#) sin ) | Z)) + (2 (#) (( exp_R (#) cos ) | Z))) . x) by Th5

        .= ((( 0 (#) (( exp_R (#) sin ) | Z)) . x) + ((2 (#) (( exp_R (#) cos ) | Z)) . x)) by A10, A8, A11, VALUED_1:def 1

        .= (( 0 * ((( exp_R (#) sin ) | Z) . x)) + ((2 (#) (( exp_R (#) cos ) | Z)) . x)) by A9, A8, A11, VALUED_1:def 5

        .= ((2 (#) (( exp_R (#) cos ) | Z)) . x);

        hence thesis;

      end;

      hence thesis by A2, A8, PARTFUN1: 5;

    end;

    theorem :: HFDIFF_1:63

    (( diff (( exp_R (#) cos ),Z)) . 2) = (2 (#) (( exp_R (#) ( - sin )) | Z))

    proof



       A1: cos is_differentiable_on (2,Z) & exp_R is_differentiable_on (2,Z) by TAYLOR_2: 10, TAYLOR_2: 21;



       A2: ( dom (2 (#) (( exp_R (#) ( - sin )) | Z))) = ( dom (( exp_R (#) ( - sin )) | Z)) by VALUED_1:def 5

      .= (( dom ( exp_R (#) ( - sin ))) /\ Z) by RELAT_1: 61

      .= ((( dom exp_R ) /\ ( dom ( - sin ))) /\ Z) by VALUED_1:def 4

      .= (( REAL /\ REAL ) /\ Z) by SIN_COS: 24, SIN_COS: 47, VALUED_1:def 5

      .= Z by XBOOLE_1: 28;



       A3: exp_R is_differentiable_on Z by FDIFF_1: 26, TAYLOR_1: 16;

       sin is_differentiable_on Z by FDIFF_1: 26, SIN_COS: 68;

      then ( sin | Z) is_differentiable_on Z by FDIFF_2: 16;

      then (( - 1) (#) ( sin | Z)) is_differentiable_on Z by FDIFF_2: 19;

      then

       A4: ( exp_R (#) (( - 1) (#) ( sin | Z))) is_differentiable_on Z by A3, FDIFF_2: 20;



       A5: cos is_differentiable_on Z by FDIFF_1: 26, SIN_COS: 67;

      then

       A6: ( exp_R (#) cos ) is_differentiable_on Z by A3, FDIFF_2: 20;

      ( exp_R | Z) is_differentiable_on Z by A3, FDIFF_2: 16;

      then (( exp_R | Z) (#) cos ) is_differentiable_on Z by A5, FDIFF_2: 20;

      then

       A7: ((( exp_R | Z) (#) cos ) + ( exp_R (#) (( - 1) (#) ( sin | Z)))) is_differentiable_on Z by A4, FDIFF_2: 17;



       A8: ( 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 A6, FDIFF_2: 16

      .= ( dom (((( exp_R `| Z) (#) cos ) + ( exp_R (#) ( cos `| Z))) `| Z)) by A3, A5, FDIFF_2: 20

      .= ( 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: 49

      .= Z by A7, FDIFF_1:def 7;



       A9: ( dom ( 0 (#) (( exp_R (#) cos ) | Z))) = ( dom (( exp_R (#) cos ) | Z)) by VALUED_1:def 5

      .= (( dom ( exp_R (#) cos )) /\ Z) by RELAT_1: 61

      .= (( REAL /\ REAL ) /\ Z) by SIN_COS: 24, SIN_COS: 47, VALUED_1:def 4

      .= Z by XBOOLE_1: 28;



      then

       A10: ( dom (( 0 (#) (( exp_R (#) cos ) | Z)) + (2 (#) (( exp_R (#) ( - sin )) | Z)))) = (Z /\ Z) by A2, VALUED_1:def 1

      .= Z;

      for x be Element of REAL 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 be Element of REAL ;

        assume

         A11: 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 A1, Th50

        .= ((((( 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: 46

        .= ((((( 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)

        .= ((((( exp_R (#) cos ) | Z) + (2 (#) (( exp_R | Z) (#) ( - ( sin | Z))))) + ( exp_R (#) (( - 1) (#) ( cos | Z)))) . x) by RFUNCT_1: 45

        .= ((((( exp_R (#) cos ) | Z) + (2 (#) (( exp_R | Z) (#) (( - sin ) | Z)))) + ( exp_R (#) (( - 1) (#) ( cos | Z)))) . x) by RFUNCT_1: 46

        .= ((((( exp_R (#) cos ) | Z) + (2 (#) (( exp_R (#) ( - sin )) | Z))) + ( exp_R (#) (( - 1) (#) ( cos | Z)))) . x) by RFUNCT_1: 45

        .= ((((( exp_R (#) cos ) | Z) + ( exp_R (#) (( - 1) (#) ( cos | Z)))) + (2 (#) (( exp_R (#) ( - sin )) | Z))) . x) by RFUNCT_1: 8

        .= ((((( exp_R (#) cos ) | Z) + (( - 1) (#) ( exp_R (#) ( cos | Z)))) + (2 (#) (( exp_R (#) ( - sin )) | Z))) . x) by RFUNCT_1: 13

        .= ((((( exp_R (#) cos ) | Z) + (( - 1) (#) (( exp_R (#) cos ) | Z))) + (2 (#) (( exp_R (#) ( - sin )) | Z))) . x) by RFUNCT_1: 45

        .= ((((1 (#) (( exp_R (#) cos ) | Z)) + (( - 1) (#) (( exp_R (#) cos ) | Z))) + (2 (#) (( exp_R (#) ( - sin )) | Z))) . x) by RFUNCT_1: 21

        .= ((((1 + ( - 1)) (#) (( exp_R (#) cos ) | Z)) + (2 (#) (( exp_R (#) ( - sin )) | Z))) . x) by Th5

        .= ((( 0 (#) (( exp_R (#) cos ) | Z)) . x) + ((2 (#) (( exp_R (#) ( - sin )) | Z)) . x)) by A10, A8, A11, VALUED_1:def 1

        .= (( 0 * ((( exp_R (#) cos ) | Z) . x)) + ((2 (#) (( exp_R (#) ( - sin )) | Z)) . x)) by A9, A8, A11, VALUED_1:def 5

        .= ((2 (#) (( exp_R (#) ( - sin )) | Z)) . x);

        hence thesis;

      end;

      hence thesis by A2, A8, PARTFUN1: 5;

    end;



     Lm3: f is_differentiable_on Z implies ((f `| Z) `| Z) = (( diff (f,Z)) . 2)

    proof

      assume f is_differentiable_on Z;



      then ((f `| Z) `| Z) = (((f | Z) `| Z) `| Z) by 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 :: HFDIFF_1:64



     Th64: 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: f2 is_differentiable_on Z by A2, Th7;

      set g2 = (( diff (f2,Z)) . 2);

      set g1 = (( diff (f1,Z)) . 2);

      (( 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 A3, FDIFF_2: 16;

      then

       A4: (f2 `| Z) is_differentiable_on Z by A2;



       A5: f1 is_differentiable_on (2,Z) & f2 is_differentiable_on (2,Z) by A1, A2, TAYLOR_1: 23;



       A6: f1 is_differentiable_on Z by A1, Th7;



       A7: (( diff (f1,Z)) . 2) is_differentiable_on Z by A1;

      then

       A8: ((( diff (f1,Z)) . 2) (#) f2) is_differentiable_on Z by A3, FDIFF_2: 20;

      (( 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;

      then

       A9: (f1 `| Z) is_differentiable_on Z by A1;

      then

       A10: ((f1 `| Z) (#) (f2 `| Z)) is_differentiable_on Z by A4, FDIFF_2: 20;

      then

       A11: (2 (#) ((f1 `| Z) (#) (f2 `| Z))) is_differentiable_on Z by FDIFF_2: 19;

      then

       A12: (((( diff (f1,Z)) . 2) (#) f2) + (2 (#) ((f1 `| Z) (#) (f2 `| Z)))) is_differentiable_on Z by A8, FDIFF_2: 17;



       A13: (( diff (f2,Z)) . 2) is_differentiable_on Z by A2;

      then

       A14: (f1 (#) (( diff (f2,Z)) . 2)) is_differentiable_on Z by A6, FDIFF_2: 20;

      (( 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 A5, Th50

      .= (((((( diff (f1,Z)) . 2) (#) f2) + (2 (#) ((f1 `| Z) (#) (f2 `| Z)))) `| Z) + ((f1 (#) (( diff (f2,Z)) . 2)) `| Z)) by A14, A12, FDIFF_2: 17

      .= (((((( diff (f1,Z)) . 2) (#) f2) `| Z) + ((2 (#) ((f1 `| Z) (#) (f2 `| Z))) `| Z)) + ((f1 (#) (( diff (f2,Z)) . 2)) `| Z)) by A8, A11, FDIFF_2: 17

      .= (((((( diff (f1,Z)) . 2) (#) f2) `| Z) + (2 (#) (((f1 `| Z) (#) (f2 `| Z)) `| Z))) + ((f1 (#) (( diff (f2,Z)) . 2)) `| Z)) by A10, FDIFF_2: 19

      .= ((((((( 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 A3, A7, FDIFF_2: 20

      .= ((((((( 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 A6, A13, FDIFF_2: 20

      .= (((((( 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 A9, A4, FDIFF_2: 20

      .= (((((( 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 A1, Lm3, Th7

      .= (((((( 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 A2, Lm3, Th7

      .= (((((( 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: 21

      .= (((((( 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: 16

      .= ((((( 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: 8

      .= ((((( 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: 8

      .= ((((( 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: 12

      .= ((((( diff (f1,Z)) . 3) (#) f2) + (((1 + 2) (#) (g1 (#) (f2 `| Z))) + (2 (#) ((f1 `| Z) (#) g2)))) + (((f1 `| Z) (#) g2) + (f1 (#) (( diff (f2,Z)) . 3)))) by Th5

      .= (((( diff (f1,Z)) . 3) (#) f2) + (((3 (#) (g1 (#) (f2 `| Z))) + (2 (#) ((f1 `| Z) (#) g2))) + (((f1 `| Z) (#) g2) + (f1 (#) (( diff (f2,Z)) . 3))))) by RFUNCT_1: 8

      .= (((( diff (f1,Z)) . 3) (#) f2) + ((3 (#) (g1 (#) (f2 `| Z))) + ((2 (#) ((f1 `| Z) (#) g2)) + (((f1 `| Z) (#) g2) + (f1 (#) (( diff (f2,Z)) . 3)))))) by RFUNCT_1: 8

      .= (((( diff (f1,Z)) . 3) (#) f2) + ((3 (#) (g1 (#) (f2 `| Z))) + (((2 (#) ((f1 `| Z) (#) g2)) + ((f1 `| Z) (#) g2)) + (f1 (#) (( diff (f2,Z)) . 3))))) by RFUNCT_1: 8

      .= (((( 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: 21

      .= (((( diff (f1,Z)) . 3) (#) f2) + ((3 (#) (g1 (#) (f2 `| Z))) + (((2 + 1) (#) ((f1 `| Z) (#) g2)) + (f1 (#) (( diff (f2,Z)) . 3))))) by Th5

      .= (((( diff (f1,Z)) . 3) (#) f2) + (((3 (#) (g1 (#) (f2 `| Z))) + (3 (#) ((f1 `| Z) (#) g2))) + (f1 (#) (( diff (f2,Z)) . 3)))) by RFUNCT_1: 8

      .= ((((( diff (f1,Z)) . 3) (#) f2) + ((3 (#) (g1 (#) (f2 `| Z))) + (3 (#) ((f1 `| Z) (#) g2)))) + (f1 (#) (( diff (f2,Z)) . 3))) by RFUNCT_1: 8;

      hence thesis;

    end;

    theorem :: HFDIFF_1:65

    (( diff (( sin ^2 ),Z)) . 3) = (( - 8) (#) (( cos (#) sin ) | Z))

    proof

       sin is_differentiable_on (3,Z) by TAYLOR_2: 21;



      then (( 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 Th64

      .= (((((( - 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))))

      .= ((((( - 1) (#) ( cos | Z)) (#) sin ) + ((3 (#) ((( - 1) (#) ( sin | Z)) (#) ( sin `| Z))) + (3 (#) (( sin `| Z) (#) ((( - 1) |^ 1) (#) ( sin | Z)))))) + ( sin (#) ((( - 1) |^ 1) (#) ( cos | Z))))

      .= ((((( - 1) (#) ( cos | Z)) (#) sin ) + ((3 (#) ((( - 1) (#) ( sin | Z)) (#) ( sin `| Z))) + (3 (#) (( sin `| Z) (#) (( - 1) (#) ( sin | Z)))))) + ( sin (#) ((( - 1) |^ 1) (#) ( cos | Z))))

      .= ((((( - 1) (#) ( cos | Z)) (#) sin ) + ((3 (#) ((( - 1) (#) ( sin | Z)) (#) ( sin `| Z))) + (3 (#) (( sin `| Z) (#) (( - 1) (#) ( sin | Z)))))) + ( sin (#) (( - 1) (#) ( cos | Z))))

      .= ((((( - 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 Th5

      .= ((6 (#) (( cos | Z) (#) (( - 1) (#) ( sin | Z)))) + (((( - 1) (#) ( cos | Z)) (#) sin ) + ((( - 1) (#) ( cos | Z)) (#) sin ))) by RFUNCT_1: 8

      .= ((6 (#) (( cos | Z) (#) (( - 1) (#) ( sin | Z)))) + ((1 (#) ((( - 1) (#) ( cos | Z)) (#) sin )) + ((( - 1) (#) ( cos | Z)) (#) sin ))) by RFUNCT_1: 21

      .= ((6 (#) (( cos | Z) (#) (( - 1) (#) ( sin | Z)))) + ((1 (#) ((( - 1) (#) ( cos | Z)) (#) sin )) + (1 (#) ((( - 1) (#) ( cos | Z)) (#) sin )))) by RFUNCT_1: 21

      .= ((6 (#) (( cos | Z) (#) (( - 1) (#) ( sin | Z)))) + ((1 + 1) (#) ((( - 1) (#) ( cos | Z)) (#) sin ))) by Th5

      .= ((6 (#) (( - 1) (#) (( cos | Z) (#) ( sin | Z)))) + (2 (#) ((( - 1) (#) ( cos | Z)) (#) sin ))) by RFUNCT_1: 13

      .= ((6 (#) (( - 1) (#) (( cos (#) sin ) | Z))) + (2 (#) ((( - 1) (#) ( cos | Z)) (#) sin ))) by RFUNCT_1: 45

      .= ((6 (#) (( - 1) (#) (( cos (#) sin ) | Z))) + (2 (#) (( - 1) (#) (( cos | Z) (#) sin )))) by RFUNCT_1: 12

      .= ((6 (#) (( - 1) (#) (( cos (#) sin ) | Z))) + (2 (#) (( - 1) (#) (( cos (#) sin ) | Z)))) by RFUNCT_1: 45

      .= ((6 + 2) (#) (( - 1) (#) (( cos (#) sin ) | Z))) by Th5

      .= ((8 * ( - 1)) (#) (( cos (#) sin ) | Z)) by RFUNCT_1: 17

      .= (( - 8) (#) (( cos (#) sin ) | Z));

      hence thesis;

    end;

    theorem :: HFDIFF_1:66

    f is_differentiable_on (2,Z) implies (( diff ((f ^2 ),Z)) . 2) = ((2 (#) (f (#) (( diff (f,Z)) . 2))) + (2 (#) ((f `| Z) ^2 )))

    proof

      assume f is_differentiable_on (2,Z);



      then (( diff ((f ^2 ),Z)) . 2) = (((( diff (f,Z)) . 2) (#) f) + ((2 (#) ((f `| Z) (#) (f `| Z))) + (f (#) (( diff (f,Z)) . 2)))) by Th50

      .= ((((( diff (f,Z)) . 2) (#) f) + (f (#) (( diff (f,Z)) . 2))) + (2 (#) ((f `| Z) (#) (f `| Z)))) by RFUNCT_1: 8

      .= (((1 (#) (f (#) (( diff (f,Z)) . 2))) + (f (#) (( diff (f,Z)) . 2))) + (2 (#) ((f `| Z) (#) (f `| Z)))) by RFUNCT_1: 21

      .= (((1 (#) (f (#) (( diff (f,Z)) . 2))) + (1 (#) (f (#) (( diff (f,Z)) . 2)))) + (2 (#) ((f `| Z) (#) (f `| Z)))) by RFUNCT_1: 21

      .= (((1 + 1) (#) (f (#) (( diff (f,Z)) . 2))) + (2 (#) ((f `| Z) (#) (f `| Z)))) by Th5

      .= ((2 (#) (f (#) (( diff (f,Z)) . 2))) + (2 (#) ((f `| Z) (#) (f `| Z))))

      .= ((2 (#) (f (#) (( diff (f,Z)) . 2))) + (2 (#) ((f `| Z) ^2 )));

      hence thesis;

    end;



     Lm4: (f / f) = ((( dom f) \ (f " { 0 })) --> 1)

    proof



       A1: ( dom (f / f)) = (( dom f) /\ (( dom f) \ (f " { 0 }))) by RFUNCT_1:def 1

      .= (( dom f) \ (f " { 0 })) by XBOOLE_1: 28, XBOOLE_1: 36;

      for c be object st c in ( dom (f / f)) holds ((f / f) . c) = 1

      proof

        let c be object;

        reconsider cc = c as set by TARSKI: 1;

        assume

         A2: c in ( dom (f / f));

        then c in ( dom f) & not c in (f " { 0 }) by A1, XBOOLE_0:def 5;

        then not (f . c) in { 0 } by FUNCT_1:def 7;

        then

         A3: (f . c) <> 0 by TARSKI:def 1;

        ((f / f) . c) = ((f . cc) * ((f . cc) " )) by A2, RFUNCT_1:def 1;

        hence thesis by A3, XCMPLX_0:def 7;

      end;

      hence thesis by A1, FUNCOP_1: 11;

    end;



     Lm5: ((f (#) (f (#) f)) " { 0 }) = (f " { 0 })

    proof

      thus ((f (#) (f (#) f)) " { 0 }) c= (f " { 0 })

      proof

        let x be object;

        assume

         A1: x in ((f (#) (f (#) f)) " { 0 });

        then ((f (#) (f (#) f)) . x) in { 0 } by FUNCT_1:def 7;

        then ((f (#) (f (#) f)) . x) = 0 by TARSKI:def 1;

        then ((f . x) * ((f (#) f) . x)) = 0 by VALUED_1: 5;

        then (((f . x) * (f . x)) * (f . x)) = 0 by VALUED_1: 5;

        then (f . x) = 0 or ((f . x) * (f . x)) = 0 by XCMPLX_1: 6;

        then (f . x) = 0 or (f . x) = 0 or (f . x) = 0 by XCMPLX_1: 6;

        then

         A2: (f . x) in { 0 } by TARSKI:def 1;

        x in ( dom (f (#) (f (#) f))) by A1, FUNCT_1:def 7;

        then x in (( dom f) /\ ( dom (f (#) f))) by VALUED_1:def 4;

        then x in ( dom f) by XBOOLE_0:def 4;

        hence thesis by A2, FUNCT_1:def 7;

      end;

      let x be object;

      assume

       A3: x in (f " { 0 });

      then (f . x) in { 0 } by FUNCT_1:def 7;

      then

       A4: (f . x) = 0 by TARSKI:def 1;

      x in (( dom f) /\ ( dom f)) by A3, FUNCT_1:def 7;

      then x in (( dom (f (#) f)) /\ ( dom f)) by VALUED_1:def 4;

      then

       A5: x in ( dom (f (#) (f (#) f))) by VALUED_1:def 4;

      ((f (#) (f (#) f)) . x) = ((f . x) * ((f (#) f) . x)) by VALUED_1: 5

      .= ((f . x) * (f . x)) by A4

      .= 0 by A4;

      then ((f (#) (f (#) f)) . x) in { 0 } by TARSKI:def 1;

      hence thesis by A5, FUNCT_1:def 7;

    end;

    theorem :: HFDIFF_1:67

    f is_differentiable_on (2,Z) & (for x0 st x0 in Z holds (f . x0) <> 0 ) implies (( diff ((f ^ ),Z)) . 2) = ((((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 A1, Th7;

      then

       A4: (f ^ ) is_differentiable_on Z by A2, FDIFF_2: 22;



       A5: Z c= ( dom f) by A3, FDIFF_1:def 6;



       A6: for x0 st x0 in Z holds ((f (#) f) . x0) <> 0

      proof

        let x0;

        assume

         A7: x0 in Z;

        then

         A8: (f . x0) <> 0 by A2;

        ( dom (f (#) f)) = (( dom f) /\ ( dom f)) by VALUED_1:def 4

        .= ( dom f);

        then ((f (#) f) . x0) = ((f . x0) * (f . x0)) by A5, A7, VALUED_1:def 4;

        hence thesis by A8, XCMPLX_1: 6;

      end;

      (( 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 A3, FDIFF_2: 16;

      then

       A9: (f `| Z) is_differentiable_on Z by A1;

      then ((f | Z) `| Z) is_differentiable_on Z by A3, FDIFF_2: 16;

      then

       A10: ((( diff (f,Z)) . 0 ) `| Z) is_differentiable_on Z by TAYLOR_1:def 5;



       A11: (f (#) f) is_differentiable_on Z by A3, FDIFF_2: 20;

      then

       A12: ((f `| Z) / (f (#) f)) is_differentiable_on Z by A9, A6, FDIFF_2: 21;

      (( 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 A4, FDIFF_2: 16

      .= (( - ((f `| Z) / (f (#) f))) `| Z) by A2, A3, FDIFF_2: 22

      .= (( - 1) (#) (((f `| Z) / (f (#) f)) `| Z)) by A12, FDIFF_2: 19

      .= (( - 1) (#) (((((f `| Z) `| Z) (#) (f (#) f)) - (((f (#) f) `| Z) (#) (f `| Z))) / ((f (#) f) (#) (f (#) f)))) by A9, A11, A6, FDIFF_2: 21

      .= (( - 1) (#) ((((( diff (f,Z)) . 2) (#) (f (#) f)) - (((f (#) f) `| Z) (#) (f `| Z))) / ((f (#) f) (#) (f (#) f)))) by A1, Lm3, Th7

      .= (( - 1) (#) ((((( diff (f,Z)) . 2) (#) (f (#) f)) - ((((f `| Z) (#) f) + (f (#) (f `| Z))) (#) (f `| Z))) / ((f (#) f) (#) (f (#) f)))) by A3, FDIFF_2: 20

      .= (( - 1) (#) ((((( diff (f,Z)) . 2) (#) (f ^2 )) - ((f (#) ((f `| Z) + (f `| Z))) (#) (f `| Z))) / ((f (#) f) (#) (f (#) f)))) by RFUNCT_1: 11

      .= (( - 1) (#) ((((( diff (f,Z)) . 2) (#) (f ^2 )) - ((f (#) ((1 (#) (f `| Z)) + (f `| Z))) (#) (f `| Z))) / ((f (#) f) (#) (f (#) f)))) by RFUNCT_1: 21

      .= (( - 1) (#) ((((( diff (f,Z)) . 2) (#) (f ^2 )) - ((f (#) ((1 (#) (f `| Z)) + (1 (#) (f `| Z)))) (#) (f `| Z))) / ((f (#) f) (#) (f (#) f)))) by RFUNCT_1: 21

      .= (( - 1) (#) ((((( diff (f,Z)) . 2) (#) (f ^2 )) - ((f (#) ((1 + 1) (#) (f `| Z))) (#) (f `| Z))) / ((f (#) f) (#) (f (#) f)))) by Th5

      .= (( - 1) (#) (((f (#) ((( diff (f,Z)) . 2) (#) f)) - ((f (#) (2 (#) (f `| Z))) (#) (f `| Z))) / ((f (#) f) (#) (f (#) f)))) by RFUNCT_1: 9

      .= ((( - 1) (#) ((f (#) ((( diff (f,Z)) . 2) (#) f)) - ((f (#) (2 (#) (f `| Z))) (#) (f `| Z)))) / ((f (#) f) (#) (f (#) f))) by RFUNCT_1: 32

      .= ((((f (#) (2 (#) (f `| Z))) (#) (f `| Z)) - (f (#) ((( diff (f,Z)) . 2) (#) f))) / ((f (#) f) (#) (f (#) f))) by RFUNCT_1: 19

      .= (((f (#) ((2 (#) (f `| Z)) (#) (f `| Z))) - (f (#) ((( diff (f,Z)) . 2) (#) f))) / ((f (#) f) (#) (f (#) f))) by RFUNCT_1: 9

      .= ((f (#) (((2 (#) (f `| Z)) (#) (f `| Z)) - ((( diff (f,Z)) . 2) (#) f))) / ((f (#) f) (#) (f (#) f))) by RFUNCT_1: 15

      .= ((f (#) (((2 (#) (f `| Z)) (#) (f `| Z)) - ((( diff (f,Z)) . 2) (#) f))) / (f (#) (f (#) (f (#) f)))) by RFUNCT_1: 9

      .= ((f / f) (#) ((((2 (#) (f `| Z)) (#) (f `| Z)) - ((( diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f)))) by RFUNCT_1: 34;



      then

       A13: (( diff ((f ^ ),Z)) . 2) = ((f / f) (#) ((((2 (#) (f `| Z)) (#) (f `| Z)) - ((( diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f))))

      .= (((( dom f) \ (f " { 0 })) --> 1) (#) ((((2 (#) (f `| Z)) (#) (f `| Z)) - ((( diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f)))) by Lm4;



       A14: ( dom (( diff (f,Z)) . (1 + 1))) = ( dom ((( diff (f,Z)) . ( 0 + 1)) `| Z)) by TAYLOR_1:def 5

      .= ( dom (((( diff (f,Z)) . 0 ) `| Z) `| Z)) by TAYLOR_1:def 5

      .= Z by A10, FDIFF_1:def 7;



       A15: ( dom ((( diff (f,Z)) . 2) (#) f)) = (( dom (( diff (f,Z)) . 2)) /\ ( dom f)) by VALUED_1:def 4

      .= (Z /\ ( dom f)) by A14;



       A16: ( dom ((2 (#) (f `| Z)) (#) (f `| Z))) = ( dom (2 (#) ((f `| Z) (#) (f `| Z)))) by RFUNCT_1: 13

      .= ( dom ((f `| Z) (#) (f `| Z))) by VALUED_1:def 5

      .= (( dom (f `| Z)) /\ ( dom (f `| Z))) by VALUED_1:def 4

      .= ( dom (f `| Z))

      .= Z by A3, FDIFF_1:def 7;

      set g1 = ((((2 (#) (f `| Z)) (#) (f `| Z)) - ((( diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f)));

      set g2 = ((f / f) (#) ((((2 (#) (f `| Z)) (#) (f `| Z)) - ((( diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f))));



       A17: ( dom (f (#) (f (#) f))) = (( dom f) /\ ( dom (f (#) f))) by VALUED_1:def 4

      .= (( dom f) /\ (( dom f) /\ ( dom f))) by VALUED_1:def 4

      .= (( dom f) /\ ( dom f))

      .= ( dom f);



       A18: (f / f) = ((( dom f) \ (f " { 0 })) --> 1) by Lm4;

      then

       A19: ( dom (f / f)) = (( dom f) \ (f " { 0 })) by FUNCOP_1: 13;



       A20: ( dom g2) = (( dom (f / f)) /\ ( dom g1)) by VALUED_1:def 4;

      then

       A21: ( dom g2) c= ( dom (f / f)) by XBOOLE_1: 17;



       A22: for x be Element of REAL st x in ( dom g2) holds (g2 . x) = (g1 . x)

      proof

        let x be Element of REAL ;

        assume

         A23: x in ( dom g2);

        (g2 . x) = (((f / f) (#) g1) . x)

        .= (((f / f) . x) * (g1 . x)) by A23, VALUED_1:def 4

        .= (1 * (g1 . x)) by A18, A19, A21, A23, FUNCOP_1: 7

        .= (g1 . x);

        hence thesis;

      end;

      ( dom ((((2 (#) (f `| Z)) (#) (f `| Z)) - ((( diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f)))) = (( dom (((2 (#) (f `| Z)) (#) (f `| Z)) - ((( diff (f,Z)) . 2) (#) f))) /\ (( dom (f (#) (f (#) f))) \ ((f (#) (f (#) f)) " { 0 }))) by RFUNCT_1:def 1

      .= ((( dom ((2 (#) (f `| Z)) (#) (f `| Z))) /\ ( dom ((( diff (f,Z)) . 2) (#) f))) /\ (( dom (f (#) (f (#) f))) \ ((f (#) (f (#) f)) " { 0 }))) by VALUED_1: 12

      .= ((Z /\ ( dom ((( diff (f,Z)) . 2) (#) f))) /\ (( dom (f (#) (f (#) f))) \ ((f (#) (f (#) f)) " { 0 }))) by A16

      .= ((Z /\ (Z /\ ( dom f))) /\ (( dom (f (#) (f (#) f))) \ ((f (#) (f (#) f)) " { 0 }))) by A15

      .= (((Z /\ Z) /\ ( dom f)) /\ (( dom (f (#) (f (#) f))) \ ((f (#) (f (#) f)) " { 0 }))) by XBOOLE_1: 16

      .= ((Z /\ ( dom f)) /\ (( dom (f (#) (f (#) f))) \ ((f (#) (f (#) f)) " { 0 })))

      .= ((Z /\ ( dom f)) /\ (( dom f) \ ((f (#) (f (#) f)) " { 0 }))) by A17

      .= (((Z /\ ( dom f)) /\ ( dom f)) \ ((f (#) (f (#) f)) " { 0 })) by XBOOLE_1: 49

      .= ((Z /\ (( dom f) /\ ( dom f))) \ ((f (#) (f (#) f)) " { 0 })) by XBOOLE_1: 16

      .= ((Z /\ ( dom f)) \ ((f (#) (f (#) f)) " { 0 }))

      .= (Z \ ((f (#) (f (#) f)) " { 0 })) by A5, XBOOLE_1: 28

      .= (Z \ (f " { 0 })) by Lm5;

      then ( dom g2) = ( dom g1) by A5, A19, A20, XBOOLE_1: 28, XBOOLE_1: 33;

      hence thesis by A18, A13, A22, PARTFUN1: 5;

    end;

    theorem :: HFDIFF_1:68

    (( diff (( exp_R (#) sin ),Z)) . 3) = ((2 (#) ( exp_R (#) (( - sin ) + cos ))) | Z)

    proof

       sin is_differentiable_on (3,Z) & exp_R is_differentiable_on (3,Z) by TAYLOR_2: 10, TAYLOR_2: 21;



      then (( 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 Th64

      .= (((( 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))))

      .= (((( exp_R | Z) (#) sin ) + ((3 (#) (( exp_R | Z) (#) ( cos | Z))) + (3 (#) (( exp_R | Z) (#) (( - 1) (#) ( sin | Z)))))) + ( exp_R (#) (( - 1) (#) ( cos | Z))))

      .= (((( 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: 45

      .= (((( exp_R (#) sin ) | Z) + ((3 (#) (( exp_R (#) cos ) | Z)) + (3 (#) (( exp_R | Z) (#) (( - 1) (#) ( sin | Z)))))) + ( exp_R (#) (( - 1) (#) ( cos | Z)))) by RFUNCT_1: 45

      .= (((( exp_R (#) sin ) | Z) + ((3 (#) (( exp_R (#) cos ) | Z)) + (3 (#) (( - 1) (#) (( exp_R | Z) (#) ( sin | Z)))))) + ( exp_R (#) (( - 1) (#) ( cos | Z)))) by RFUNCT_1: 13

      .= (((( exp_R (#) sin ) | Z) + ((3 (#) (( exp_R (#) cos ) | Z)) + ((3 * ( - 1)) (#) (( exp_R | Z) (#) ( sin | Z))))) + ( exp_R (#) (( - 1) (#) ( cos | Z)))) by RFUNCT_1: 17

      .= (((( exp_R (#) sin ) | Z) + ((3 (#) (( exp_R (#) cos ) | Z)) + (( - 3) (#) (( exp_R (#) sin ) | Z)))) + ( exp_R (#) (( - 1) (#) ( cos | Z)))) by RFUNCT_1: 45

      .= (((( exp_R (#) sin ) | Z) + ((3 (#) (( exp_R (#) cos ) | Z)) + (( - 3) (#) (( exp_R (#) sin ) | Z)))) + (( - 1) (#) ( exp_R (#) ( cos | Z)))) by RFUNCT_1: 13

      .= (((( exp_R (#) sin ) | Z) + ((3 (#) (( exp_R (#) cos ) | Z)) + (( - 3) (#) (( exp_R (#) sin ) | Z)))) + (( - 1) (#) (( exp_R (#) cos ) | Z))) by RFUNCT_1: 45

      .= ((((( exp_R (#) sin ) | Z) + (3 (#) (( exp_R (#) cos ) | Z))) + (( - 3) (#) (( exp_R (#) sin ) | Z))) + (( - 1) (#) (( exp_R (#) cos ) | Z))) by RFUNCT_1: 8

      .= ((((3 (#) (( exp_R (#) cos ) | Z)) + (1 (#) (( exp_R (#) sin ) | Z))) + (( - 3) (#) (( exp_R (#) sin ) | Z))) + (( - 1) (#) (( exp_R (#) cos ) | Z))) by RFUNCT_1: 21

      .= (((3 (#) (( exp_R (#) cos ) | Z)) + ((1 (#) (( exp_R (#) sin ) | Z)) + (( - 3) (#) (( exp_R (#) sin ) | Z)))) + (( - 1) (#) (( exp_R (#) cos ) | Z))) by RFUNCT_1: 8

      .= (((3 (#) (( exp_R (#) cos ) | Z)) + ((1 + ( - 3)) (#) (( exp_R (#) sin ) | Z))) + (( - 1) (#) (( exp_R (#) cos ) | Z))) by Th5

      .= ((( - 2) (#) (( exp_R (#) sin ) | Z)) + ((3 (#) (( exp_R (#) cos ) | Z)) + (( - 1) (#) (( exp_R (#) cos ) | Z)))) by RFUNCT_1: 8

      .= ((( - 2) (#) (( exp_R (#) sin ) | Z)) + ((3 + ( - 1)) (#) (( exp_R (#) cos ) | Z))) by Th5

      .= (((( - 2) (#) ( exp_R (#) sin )) | Z) + (2 (#) (( exp_R (#) cos ) | Z))) by RFUNCT_1: 49

      .= (((( - 2) (#) ( exp_R (#) sin )) | Z) + ((2 (#) ( exp_R (#) cos )) | Z)) by RFUNCT_1: 49

      .= ((((2 * ( - 1)) (#) ( exp_R (#) sin )) + (2 (#) ( exp_R (#) cos ))) | Z) by RFUNCT_1: 44

      .= (((2 (#) (( - 1) (#) ( exp_R (#) sin ))) + (2 (#) ( exp_R (#) cos ))) | Z) by RFUNCT_1: 17

      .= ((2 (#) ((( - 1) (#) ( exp_R (#) sin )) + ( exp_R (#) cos ))) | Z) by RFUNCT_1: 16

      .= ((2 (#) (( exp_R (#) (( - 1) (#) sin )) + ( exp_R (#) cos ))) | Z) by RFUNCT_1: 13

      .= ((2 (#) ( exp_R (#) (( - sin ) + cos ))) | Z) by RFUNCT_1: 11;

      hence thesis;

    end;