fdiff_7.miz



    begin

    reserve y for set,

x,r,a,b for Real,

n for Element of NAT ,

Z for open Subset of REAL ,

f,f1,f2,f3 for PartFunc of REAL , REAL ;

    theorem :: FDIFF_7:1

    

     Th1: (x #Z 2) = (x ^2 )

    proof

      (x #Z 2) = (x |^ 2) by PREPOWER: 36

      .= (x ^2 ) by NEWTON: 81;

      hence thesis;

    end;

    theorem :: FDIFF_7:2

    

     Th2: x > 0 implies (x #R (1 / 2)) = ( sqrt x)

    proof

      assume

       A1: x > 0 ;

      then

       A2: (x #R (1 / 2)) > 0 by PREPOWER: 81;

      x = (x #R ((1 / 2) * 2)) by A1, PREPOWER: 72

      .= ((x #R (1 / 2)) #R 2) by A1, PREPOWER: 91

      .= ((x #R (1 / 2)) #Q 2) by A1, PREPOWER: 74, PREPOWER: 81

      .= ((x #R (1 / 2)) to_power 2) by A1, POWER: 44, PREPOWER: 81

      .= ((x #R (1 / 2)) ^2 ) by POWER: 46;

      hence thesis by A1, A2, SQUARE_1:def 2;

    end;

    theorem :: FDIFF_7:3

    

     Th3: x > 0 implies (x #R ( - (1 / 2))) = (1 / ( sqrt x))

    proof

      assume

       A1: x > 0 ;

      

      hence (x #R ( - (1 / 2))) = (1 / (x #R (1 / 2))) by PREPOWER: 76

      .= (1 / ( sqrt x)) by A1, Th2;

    end;

    

     Lm1: (2 * (( cos . (x / 2)) ^2 )) = (1 + ( cos . x))

    proof

      (( cos (x / 2)) ^2 ) = ((1 + ( cos (2 * (x / 2)))) / 2) by SIN_COS5: 21

      .= ((1 + ( cos x)) / 2);

      

      then (2 * (( cos . (x / 2)) ^2 )) = (2 * ((1 + ( cos x)) / 2)) by SIN_COS:def 19

      .= (1 + ( cos . x)) by SIN_COS:def 19;

      hence thesis;

    end;

    

     Lm2: (2 * (( sin . (x / 2)) ^2 )) = (1 - ( cos . x))

    proof

      (( sin (x / 2)) ^2 ) = ((1 - ( cos (2 * (x / 2)))) / 2) by SIN_COS5: 20

      .= ((1 - ( cos x)) / 2);

      

      then (2 * (( sin . (x / 2)) ^2 )) = (2 * ((1 - ( cos x)) / 2)) by SIN_COS:def 17

      .= (1 - ( cos . x)) by SIN_COS:def 19;

      hence thesis;

    end;

    theorem :: FDIFF_7:4

    Z c= ].( - 1), 1.[ & Z c= ( dom (r (#) arcsin )) implies (r (#) arcsin ) is_differentiable_on Z & for x st x in Z holds (((r (#) arcsin ) `| Z) . x) = (r / ( sqrt (1 - (x ^2 ))))

    proof

      assume that

       A1: Z c= ].( - 1), 1.[ and

       A2: Z c= ( dom (r (#) arcsin ));

      

       A3: arcsin is_differentiable_on Z by A1, FDIFF_1: 26, SIN_COS6: 83;

      for x st x in Z holds (((r (#) arcsin ) `| Z) . x) = (r / ( sqrt (1 - (x ^2 ))))

      proof

        let x;

        assume

         A4: x in Z;

        then

         A5: ( - 1) < x & x < 1 by A1, XXREAL_1: 4;

        (((r (#) arcsin ) `| Z) . x) = (r * ( diff ( arcsin ,x))) by A2, A3, A4, FDIFF_1: 20

        .= (r * (1 / ( sqrt (1 - (x ^2 ))))) by A5, SIN_COS6: 83

        .= (r / ( sqrt (1 - (x ^2 )))) by XCMPLX_1: 99;

        hence thesis;

      end;

      hence thesis by A2, A3, FDIFF_1: 20;

    end;

    theorem :: FDIFF_7:5

    Z c= ].( - 1), 1.[ & Z c= ( dom (r (#) arccos )) implies (r (#) arccos ) is_differentiable_on Z & for x st x in Z holds (((r (#) arccos ) `| Z) . x) = ( - (r / ( sqrt (1 - (x ^2 )))))

    proof

      assume that

       A1: Z c= ].( - 1), 1.[ and

       A2: Z c= ( dom (r (#) arccos ));

      

       A3: arccos is_differentiable_on Z by A1, FDIFF_1: 26, SIN_COS6: 106;

      for x st x in Z holds (((r (#) arccos ) `| Z) . x) = ( - (r / ( sqrt (1 - (x ^2 )))))

      proof

        let x;

        assume

         A4: x in Z;

        then

         A5: ( - 1) < x & x < 1 by A1, XXREAL_1: 4;

        (((r (#) arccos ) `| Z) . x) = (r * ( diff ( arccos ,x))) by A2, A3, A4, FDIFF_1: 20

        .= (r * ( - (1 / ( sqrt (1 - (x ^2 )))))) by A5, SIN_COS6: 106

        .= ( - (r * (1 / ( sqrt (1 - (x ^2 ))))))

        .= ( - (r / ( sqrt (1 - (x ^2 ))))) by XCMPLX_1: 99;

        hence thesis;

      end;

      hence thesis by A2, A3, FDIFF_1: 20;

    end;

    theorem :: FDIFF_7:6

    

     Th6: f is_differentiable_in x & (f . x) > ( - 1) & (f . x) < 1 implies ( arcsin * f) is_differentiable_in x & ( diff (( arcsin * f),x)) = (( diff (f,x)) / ( sqrt (1 - ((f . x) ^2 ))))

    proof

      assume that

       A1: f is_differentiable_in x and

       A2: (f . x) > ( - 1) & (f . x) < 1;

      (f . x) in ].( - 1), 1.[ by A2;

      then

       A3: arcsin is_differentiable_in (f . x) by FDIFF_1: 9, SIN_COS6: 83;

      

      then ( diff (( arcsin * f),x)) = (( diff ( arcsin ,(f . x))) * ( diff (f,x))) by A1, FDIFF_2: 13

      .= (( diff (f,x)) * (1 / ( sqrt (1 - ((f . x) ^2 ))))) by A2, SIN_COS6: 83

      .= (( diff (f,x)) / ( sqrt (1 - ((f . x) ^2 )))) by XCMPLX_1: 99;

      hence thesis by A1, A3, FDIFF_2: 13;

    end;

    theorem :: FDIFF_7:7

    

     Th7: f is_differentiable_in x & (f . x) > ( - 1) & (f . x) < 1 implies ( arccos * f) is_differentiable_in x & ( diff (( arccos * f),x)) = ( - (( diff (f,x)) / ( sqrt (1 - ((f . x) ^2 )))))

    proof

      assume that

       A1: f is_differentiable_in x and

       A2: (f . x) > ( - 1) & (f . x) < 1;

      (f . x) in ].( - 1), 1.[ by A2;

      then

       A3: arccos is_differentiable_in (f . x) by FDIFF_1: 9, SIN_COS6: 106;

      

      then ( diff (( arccos * f),x)) = (( diff ( arccos ,(f . x))) * ( diff (f,x))) by A1, FDIFF_2: 13

      .= (( - (1 / ( sqrt (1 - ((f . x) ^2 ))))) * ( diff (f,x))) by A2, SIN_COS6: 106

      .= ( - (( diff (f,x)) * (1 / ( sqrt (1 - ((f . x) ^2 ))))))

      .= ( - (( diff (f,x)) / ( sqrt (1 - ((f . x) ^2 ))))) by XCMPLX_1: 99;

      hence thesis by A1, A3, FDIFF_2: 13;

    end;

    theorem :: FDIFF_7:8

    Z c= ( dom ( ln * arcsin )) & Z c= ].( - 1), 1.[ & (for x st x in Z holds ( arcsin . x) > 0 ) implies ( ln * arcsin ) is_differentiable_on Z & for x st x in Z holds ((( ln * arcsin ) `| Z) . x) = (1 / (( sqrt (1 - (x ^2 ))) * ( arcsin . x)))

    proof

      assume that

       A1: Z c= ( dom ( ln * arcsin )) and

       A2: Z c= ].( - 1), 1.[ and

       A3: for x st x in Z holds ( arcsin . x) > 0 ;

      

       A4: for x st x in Z holds ( ln * arcsin ) is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then arcsin is_differentiable_in x & ( arcsin . x) > 0 by A2, A3, FDIFF_1: 9, SIN_COS6: 83;

        hence thesis by TAYLOR_1: 20;

      end;

      then

       A5: ( ln * arcsin ) is_differentiable_on Z by A1, FDIFF_1: 9;

      for x st x in Z holds ((( ln * arcsin ) `| Z) . x) = (1 / (( sqrt (1 - (x ^2 ))) * ( arcsin . x)))

      proof

        let x;

        assume

         A6: x in Z;

        then

         A7: ( - 1) < x & x < 1 by A2, XXREAL_1: 4;

         arcsin is_differentiable_in x & ( arcsin . x) > 0 by A2, A3, A6, FDIFF_1: 9, SIN_COS6: 83;

        

        then ( diff (( ln * arcsin ),x)) = (( diff ( arcsin ,x)) / ( arcsin . x)) by TAYLOR_1: 20

        .= ((1 / ( sqrt (1 - (x ^2 )))) / ( arcsin . x)) by A7, SIN_COS6: 83

        .= (1 / (( sqrt (1 - (x ^2 ))) * ( arcsin . x))) by XCMPLX_1: 78;

        hence thesis by A5, A6, FDIFF_1:def 7;

      end;

      hence thesis by A1, A4, FDIFF_1: 9;

    end;

    theorem :: FDIFF_7:9

    Z c= ( dom ( ln * arccos )) & Z c= ].( - 1), 1.[ & (for x st x in Z holds ( arccos . x) > 0 ) implies ( ln * arccos ) is_differentiable_on Z & for x st x in Z holds ((( ln * arccos ) `| Z) . x) = ( - (1 / (( sqrt (1 - (x ^2 ))) * ( arccos . x))))

    proof

      assume that

       A1: Z c= ( dom ( ln * arccos )) and

       A2: Z c= ].( - 1), 1.[ and

       A3: for x st x in Z holds ( arccos . x) > 0 ;

      

       A4: for x st x in Z holds ( ln * arccos ) is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then arccos is_differentiable_in x & ( arccos . x) > 0 by A2, A3, FDIFF_1: 9, SIN_COS6: 106;

        hence thesis by TAYLOR_1: 20;

      end;

      then

       A5: ( ln * arccos ) is_differentiable_on Z by A1, FDIFF_1: 9;

      for x st x in Z holds ((( ln * arccos ) `| Z) . x) = ( - (1 / (( sqrt (1 - (x ^2 ))) * ( arccos . x))))

      proof

        let x;

        assume

         A6: x in Z;

        then

         A7: ( - 1) < x & x < 1 by A2, XXREAL_1: 4;

         arccos is_differentiable_in x & ( arccos . x) > 0 by A2, A3, A6, FDIFF_1: 9, SIN_COS6: 106;

        

        then ( diff (( ln * arccos ),x)) = (( diff ( arccos ,x)) / ( arccos . x)) by TAYLOR_1: 20

        .= (( - (1 / ( sqrt (1 - (x ^2 ))))) / ( arccos . x)) by A7, SIN_COS6: 106

        .= ( - ((1 / ( sqrt (1 - (x ^2 )))) / ( arccos . x))) by XCMPLX_1: 187

        .= ( - (1 / (( sqrt (1 - (x ^2 ))) * ( arccos . x)))) by XCMPLX_1: 78;

        hence thesis by A5, A6, FDIFF_1:def 7;

      end;

      hence thesis by A1, A4, FDIFF_1: 9;

    end;

    theorem :: FDIFF_7:10

    

     Th10: Z c= ( dom (( #Z n) * arcsin )) & Z c= ].( - 1), 1.[ implies (( #Z n) * arcsin ) is_differentiable_on Z & for x st x in Z holds (((( #Z n) * arcsin ) `| Z) . x) = ((n * (( arcsin . x) #Z (n - 1))) / ( sqrt (1 - (x ^2 ))))

    proof

      assume that

       A1: Z c= ( dom (( #Z n) * arcsin )) and

       A2: Z c= ].( - 1), 1.[;

      

       A3: for x st x in Z holds (( #Z n) * arcsin ) is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then arcsin is_differentiable_in x by A2, FDIFF_1: 9, SIN_COS6: 83;

        hence thesis by TAYLOR_1: 3;

      end;

      then

       A4: (( #Z n) * arcsin ) is_differentiable_on Z by A1, FDIFF_1: 9;

      for x st x in Z holds (((( #Z n) * arcsin ) `| Z) . x) = ((n * (( arcsin . x) #Z (n - 1))) / ( sqrt (1 - (x ^2 ))))

      proof

        let x;

        assume

         A5: x in Z;

        then

         A6: ( - 1) < x & x < 1 by A2, XXREAL_1: 4;

        

         A7: arcsin is_differentiable_in x by A2, A5, FDIFF_1: 9, SIN_COS6: 83;

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

        .= ((n * (( arcsin . x) #Z (n - 1))) * ( diff ( arcsin ,x))) by A7, TAYLOR_1: 3

        .= ((n * (( arcsin . x) #Z (n - 1))) * (1 / ( sqrt (1 - (x ^2 ))))) by A6, SIN_COS6: 83

        .= ((n * (( arcsin . x) #Z (n - 1))) / ( sqrt (1 - (x ^2 )))) by XCMPLX_1: 99;

        hence thesis;

      end;

      hence thesis by A1, A3, FDIFF_1: 9;

    end;

    theorem :: FDIFF_7:11

    

     Th11: Z c= ( dom (( #Z n) * arccos )) & Z c= ].( - 1), 1.[ implies (( #Z n) * arccos ) is_differentiable_on Z & for x st x in Z holds (((( #Z n) * arccos ) `| Z) . x) = ( - ((n * (( arccos . x) #Z (n - 1))) / ( sqrt (1 - (x ^2 )))))

    proof

      assume that

       A1: Z c= ( dom (( #Z n) * arccos )) and

       A2: Z c= ].( - 1), 1.[;

      

       A3: for x st x in Z holds (( #Z n) * arccos ) is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then arccos is_differentiable_in x by A2, FDIFF_1: 9, SIN_COS6: 106;

        hence thesis by TAYLOR_1: 3;

      end;

      then

       A4: (( #Z n) * arccos ) is_differentiable_on Z by A1, FDIFF_1: 9;

      for x st x in Z holds (((( #Z n) * arccos ) `| Z) . x) = ( - ((n * (( arccos . x) #Z (n - 1))) / ( sqrt (1 - (x ^2 )))))

      proof

        let x;

        assume

         A5: x in Z;

        then

         A6: ( - 1) < x & x < 1 by A2, XXREAL_1: 4;

        

         A7: arccos is_differentiable_in x by A2, A5, FDIFF_1: 9, SIN_COS6: 106;

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

        .= ((n * (( arccos . x) #Z (n - 1))) * ( diff ( arccos ,x))) by A7, TAYLOR_1: 3

        .= ((n * (( arccos . x) #Z (n - 1))) * ( - (1 / ( sqrt (1 - (x ^2 )))))) by A6, SIN_COS6: 106

        .= ( - ((n * (( arccos . x) #Z (n - 1))) * (1 / ( sqrt (1 - (x ^2 ))))))

        .= ( - ((n * (( arccos . x) #Z (n - 1))) / ( sqrt (1 - (x ^2 ))))) by XCMPLX_1: 99;

        hence thesis;

      end;

      hence thesis by A1, A3, FDIFF_1: 9;

    end;

    theorem :: FDIFF_7:12

    Z c= ( dom ((1 / 2) (#) (( #Z 2) * arcsin ))) & Z c= ].( - 1), 1.[ implies ((1 / 2) (#) (( #Z 2) * arcsin )) is_differentiable_on Z & for x st x in Z holds ((((1 / 2) (#) (( #Z 2) * arcsin )) `| Z) . x) = (( arcsin . x) / ( sqrt (1 - (x ^2 ))))

    proof

      assume that

       A1: Z c= ( dom ((1 / 2) (#) (( #Z 2) * arcsin ))) and

       A2: Z c= ].( - 1), 1.[;

      

       A3: Z c= ( dom (( #Z 2) * arcsin )) by A1, VALUED_1:def 5;

      then

       A4: (( #Z 2) * arcsin ) is_differentiable_on Z by A2, Th10;

      for x st x in Z holds ((((1 / 2) (#) (( #Z 2) * arcsin )) `| Z) . x) = (( arcsin . x) / ( sqrt (1 - (x ^2 ))))

      proof

        let x;

        assume

         A5: x in Z;

        

        then ((((1 / 2) (#) (( #Z 2) * arcsin )) `| Z) . x) = ((1 / 2) * ( diff ((( #Z 2) * arcsin ),x))) by A1, A4, FDIFF_1: 20

        .= ((1 / 2) * (((( #Z 2) * arcsin ) `| Z) . x)) by A4, A5, FDIFF_1:def 7

        .= ((1 / 2) * ((2 * (( arcsin . x) #Z (2 - 1))) / ( sqrt (1 - (x ^2 ))))) by A2, A3, A5, Th10

        .= (((1 / 2) * (2 * (( arcsin . x) #Z (2 - 1)))) / ( sqrt (1 - (x ^2 )))) by XCMPLX_1: 74

        .= (( arcsin . x) / ( sqrt (1 - (x ^2 )))) by PREPOWER: 35;

        hence thesis;

      end;

      hence thesis by A1, A4, FDIFF_1: 20;

    end;

    theorem :: FDIFF_7:13

    Z c= ( dom ((1 / 2) (#) (( #Z 2) * arccos ))) & Z c= ].( - 1), 1.[ implies ((1 / 2) (#) (( #Z 2) * arccos )) is_differentiable_on Z & for x st x in Z holds ((((1 / 2) (#) (( #Z 2) * arccos )) `| Z) . x) = ( - (( arccos . x) / ( sqrt (1 - (x ^2 )))))

    proof

      assume that

       A1: Z c= ( dom ((1 / 2) (#) (( #Z 2) * arccos ))) and

       A2: Z c= ].( - 1), 1.[;

      

       A3: Z c= ( dom (( #Z 2) * arccos )) by A1, VALUED_1:def 5;

      then

       A4: (( #Z 2) * arccos ) is_differentiable_on Z by A2, Th11;

      for x st x in Z holds ((((1 / 2) (#) (( #Z 2) * arccos )) `| Z) . x) = ( - (( arccos . x) / ( sqrt (1 - (x ^2 )))))

      proof

        let x;

        assume

         A5: x in Z;

        

        then ((((1 / 2) (#) (( #Z 2) * arccos )) `| Z) . x) = ((1 / 2) * ( diff ((( #Z 2) * arccos ),x))) by A1, A4, FDIFF_1: 20

        .= ((1 / 2) * (((( #Z 2) * arccos ) `| Z) . x)) by A4, A5, FDIFF_1:def 7

        .= ((1 / 2) * ( - ((2 * (( arccos . x) #Z (2 - 1))) / ( sqrt (1 - (x ^2 )))))) by A2, A3, A5, Th11

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

        .= ( - (((1 / 2) * (2 * (( arccos . x) #Z (2 - 1)))) / ( sqrt (1 - (x ^2 ))))) by XCMPLX_1: 74

        .= ( - (( arccos . x) / ( sqrt (1 - (x ^2 ))))) by PREPOWER: 35;

        hence thesis;

      end;

      hence thesis by A1, A4, FDIFF_1: 20;

    end;

    theorem :: FDIFF_7:14

    

     Th14: Z c= ( dom ( arcsin * f)) & (for x st x in Z holds (f . x) = ((a * x) + b) & (f . x) > ( - 1) & (f . x) < 1) implies ( arcsin * f) is_differentiable_on Z & for x st x in Z holds ((( arcsin * f) `| Z) . x) = (a / ( sqrt (1 - (((a * x) + b) ^2 ))))

    proof

      assume that

       A1: Z c= ( dom ( arcsin * f)) and

       A2: for x st x in Z holds (f . x) = ((a * x) + b) & (f . x) > ( - 1) & (f . x) < 1;

      for y be object st y in Z holds y in ( dom f) by A1, FUNCT_1: 11;

      then

       A3: Z c= ( dom f) by TARSKI:def 3;

      

       A4: for x st x in Z holds (f . x) = ((a * x) + b) by A2;

      then

       A5: f is_differentiable_on Z by A3, FDIFF_1: 23;

      

       A6: for x st x in Z holds ( arcsin * f) is_differentiable_in x

      proof

        let x;

        assume

         A7: x in Z;

        then

         A8: (f . x) < 1 by A2;

        f is_differentiable_in x & (f . x) > ( - 1) by A2, A5, A7, FDIFF_1: 9;

        hence thesis by A8, Th6;

      end;

      then

       A9: ( arcsin * f) is_differentiable_on Z by A1, FDIFF_1: 9;

      for x st x in Z holds ((( arcsin * f) `| Z) . x) = (a / ( sqrt (1 - (((a * x) + b) ^2 ))))

      proof

        let x;

        assume

         A10: x in Z;

        then

         A11: (f . x) < 1 by A2;

        f is_differentiable_in x & (f . x) > ( - 1) by A2, A5, A10, FDIFF_1: 9;

        

        then ( diff (( arcsin * f),x)) = (( diff (f,x)) / ( sqrt (1 - ((f . x) ^2 )))) by A11, Th6

        .= (((f `| Z) . x) / ( sqrt (1 - ((f . x) ^2 )))) by A5, A10, FDIFF_1:def 7

        .= (a / ( sqrt (1 - ((f . x) ^2 )))) by A4, A3, A10, FDIFF_1: 23

        .= (a / ( sqrt (1 - (((a * x) + b) ^2 )))) by A2, A10;

        hence thesis by A9, A10, FDIFF_1:def 7;

      end;

      hence thesis by A1, A6, FDIFF_1: 9;

    end;

    theorem :: FDIFF_7:15

    

     Th15: Z c= ( dom ( arccos * f)) & (for x st x in Z holds (f . x) = ((a * x) + b) & (f . x) > ( - 1) & (f . x) < 1) implies ( arccos * f) is_differentiable_on Z & for x st x in Z holds ((( arccos * f) `| Z) . x) = ( - (a / ( sqrt (1 - (((a * x) + b) ^2 )))))

    proof

      assume that

       A1: Z c= ( dom ( arccos * f)) and

       A2: for x st x in Z holds (f . x) = ((a * x) + b) & (f . x) > ( - 1) & (f . x) < 1;

      for y be object st y in Z holds y in ( dom f) by A1, FUNCT_1: 11;

      then

       A3: Z c= ( dom f) by TARSKI:def 3;

      

       A4: for x st x in Z holds (f . x) = ((a * x) + b) by A2;

      then

       A5: f is_differentiable_on Z by A3, FDIFF_1: 23;

      

       A6: for x st x in Z holds ( arccos * f) is_differentiable_in x

      proof

        let x;

        assume

         A7: x in Z;

        then

         A8: (f . x) < 1 by A2;

        f is_differentiable_in x & (f . x) > ( - 1) by A2, A5, A7, FDIFF_1: 9;

        hence thesis by A8, Th7;

      end;

      then

       A9: ( arccos * f) is_differentiable_on Z by A1, FDIFF_1: 9;

      for x st x in Z holds ((( arccos * f) `| Z) . x) = ( - (a / ( sqrt (1 - (((a * x) + b) ^2 )))))

      proof

        let x;

        assume

         A10: x in Z;

        then

         A11: (f . x) < 1 by A2;

        f is_differentiable_in x & (f . x) > ( - 1) by A2, A5, A10, FDIFF_1: 9;

        

        then ( diff (( arccos * f),x)) = ( - (( diff (f,x)) / ( sqrt (1 - ((f . x) ^2 ))))) by A11, Th7

        .= ( - (((f `| Z) . x) / ( sqrt (1 - ((f . x) ^2 ))))) by A5, A10, FDIFF_1:def 7

        .= ( - (a / ( sqrt (1 - ((f . x) ^2 ))))) by A4, A3, A10, FDIFF_1: 23

        .= ( - (a / ( sqrt (1 - (((a * x) + b) ^2 ))))) by A2, A10;

        hence thesis by A9, A10, FDIFF_1:def 7;

      end;

      hence thesis by A1, A6, FDIFF_1: 9;

    end;

    theorem :: FDIFF_7:16

    

     Th16: Z c= ( dom (( id Z) (#) arcsin )) & Z c= ].( - 1), 1.[ implies (( id Z) (#) arcsin ) is_differentiable_on Z & for x st x in Z holds (((( id Z) (#) arcsin ) `| Z) . x) = (( arcsin . x) + (x / ( sqrt (1 - (x ^2 )))))

    proof

      assume that

       A1: Z c= ( dom (( id Z) (#) arcsin )) and

       A2: Z c= ].( - 1), 1.[;

      

       A3: for x st x in Z holds (( id Z) . x) = ((1 * x) + 0 ) by FUNCT_1: 18;

      Z c= (( dom ( id Z)) /\ ( dom arcsin )) by A1, VALUED_1:def 4;

      then

       A4: Z c= ( dom ( id Z)) by XBOOLE_1: 18;

      then

       A5: ( id Z) is_differentiable_on Z by A3, FDIFF_1: 23;

      

       A6: arcsin is_differentiable_on Z by A2, FDIFF_1: 26, SIN_COS6: 83;

      for x st x in Z holds (((( id Z) (#) arcsin ) `| Z) . x) = (( arcsin . x) + (x / ( sqrt (1 - (x ^2 )))))

      proof

        let x;

        assume

         A7: x in Z;

        then

         A8: ( - 1) < x & x < 1 by A2, XXREAL_1: 4;

        (((( id Z) (#) arcsin ) `| Z) . x) = ((( arcsin . x) * ( diff (( id Z),x))) + ((( id Z) . x) * ( diff ( arcsin ,x)))) by A1, A5, A6, A7, FDIFF_1: 21

        .= ((( arcsin . x) * ((( id Z) `| Z) . x)) + ((( id Z) . x) * ( diff ( arcsin ,x)))) by A5, A7, FDIFF_1:def 7

        .= ((( arcsin . x) * 1) + ((( id Z) . x) * ( diff ( arcsin ,x)))) by A4, A3, A7, FDIFF_1: 23

        .= ((( arcsin . x) * 1) + ((( id Z) . x) * (1 / ( sqrt (1 - (x ^2 )))))) by A8, SIN_COS6: 83

        .= (( arcsin . x) + (x * (1 / ( sqrt (1 - (x ^2 )))))) by A7, FUNCT_1: 18

        .= (( arcsin . x) + (x / ( sqrt (1 - (x ^2 ))))) by XCMPLX_1: 99;

        hence thesis;

      end;

      hence thesis by A1, A5, A6, FDIFF_1: 21;

    end;

    theorem :: FDIFF_7:17

    

     Th17: Z c= ( dom (( id Z) (#) arccos )) & Z c= ].( - 1), 1.[ implies (( id Z) (#) arccos ) is_differentiable_on Z & for x st x in Z holds (((( id Z) (#) arccos ) `| Z) . x) = (( arccos . x) - (x / ( sqrt (1 - (x ^2 )))))

    proof

      assume that

       A1: Z c= ( dom (( id Z) (#) arccos )) and

       A2: Z c= ].( - 1), 1.[;

      

       A3: for x st x in Z holds (( id Z) . x) = ((1 * x) + 0 ) by FUNCT_1: 18;

      Z c= (( dom ( id Z)) /\ ( dom arccos )) by A1, VALUED_1:def 4;

      then

       A4: Z c= ( dom ( id Z)) by XBOOLE_1: 18;

      then

       A5: ( id Z) is_differentiable_on Z by A3, FDIFF_1: 23;

      

       A6: arccos is_differentiable_on Z by A2, FDIFF_1: 26, SIN_COS6: 106;

      for x st x in Z holds (((( id Z) (#) arccos ) `| Z) . x) = (( arccos . x) - (x / ( sqrt (1 - (x ^2 )))))

      proof

        let x;

        assume

         A7: x in Z;

        then

         A8: ( - 1) < x & x < 1 by A2, XXREAL_1: 4;

        (((( id Z) (#) arccos ) `| Z) . x) = ((( arccos . x) * ( diff (( id Z),x))) + ((( id Z) . x) * ( diff ( arccos ,x)))) by A1, A5, A6, A7, FDIFF_1: 21

        .= ((( arccos . x) * ((( id Z) `| Z) . x)) + ((( id Z) . x) * ( diff ( arccos ,x)))) by A5, A7, FDIFF_1:def 7

        .= ((( arccos . x) * 1) + ((( id Z) . x) * ( diff ( arccos ,x)))) by A4, A3, A7, FDIFF_1: 23

        .= ((( arccos . x) * 1) + ((( id Z) . x) * ( - (1 / ( sqrt (1 - (x ^2 ))))))) by A8, SIN_COS6: 106

        .= (( arccos . x) + (x * ( - (1 / ( sqrt (1 - (x ^2 ))))))) by A7, FUNCT_1: 18

        .= (( arccos . x) - (x * (1 / ( sqrt (1 - (x ^2 ))))))

        .= (( arccos . x) - (x / ( sqrt (1 - (x ^2 ))))) by XCMPLX_1: 99;

        hence thesis;

      end;

      hence thesis by A1, A5, A6, FDIFF_1: 21;

    end;

    theorem :: FDIFF_7:18

    Z c= ( dom (f (#) arcsin )) & Z c= ].( - 1), 1.[ & (for x st x in Z holds (f . x) = ((a * x) + b)) implies (f (#) arcsin ) is_differentiable_on Z & for x st x in Z holds (((f (#) arcsin ) `| Z) . x) = ((a * ( arcsin . x)) + (((a * x) + b) / ( sqrt (1 - (x ^2 )))))

    proof

      assume that

       A1: Z c= ( dom (f (#) arcsin )) and

       A2: Z c= ].( - 1), 1.[ and

       A3: for x st x in Z holds (f . x) = ((a * x) + b);

      Z c= (( dom f) /\ ( dom arcsin )) by A1, VALUED_1:def 4;

      then

       A4: Z c= ( dom f) by XBOOLE_1: 18;

      then

       A5: f is_differentiable_on Z by A3, FDIFF_1: 23;

      

       A6: arcsin is_differentiable_on Z by A2, FDIFF_1: 26, SIN_COS6: 83;

      for x st x in Z holds (((f (#) arcsin ) `| Z) . x) = ((a * ( arcsin . x)) + (((a * x) + b) / ( sqrt (1 - (x ^2 )))))

      proof

        let x;

        assume

         A7: x in Z;

        then

         A8: ( - 1) < x & x < 1 by A2, XXREAL_1: 4;

        (((f (#) arcsin ) `| Z) . x) = ((( arcsin . x) * ( diff (f,x))) + ((f . x) * ( diff ( arcsin ,x)))) by A1, A5, A6, A7, FDIFF_1: 21

        .= ((( arcsin . x) * ((f `| Z) . x)) + ((f . x) * ( diff ( arcsin ,x)))) by A5, A7, FDIFF_1:def 7

        .= ((( arcsin . x) * a) + ((f . x) * ( diff ( arcsin ,x)))) by A3, A4, A7, FDIFF_1: 23

        .= ((( arcsin . x) * a) + ((f . x) * (1 / ( sqrt (1 - (x ^2 )))))) by A8, SIN_COS6: 83

        .= ((a * ( arcsin . x)) + (((a * x) + b) * (1 / ( sqrt (1 - (x ^2 )))))) by A3, A7

        .= ((a * ( arcsin . x)) + (((a * x) + b) / ( sqrt (1 - (x ^2 ))))) by XCMPLX_1: 99;

        hence thesis;

      end;

      hence thesis by A1, A5, A6, FDIFF_1: 21;

    end;

    theorem :: FDIFF_7:19

    Z c= ( dom (f (#) arccos )) & Z c= ].( - 1), 1.[ & (for x st x in Z holds (f . x) = ((a * x) + b)) implies (f (#) arccos ) is_differentiable_on Z & for x st x in Z holds (((f (#) arccos ) `| Z) . x) = ((a * ( arccos . x)) - (((a * x) + b) / ( sqrt (1 - (x ^2 )))))

    proof

      assume that

       A1: Z c= ( dom (f (#) arccos )) and

       A2: Z c= ].( - 1), 1.[ and

       A3: for x st x in Z holds (f . x) = ((a * x) + b);

      Z c= (( dom f) /\ ( dom arccos )) by A1, VALUED_1:def 4;

      then

       A4: Z c= ( dom f) by XBOOLE_1: 18;

      then

       A5: f is_differentiable_on Z by A3, FDIFF_1: 23;

      

       A6: arccos is_differentiable_on Z by A2, FDIFF_1: 26, SIN_COS6: 106;

      for x st x in Z holds (((f (#) arccos ) `| Z) . x) = ((a * ( arccos . x)) - (((a * x) + b) / ( sqrt (1 - (x ^2 )))))

      proof

        let x;

        assume

         A7: x in Z;

        then

         A8: ( - 1) < x & x < 1 by A2, XXREAL_1: 4;

        (((f (#) arccos ) `| Z) . x) = ((( arccos . x) * ( diff (f,x))) + ((f . x) * ( diff ( arccos ,x)))) by A1, A5, A6, A7, FDIFF_1: 21

        .= ((( arccos . x) * ((f `| Z) . x)) + ((f . x) * ( diff ( arccos ,x)))) by A5, A7, FDIFF_1:def 7

        .= ((( arccos . x) * a) + ((f . x) * ( diff ( arccos ,x)))) by A3, A4, A7, FDIFF_1: 23

        .= ((( arccos . x) * a) + ((f . x) * ( - (1 / ( sqrt (1 - (x ^2 ))))))) by A8, SIN_COS6: 106

        .= ((( arccos . x) * a) - ((f . x) * (1 / ( sqrt (1 - (x ^2 ))))))

        .= ((a * ( arccos . x)) - (((a * x) + b) * (1 / ( sqrt (1 - (x ^2 )))))) by A3, A7

        .= ((a * ( arccos . x)) - (((a * x) + b) / ( sqrt (1 - (x ^2 ))))) by XCMPLX_1: 99;

        hence thesis;

      end;

      hence thesis by A1, A5, A6, FDIFF_1: 21;

    end;

    theorem :: FDIFF_7:20

    Z c= ( dom ((1 / 2) (#) ( arcsin * f))) & (for x st x in Z holds (f . x) = (2 * x) & (f . x) > ( - 1) & (f . x) < 1) implies ((1 / 2) (#) ( arcsin * f)) is_differentiable_on Z & for x st x in Z holds ((((1 / 2) (#) ( arcsin * f)) `| Z) . x) = (1 / ( sqrt (1 - ((2 * x) ^2 ))))

    proof

      assume that

       A1: Z c= ( dom ((1 / 2) (#) ( arcsin * f))) and

       A2: for x st x in Z holds (f . x) = (2 * x) & (f . x) > ( - 1) & (f . x) < 1;

      

       A3: Z c= ( dom ( arcsin * f)) & for x st x in Z holds (f . x) = ((2 * x) + 0 ) & (f . x) > ( - 1) & (f . x) < 1 by A1, A2, VALUED_1:def 5;

      then

       A4: ( arcsin * f) is_differentiable_on Z by Th14;

      for x st x in Z holds ((((1 / 2) (#) ( arcsin * f)) `| Z) . x) = (1 / ( sqrt (1 - ((2 * x) ^2 ))))

      proof

        let x;

        assume

         A5: x in Z;

        

        then ((((1 / 2) (#) ( arcsin * f)) `| Z) . x) = ((1 / 2) * ( diff (( arcsin * f),x))) by A1, A4, FDIFF_1: 20

        .= ((1 / 2) * ((( arcsin * f) `| Z) . x)) by A4, A5, FDIFF_1:def 7

        .= ((1 / 2) * (2 / ( sqrt (1 - (((2 * x) + 0 ) ^2 ))))) by A3, A5, Th14

        .= (((1 / 2) * 2) / ( sqrt (1 - ((2 * x) ^2 )))) by XCMPLX_1: 74

        .= (1 / ( sqrt (1 - ((2 * x) ^2 ))));

        hence thesis;

      end;

      hence thesis by A1, A4, FDIFF_1: 20;

    end;

    theorem :: FDIFF_7:21

    Z c= ( dom ((1 / 2) (#) ( arccos * f))) & (for x st x in Z holds (f . x) = (2 * x) & (f . x) > ( - 1) & (f . x) < 1) implies ((1 / 2) (#) ( arccos * f)) is_differentiable_on Z & for x st x in Z holds ((((1 / 2) (#) ( arccos * f)) `| Z) . x) = ( - (1 / ( sqrt (1 - ((2 * x) ^2 )))))

    proof

      assume that

       A1: Z c= ( dom ((1 / 2) (#) ( arccos * f))) and

       A2: for x st x in Z holds (f . x) = (2 * x) & (f . x) > ( - 1) & (f . x) < 1;

      

       A3: Z c= ( dom ( arccos * f)) & for x st x in Z holds (f . x) = ((2 * x) + 0 ) & (f . x) > ( - 1) & (f . x) < 1 by A1, A2, VALUED_1:def 5;

      then

       A4: ( arccos * f) is_differentiable_on Z by Th15;

      for x st x in Z holds ((((1 / 2) (#) ( arccos * f)) `| Z) . x) = ( - (1 / ( sqrt (1 - ((2 * x) ^2 )))))

      proof

        let x;

        assume

         A5: x in Z;

        

        then ((((1 / 2) (#) ( arccos * f)) `| Z) . x) = ((1 / 2) * ( diff (( arccos * f),x))) by A1, A4, FDIFF_1: 20

        .= ((1 / 2) * ((( arccos * f) `| Z) . x)) by A4, A5, FDIFF_1:def 7

        .= ((1 / 2) * ( - (2 / ( sqrt (1 - (((2 * x) + 0 ) ^2 )))))) by A3, A5, Th15

        .= ( - ((1 / 2) * (2 / ( sqrt (1 - ((2 * x) ^2 ))))))

        .= ( - (((1 / 2) * 2) / ( sqrt (1 - ((2 * x) ^2 ))))) by XCMPLX_1: 74

        .= ( - (1 / ( sqrt (1 - ((2 * x) ^2 )))));

        hence thesis;

      end;

      hence thesis by A1, A4, FDIFF_1: 20;

    end;

    theorem :: FDIFF_7:22

    

     Th22: Z c= ( dom (( #R (1 / 2)) * f)) & f = (f1 - f2) & f2 = ( #Z 2) & (for x st x in Z holds (f1 . x) = 1 & (f . x) > 0 ) implies (( #R (1 / 2)) * f) is_differentiable_on Z & for x st x in Z holds (((( #R (1 / 2)) * f) `| Z) . x) = ( - (x * ((1 - (x #Z 2)) #R ( - (1 / 2)))))

    proof

      assume that

       A1: Z c= ( dom (( #R (1 / 2)) * f)) and

       A2: f = (f1 - f2) and

       A3: f2 = ( #Z 2) and

       A4: for x st x in Z holds (f1 . x) = 1 & (f . x) > 0 ;

      for y be object st y in Z holds y in ( dom f) by A1, FUNCT_1: 11;

      then

       A5: Z c= ( dom (f1 + (( - 1) (#) f2))) by A2, TARSKI:def 3;

      

       A6: for x st x in Z holds (f1 . x) = (1 + ( 0 * x)) by A4;

      then

       A7: f is_differentiable_on Z by A2, A3, A5, FDIFF_4: 12;

      

       A8: for x st x in Z holds (( #R (1 / 2)) * f) is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then f is_differentiable_in x & (f . x) > 0 by A4, A7, FDIFF_1: 9;

        hence thesis by TAYLOR_1: 22;

      end;

      then

       A9: (( #R (1 / 2)) * f) is_differentiable_on Z by A1, FDIFF_1: 9;

      for x st x in Z holds (((( #R (1 / 2)) * f) `| Z) . x) = ( - (x * ((1 - (x #Z 2)) #R ( - (1 / 2)))))

      proof

        let x;

        assume

         A10: x in Z;

        then

         A11: f is_differentiable_in x & (f . x) > 0 by A4, A7, FDIFF_1: 9;

        x in ( dom (f1 - f2)) by A1, A2, A10, FUNCT_1: 11;

        

        then

         A12: ((f1 - f2) . x) = ((f1 . x) - (f2 . x)) by VALUED_1: 13

        .= (1 - (f2 . x)) by A4, A10

        .= (1 - (x #Z 2)) by A3, TAYLOR_1:def 1;

        (((( #R (1 / 2)) * f) `| Z) . x) = ( diff ((( #R (1 / 2)) * f),x)) by A9, A10, FDIFF_1:def 7

        .= (((1 / 2) * ((f . x) #R ((1 / 2) - 1))) * ( diff (f,x))) by A11, TAYLOR_1: 22

        .= (((1 / 2) * ((f . x) #R ((1 / 2) - 1))) * ((f `| Z) . x)) by A7, A10, FDIFF_1:def 7

        .= (((1 / 2) * ((f . x) #R ((1 / 2) - 1))) * ( 0 + ((2 * ( - 1)) * x))) by A2, A3, A5, A6, A10, FDIFF_4: 12

        .= ( - (x * ((1 - (x #Z 2)) #R ( - (1 / 2))))) by A2, A12;

        hence thesis;

      end;

      hence thesis by A1, A8, FDIFF_1: 9;

    end;

    theorem :: FDIFF_7:23

    Z c= ( dom ((( id Z) (#) arcsin ) + (( #R (1 / 2)) * f))) & Z c= ].( - 1), 1.[ & f = (f1 - f2) & f2 = ( #Z 2) & (for x st x in Z holds (f1 . x) = 1 & (f . x) > 0 & x <> 0 ) implies ((( id Z) (#) arcsin ) + (( #R (1 / 2)) * f)) is_differentiable_on Z & for x st x in Z holds ((((( id Z) (#) arcsin ) + (( #R (1 / 2)) * f)) `| Z) . x) = ( arcsin . x)

    proof

      assume that

       A1: Z c= ( dom ((( id Z) (#) arcsin ) + (( #R (1 / 2)) * f))) and

       A2: Z c= ].( - 1), 1.[ and

       A3: f = (f1 - f2) and

       A4: f2 = ( #Z 2) and

       A5: for x st x in Z holds (f1 . x) = 1 & (f . x) > 0 & x <> 0 ;

      

       A6: Z c= (( dom (( id Z) (#) arcsin )) /\ ( dom (( #R (1 / 2)) * f))) by A1, VALUED_1:def 1;

      then

       A7: Z c= ( dom (( #R (1 / 2)) * f)) by XBOOLE_1: 18;

      

       A8: Z c= ( dom (( id Z) (#) arcsin )) by A6, XBOOLE_1: 18;

      then

       A9: (( id Z) (#) arcsin ) is_differentiable_on Z by A2, Th16;

      

       A10: for x st x in Z holds (f1 . x) = 1 & (f . x) > 0 by A5;

      then

       A11: (( #R (1 / 2)) * f) is_differentiable_on Z by A3, A4, A7, Th22;

      

       A12: for x st x in Z holds (x * ((1 - (x #Z 2)) #R ( - (1 / 2)))) = (x / ( sqrt (1 - (x ^2 ))))

      proof

        let x;

        assume

         A13: x in Z;

        then x in ( dom (f1 - f2)) by A3, A7, FUNCT_1: 11;

        

        then

         A14: ((f1 - f2) . x) = ((f1 . x) - (f2 . x)) by VALUED_1: 13

        .= (1 - (f2 . x)) by A5, A13

        .= (1 - (x #Z 2)) by A4, TAYLOR_1:def 1;

        (f . x) > 0 by A5, A13;

        then

         A15: (1 - (x ^2 )) > 0 by A3, A14, Th1;

        ((1 - (x #Z 2)) #R ( - (1 / 2))) = ((1 - (x ^2 )) #R ( - (1 / 2))) by Th1

        .= (1 / ( sqrt (1 - (x ^2 )))) by A15, Th3;

        hence thesis by XCMPLX_1: 99;

      end;

      for x st x in Z holds ((((( id Z) (#) arcsin ) + (( #R (1 / 2)) * f)) `| Z) . x) = ( arcsin . x)

      proof

        let x;

        assume

         A16: x in Z;

        

        hence ((((( id Z) (#) arcsin ) + (( #R (1 / 2)) * f)) `| Z) . x) = (( diff ((( id Z) (#) arcsin ),x)) + ( diff ((( #R (1 / 2)) * f),x))) by A1, A9, A11, FDIFF_1: 18

        .= ((((( id Z) (#) arcsin ) `| Z) . x) + ( diff ((( #R (1 / 2)) * f),x))) by A9, A16, FDIFF_1:def 7

        .= ((((( id Z) (#) arcsin ) `| Z) . x) + (((( #R (1 / 2)) * f) `| Z) . x)) by A11, A16, FDIFF_1:def 7

        .= ((( arcsin . x) + (x / ( sqrt (1 - (x ^2 ))))) + (((( #R (1 / 2)) * f) `| Z) . x)) by A2, A8, A16, Th16

        .= ((( arcsin . x) + (x / ( sqrt (1 - (x ^2 ))))) + ( - (x * ((1 - (x #Z 2)) #R ( - (1 / 2)))))) by A3, A4, A10, A7, A16, Th22

        .= ((( arcsin . x) + (x / ( sqrt (1 - (x ^2 ))))) - (x * ((1 - (x #Z 2)) #R ( - (1 / 2)))))

        .= ((( arcsin . x) + (x / ( sqrt (1 - (x ^2 ))))) - (x / ( sqrt (1 - (x ^2 ))))) by A12, A16

        .= ( arcsin . x);

      end;

      hence thesis by A1, A9, A11, FDIFF_1: 18;

    end;

    theorem :: FDIFF_7:24

    Z c= ( dom ((( id Z) (#) arccos ) - (( #R (1 / 2)) * f))) & Z c= ].( - 1), 1.[ & f = (f1 - f2) & f2 = ( #Z 2) & (for x st x in Z holds (f1 . x) = 1 & (f . x) > 0 & x <> 0 ) implies ((( id Z) (#) arccos ) - (( #R (1 / 2)) * f)) is_differentiable_on Z & for x st x in Z holds ((((( id Z) (#) arccos ) - (( #R (1 / 2)) * f)) `| Z) . x) = ( arccos . x)

    proof

      assume that

       A1: Z c= ( dom ((( id Z) (#) arccos ) - (( #R (1 / 2)) * f))) and

       A2: Z c= ].( - 1), 1.[ and

       A3: f = (f1 - f2) and

       A4: f2 = ( #Z 2) and

       A5: for x st x in Z holds (f1 . x) = 1 & (f . x) > 0 & x <> 0 ;

      

       A6: Z c= (( dom (( id Z) (#) arccos )) /\ ( dom (( #R (1 / 2)) * f))) by A1, VALUED_1: 12;

      then

       A7: Z c= ( dom (( #R (1 / 2)) * f)) by XBOOLE_1: 18;

      

       A8: Z c= ( dom (( id Z) (#) arccos )) by A6, XBOOLE_1: 18;

      then

       A9: (( id Z) (#) arccos ) is_differentiable_on Z by A2, Th17;

      

       A10: for x st x in Z holds (f1 . x) = 1 & (f . x) > 0 by A5;

      then

       A11: (( #R (1 / 2)) * f) is_differentiable_on Z by A3, A4, A7, Th22;

      

       A12: for x st x in Z holds (x * ((1 - (x #Z 2)) #R ( - (1 / 2)))) = (x / ( sqrt (1 - (x ^2 ))))

      proof

        let x;

        assume

         A13: x in Z;

        then x in ( dom (f1 - f2)) by A3, A7, FUNCT_1: 11;

        

        then

         A14: ((f1 - f2) . x) = ((f1 . x) - (f2 . x)) by VALUED_1: 13

        .= (1 - (f2 . x)) by A5, A13

        .= (1 - (x #Z 2)) by A4, TAYLOR_1:def 1;

        (f . x) > 0 by A5, A13;

        then

         A15: (1 - (x ^2 )) > 0 by A3, A14, Th1;

        ((1 - (x #Z 2)) #R ( - (1 / 2))) = ((1 - (x ^2 )) #R ( - (1 / 2))) by Th1

        .= (1 / ( sqrt (1 - (x ^2 )))) by A15, Th3;

        hence thesis by XCMPLX_1: 99;

      end;

      for x st x in Z holds ((((( id Z) (#) arccos ) - (( #R (1 / 2)) * f)) `| Z) . x) = ( arccos . x)

      proof

        let x;

        assume

         A16: x in Z;

        

        hence ((((( id Z) (#) arccos ) - (( #R (1 / 2)) * f)) `| Z) . x) = (( diff ((( id Z) (#) arccos ),x)) - ( diff ((( #R (1 / 2)) * f),x))) by A1, A9, A11, FDIFF_1: 19

        .= ((((( id Z) (#) arccos ) `| Z) . x) - ( diff ((( #R (1 / 2)) * f),x))) by A9, A16, FDIFF_1:def 7

        .= ((((( id Z) (#) arccos ) `| Z) . x) - (((( #R (1 / 2)) * f) `| Z) . x)) by A11, A16, FDIFF_1:def 7

        .= ((( arccos . x) - (x / ( sqrt (1 - (x ^2 ))))) - (((( #R (1 / 2)) * f) `| Z) . x)) by A2, A8, A16, Th17

        .= ((( arccos . x) - (x / ( sqrt (1 - (x ^2 ))))) - ( - (x * ((1 - (x #Z 2)) #R ( - (1 / 2)))))) by A3, A4, A10, A7, A16, Th22

        .= ((( arccos . x) - (x / ( sqrt (1 - (x ^2 ))))) + (x * ((1 - (x #Z 2)) #R ( - (1 / 2)))))

        .= ((( arccos . x) - (x / ( sqrt (1 - (x ^2 ))))) + (x / ( sqrt (1 - (x ^2 ))))) by A12, A16

        .= ( arccos . x);

      end;

      hence thesis by A1, A9, A11, FDIFF_1: 19;

    end;

    theorem :: FDIFF_7:25

    

     Th25: Z c= ( dom (( id Z) (#) ( arcsin * f))) & (for x st x in Z holds (f . x) = (x / a) & (f . x) > ( - 1) & (f . x) < 1) implies (( id Z) (#) ( arcsin * f)) is_differentiable_on Z & for x st x in Z holds (((( id Z) (#) ( arcsin * f)) `| Z) . x) = (( arcsin . (x / a)) + (x / (a * ( sqrt (1 - ((x / a) ^2 ))))))

    proof

      assume that

       A1: Z c= ( dom (( id Z) (#) ( arcsin * f))) and

       A2: for x st x in Z holds (f . x) = (x / a) & (f . x) > ( - 1) & (f . x) < 1;

      

       A3: Z c= (( dom ( id Z)) /\ ( dom ( arcsin * f))) by A1, VALUED_1:def 4;

      then

       A4: Z c= ( dom ( id Z)) by XBOOLE_1: 18;

      

       A5: Z c= ( dom ( arcsin * f)) by A3, XBOOLE_1: 18;

      for x st x in Z holds (f . x) = (((1 / a) * x) + 0 )

      proof

        let x;

        assume x in Z;

        then (f . x) = (x / a) by A2;

        hence thesis by XCMPLX_1: 99;

      end;

      then

       A6: for x st x in Z holds (f . x) = (((1 / a) * x) + 0 ) & (f . x) > ( - 1) & (f . x) < 1 by A2;

      then

       A7: ( arcsin * f) is_differentiable_on Z by A5, Th14;

      

       A8: for x st x in Z holds (( id Z) . x) = ((1 * x) + 0 ) by FUNCT_1: 18;

      then

       A9: ( id Z) is_differentiable_on Z by A4, FDIFF_1: 23;

      

       A10: for x st x in Z holds ((( arcsin * f) `| Z) . x) = (1 / (a * ( sqrt (1 - ((x / a) ^2 )))))

      proof

        let x;

        assume x in Z;

        

        then ((( arcsin * f) `| Z) . x) = ((1 / a) / ( sqrt (1 - ((((1 / a) * x) + 0 ) ^2 )))) by A6, A5, Th14

        .= ((1 / a) / ( sqrt (1 - ((x / a) ^2 )))) by XCMPLX_1: 99

        .= (1 / (a * ( sqrt (1 - ((x / a) ^2 ))))) by XCMPLX_1: 78;

        hence thesis;

      end;

      for x st x in Z holds (((( id Z) (#) ( arcsin * f)) `| Z) . x) = (( arcsin . (x / a)) + (x / (a * ( sqrt (1 - ((x / a) ^2 ))))))

      proof

        let x;

        assume

         A11: x in Z;

        

        then

         A12: (( arcsin * f) . x) = ( arcsin . (f . x)) by A5, FUNCT_1: 12

        .= ( arcsin . (x / a)) by A2, A11;

        (((( id Z) (#) ( arcsin * f)) `| Z) . x) = (((( arcsin * f) . x) * ( diff (( id Z),x))) + ((( id Z) . x) * ( diff (( arcsin * f),x)))) by A1, A9, A7, A11, FDIFF_1: 21

        .= (((( arcsin * f) . x) * ((( id Z) `| Z) . x)) + ((( id Z) . x) * ( diff (( arcsin * f),x)))) by A9, A11, FDIFF_1:def 7

        .= (((( arcsin * f) . x) * 1) + ((( id Z) . x) * ( diff (( arcsin * f),x)))) by A4, A8, A11, FDIFF_1: 23

        .= (((( arcsin * f) . x) * 1) + ((( id Z) . x) * ((( arcsin * f) `| Z) . x))) by A7, A11, FDIFF_1:def 7

        .= ((( arcsin * f) . x) + (x * ((( arcsin * f) `| Z) . x))) by A11, FUNCT_1: 18

        .= (( arcsin . (x / a)) + (x * (1 / (a * ( sqrt (1 - ((x / a) ^2 ))))))) by A10, A11, A12

        .= (( arcsin . (x / a)) + (x / (a * ( sqrt (1 - ((x / a) ^2 )))))) by XCMPLX_1: 99;

        hence thesis;

      end;

      hence thesis by A1, A9, A7, FDIFF_1: 21;

    end;

    theorem :: FDIFF_7:26

    

     Th26: Z c= ( dom (( id Z) (#) ( arccos * f))) & (for x st x in Z holds (f . x) = (x / a) & (f . x) > ( - 1) & (f . x) < 1) implies (( id Z) (#) ( arccos * f)) is_differentiable_on Z & for x st x in Z holds (((( id Z) (#) ( arccos * f)) `| Z) . x) = (( arccos . (x / a)) - (x / (a * ( sqrt (1 - ((x / a) ^2 ))))))

    proof

      assume that

       A1: Z c= ( dom (( id Z) (#) ( arccos * f))) and

       A2: for x st x in Z holds (f . x) = (x / a) & (f . x) > ( - 1) & (f . x) < 1;

      

       A3: Z c= (( dom ( id Z)) /\ ( dom ( arccos * f))) by A1, VALUED_1:def 4;

      then

       A4: Z c= ( dom ( id Z)) by XBOOLE_1: 18;

      

       A5: Z c= ( dom ( arccos * f)) by A3, XBOOLE_1: 18;

      for x st x in Z holds (f . x) = (((1 / a) * x) + 0 )

      proof

        let x;

        assume x in Z;

        then (f . x) = (x / a) by A2;

        hence thesis by XCMPLX_1: 99;

      end;

      then

       A6: for x st x in Z holds (f . x) = (((1 / a) * x) + 0 ) & (f . x) > ( - 1) & (f . x) < 1 by A2;

      then

       A7: ( arccos * f) is_differentiable_on Z by A5, Th15;

      

       A8: for x st x in Z holds (( id Z) . x) = ((1 * x) + 0 ) by FUNCT_1: 18;

      then

       A9: ( id Z) is_differentiable_on Z by A4, FDIFF_1: 23;

      

       A10: for x st x in Z holds ((( arccos * f) `| Z) . x) = ( - (1 / (a * ( sqrt (1 - ((x / a) ^2 ))))))

      proof

        let x;

        assume x in Z;

        

        then ((( arccos * f) `| Z) . x) = ( - ((1 / a) / ( sqrt (1 - ((((1 / a) * x) + 0 ) ^2 ))))) by A6, A5, Th15

        .= ( - ((1 / a) / ( sqrt (1 - ((x / a) ^2 ))))) by XCMPLX_1: 99

        .= ( - (1 / (a * ( sqrt (1 - ((x / a) ^2 )))))) by XCMPLX_1: 78;

        hence thesis;

      end;

      for x st x in Z holds (((( id Z) (#) ( arccos * f)) `| Z) . x) = (( arccos . (x / a)) - (x / (a * ( sqrt (1 - ((x / a) ^2 ))))))

      proof

        let x;

        assume

         A11: x in Z;

        

        then

         A12: (( arccos * f) . x) = ( arccos . (f . x)) by A5, FUNCT_1: 12

        .= ( arccos . (x / a)) by A2, A11;

        (((( id Z) (#) ( arccos * f)) `| Z) . x) = (((( arccos * f) . x) * ( diff (( id Z),x))) + ((( id Z) . x) * ( diff (( arccos * f),x)))) by A1, A9, A7, A11, FDIFF_1: 21

        .= (((( arccos * f) . x) * ((( id Z) `| Z) . x)) + ((( id Z) . x) * ( diff (( arccos * f),x)))) by A9, A11, FDIFF_1:def 7

        .= (((( arccos * f) . x) * 1) + ((( id Z) . x) * ( diff (( arccos * f),x)))) by A4, A8, A11, FDIFF_1: 23

        .= (((( arccos * f) . x) * 1) + ((( id Z) . x) * ((( arccos * f) `| Z) . x))) by A7, A11, FDIFF_1:def 7

        .= ((( arccos * f) . x) + (x * ((( arccos * f) `| Z) . x))) by A11, FUNCT_1: 18

        .= (( arccos . (x / a)) + (x * ( - (1 / (a * ( sqrt (1 - ((x / a) ^2 )))))))) by A10, A11, A12

        .= (( arccos . (x / a)) - (x * (1 / (a * ( sqrt (1 - ((x / a) ^2 )))))))

        .= (( arccos . (x / a)) - (x / (a * ( sqrt (1 - ((x / a) ^2 )))))) by XCMPLX_1: 99;

        hence thesis;

      end;

      hence thesis by A1, A9, A7, FDIFF_1: 21;

    end;

    theorem :: FDIFF_7:27

    

     Th27: Z c= ( dom (( #R (1 / 2)) * f)) & f = (f1 - f2) & f2 = ( #Z 2) & (for x st x in Z holds (f1 . x) = (a ^2 ) & (f . x) > 0 ) implies (( #R (1 / 2)) * f) is_differentiable_on Z & for x st x in Z holds (((( #R (1 / 2)) * f) `| Z) . x) = ( - (x * (((a ^2 ) - (x #Z 2)) #R ( - (1 / 2)))))

    proof

      assume that

       A1: Z c= ( dom (( #R (1 / 2)) * f)) and

       A2: f = (f1 - f2) and

       A3: f2 = ( #Z 2) and

       A4: for x st x in Z holds (f1 . x) = (a ^2 ) & (f . x) > 0 ;

      for y be object st y in Z holds y in ( dom f) by A1, FUNCT_1: 11;

      then

       A5: Z c= ( dom (f1 + (( - 1) (#) f2))) by A2, TARSKI:def 3;

      

       A6: for x st x in Z holds (f1 . x) = ((a ^2 ) + ( 0 * x)) by A4;

      then

       A7: f is_differentiable_on Z by A2, A3, A5, FDIFF_4: 12;

      

       A8: for x st x in Z holds (( #R (1 / 2)) * f) is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then f is_differentiable_in x & (f . x) > 0 by A4, A7, FDIFF_1: 9;

        hence thesis by TAYLOR_1: 22;

      end;

      then

       A9: (( #R (1 / 2)) * f) is_differentiable_on Z by A1, FDIFF_1: 9;

      for x st x in Z holds (((( #R (1 / 2)) * f) `| Z) . x) = ( - (x * (((a ^2 ) - (x #Z 2)) #R ( - (1 / 2)))))

      proof

        let x;

        assume

         A10: x in Z;

        then

         A11: f is_differentiable_in x & (f . x) > 0 by A4, A7, FDIFF_1: 9;

        x in ( dom (f1 - f2)) by A1, A2, A10, FUNCT_1: 11;

        

        then

         A12: ((f1 - f2) . x) = ((f1 . x) - (f2 . x)) by VALUED_1: 13

        .= ((a ^2 ) - (f2 . x)) by A4, A10

        .= ((a ^2 ) - (x #Z 2)) by A3, TAYLOR_1:def 1;

        (((( #R (1 / 2)) * f) `| Z) . x) = ( diff ((( #R (1 / 2)) * f),x)) by A9, A10, FDIFF_1:def 7

        .= (((1 / 2) * ((f . x) #R ((1 / 2) - 1))) * ( diff (f,x))) by A11, TAYLOR_1: 22

        .= (((1 / 2) * ((f . x) #R ((1 / 2) - 1))) * ((f `| Z) . x)) by A7, A10, FDIFF_1:def 7

        .= (((1 / 2) * ((f . x) #R ((1 / 2) - 1))) * ( 0 + ((2 * ( - 1)) * x))) by A2, A3, A5, A6, A10, FDIFF_4: 12

        .= ( - (x * (((a ^2 ) - (x #Z 2)) #R ( - (1 / 2))))) by A2, A12;

        hence thesis;

      end;

      hence thesis by A1, A8, FDIFF_1: 9;

    end;

    theorem :: FDIFF_7:28

    Z c= ( dom ((( id Z) (#) ( arcsin * f3)) + (( #R (1 / 2)) * f))) & f = (f1 - f2) & f2 = ( #Z 2) & (for x st x in Z holds (f1 . x) = (a ^2 ) & (f . x) > 0 & (f3 . x) = (x / a) & (f3 . x) > ( - 1) & (f3 . x) < 1 & x <> 0 & a > 0 ) implies ((( id Z) (#) ( arcsin * f3)) + (( #R (1 / 2)) * f)) is_differentiable_on Z & for x st x in Z holds ((((( id Z) (#) ( arcsin * f3)) + (( #R (1 / 2)) * f)) `| Z) . x) = ( arcsin . (x / a))

    proof

      assume that

       A1: Z c= ( dom ((( id Z) (#) ( arcsin * f3)) + (( #R (1 / 2)) * f))) and

       A2: f = (f1 - f2) & f2 = ( #Z 2) and

       A3: for x st x in Z holds (f1 . x) = (a ^2 ) & (f . x) > 0 & (f3 . x) = (x / a) & (f3 . x) > ( - 1) & (f3 . x) < 1 & x <> 0 & a > 0 ;

      

       A4: Z c= (( dom (( id Z) (#) ( arcsin * f3))) /\ ( dom (( #R (1 / 2)) * f))) by A1, VALUED_1:def 1;

      then

       A5: Z c= ( dom (( #R (1 / 2)) * f)) by XBOOLE_1: 18;

      

       A6: for x st x in Z holds (f1 . x) = (a ^2 ) & (f . x) > 0 by A3;

      then

       A7: (( #R (1 / 2)) * f) is_differentiable_on Z by A2, A5, Th27;

      

       A8: for x st x in Z holds (f3 . x) = (x / a) & (f3 . x) > ( - 1) & (f3 . x) < 1 by A3;

      

       A9: Z c= ( dom (( id Z) (#) ( arcsin * f3))) by A4, XBOOLE_1: 18;

      then

       A10: (( id Z) (#) ( arcsin * f3)) is_differentiable_on Z by A8, Th25;

      

       A11: for x st x in Z holds (((a ^2 ) - (x #Z 2)) #R ( - (1 / 2))) = (1 / (a * ( sqrt (1 - ((x / a) ^2 )))))

      proof

        let x;

        assume

         A12: x in Z;

        then

         A13: (f3 . x) = (x / a) by A3;

        (f3 . x) < 1 by A3, A12;

        then

         A14: (1 - (f3 . x)) > (1 - 1) by XREAL_1: 10;

        (f3 . x) > ( - 1) by A3, A12;

        then (1 + (f3 . x)) > (1 + ( - 1)) by XREAL_1: 6;

        then

         A15: ((1 + (f3 . x)) * (1 - (f3 . x))) > 0 by A14, XREAL_1: 129;

        

         A16: a > 0 by A3, A12;

        then

         A17: (a ^2 ) > 0 by SQUARE_1: 12;

        (1 / (a * ( sqrt (1 - ((x / a) ^2 ))))) = (1 / (( sqrt (a ^2 )) * ( sqrt (1 - ((x / a) ^2 ))))) by A16, SQUARE_1: 22

        .= (1 / ( sqrt ((a ^2 ) * (1 - ((x / a) ^2 ))))) by A17, A13, A15, SQUARE_1: 29

        .= ((((a ^2 ) * 1) - ((a * (x / a)) ^2 )) #R ( - (1 / 2))) by A17, A13, A15, Th3, XREAL_1: 129

        .= (((a ^2 ) - (((x * a) / a) ^2 )) #R ( - (1 / 2))) by XCMPLX_1: 74

        .= (((a ^2 ) - ((x * (a / a)) ^2 )) #R ( - (1 / 2))) by XCMPLX_1: 74

        .= (((a ^2 ) - ((x * 1) ^2 )) #R ( - (1 / 2))) by A16, XCMPLX_1: 60

        .= (((a ^2 ) - (x #Z 2)) #R ( - (1 / 2))) by Th1;

        hence thesis;

      end;

      for x st x in Z holds ((((( id Z) (#) ( arcsin * f3)) + (( #R (1 / 2)) * f)) `| Z) . x) = ( arcsin . (x / a))

      proof

        let x;

        assume

         A18: x in Z;

        

        then ((((( id Z) (#) ( arcsin * f3)) + (( #R (1 / 2)) * f)) `| Z) . x) = (( diff ((( id Z) (#) ( arcsin * f3)),x)) + ( diff ((( #R (1 / 2)) * f),x))) by A1, A10, A7, FDIFF_1: 18

        .= ((((( id Z) (#) ( arcsin * f3)) `| Z) . x) + ( diff ((( #R (1 / 2)) * f),x))) by A10, A18, FDIFF_1:def 7

        .= ((((( id Z) (#) ( arcsin * f3)) `| Z) . x) + (((( #R (1 / 2)) * f) `| Z) . x)) by A7, A18, FDIFF_1:def 7

        .= ((( arcsin . (x / a)) + (x / (a * ( sqrt (1 - ((x / a) ^2 )))))) + (((( #R (1 / 2)) * f) `| Z) . x)) by A9, A8, A18, Th25

        .= ((( arcsin . (x / a)) + (x / (a * ( sqrt (1 - ((x / a) ^2 )))))) + ( - (x * (((a ^2 ) - (x #Z 2)) #R ( - (1 / 2)))))) by A2, A5, A6, A18, Th27

        .= ((( arcsin . (x / a)) + (x / (a * ( sqrt (1 - ((x / a) ^2 )))))) - (x * (((a ^2 ) - (x #Z 2)) #R ( - (1 / 2)))))

        .= ((( arcsin . (x / a)) + (x / (a * ( sqrt (1 - ((x / a) ^2 )))))) - (x * (1 / (a * ( sqrt (1 - ((x / a) ^2 ))))))) by A11, A18

        .= ((( arcsin . (x / a)) + (x / (a * ( sqrt (1 - ((x / a) ^2 )))))) - (x / (a * ( sqrt (1 - ((x / a) ^2 )))))) by XCMPLX_1: 99

        .= ( arcsin . (x / a));

        hence thesis;

      end;

      hence thesis by A1, A10, A7, FDIFF_1: 18;

    end;

    theorem :: FDIFF_7:29

    Z c= ( dom ((( id Z) (#) ( arccos * f3)) - (( #R (1 / 2)) * f))) & f = (f1 - f2) & f2 = ( #Z 2) & (for x st x in Z holds (f1 . x) = (a ^2 ) & (f . x) > 0 & (f3 . x) = (x / a) & (f3 . x) > ( - 1) & (f3 . x) < 1 & x <> 0 & a > 0 ) implies ((( id Z) (#) ( arccos * f3)) - (( #R (1 / 2)) * f)) is_differentiable_on Z & for x st x in Z holds ((((( id Z) (#) ( arccos * f3)) - (( #R (1 / 2)) * f)) `| Z) . x) = ( arccos . (x / a))

    proof

      assume that

       A1: Z c= ( dom ((( id Z) (#) ( arccos * f3)) - (( #R (1 / 2)) * f))) and

       A2: f = (f1 - f2) & f2 = ( #Z 2) and

       A3: for x st x in Z holds (f1 . x) = (a ^2 ) & (f . x) > 0 & (f3 . x) = (x / a) & (f3 . x) > ( - 1) & (f3 . x) < 1 & x <> 0 & a > 0 ;

      

       A4: Z c= (( dom (( id Z) (#) ( arccos * f3))) /\ ( dom (( #R (1 / 2)) * f))) by A1, VALUED_1: 12;

      then

       A5: Z c= ( dom (( #R (1 / 2)) * f)) by XBOOLE_1: 18;

      

       A6: for x st x in Z holds (f1 . x) = (a ^2 ) & (f . x) > 0 by A3;

      then

       A7: (( #R (1 / 2)) * f) is_differentiable_on Z by A2, A5, Th27;

      

       A8: for x st x in Z holds (f3 . x) = (x / a) & (f3 . x) > ( - 1) & (f3 . x) < 1 by A3;

      

       A9: Z c= ( dom (( id Z) (#) ( arccos * f3))) by A4, XBOOLE_1: 18;

      then

       A10: (( id Z) (#) ( arccos * f3)) is_differentiable_on Z by A8, Th26;

      

       A11: for x st x in Z holds (((a ^2 ) - (x #Z 2)) #R ( - (1 / 2))) = (1 / (a * ( sqrt (1 - ((x / a) ^2 )))))

      proof

        let x;

        assume

         A12: x in Z;

        then

         A13: (f3 . x) = (x / a) by A3;

        (f3 . x) < 1 by A3, A12;

        then

         A14: (1 - (f3 . x)) > (1 - 1) by XREAL_1: 10;

        (f3 . x) > ( - 1) by A3, A12;

        then (1 + (f3 . x)) > (1 + ( - 1)) by XREAL_1: 6;

        then

         A15: ((1 + (f3 . x)) * (1 - (f3 . x))) > 0 by A14, XREAL_1: 129;

        

         A16: a > 0 by A3, A12;

        then

         A17: (a ^2 ) > 0 by SQUARE_1: 12;

        (1 / (a * ( sqrt (1 - ((x / a) ^2 ))))) = (1 / (( sqrt (a ^2 )) * ( sqrt (1 - ((x / a) ^2 ))))) by A16, SQUARE_1: 22

        .= (1 / ( sqrt ((a ^2 ) * (1 - ((x / a) ^2 ))))) by A17, A13, A15, SQUARE_1: 29

        .= ((((a ^2 ) * 1) - ((a * (x / a)) ^2 )) #R ( - (1 / 2))) by A17, A13, A15, Th3, XREAL_1: 129

        .= (((a ^2 ) - (((x * a) / a) ^2 )) #R ( - (1 / 2))) by XCMPLX_1: 74

        .= (((a ^2 ) - ((x * (a / a)) ^2 )) #R ( - (1 / 2))) by XCMPLX_1: 74

        .= (((a ^2 ) - ((x * 1) ^2 )) #R ( - (1 / 2))) by A16, XCMPLX_1: 60

        .= (((a ^2 ) - (x #Z 2)) #R ( - (1 / 2))) by Th1;

        hence thesis;

      end;

      for x st x in Z holds ((((( id Z) (#) ( arccos * f3)) - (( #R (1 / 2)) * f)) `| Z) . x) = ( arccos . (x / a))

      proof

        let x;

        assume

         A18: x in Z;

        

        then ((((( id Z) (#) ( arccos * f3)) - (( #R (1 / 2)) * f)) `| Z) . x) = (( diff ((( id Z) (#) ( arccos * f3)),x)) - ( diff ((( #R (1 / 2)) * f),x))) by A1, A10, A7, FDIFF_1: 19

        .= ((((( id Z) (#) ( arccos * f3)) `| Z) . x) - ( diff ((( #R (1 / 2)) * f),x))) by A10, A18, FDIFF_1:def 7

        .= ((((( id Z) (#) ( arccos * f3)) `| Z) . x) - (((( #R (1 / 2)) * f) `| Z) . x)) by A7, A18, FDIFF_1:def 7

        .= ((( arccos . (x / a)) - (x / (a * ( sqrt (1 - ((x / a) ^2 )))))) - (((( #R (1 / 2)) * f) `| Z) . x)) by A9, A8, A18, Th26

        .= ((( arccos . (x / a)) - (x / (a * ( sqrt (1 - ((x / a) ^2 )))))) - ( - (x * (((a ^2 ) - (x #Z 2)) #R ( - (1 / 2)))))) by A2, A5, A6, A18, Th27

        .= ((( arccos . (x / a)) - (x / (a * ( sqrt (1 - ((x / a) ^2 )))))) + (x * (((a ^2 ) - (x #Z 2)) #R ( - (1 / 2)))))

        .= ((( arccos . (x / a)) - (x / (a * ( sqrt (1 - ((x / a) ^2 )))))) + (x * (1 / (a * ( sqrt (1 - ((x / a) ^2 ))))))) by A11, A18

        .= ((( arccos . (x / a)) - (x / (a * ( sqrt (1 - ((x / a) ^2 )))))) + (x / (a * ( sqrt (1 - ((x / a) ^2 )))))) by XCMPLX_1: 99

        .= ( arccos . (x / a));

        hence thesis;

      end;

      hence thesis by A1, A10, A7, FDIFF_1: 19;

    end;

    theorem :: FDIFF_7:30

    Z c= ( dom (( - (1 / n)) (#) (( #Z n) * ( sin ^ )))) & n > 0 & (for x st x in Z holds ( sin . x) <> 0 ) implies (( - (1 / n)) (#) (( #Z n) * ( sin ^ ))) is_differentiable_on Z & for x st x in Z holds (((( - (1 / n)) (#) (( #Z n) * ( sin ^ ))) `| Z) . x) = (( cos . x) / (( sin . x) #Z (n + 1)))

    proof

      assume that

       A1: Z c= ( dom (( - (1 / n)) (#) (( #Z n) * ( sin ^ )))) and

       A2: n > 0 and

       A3: for x st x in Z holds ( sin . x) <> 0 ;

      

       A4: Z c= ( dom (( #Z n) * ( sin ^ ))) by A1, VALUED_1:def 5;

      

       A5: ( sin ^ ) is_differentiable_on Z by A3, FDIFF_4: 40;

      now

        let x;

        assume x in Z;

        then ( sin ^ ) is_differentiable_in x by A5, FDIFF_1: 9;

        hence (( #Z n) * ( sin ^ )) is_differentiable_in x by TAYLOR_1: 3;

      end;

      then

       A6: (( #Z n) * ( sin ^ )) is_differentiable_on Z by A4, FDIFF_1: 9;

      for y be object st y in Z holds y in ( dom ( sin ^ )) by A4, FUNCT_1: 11;

      then

       A7: Z c= ( dom ( sin ^ )) by TARSKI:def 3;

      for x st x in Z holds (((( - (1 / n)) (#) (( #Z n) * ( sin ^ ))) `| Z) . x) = (( cos . x) / (( sin . x) #Z (n + 1)))

      proof

        let x;

        assume

         A8: x in Z;

        then

         A9: ( sin ^ ) is_differentiable_in x by A5, FDIFF_1: 9;

        

         A10: (( sin ^ ) . x) = (( sin . x) " ) by A7, A8, RFUNCT_1:def 2

        .= (1 / ( sin . x)) by XCMPLX_1: 215;

        (((( - (1 / n)) (#) (( #Z n) * ( sin ^ ))) `| Z) . x) = (( - (1 / n)) * ( diff ((( #Z n) * ( sin ^ )),x))) by A1, A6, A8, FDIFF_1: 20

        .= (( - (1 / n)) * ((n * ((( sin ^ ) . x) #Z (n - 1))) * ( diff (( sin ^ ),x)))) by A9, TAYLOR_1: 3

        .= (( - (1 / n)) * ((n * ((( sin ^ ) . x) #Z (n - 1))) * ((( sin ^ ) `| Z) . x))) by A5, A8, FDIFF_1:def 7

        .= (( - (1 / n)) * ((n * ((( sin ^ ) . x) #Z (n - 1))) * ( - (( cos . x) / (( sin . x) ^2 ))))) by A3, A8, FDIFF_4: 40

        .= ( - ((((1 / n) * n) * ((( sin ^ ) . x) #Z (n - 1))) * ( - (( cos . x) / (( sin . x) ^2 )))))

        .= ( - ((1 * ((( sin ^ ) . x) #Z (n - 1))) * ( - (( cos . x) / (( sin . x) ^2 ))))) by A2, XCMPLX_1: 106

        .= ( - (((1 / ( sin . x)) #Z (n - 1)) * ( - (( cos . x) / (( sin . x) #Z 2))))) by A10, Th1

        .= ( - (( - (( cos . x) / (( sin . x) #Z 2))) * (1 / (( sin . x) #Z (n - 1))))) by PREPOWER: 42

        .= ((( cos . x) / (( sin . x) #Z 2)) * (1 / (( sin . x) #Z (n - 1))))

        .= ((( cos . x) / (( sin . x) #Z 2)) / (( sin . x) #Z (n - 1))) by XCMPLX_1: 99

        .= (( cos . x) / ((( sin . x) #Z 2) * (( sin . x) #Z (n - 1)))) by XCMPLX_1: 78

        .= (( cos . x) / (( sin . x) #Z (2 + (n - 1)))) by A3, A8, PREPOWER: 44

        .= (( cos . x) / (( sin . x) #Z (n + 1)));

        hence thesis;

      end;

      hence thesis by A1, A6, FDIFF_1: 20;

    end;

    theorem :: FDIFF_7:31

    Z c= ( dom ((1 / n) (#) (( #Z n) * ( cos ^ )))) & n > 0 & (for x st x in Z holds ( cos . x) <> 0 ) implies ((1 / n) (#) (( #Z n) * ( cos ^ ))) is_differentiable_on Z & for x st x in Z holds ((((1 / n) (#) (( #Z n) * ( cos ^ ))) `| Z) . x) = (( sin . x) / (( cos . x) #Z (n + 1)))

    proof

      assume that

       A1: Z c= ( dom ((1 / n) (#) (( #Z n) * ( cos ^ )))) and

       A2: n > 0 and

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

      

       A4: Z c= ( dom (( #Z n) * ( cos ^ ))) by A1, VALUED_1:def 5;

      

       A5: ( cos ^ ) is_differentiable_on Z by A3, FDIFF_4: 39;

      now

        let x;

        assume x in Z;

        then ( cos ^ ) is_differentiable_in x by A5, FDIFF_1: 9;

        hence (( #Z n) * ( cos ^ )) is_differentiable_in x by TAYLOR_1: 3;

      end;

      then

       A6: (( #Z n) * ( cos ^ )) is_differentiable_on Z by A4, FDIFF_1: 9;

      for y be object st y in Z holds y in ( dom ( cos ^ )) by A4, FUNCT_1: 11;

      then

       A7: Z c= ( dom ( cos ^ )) by TARSKI:def 3;

      for x st x in Z holds ((((1 / n) (#) (( #Z n) * ( cos ^ ))) `| Z) . x) = (( sin . x) / (( cos . x) #Z (n + 1)))

      proof

        let x;

        assume

         A8: x in Z;

        then

         A9: ( cos ^ ) is_differentiable_in x by A5, FDIFF_1: 9;

        

         A10: (( cos ^ ) . x) = (( cos . x) " ) by A7, A8, RFUNCT_1:def 2

        .= (1 / ( cos . x)) by XCMPLX_1: 215;

        ((((1 / n) (#) (( #Z n) * ( cos ^ ))) `| Z) . x) = ((1 / n) * ( diff ((( #Z n) * ( cos ^ )),x))) by A1, A6, A8, FDIFF_1: 20

        .= ((1 / n) * ((n * ((( cos ^ ) . x) #Z (n - 1))) * ( diff (( cos ^ ),x)))) by A9, TAYLOR_1: 3

        .= ((1 / n) * ((n * ((( cos ^ ) . x) #Z (n - 1))) * ((( cos ^ ) `| Z) . x))) by A5, A8, FDIFF_1:def 7

        .= ((1 / n) * ((n * ((( cos ^ ) . x) #Z (n - 1))) * (( sin . x) / (( cos . x) ^2 )))) by A3, A8, FDIFF_4: 39

        .= ((((1 / n) * n) * ((( cos ^ ) . x) #Z (n - 1))) * (( sin . x) / (( cos . x) ^2 )))

        .= ((1 * ((( cos ^ ) . x) #Z (n - 1))) * (( sin . x) / (( cos . x) ^2 ))) by A2, XCMPLX_1: 106

        .= (((1 / ( cos . x)) #Z (n - 1)) * (( sin . x) / (( cos . x) #Z 2))) by A10, Th1

        .= ((1 / (( cos . x) #Z (n - 1))) * (( sin . x) / (( cos . x) #Z 2))) by PREPOWER: 42

        .= ((( sin . x) / (( cos . x) #Z 2)) / (( cos . x) #Z (n - 1))) by XCMPLX_1: 99

        .= (( sin . x) / ((( cos . x) #Z 2) * (( cos . x) #Z (n - 1)))) by XCMPLX_1: 78

        .= (( sin . x) / (( cos . x) #Z (2 + (n - 1)))) by A3, A8, PREPOWER: 44

        .= (( sin . x) / (( cos . x) #Z (n + 1)));

        hence thesis;

      end;

      hence thesis by A1, A6, FDIFF_1: 20;

    end;

    

     Lm3: ( right_open_halfline 0 ) = { g where g be Real : 0 < g } by XXREAL_1: 230;

    theorem :: FDIFF_7:32

    Z c= ( dom ( sin * ln )) & (for x st x in Z holds x > 0 ) implies ( sin * ln ) is_differentiable_on Z & for x st x in Z holds ((( sin * ln ) `| Z) . x) = (( cos . ( ln . x)) / x)

    proof

      assume that

       A1: Z c= ( dom ( sin * ln )) and

       A2: for x st x in Z holds x > 0 ;

      

       A3: for x st x in Z holds ( sin * ln ) is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then

         A4: ln is_differentiable_in x by A2, TAYLOR_1: 18;

         sin is_differentiable_in ( ln . x) by SIN_COS: 64;

        hence thesis by A4, FDIFF_2: 13;

      end;

      then

       A5: ( sin * ln ) is_differentiable_on Z by A1, FDIFF_1: 9;

      for x st x in Z holds ((( sin * ln ) `| Z) . x) = (( cos . ( ln . x)) / x)

      proof

        let x;

        

         A6: sin is_differentiable_in ( ln . x) by SIN_COS: 64;

        assume

         A7: x in Z;

        then x > 0 by A2;

        then

         A8: x in ( right_open_halfline 0 ) by Lm3;

         ln is_differentiable_in x by A2, A7, TAYLOR_1: 18;

        

        then ( diff (( sin * ln ),x)) = (( diff ( sin ,( ln . x))) * ( diff ( ln ,x))) by A6, FDIFF_2: 13

        .= (( cos . ( ln . x)) * ( diff ( ln ,x))) by SIN_COS: 64

        .= (( cos . ( ln . x)) * (1 / x)) by A8, TAYLOR_1: 18

        .= (( cos . ( ln . x)) / x) by XCMPLX_1: 99;

        hence thesis by A5, A7, FDIFF_1:def 7;

      end;

      hence thesis by A1, A3, FDIFF_1: 9;

    end;

    theorem :: FDIFF_7:33

    Z c= ( dom ( cos * ln )) & (for x st x in Z holds x > 0 ) implies ( cos * ln ) is_differentiable_on Z & for x st x in Z holds ((( cos * ln ) `| Z) . x) = ( - (( sin . ( ln . x)) / x))

    proof

      assume that

       A1: Z c= ( dom ( cos * ln )) and

       A2: for x st x in Z holds x > 0 ;

      

       A3: for x st x in Z holds ( cos * ln ) is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then

         A4: ln is_differentiable_in x by A2, TAYLOR_1: 18;

         cos is_differentiable_in ( ln . x) by SIN_COS: 63;

        hence thesis by A4, FDIFF_2: 13;

      end;

      then

       A5: ( cos * ln ) is_differentiable_on Z by A1, FDIFF_1: 9;

      for x st x in Z holds ((( cos * ln ) `| Z) . x) = ( - (( sin . ( ln . x)) / x))

      proof

        let x;

        

         A6: cos is_differentiable_in ( ln . x) by SIN_COS: 63;

        assume

         A7: x in Z;

        then x > 0 by A2;

        then

         A8: x in ( right_open_halfline 0 ) by Lm3;

         ln is_differentiable_in x by A2, A7, TAYLOR_1: 18;

        

        then ( diff (( cos * ln ),x)) = (( diff ( cos ,( ln . x))) * ( diff ( ln ,x))) by A6, FDIFF_2: 13

        .= (( - ( sin . ( ln . x))) * ( diff ( ln ,x))) by SIN_COS: 63

        .= (( - ( sin . ( ln . x))) * (1 / x)) by A8, TAYLOR_1: 18

        .= (( - ( sin . ( ln . x))) / x) by XCMPLX_1: 99

        .= ( - (( sin . ( ln . x)) / x)) by XCMPLX_1: 187;

        hence thesis by A5, A7, FDIFF_1:def 7;

      end;

      hence thesis by A1, A3, FDIFF_1: 9;

    end;

    theorem :: FDIFF_7:34

    Z c= ( dom ( sin * exp_R )) implies ( sin * exp_R ) is_differentiable_on Z & for x st x in Z holds ((( sin * exp_R ) `| Z) . x) = (( exp_R . x) * ( cos . ( exp_R . x)))

    proof

      

       A1: for x st x in Z holds ( sin * exp_R ) is_differentiable_in x

      proof

        let x;

        assume x in Z;

         exp_R is_differentiable_in x & sin is_differentiable_in ( exp_R . x) by SIN_COS: 64, SIN_COS: 65;

        hence thesis by FDIFF_2: 13;

      end;

      assume

       A2: Z c= ( dom ( sin * exp_R ));

      then

       A3: ( sin * exp_R ) is_differentiable_on Z by A1, FDIFF_1: 9;

      for x st x in Z holds ((( sin * exp_R ) `| Z) . x) = (( exp_R . x) * ( cos . ( exp_R . x)))

      proof

        let x;

         exp_R is_differentiable_in x & sin is_differentiable_in ( exp_R . x) by SIN_COS: 64, SIN_COS: 65;

        

        then

         A4: ( diff (( sin * exp_R ),x)) = (( diff ( sin ,( exp_R . x))) * ( diff ( exp_R ,x))) by FDIFF_2: 13

        .= (( cos . ( exp_R . x)) * ( diff ( exp_R ,x))) by SIN_COS: 64

        .= (( exp_R . x) * ( cos . ( exp_R . x))) by SIN_COS: 65;

        assume x in Z;

        hence thesis by A3, A4, FDIFF_1:def 7;

      end;

      hence thesis by A2, A1, FDIFF_1: 9;

    end;

    theorem :: FDIFF_7:35

    Z c= ( dom ( cos * exp_R )) implies ( cos * exp_R ) is_differentiable_on Z & for x st x in Z holds ((( cos * exp_R ) `| Z) . x) = ( - (( exp_R . x) * ( sin . ( exp_R . x))))

    proof

      

       A1: for x st x in Z holds ( cos * exp_R ) is_differentiable_in x

      proof

        let x;

        assume x in Z;

         exp_R is_differentiable_in x & cos is_differentiable_in ( exp_R . x) by SIN_COS: 63, SIN_COS: 65;

        hence thesis by FDIFF_2: 13;

      end;

      assume

       A2: Z c= ( dom ( cos * exp_R ));

      then

       A3: ( cos * exp_R ) is_differentiable_on Z by A1, FDIFF_1: 9;

      for x st x in Z holds ((( cos * exp_R ) `| Z) . x) = ( - (( exp_R . x) * ( sin . ( exp_R . x))))

      proof

        let x;

         exp_R is_differentiable_in x & cos is_differentiable_in ( exp_R . x) by SIN_COS: 63, SIN_COS: 65;

        

        then

         A4: ( diff (( cos * exp_R ),x)) = (( diff ( cos ,( exp_R . x))) * ( diff ( exp_R ,x))) by FDIFF_2: 13

        .= (( - ( sin . ( exp_R . x))) * ( diff ( exp_R ,x))) by SIN_COS: 63

        .= (( - ( sin . ( exp_R . x))) * ( exp_R . x)) by SIN_COS: 65

        .= ( - (( exp_R . x) * ( sin . ( exp_R . x))));

        assume x in Z;

        hence thesis by A3, A4, FDIFF_1:def 7;

      end;

      hence thesis by A2, A1, FDIFF_1: 9;

    end;

    theorem :: FDIFF_7:36

    Z c= ( dom ( exp_R * cos )) implies ( exp_R * cos ) is_differentiable_on Z & for x st x in Z holds ((( exp_R * cos ) `| Z) . x) = ( - (( exp_R . ( cos . x)) * ( sin . x)))

    proof

      

       A1: for x st x in Z holds ( exp_R * cos ) is_differentiable_in x

      proof

        let x;

        assume x in Z;

         cos is_differentiable_in x & exp_R is_differentiable_in ( cos . x) by SIN_COS: 63, SIN_COS: 65;

        hence thesis by FDIFF_2: 13;

      end;

      assume

       A2: Z c= ( dom ( exp_R * cos ));

      then

       A3: ( exp_R * cos ) is_differentiable_on Z by A1, FDIFF_1: 9;

      for x st x in Z holds ((( exp_R * cos ) `| Z) . x) = ( - (( exp_R . ( cos . x)) * ( sin . x)))

      proof

        let x;

         cos is_differentiable_in x & exp_R is_differentiable_in ( cos . x) by SIN_COS: 63, SIN_COS: 65;

        

        then

         A4: ( diff (( exp_R * cos ),x)) = (( diff ( exp_R ,( cos . x))) * ( diff ( cos ,x))) by FDIFF_2: 13

        .= (( diff ( exp_R ,( cos . x))) * ( - ( sin . x))) by SIN_COS: 63

        .= (( exp_R . ( cos . x)) * ( - ( sin . x))) by SIN_COS: 65

        .= ( - (( exp_R . ( cos . x)) * ( sin . x)));

        assume x in Z;

        hence thesis by A3, A4, FDIFF_1:def 7;

      end;

      hence thesis by A2, A1, FDIFF_1: 9;

    end;

    theorem :: FDIFF_7:37

    Z c= ( dom ( exp_R * sin )) implies ( exp_R * sin ) is_differentiable_on Z & for x st x in Z holds ((( exp_R * sin ) `| Z) . x) = (( exp_R . ( sin . x)) * ( cos . x))

    proof

      

       A1: for x st x in Z holds ( exp_R * sin ) is_differentiable_in x

      proof

        let x;

        assume x in Z;

         sin is_differentiable_in x & exp_R is_differentiable_in ( sin . x) by SIN_COS: 64, SIN_COS: 65;

        hence thesis by FDIFF_2: 13;

      end;

      assume

       A2: Z c= ( dom ( exp_R * sin ));

      then

       A3: ( exp_R * sin ) is_differentiable_on Z by A1, FDIFF_1: 9;

      for x st x in Z holds ((( exp_R * sin ) `| Z) . x) = (( exp_R . ( sin . x)) * ( cos . x))

      proof

        let x;

         sin is_differentiable_in x & exp_R is_differentiable_in ( sin . x) by SIN_COS: 64, SIN_COS: 65;

        

        then

         A4: ( diff (( exp_R * sin ),x)) = (( diff ( exp_R ,( sin . x))) * ( diff ( sin ,x))) by FDIFF_2: 13

        .= (( diff ( exp_R ,( sin . x))) * ( cos . x)) by SIN_COS: 64

        .= (( exp_R . ( sin . x)) * ( cos . x)) by SIN_COS: 65;

        assume x in Z;

        hence thesis by A3, A4, FDIFF_1:def 7;

      end;

      hence thesis by A2, A1, FDIFF_1: 9;

    end;

    theorem :: FDIFF_7:38

    

     Th38: Z c= ( dom ( sin + cos )) implies ( sin + cos ) is_differentiable_on Z & for x st x in Z holds ((( sin + cos ) `| Z) . x) = (( cos . x) - ( sin . x))

    proof

      

       A1: sin is_differentiable_on Z & cos is_differentiable_on Z by FDIFF_1: 26, SIN_COS: 67, SIN_COS: 68;

      assume

       A2: Z c= ( dom ( sin + cos ));

      now

        let x;

        assume x in Z;

        

        hence ((( sin + cos ) `| Z) . x) = (( diff ( sin ,x)) + ( diff ( cos ,x))) by A2, A1, FDIFF_1: 18

        .= (( cos . x) + ( diff ( cos ,x))) by SIN_COS: 64

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

        .= (( cos . x) - ( sin . x));

      end;

      hence thesis by A2, A1, FDIFF_1: 18;

    end;

    theorem :: FDIFF_7:39

    

     Th39: Z c= ( dom ( sin - cos )) implies ( sin - cos ) is_differentiable_on Z & for x st x in Z holds ((( sin - cos ) `| Z) . x) = (( cos . x) + ( sin . x))

    proof

      

       A1: sin is_differentiable_on Z & cos is_differentiable_on Z by FDIFF_1: 26, SIN_COS: 67, SIN_COS: 68;

      assume

       A2: Z c= ( dom ( sin - cos ));

      now

        let x;

        assume x in Z;

        

        hence ((( sin - cos ) `| Z) . x) = (( diff ( sin ,x)) - ( diff ( cos ,x))) by A2, A1, FDIFF_1: 19

        .= (( cos . x) - ( diff ( cos ,x))) by SIN_COS: 64

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

        .= (( cos . x) + ( sin . x));

      end;

      hence thesis by A2, A1, FDIFF_1: 19;

    end;

    theorem :: FDIFF_7:40

    Z c= ( dom ( exp_R (#) ( sin - cos ))) implies ( exp_R (#) ( sin - cos )) is_differentiable_on Z & for x st x in Z holds ((( exp_R (#) ( sin - cos )) `| Z) . x) = ((2 * ( exp_R . x)) * ( sin . x))

    proof

      assume

       A1: Z c= ( dom ( exp_R (#) ( sin - cos )));

      then Z c= (( dom ( sin - cos )) /\ ( dom exp_R )) by VALUED_1:def 4;

      then

       A2: Z c= ( dom ( sin - cos )) by XBOOLE_1: 18;

      then

       A3: ( sin - cos ) is_differentiable_on Z by Th39;

      

       A4: exp_R is_differentiable_on Z by FDIFF_1: 26, TAYLOR_1: 16;

      for x st x in Z holds ((( exp_R (#) ( sin - cos )) `| Z) . x) = ((2 * ( exp_R . x)) * ( sin . x))

      proof

        let x;

        assume

         A5: x in Z;

        

        then ((( exp_R (#) ( sin - cos )) `| Z) . x) = (((( sin - cos ) . x) * ( diff ( exp_R ,x))) + (( exp_R . x) * ( diff (( sin - cos ),x)))) by A1, A3, A4, FDIFF_1: 21

        .= (((( sin . x) - ( cos . x)) * ( diff ( exp_R ,x))) + (( exp_R . x) * ( diff (( sin - cos ),x)))) by A2, A5, VALUED_1: 13

        .= (((( sin . x) - ( cos . x)) * ( exp_R . x)) + (( exp_R . x) * ( diff (( sin - cos ),x)))) by TAYLOR_1: 16

        .= (((( sin . x) - ( cos . x)) * ( exp_R . x)) + (( exp_R . x) * ((( sin - cos ) `| Z) . x))) by A3, A5, FDIFF_1:def 7

        .= (((( sin . x) - ( cos . x)) * ( exp_R . x)) + (( exp_R . x) * (( cos . x) + ( sin . x)))) by A2, A5, Th39

        .= ((2 * ( exp_R . x)) * ( sin . x));

        hence thesis;

      end;

      hence thesis by A1, A3, A4, FDIFF_1: 21;

    end;

    theorem :: FDIFF_7:41

    Z c= ( dom ( exp_R (#) ( sin + cos ))) implies ( exp_R (#) ( sin + cos )) is_differentiable_on Z & for x st x in Z holds ((( exp_R (#) ( sin + cos )) `| Z) . x) = ((2 * ( exp_R . x)) * ( cos . x))

    proof

      assume

       A1: Z c= ( dom ( exp_R (#) ( sin + cos )));

      then Z c= (( dom ( sin + cos )) /\ ( dom exp_R )) by VALUED_1:def 4;

      then

       A2: Z c= ( dom ( sin + cos )) by XBOOLE_1: 18;

      then

       A3: ( sin + cos ) is_differentiable_on Z by Th38;

      

       A4: exp_R is_differentiable_on Z by FDIFF_1: 26, TAYLOR_1: 16;

      for x st x in Z holds ((( exp_R (#) ( sin + cos )) `| Z) . x) = ((2 * ( exp_R . x)) * ( cos . x))

      proof

        let x;

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

        assume

         A5: x in Z;

        

        then ((( exp_R (#) ( sin + cos )) `| Z) . x) = (((( sin + cos ) . xx) * ( diff ( exp_R ,x))) + (( exp_R . x) * ( diff (( sin + cos ),x)))) by A1, A3, A4, FDIFF_1: 21

        .= (((( sin . xx) + ( cos . xx)) * ( diff ( exp_R ,x))) + (( exp_R . x) * ( diff (( sin + cos ),x)))) by VALUED_1: 1

        .= (((( sin . x) + ( cos . x)) * ( exp_R . x)) + (( exp_R . x) * ( diff (( sin + cos ),x)))) by TAYLOR_1: 16

        .= (((( sin . x) + ( cos . x)) * ( exp_R . x)) + (( exp_R . x) * ((( sin + cos ) `| Z) . x))) by A3, A5, FDIFF_1:def 7

        .= (((( sin . x) + ( cos . x)) * ( exp_R . x)) + (( exp_R . x) * (( cos . x) - ( sin . x)))) by A2, A5, Th38

        .= ((2 * ( exp_R . x)) * ( cos . x));

        hence thesis;

      end;

      hence thesis by A1, A3, A4, FDIFF_1: 21;

    end;

    theorem :: FDIFF_7:42

    Z c= ( dom (( sin + cos ) / exp_R )) implies (( sin + cos ) / exp_R ) is_differentiable_on Z & for x st x in Z holds (((( sin + cos ) / exp_R ) `| Z) . x) = ( - ((2 * ( sin . x)) / ( exp_R . x)))

    proof

      assume Z c= ( dom (( sin + cos ) / exp_R ));

      then Z c= (( dom ( sin + cos )) /\ (( dom exp_R ) \ ( exp_R " { 0 }))) by RFUNCT_1:def 1;

      then

       A1: Z c= ( dom ( sin + cos )) by XBOOLE_1: 18;

      then

       A2: ( sin + cos ) is_differentiable_on Z by Th38;

      

       A3: exp_R is_differentiable_on Z & for x st x in Z holds ( exp_R . x) <> 0 by FDIFF_1: 26, SIN_COS: 54, TAYLOR_1: 16;

      then

       A4: (( sin + cos ) / exp_R ) is_differentiable_on Z by A2, FDIFF_2: 21;

      for x st x in Z holds (((( sin + cos ) / exp_R ) `| Z) . x) = ( - ((2 * ( sin . x)) / ( exp_R . x)))

      proof

        let x;

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

        

         A5: (( sin + cos ) . xx) = (( sin . xx) + ( cos . xx)) by VALUED_1: 1;

        

         A6: ( exp_R . x) <> 0 by SIN_COS: 54;

        assume

         A7: x in Z;

        then exp_R is_differentiable_in x & ( sin + cos ) is_differentiable_in x by A2, FDIFF_1: 9, SIN_COS: 65;

        

        then ( diff ((( sin + cos ) / exp_R ),x)) = (((( diff (( sin + cos ),x)) * ( exp_R . x)) - (( diff ( exp_R ,x)) * (( sin + cos ) . x))) / (( exp_R . x) ^2 )) by A6, FDIFF_2: 14

        .= (((((( sin + cos ) `| Z) . x) * ( exp_R . x)) - (( diff ( exp_R ,x)) * (( sin + cos ) . x))) / (( exp_R . x) ^2 )) by A2, A7, FDIFF_1:def 7

        .= ((((( cos . x) - ( sin . x)) * ( exp_R . x)) - (( diff ( exp_R ,x)) * (( sin + cos ) . x))) / (( exp_R . x) ^2 )) by A1, A7, Th38

        .= ((((( cos . x) - ( sin . x)) * ( exp_R . x)) - (( exp_R . x) * (( sin . x) + ( cos . x)))) / (( exp_R . x) ^2 )) by A5, SIN_COS: 65

        .= ((( - (2 * ( sin . x))) * ( exp_R . x)) / (( exp_R . x) * ( exp_R . x)))

        .= (( - (2 * ( sin . x))) * (( exp_R . x) / (( exp_R . x) * ( exp_R . x)))) by XCMPLX_1: 74

        .= (( - (2 * ( sin . x))) * ((( exp_R . x) / ( exp_R . x)) / ( exp_R . x))) by XCMPLX_1: 78

        .= (( - (2 * ( sin . x))) * (1 / ( exp_R . x))) by A6, XCMPLX_1: 60

        .= (( - (2 * ( sin . x))) / ( exp_R . x)) by XCMPLX_1: 99

        .= ( - ((2 * ( sin . x)) / ( exp_R . x))) by XCMPLX_1: 187;

        hence thesis by A4, A7, FDIFF_1:def 7;

      end;

      hence thesis by A2, A3, FDIFF_2: 21;

    end;

    theorem :: FDIFF_7:43

    Z c= ( dom (( sin - cos ) / exp_R )) implies (( sin - cos ) / exp_R ) is_differentiable_on Z & for x st x in Z holds (((( sin - cos ) / exp_R ) `| Z) . x) = ((2 * ( cos . x)) / ( exp_R . x))

    proof

      assume Z c= ( dom (( sin - cos ) / exp_R ));

      then Z c= (( dom ( sin - cos )) /\ (( dom exp_R ) \ ( exp_R " { 0 }))) by RFUNCT_1:def 1;

      then

       A1: Z c= ( dom ( sin - cos )) by XBOOLE_1: 18;

      then

       A2: ( sin - cos ) is_differentiable_on Z by Th39;

      

       A3: exp_R is_differentiable_on Z & for x st x in Z holds ( exp_R . x) <> 0 by FDIFF_1: 26, SIN_COS: 54, TAYLOR_1: 16;

      then

       A4: (( sin - cos ) / exp_R ) is_differentiable_on Z by A2, FDIFF_2: 21;

      for x st x in Z holds (((( sin - cos ) / exp_R ) `| Z) . x) = ((2 * ( cos . x)) / ( exp_R . x))

      proof

        let x;

        

         A5: ( exp_R . x) <> 0 by SIN_COS: 54;

        assume

         A6: x in Z;

        then

         A7: (( sin - cos ) . x) = (( sin . x) - ( cos . x)) by A1, VALUED_1: 13;

         exp_R is_differentiable_in x & ( sin - cos ) is_differentiable_in x by A2, A6, FDIFF_1: 9, SIN_COS: 65;

        

        then ( diff ((( sin - cos ) / exp_R ),x)) = (((( diff (( sin - cos ),x)) * ( exp_R . x)) - (( diff ( exp_R ,x)) * (( sin - cos ) . x))) / (( exp_R . x) ^2 )) by A5, FDIFF_2: 14

        .= (((((( sin - cos ) `| Z) . x) * ( exp_R . x)) - (( diff ( exp_R ,x)) * (( sin - cos ) . x))) / (( exp_R . x) ^2 )) by A2, A6, FDIFF_1:def 7

        .= ((((( cos . x) + ( sin . x)) * ( exp_R . x)) - (( diff ( exp_R ,x)) * (( sin - cos ) . x))) / (( exp_R . x) ^2 )) by A1, A6, Th39

        .= ((((( cos . x) + ( sin . x)) * ( exp_R . x)) - (( exp_R . x) * (( sin . x) - ( cos . x)))) / (( exp_R . x) ^2 )) by A7, SIN_COS: 65

        .= (((2 * ( cos . x)) * ( exp_R . x)) / (( exp_R . x) * ( exp_R . x)))

        .= ((2 * ( cos . x)) * (( exp_R . x) / (( exp_R . x) * ( exp_R . x)))) by XCMPLX_1: 74

        .= ((2 * ( cos . x)) * ((( exp_R . x) / ( exp_R . x)) / ( exp_R . x))) by XCMPLX_1: 78

        .= ((2 * ( cos . x)) * (1 / ( exp_R . x))) by A5, XCMPLX_1: 60

        .= ((2 * ( cos . x)) / ( exp_R . x)) by XCMPLX_1: 99;

        hence thesis by A4, A6, FDIFF_1:def 7;

      end;

      hence thesis by A2, A3, FDIFF_2: 21;

    end;

    theorem :: FDIFF_7:44

    Z c= ( dom ( exp_R (#) sin )) implies ( exp_R (#) sin ) is_differentiable_on Z & for x st x in Z holds ((( exp_R (#) sin ) `| Z) . x) = (( exp_R . x) * (( sin . x) + ( cos . x)))

    proof

      

       A1: sin is_differentiable_on Z & exp_R is_differentiable_on Z by FDIFF_1: 26, SIN_COS: 68, TAYLOR_1: 16;

      assume

       A2: Z c= ( dom ( exp_R (#) sin ));

      now

        let x;

        assume x in Z;

        

        hence ((( exp_R (#) sin ) `| Z) . x) = ((( sin . x) * ( diff ( exp_R ,x))) + (( exp_R . x) * ( diff ( sin ,x)))) by A2, A1, FDIFF_1: 21

        .= ((( sin . x) * ( exp_R . x)) + (( exp_R . x) * ( diff ( sin ,x)))) by TAYLOR_1: 16

        .= ((( sin . x) * ( exp_R . x)) + (( exp_R . x) * ( cos . x))) by SIN_COS: 64

        .= (( exp_R . x) * (( sin . x) + ( cos . x)));

      end;

      hence thesis by A2, A1, FDIFF_1: 21;

    end;

    theorem :: FDIFF_7:45

    Z c= ( dom ( exp_R (#) cos )) implies ( exp_R (#) cos ) is_differentiable_on Z & for x st x in Z holds ((( exp_R (#) cos ) `| Z) . x) = (( exp_R . x) * (( cos . x) - ( sin . x)))

    proof

      

       A1: cos is_differentiable_on Z & exp_R is_differentiable_on Z by FDIFF_1: 26, SIN_COS: 67, TAYLOR_1: 16;

      assume

       A2: Z c= ( dom ( exp_R (#) cos ));

      now

        let x;

        assume x in Z;

        

        hence ((( exp_R (#) cos ) `| Z) . x) = ((( cos . x) * ( diff ( exp_R ,x))) + (( exp_R . x) * ( diff ( cos ,x)))) by A2, A1, FDIFF_1: 21

        .= ((( cos . x) * ( exp_R . x)) + (( exp_R . x) * ( diff ( cos ,x)))) by TAYLOR_1: 16

        .= ((( cos . x) * ( exp_R . x)) + (( exp_R . x) * ( - ( sin . x)))) by SIN_COS: 63

        .= (( exp_R . x) * (( cos . x) - ( sin . x)));

      end;

      hence thesis by A2, A1, FDIFF_1: 21;

    end;

    theorem :: FDIFF_7:46

    

     Th46: ( cos . x) <> 0 implies ( sin / cos ) is_differentiable_in x & ( diff (( sin / cos ),x)) = (1 / (( cos . x) ^2 ))

    proof

      assume

       A1: ( cos . x) <> 0 ;

      

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

      

      then ( diff (( sin / cos ),x)) = (((( diff ( sin ,x)) * ( cos . x)) - (( diff ( cos ,x)) * ( sin . x))) / (( cos . x) ^2 )) by A1, FDIFF_2: 14

      .= (((( cos . x) * ( cos . x)) - (( diff ( cos ,x)) * ( sin . x))) / (( cos . x) ^2 )) by SIN_COS: 64

      .= (((( cos . x) * ( cos . x)) - (( - ( sin . x)) * ( sin . x))) / (( cos . x) ^2 )) by SIN_COS: 63

      .= (((( cos . x) * ( cos . x)) + (( sin . x) * ( sin . x))) / (( cos . x) ^2 ))

      .= (1 / (( cos . x) ^2 )) by SIN_COS: 28;

      hence thesis by A2, A1, FDIFF_2: 14;

    end;

    theorem :: FDIFF_7:47

    

     Th47: ( sin . x) <> 0 implies ( cos / sin ) is_differentiable_in x & ( diff (( cos / sin ),x)) = ( - (1 / (( sin . x) ^2 )))

    proof

      assume

       A1: ( sin . x) <> 0 ;

      

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

      

      then ( diff (( cos / sin ),x)) = (((( diff ( cos ,x)) * ( sin . x)) - (( diff ( sin ,x)) * ( cos . x))) / (( sin . x) ^2 )) by A1, FDIFF_2: 14

      .= (((( - ( sin . x)) * ( sin . x)) - (( diff ( sin ,x)) * ( cos . x))) / (( sin . x) ^2 )) by SIN_COS: 63

      .= ((( - (( sin . x) * ( sin . x))) - (( cos . x) * ( cos . x))) / (( sin . x) ^2 )) by SIN_COS: 64

      .= (( - ((( cos . x) ^2 ) + (( sin . x) * ( sin . x)))) / (( sin . x) ^2 ))

      .= ( - (((( cos . x) ^2 ) + (( sin . x) ^2 )) / (( sin . x) ^2 ))) by XCMPLX_1: 187

      .= ( - (1 / (( sin . x) ^2 ))) by SIN_COS: 28;

      hence thesis by A2, A1, FDIFF_2: 14;

    end;

    theorem :: FDIFF_7:48

    Z c= ( dom (( #Z 2) * ( sin / cos ))) & (for x st x in Z holds ( cos . x) <> 0 ) implies (( #Z 2) * ( sin / cos )) is_differentiable_on Z & for x st x in Z holds (((( #Z 2) * ( sin / cos )) `| Z) . x) = ((2 * ( sin . x)) / (( cos . x) #Z 3))

    proof

      assume that

       A1: Z c= ( dom (( #Z 2) * ( sin / cos ))) and

       A2: for x st x in Z holds ( cos . x) <> 0 ;

      for y be object st y in Z holds y in ( dom ( sin / cos )) by A1, FUNCT_1: 11;

      then

       A3: Z c= ( dom ( sin / cos )) by TARSKI:def 3;

      

       A4: for x st x in Z holds (( #Z 2) * ( sin / cos )) is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then ( cos . x) <> 0 by A2;

        then ( sin / cos ) is_differentiable_in x by Th46;

        hence thesis by TAYLOR_1: 3;

      end;

      then

       A5: (( #Z 2) * ( sin / cos )) is_differentiable_on Z by A1, FDIFF_1: 9;

      for x st x in Z holds (((( #Z 2) * ( sin / cos )) `| Z) . x) = ((2 * ( sin . x)) / (( cos . x) #Z 3))

      proof

        let x;

        assume

         A6: x in Z;

        

        then

         A7: (( sin / cos ) . x) = (( sin . x) * (( cos . x) " )) by A3, RFUNCT_1:def 1

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

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

        

         A8: ( cos . x) <> 0 by A2, A6;

        then

         A9: ( sin / cos ) is_differentiable_in x by Th46;

        (((( #Z 2) * ( sin / cos )) `| Z) . x) = ( diff ((( #Z 2) * ( sin / cos )),x)) by A5, A6, FDIFF_1:def 7

        .= ((2 * ((( sin / cos ) . x) #Z (2 - 1))) * ( diff (( sin / cos ),x))) by A9, TAYLOR_1: 3

        .= ((2 * ((( sin / cos ) . x) #Z (2 - 1))) * (1 / (( cos . x) ^2 ))) by A8, Th46

        .= ((2 * ((( sin / cos ) . x) #Z 1)) / (( cos . x) ^2 )) by XCMPLX_1: 99

        .= ((2 * (( sin . x) / ( cos . x))) / (( cos . x) ^2 )) by A7, PREPOWER: 35

        .= (((2 * ( sin . x)) / ( cos . x)) / (( cos . x) ^2 )) by XCMPLX_1: 74

        .= ((2 * ( sin . x)) / (( cos . x) * (( cos . x) ^2 ))) by XCMPLX_1: 78

        .= ((2 * ( sin . x)) / (( cos . x) * (( cos . x) #Z 2))) by Th1

        .= ((2 * ( sin . x)) / ((( cos . x) #Z 1) * (( cos . x) #Z 2))) by PREPOWER: 35

        .= ((2 * ( sin . x)) / (( cos . x) #Z (1 + 2))) by A2, A6, PREPOWER: 44

        .= ((2 * ( sin . x)) / (( cos . x) #Z 3));

        hence thesis;

      end;

      hence thesis by A1, A4, FDIFF_1: 9;

    end;

    theorem :: FDIFF_7:49

    Z c= ( dom (( #Z 2) * ( cos / sin ))) & (for x st x in Z holds ( sin . x) <> 0 ) implies (( #Z 2) * ( cos / sin )) is_differentiable_on Z & for x st x in Z holds (((( #Z 2) * ( cos / sin )) `| Z) . x) = ( - ((2 * ( cos . x)) / (( sin . x) #Z 3)))

    proof

      assume that

       A1: Z c= ( dom (( #Z 2) * ( cos / sin ))) and

       A2: for x st x in Z holds ( sin . x) <> 0 ;

      for y be object st y in Z holds y in ( dom ( cos / sin )) by A1, FUNCT_1: 11;

      then

       A3: Z c= ( dom ( cos / sin )) by TARSKI:def 3;

      

       A4: for x st x in Z holds (( #Z 2) * ( cos / sin )) is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then ( sin . x) <> 0 by A2;

        then ( cos / sin ) is_differentiable_in x by Th47;

        hence thesis by TAYLOR_1: 3;

      end;

      then

       A5: (( #Z 2) * ( cos / sin )) is_differentiable_on Z by A1, FDIFF_1: 9;

      for x st x in Z holds (((( #Z 2) * ( cos / sin )) `| Z) . x) = ( - ((2 * ( cos . x)) / (( sin . x) #Z 3)))

      proof

        let x;

        assume

         A6: x in Z;

        

        then

         A7: (( cos / sin ) . x) = (( cos . x) * (( sin . x) " )) by A3, RFUNCT_1:def 1

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

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

        

         A8: ( sin . x) <> 0 by A2, A6;

        then

         A9: ( cos / sin ) is_differentiable_in x by Th47;

        (((( #Z 2) * ( cos / sin )) `| Z) . x) = ( diff ((( #Z 2) * ( cos / sin )),x)) by A5, A6, FDIFF_1:def 7

        .= ((2 * ((( cos / sin ) . x) #Z (2 - 1))) * ( diff (( cos / sin ),x))) by A9, TAYLOR_1: 3

        .= ((2 * ((( cos / sin ) . x) #Z (2 - 1))) * ( - (1 / (( sin . x) ^2 )))) by A8, Th47

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

        .= ( - ((2 * ((( cos / sin ) . x) #Z 1)) / (( sin . x) ^2 ))) by XCMPLX_1: 99

        .= ( - ((2 * (( cos . x) / ( sin . x))) / (( sin . x) ^2 ))) by A7, PREPOWER: 35

        .= ( - (((2 * ( cos . x)) / ( sin . x)) / (( sin . x) ^2 ))) by XCMPLX_1: 74

        .= ( - ((2 * ( cos . x)) / (( sin . x) * (( sin . x) ^2 )))) by XCMPLX_1: 78

        .= ( - ((2 * ( cos . x)) / (( sin . x) * (( sin . x) #Z 2)))) by Th1

        .= ( - ((2 * ( cos . x)) / ((( sin . x) #Z 1) * (( sin . x) #Z 2)))) by PREPOWER: 35

        .= ( - ((2 * ( cos . x)) / (( sin . x) #Z (1 + 2)))) by A2, A6, PREPOWER: 44

        .= ( - ((2 * ( cos . x)) / (( sin . x) #Z 3)));

        hence thesis;

      end;

      hence thesis by A1, A4, FDIFF_1: 9;

    end;

    theorem :: FDIFF_7:50

    Z c= ( dom (( sin / cos ) * f)) & (for x st x in Z holds (f . x) = (x / 2) & ( cos . (f . x)) <> 0 ) implies (( sin / cos ) * f) is_differentiable_on Z & for x st x in Z holds (((( sin / cos ) * f) `| Z) . x) = (1 / (1 + ( cos . x)))

    proof

      assume that

       A1: Z c= ( dom (( sin / cos ) * f)) and

       A2: for x st x in Z holds (f . x) = (x / 2) & ( cos . (f . x)) <> 0 ;

      

       A3: for x st x in Z holds (f . x) = (((1 / 2) * x) + 0 )

      proof

        let x;

        assume x in Z;

        then (f . x) = (x / 2) by A2;

        hence thesis;

      end;

      for y be object st y in Z holds y in ( dom f) by A1, FUNCT_1: 11;

      then

       A4: Z c= ( dom f) by TARSKI:def 3;

      then

       A5: f is_differentiable_on Z by A3, FDIFF_1: 23;

      

       A6: for x st x in Z holds (( sin / cos ) * f) is_differentiable_in x

      proof

        let x;

        assume

         A7: x in Z;

        then ( cos . (f . x)) <> 0 by A2;

        then

         A8: ( sin / cos ) is_differentiable_in (f . x) by Th46;

        f is_differentiable_in x by A5, A7, FDIFF_1: 9;

        hence thesis by A8, FDIFF_2: 13;

      end;

      then

       A9: (( sin / cos ) * f) is_differentiable_on Z by A1, FDIFF_1: 9;

      for x st x in Z holds (((( sin / cos ) * f) `| Z) . x) = (1 / (1 + ( cos . x)))

      proof

        let x;

        assume

         A10: x in Z;

        then

         A11: f is_differentiable_in x by A5, FDIFF_1: 9;

        

         A12: ( cos . (f . x)) <> 0 by A2, A10;

        then ( sin / cos ) is_differentiable_in (f . x) by Th46;

        

        then ( diff ((( sin / cos ) * f),x)) = (( diff (( sin / cos ),(f . x))) * ( diff (f,x))) by A11, FDIFF_2: 13

        .= ((1 / (( cos . (f . x)) ^2 )) * ( diff (f,x))) by A12, Th46

        .= (( diff (f,x)) / (( cos . (f . x)) ^2 )) by XCMPLX_1: 99

        .= (( diff (f,x)) / (( cos . (x / 2)) ^2 )) by A2, A10

        .= (((f `| Z) . x) / (( cos . (x / 2)) ^2 )) by A5, A10, FDIFF_1:def 7

        .= ((1 / 2) / (( cos . (x / 2)) ^2 )) by A3, A4, A10, FDIFF_1: 23

        .= (1 / (2 * (( cos . (x / 2)) ^2 ))) by XCMPLX_1: 78

        .= (1 / (1 + ( cos . x))) by Lm1;

        hence thesis by A9, A10, FDIFF_1:def 7;

      end;

      hence thesis by A1, A6, FDIFF_1: 9;

    end;

    theorem :: FDIFF_7:51

    Z c= ( dom (( cos / sin ) * f)) & (for x st x in Z holds (f . x) = (x / 2) & ( sin . (f . x)) <> 0 ) implies (( cos / sin ) * f) is_differentiable_on Z & for x st x in Z holds (((( cos / sin ) * f) `| Z) . x) = ( - (1 / (1 - ( cos . x))))

    proof

      assume that

       A1: Z c= ( dom (( cos / sin ) * f)) and

       A2: for x st x in Z holds (f . x) = (x / 2) & ( sin . (f . x)) <> 0 ;

      

       A3: for x st x in Z holds (f . x) = (((1 / 2) * x) + 0 )

      proof

        let x;

        assume x in Z;

        then (f . x) = (x / 2) by A2;

        hence thesis;

      end;

      for y be object st y in Z holds y in ( dom f) by A1, FUNCT_1: 11;

      then

       A4: Z c= ( dom f) by TARSKI:def 3;

      then

       A5: f is_differentiable_on Z by A3, FDIFF_1: 23;

      

       A6: for x st x in Z holds (( cos / sin ) * f) is_differentiable_in x

      proof

        let x;

        assume

         A7: x in Z;

        then ( sin . (f . x)) <> 0 by A2;

        then

         A8: ( cos / sin ) is_differentiable_in (f . x) by Th47;

        f is_differentiable_in x by A5, A7, FDIFF_1: 9;

        hence thesis by A8, FDIFF_2: 13;

      end;

      then

       A9: (( cos / sin ) * f) is_differentiable_on Z by A1, FDIFF_1: 9;

      for x st x in Z holds (((( cos / sin ) * f) `| Z) . x) = ( - (1 / (1 - ( cos . x))))

      proof

        let x;

        assume

         A10: x in Z;

        then

         A11: f is_differentiable_in x by A5, FDIFF_1: 9;

        

         A12: ( sin . (f . x)) <> 0 by A2, A10;

        then ( cos / sin ) is_differentiable_in (f . x) by Th47;

        

        then ( diff ((( cos / sin ) * f),x)) = (( diff (( cos / sin ),(f . x))) * ( diff (f,x))) by A11, FDIFF_2: 13

        .= (( - (1 / (( sin . (f . x)) ^2 ))) * ( diff (f,x))) by A12, Th47

        .= ( - ((1 / (( sin . (f . x)) ^2 )) * ( diff (f,x))))

        .= ( - (( diff (f,x)) / (( sin . (f . x)) ^2 ))) by XCMPLX_1: 99

        .= ( - (( diff (f,x)) / (( sin . (x / 2)) ^2 ))) by A2, A10

        .= ( - (((f `| Z) . x) / (( sin . (x / 2)) ^2 ))) by A5, A10, FDIFF_1:def 7

        .= ( - ((1 / 2) / (( sin . (x / 2)) ^2 ))) by A3, A4, A10, FDIFF_1: 23

        .= ( - (1 / (2 * (( sin . (x / 2)) ^2 )))) by XCMPLX_1: 78

        .= ( - (1 / (1 - ( cos . x)))) by Lm2;

        hence thesis by A9, A10, FDIFF_1:def 7;

      end;

      hence thesis by A1, A6, FDIFF_1: 9;

    end;