fdiff_11.miz



    begin

    reserve x for Real,

n for Element of NAT ,

y for set,

Z for open Subset of REAL ,

g for PartFunc of REAL , REAL ;

    theorem :: FDIFF_11:1

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

    proof

      assume that

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

       A2: for x st x in Z holds ( sin . x) > ( - 1) & ( sin . x) < 1;

      

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

      proof

        let x;

        assume x in Z;

        then

         A4: ( sin . x) > ( - 1) & ( sin . x) < 1 by A2;

         sin is_differentiable_in x by SIN_COS: 64;

        hence thesis by A4, SIN_COS9: 85;

      end;

      then

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

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

      proof

        let x;

        

         A6: sin is_differentiable_in x by SIN_COS: 64;

        assume

         A7: x in Z;

        then

         A8: ( sin . x) > ( - 1) & ( sin . x) < 1 by A2;

        ((( arctan * sin ) `| Z) . x) = ( diff (( arctan * sin ),x)) by A5, A7, FDIFF_1:def 7

        .= (( diff ( sin ,x)) / (1 + (( sin . x) ^2 ))) by A6, A8, SIN_COS9: 85

        .= (( cos . x) / (1 + (( sin . x) ^2 ))) by SIN_COS: 64;

        hence thesis;

      end;

      hence thesis by A1, A3, FDIFF_1: 9;

    end;

    theorem :: FDIFF_11:2

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

    proof

      assume that

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

       A2: for x st x in Z holds ( sin . x) > ( - 1) & ( sin . x) < 1;

      

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

      proof

        let x;

        assume x in Z;

        then

         A4: ( sin . x) > ( - 1) & ( sin . x) < 1 by A2;

         sin is_differentiable_in x by SIN_COS: 64;

        hence thesis by A4, SIN_COS9: 86;

      end;

      then

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

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

      proof

        let x;

        

         A6: sin is_differentiable_in x by SIN_COS: 64;

        assume

         A7: x in Z;

        then

         A8: ( sin . x) > ( - 1) & ( sin . x) < 1 by A2;

        ((( arccot * sin ) `| Z) . x) = ( diff (( arccot * sin ),x)) by A5, A7, FDIFF_1:def 7

        .= ( - (( diff ( sin ,x)) / (1 + (( sin . x) ^2 )))) by A6, A8, SIN_COS9: 86

        .= ( - (( cos . x) / (1 + (( sin . x) ^2 )))) by SIN_COS: 64;

        hence thesis;

      end;

      hence thesis by A1, A3, FDIFF_1: 9;

    end;

    theorem :: FDIFF_11:3

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

    proof

      assume that

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

       A2: for x st x in Z holds ( cos . x) > ( - 1) & ( cos . x) < 1;

      

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

      proof

        let x;

        assume x in Z;

        then

         A4: ( cos . x) > ( - 1) & ( cos . x) < 1 by A2;

         cos is_differentiable_in x by SIN_COS: 63;

        hence thesis by A4, SIN_COS9: 85;

      end;

      then

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

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

      proof

        let x;

        

         A6: cos is_differentiable_in x by SIN_COS: 63;

        assume

         A7: x in Z;

        then

         A8: ( cos . x) > ( - 1) & ( cos . x) < 1 by A2;

        ((( arctan * cos ) `| Z) . x) = ( diff (( arctan * cos ),x)) by A5, A7, FDIFF_1:def 7

        .= (( diff ( cos ,x)) / (1 + (( cos . x) ^2 ))) by A6, A8, SIN_COS9: 85

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

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

        hence thesis;

      end;

      hence thesis by A1, A3, FDIFF_1: 9;

    end;

    theorem :: FDIFF_11:4

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

    proof

      assume that

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

       A2: for x st x in Z holds ( cos . x) > ( - 1) & ( cos . x) < 1;

      

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

      proof

        let x;

        assume x in Z;

        then

         A4: ( cos . x) > ( - 1) & ( cos . x) < 1 by A2;

         cos is_differentiable_in x by SIN_COS: 63;

        hence thesis by A4, SIN_COS9: 86;

      end;

      then

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

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

      proof

        let x;

        

         A6: cos is_differentiable_in x by SIN_COS: 63;

        assume

         A7: x in Z;

        then

         A8: ( cos . x) > ( - 1) & ( cos . x) < 1 by A2;

        ((( arccot * cos ) `| Z) . x) = ( diff (( arccot * cos ),x)) by A5, A7, FDIFF_1:def 7

        .= ( - (( diff ( cos ,x)) / (1 + (( cos . x) ^2 )))) by A6, A8, SIN_COS9: 86

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

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

        hence thesis;

      end;

      hence thesis by A1, A3, FDIFF_1: 9;

    end;

    theorem :: FDIFF_11:5

    Z c= ( dom ( arctan * tan )) & (for x st x in Z holds ( tan . x) > ( - 1) & ( tan . x) < 1) implies ( arctan * tan ) is_differentiable_on Z & for x st x in Z holds ((( arctan * tan ) `| Z) . x) = 1

    proof

      assume that

       A1: Z c= ( dom ( arctan * tan )) and

       A2: for x st x in Z holds ( tan . x) > ( - 1) & ( tan . x) < 1;

      ( dom ( arctan * tan )) c= ( dom tan ) by RELAT_1: 25;

      then

       A3: Z c= ( dom tan ) by A1, XBOOLE_1: 1;

      

       A4: for x st x in Z holds ( arctan * tan ) is_differentiable_in x

      proof

        let x;

        assume

         A5: x in Z;

        then ( cos . x) <> 0 by A3, FDIFF_8: 1;

        then

         A6: tan is_differentiable_in x by FDIFF_7: 46;

        ( tan . x) > ( - 1) & ( tan . x) < 1 by A2, A5;

        hence thesis by A6, SIN_COS9: 85;

      end;

      then

       A7: ( arctan * tan ) is_differentiable_on Z by A1, FDIFF_1: 9;

      for x st x in Z holds ((( arctan * tan ) `| Z) . x) = 1

      proof

        let x;

        assume

         A8: x in Z;

        then

         A9: ( tan . x) > ( - 1) & ( tan . x) < 1 by A2;

        

         A10: ( tan . x) = (( sin . x) / ( cos . x)) by A3, A8, RFUNCT_1:def 1;

        

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

        then

         A12: tan is_differentiable_in x by FDIFF_7: 46;

        

         A13: (( cos . x) ^2 ) <> 0 by A11, SQUARE_1: 12;

        ((( arctan * tan ) `| Z) . x) = ( diff (( arctan * tan ),x)) by A7, A8, FDIFF_1:def 7

        .= (( diff ( tan ,x)) / (1 + (( tan . x) ^2 ))) by A12, A9, SIN_COS9: 85

        .= ((1 / (( cos . x) ^2 )) / (1 + (( tan . x) ^2 ))) by A11, FDIFF_7: 46

        .= (1 / ((( cos . x) ^2 ) * (1 + ((( sin . x) / ( cos . x)) * (( sin . x) / ( cos . x)))))) by A10, XCMPLX_1: 78

        .= (1 / ((( cos . x) ^2 ) * (1 + ((( sin . x) ^2 ) / (( cos . x) ^2 ))))) by XCMPLX_1: 76

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

        .= (1 / ((( cos . x) ^2 ) + (( sin . x) ^2 ))) by A13, XCMPLX_1: 89

        .= (1 / 1) by SIN_COS: 28

        .= 1;

        hence thesis;

      end;

      hence thesis by A1, A4, FDIFF_1: 9;

    end;

    theorem :: FDIFF_11:6

    Z c= ( dom ( arccot * tan )) & (for x st x in Z holds ( tan . x) > ( - 1) & ( tan . x) < 1) implies ( arccot * tan ) is_differentiable_on Z & for x st x in Z holds ((( arccot * tan ) `| Z) . x) = ( - 1)

    proof

      assume that

       A1: Z c= ( dom ( arccot * tan )) and

       A2: for x st x in Z holds ( tan . x) > ( - 1) & ( tan . x) < 1;

      ( dom ( arccot * tan )) c= ( dom tan ) by RELAT_1: 25;

      then

       A3: Z c= ( dom tan ) by A1, XBOOLE_1: 1;

      

       A4: for x st x in Z holds ( arccot * tan ) is_differentiable_in x

      proof

        let x;

        assume

         A5: x in Z;

        then ( cos . x) <> 0 by A3, FDIFF_8: 1;

        then

         A6: tan is_differentiable_in x by FDIFF_7: 46;

        ( tan . x) > ( - 1) & ( tan . x) < 1 by A2, A5;

        hence thesis by A6, SIN_COS9: 86;

      end;

      then

       A7: ( arccot * tan ) is_differentiable_on Z by A1, FDIFF_1: 9;

      for x st x in Z holds ((( arccot * tan ) `| Z) . x) = ( - 1)

      proof

        let x;

        assume

         A8: x in Z;

        then

         A9: ( tan . x) > ( - 1) & ( tan . x) < 1 by A2;

        

         A10: ( tan . x) = (( sin . x) / ( cos . x)) by A3, A8, RFUNCT_1:def 1;

        

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

        then

         A12: tan is_differentiable_in x by FDIFF_7: 46;

        

         A13: (( cos . x) ^2 ) <> 0 by A11, SQUARE_1: 12;

        ((( arccot * tan ) `| Z) . x) = ( diff (( arccot * tan ),x)) by A7, A8, FDIFF_1:def 7

        .= ( - (( diff ( tan ,x)) / (1 + (( tan . x) ^2 )))) by A12, A9, SIN_COS9: 86

        .= ( - ((1 / (( cos . x) ^2 )) / (1 + (( tan . x) ^2 )))) by A11, FDIFF_7: 46

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

        .= ( - (1 / ((( cos . x) ^2 ) * (1 + ((( sin . x) ^2 ) / (( cos . x) ^2 )))))) by XCMPLX_1: 76

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

        .= ( - (1 / ((( cos . x) ^2 ) + (( sin . x) ^2 )))) by A13, XCMPLX_1: 89

        .= ( - (1 / 1)) by SIN_COS: 28

        .= ( - 1);

        hence thesis;

      end;

      hence thesis by A1, A4, FDIFF_1: 9;

    end;

    theorem :: FDIFF_11:7

    Z c= ( dom ( arctan * cot )) & (for x st x in Z holds ( cot . x) > ( - 1) & ( cot . x) < 1) implies ( arctan * cot ) is_differentiable_on Z & for x st x in Z holds ((( arctan * cot ) `| Z) . x) = ( - 1)

    proof

      assume that

       A1: Z c= ( dom ( arctan * cot )) and

       A2: for x st x in Z holds ( cot . x) > ( - 1) & ( cot . x) < 1;

      ( dom ( arctan * cot )) c= ( dom cot ) by RELAT_1: 25;

      then

       A3: Z c= ( dom cot ) by A1, XBOOLE_1: 1;

      

       A4: for x st x in Z holds ( arctan * cot ) is_differentiable_in x

      proof

        let x;

        assume

         A5: x in Z;

        then ( sin . x) <> 0 by A3, FDIFF_8: 2;

        then

         A6: cot is_differentiable_in x by FDIFF_7: 47;

        ( cot . x) > ( - 1) & ( cot . x) < 1 by A2, A5;

        hence thesis by A6, SIN_COS9: 85;

      end;

      then

       A7: ( arctan * cot ) is_differentiable_on Z by A1, FDIFF_1: 9;

      for x st x in Z holds ((( arctan * cot ) `| Z) . x) = ( - 1)

      proof

        let x;

        assume

         A8: x in Z;

        then

         A9: ( cot . x) > ( - 1) & ( cot . x) < 1 by A2;

        

         A10: ( cot . x) = (( cos . x) / ( sin . x)) by A3, A8, RFUNCT_1:def 1;

        

         A11: ( sin . x) <> 0 by A3, A8, FDIFF_8: 2;

        then

         A12: cot is_differentiable_in x by FDIFF_7: 47;

        

         A13: (( sin . x) ^2 ) <> 0 by A11, SQUARE_1: 12;

        ((( arctan * cot ) `| Z) . x) = ( diff (( arctan * cot ),x)) by A7, A8, FDIFF_1:def 7

        .= (( diff ( cot ,x)) / (1 + (( cot . x) ^2 ))) by A12, A9, SIN_COS9: 85

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

        .= ( - ((1 / (( sin . x) ^2 )) / (1 + (( cot . x) ^2 ))))

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

        .= ( - (1 / ((( sin . x) ^2 ) * (1 + ((( cos . x) ^2 ) / (( sin . x) ^2 )))))) by XCMPLX_1: 76

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

        .= ( - (1 / ((( sin . x) ^2 ) + (( cos . x) ^2 )))) by A13, XCMPLX_1: 89

        .= ( - (1 / 1)) by SIN_COS: 28

        .= ( - 1);

        hence thesis;

      end;

      hence thesis by A1, A4, FDIFF_1: 9;

    end;

    theorem :: FDIFF_11:8

    Z c= ( dom ( arccot * cot )) & (for x st x in Z holds ( cot . x) > ( - 1) & ( cot . x) < 1) implies ( arccot * cot ) is_differentiable_on Z & for x st x in Z holds ((( arccot * cot ) `| Z) . x) = 1

    proof

      assume that

       A1: Z c= ( dom ( arccot * cot )) and

       A2: for x st x in Z holds ( cot . x) > ( - 1) & ( cot . x) < 1;

      ( dom ( arccot * cot )) c= ( dom cot ) by RELAT_1: 25;

      then

       A3: Z c= ( dom cot ) by A1, XBOOLE_1: 1;

      

       A4: for x st x in Z holds ( arccot * cot ) is_differentiable_in x

      proof

        let x;

        assume

         A5: x in Z;

        then ( sin . x) <> 0 by A3, FDIFF_8: 2;

        then

         A6: cot is_differentiable_in x by FDIFF_7: 47;

        ( cot . x) > ( - 1) & ( cot . x) < 1 by A2, A5;

        hence thesis by A6, SIN_COS9: 86;

      end;

      then

       A7: ( arccot * cot ) is_differentiable_on Z by A1, FDIFF_1: 9;

      for x st x in Z holds ((( arccot * cot ) `| Z) . x) = 1

      proof

        let x;

        assume

         A8: x in Z;

        then

         A9: ( cot . x) > ( - 1) & ( cot . x) < 1 by A2;

        

         A10: ( cot . x) = (( cos . x) / ( sin . x)) by A3, A8, RFUNCT_1:def 1;

        

         A11: ( sin . x) <> 0 by A3, A8, FDIFF_8: 2;

        then

         A12: cot is_differentiable_in x by FDIFF_7: 47;

        

         A13: (( sin . x) ^2 ) <> 0 by A11, SQUARE_1: 12;

        ((( arccot * cot ) `| Z) . x) = ( diff (( arccot * cot ),x)) by A7, A8, FDIFF_1:def 7

        .= ( - (( diff ( cot ,x)) / (1 + (( cot . x) ^2 )))) by A12, A9, SIN_COS9: 86

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

        .= ((1 / (( sin . x) ^2 )) / (1 + (( cot . x) ^2 )))

        .= (1 / ((( sin . x) ^2 ) * (1 + ((( cos . x) / ( sin . x)) * (( cos . x) / ( sin . x)))))) by A10, XCMPLX_1: 78

        .= (1 / ((( sin . x) ^2 ) * (1 + ((( cos . x) ^2 ) / (( sin . x) ^2 ))))) by XCMPLX_1: 76

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

        .= (1 / ((( sin . x) ^2 ) + (( cos . x) ^2 ))) by A13, XCMPLX_1: 89

        .= (1 / 1) by SIN_COS: 28

        .= 1;

        hence thesis;

      end;

      hence thesis by A1, A4, FDIFF_1: 9;

    end;

    theorem :: FDIFF_11:9

    Z c= ( dom ( arctan * arctan )) & Z c= ].( - 1), 1.[ & (for x st x in Z holds ( arctan . x) > ( - 1) & ( arctan . x) < 1) implies ( arctan * arctan ) is_differentiable_on Z & for x st x in Z holds ((( arctan * arctan ) `| Z) . x) = (1 / ((1 + (x ^2 )) * (1 + (( arctan . x) ^2 ))))

    proof

      assume that

       A1: Z c= ( dom ( arctan * arctan )) and

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

       A3: for x st x in Z holds ( arctan . x) > ( - 1) & ( arctan . x) < 1;

      

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

      proof

        let x;

        assume

         A5: x in Z;

        then

         A6: ( arctan . x) > ( - 1) & ( arctan . x) < 1 by A3;

         arctan is_differentiable_on Z by A2, SIN_COS9: 81;

        then arctan is_differentiable_in x by A5, FDIFF_1: 9;

        hence thesis by A6, SIN_COS9: 85;

      end;

      then

       A7: ( arctan * arctan ) is_differentiable_on Z by A1, FDIFF_1: 9;

      for x st x in Z holds ((( arctan * arctan ) `| Z) . x) = (1 / ((1 + (x ^2 )) * (1 + (( arctan . x) ^2 ))))

      proof

        let x;

        assume

         A8: x in Z;

        then

         A9: ( arctan . x) > ( - 1) & ( arctan . x) < 1 by A3;

        

         A10: arctan is_differentiable_on Z by A2, SIN_COS9: 81;

        then

         A11: arctan is_differentiable_in x by A8, FDIFF_1: 9;

        ((( arctan * arctan ) `| Z) . x) = ( diff (( arctan * arctan ),x)) by A7, A8, FDIFF_1:def 7

        .= (( diff ( arctan ,x)) / (1 + (( arctan . x) ^2 ))) by A11, A9, SIN_COS9: 85

        .= ((( arctan `| Z) . x) / (1 + (( arctan . x) ^2 ))) by A8, A10, FDIFF_1:def 7

        .= ((1 / (1 + (x ^2 ))) / (1 + (( arctan . x) ^2 ))) by A2, A8, SIN_COS9: 81

        .= (1 / ((1 + (x ^2 )) * (1 + (( arctan . x) ^2 )))) by XCMPLX_1: 78;

        hence thesis;

      end;

      hence thesis by A1, A4, FDIFF_1: 9;

    end;

    theorem :: FDIFF_11:10

    Z c= ( dom ( arccot * arctan )) & Z c= ].( - 1), 1.[ & (for x st x in Z holds ( arctan . x) > ( - 1) & ( arctan . x) < 1) implies ( arccot * arctan ) is_differentiable_on Z & for x st x in Z holds ((( arccot * arctan ) `| Z) . x) = ( - (1 / ((1 + (x ^2 )) * (1 + (( arctan . x) ^2 )))))

    proof

      assume that

       A1: Z c= ( dom ( arccot * arctan )) and

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

       A3: for x st x in Z holds ( arctan . x) > ( - 1) & ( arctan . x) < 1;

      

       A4: for x st x in Z holds ( arccot * arctan ) is_differentiable_in x

      proof

        let x;

        assume

         A5: x in Z;

        then

         A6: ( arctan . x) > ( - 1) & ( arctan . x) < 1 by A3;

         arctan is_differentiable_on Z by A2, SIN_COS9: 81;

        then arctan is_differentiable_in x by A5, FDIFF_1: 9;

        hence thesis by A6, SIN_COS9: 86;

      end;

      then

       A7: ( arccot * arctan ) is_differentiable_on Z by A1, FDIFF_1: 9;

      for x st x in Z holds ((( arccot * arctan ) `| Z) . x) = ( - (1 / ((1 + (x ^2 )) * (1 + (( arctan . x) ^2 )))))

      proof

        let x;

        assume

         A8: x in Z;

        then

         A9: ( arctan . x) > ( - 1) & ( arctan . x) < 1 by A3;

        

         A10: arctan is_differentiable_on Z by A2, SIN_COS9: 81;

        then

         A11: arctan is_differentiable_in x by A8, FDIFF_1: 9;

        ((( arccot * arctan ) `| Z) . x) = ( diff (( arccot * arctan ),x)) by A7, A8, FDIFF_1:def 7

        .= ( - (( diff ( arctan ,x)) / (1 + (( arctan . x) ^2 )))) by A11, A9, SIN_COS9: 86

        .= ( - ((( arctan `| Z) . x) / (1 + (( arctan . x) ^2 )))) by A8, A10, FDIFF_1:def 7

        .= ( - ((1 / (1 + (x ^2 ))) / (1 + (( arctan . x) ^2 )))) by A2, A8, SIN_COS9: 81

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

        hence thesis;

      end;

      hence thesis by A1, A4, FDIFF_1: 9;

    end;

    theorem :: FDIFF_11:11

    Z c= ( dom ( arctan * arccot )) & Z c= ].( - 1), 1.[ & (for x st x in Z holds ( arccot . x) > ( - 1) & ( arccot . x) < 1) implies ( arctan * arccot ) is_differentiable_on Z & for x st x in Z holds ((( arctan * arccot ) `| Z) . x) = ( - (1 / ((1 + (x ^2 )) * (1 + (( arccot . x) ^2 )))))

    proof

      assume that

       A1: Z c= ( dom ( arctan * arccot )) and

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

       A3: for x st x in Z holds ( arccot . x) > ( - 1) & ( arccot . x) < 1;

      

       A4: for x st x in Z holds ( arctan * arccot ) is_differentiable_in x

      proof

        let x;

        assume

         A5: x in Z;

        then

         A6: ( arccot . x) > ( - 1) & ( arccot . x) < 1 by A3;

         arccot is_differentiable_on Z by A2, SIN_COS9: 82;

        then arccot is_differentiable_in x by A5, FDIFF_1: 9;

        hence thesis by A6, SIN_COS9: 85;

      end;

      then

       A7: ( arctan * arccot ) is_differentiable_on Z by A1, FDIFF_1: 9;

      for x st x in Z holds ((( arctan * arccot ) `| Z) . x) = ( - (1 / ((1 + (x ^2 )) * (1 + (( arccot . x) ^2 )))))

      proof

        let x;

        assume

         A8: x in Z;

        then

         A9: ( arccot . x) > ( - 1) & ( arccot . x) < 1 by A3;

        

         A10: arccot is_differentiable_on Z by A2, SIN_COS9: 82;

        then

         A11: arccot is_differentiable_in x by A8, FDIFF_1: 9;

        ((( arctan * arccot ) `| Z) . x) = ( diff (( arctan * arccot ),x)) by A7, A8, FDIFF_1:def 7

        .= (( diff ( arccot ,x)) / (1 + (( arccot . x) ^2 ))) by A11, A9, SIN_COS9: 85

        .= ((( arccot `| Z) . x) / (1 + (( arccot . x) ^2 ))) by A8, A10, FDIFF_1:def 7

        .= (( - (1 / (1 + (x ^2 )))) / (1 + (( arccot . x) ^2 ))) by A2, A8, SIN_COS9: 82

        .= ( - ((1 / (1 + (x ^2 ))) / (1 + (( arccot . x) ^2 ))))

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

        hence thesis;

      end;

      hence thesis by A1, A4, FDIFF_1: 9;

    end;

    theorem :: FDIFF_11:12

    Z c= ( dom ( arccot * arccot )) & Z c= ].( - 1), 1.[ & (for x st x in Z holds ( arccot . x) > ( - 1) & ( arccot . x) < 1) implies ( arccot * arccot ) is_differentiable_on Z & for x st x in Z holds ((( arccot * arccot ) `| Z) . x) = (1 / ((1 + (x ^2 )) * (1 + (( arccot . x) ^2 ))))

    proof

      assume that

       A1: Z c= ( dom ( arccot * arccot )) and

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

       A3: for x st x in Z holds ( arccot . x) > ( - 1) & ( arccot . x) < 1;

      

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

      proof

        let x;

        assume

         A5: x in Z;

        then

         A6: ( arccot . x) > ( - 1) & ( arccot . x) < 1 by A3;

         arccot is_differentiable_on Z by A2, SIN_COS9: 82;

        then arccot is_differentiable_in x by A5, FDIFF_1: 9;

        hence thesis by A6, SIN_COS9: 86;

      end;

      then

       A7: ( arccot * arccot ) is_differentiable_on Z by A1, FDIFF_1: 9;

      for x st x in Z holds ((( arccot * arccot ) `| Z) . x) = (1 / ((1 + (x ^2 )) * (1 + (( arccot . x) ^2 ))))

      proof

        let x;

        assume

         A8: x in Z;

        then

         A9: ( arccot . x) > ( - 1) & ( arccot . x) < 1 by A3;

        

         A10: arccot is_differentiable_on Z by A2, SIN_COS9: 82;

        then

         A11: arccot is_differentiable_in x by A8, FDIFF_1: 9;

        ((( arccot * arccot ) `| Z) . x) = ( diff (( arccot * arccot ),x)) by A7, A8, FDIFF_1:def 7

        .= ( - (( diff ( arccot ,x)) / (1 + (( arccot . x) ^2 )))) by A11, A9, SIN_COS9: 86

        .= ( - ((( arccot `| Z) . x) / (1 + (( arccot . x) ^2 )))) by A8, A10, FDIFF_1:def 7

        .= ( - (( - (1 / (1 + (x ^2 )))) / (1 + (( arccot . x) ^2 )))) by A2, A8, SIN_COS9: 82

        .= ((1 / (1 + (x ^2 ))) / (1 + (( arccot . x) ^2 )))

        .= (1 / ((1 + (x ^2 )) * (1 + (( arccot . x) ^2 )))) by XCMPLX_1: 78;

        hence thesis;

      end;

      hence thesis by A1, A4, FDIFF_1: 9;

    end;

    theorem :: FDIFF_11:13

    Z c= ( dom ( sin * arctan )) & Z c= ].( - 1), 1.[ implies ( sin * arctan ) is_differentiable_on Z & for x st x in Z holds ((( sin * arctan ) `| Z) . x) = (( cos . ( arctan . x)) / (1 + (x ^2 )))

    proof

      assume that

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

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

      

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

      proof

        let x;

        assume

         A4: x in Z;

        

         A5: sin is_differentiable_in ( arctan . x) by SIN_COS: 64;

         arctan is_differentiable_on Z by A2, SIN_COS9: 81;

        then arctan is_differentiable_in x by A4, FDIFF_1: 9;

        hence thesis by A5, FDIFF_2: 13;

      end;

      then

       A6: ( sin * arctan ) is_differentiable_on Z by A1, FDIFF_1: 9;

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

      proof

        let x;

        assume

         A7: x in Z;

        

         A8: arctan is_differentiable_on Z by A2, SIN_COS9: 81;

        then

         A9: arctan is_differentiable_in x by A7, FDIFF_1: 9;

        

         A10: sin is_differentiable_in ( arctan . x) by SIN_COS: 64;

        ((( sin * arctan ) `| Z) . x) = ( diff (( sin * arctan ),x)) by A6, A7, FDIFF_1:def 7

        .= (( diff ( sin ,( arctan . x))) * ( diff ( arctan ,x))) by A9, A10, FDIFF_2: 13

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

        .= (( cos . ( arctan . x)) * (( arctan `| Z) . x)) by A7, A8, FDIFF_1:def 7

        .= (( cos . ( arctan . x)) * (1 / (1 + (x ^2 )))) by A2, A7, SIN_COS9: 81

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

        hence thesis;

      end;

      hence thesis by A1, A3, FDIFF_1: 9;

    end;

    theorem :: FDIFF_11:14

    Z c= ( dom ( sin * arccot )) & Z c= ].( - 1), 1.[ implies ( sin * arccot ) is_differentiable_on Z & for x st x in Z holds ((( sin * arccot ) `| Z) . x) = ( - (( cos . ( arccot . x)) / (1 + (x ^2 ))))

    proof

      assume that

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

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

      

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

      proof

        let x;

        assume

         A4: x in Z;

        

         A5: sin is_differentiable_in ( arccot . x) by SIN_COS: 64;

         arccot is_differentiable_on Z by A2, SIN_COS9: 82;

        then arccot is_differentiable_in x by A4, FDIFF_1: 9;

        hence thesis by A5, FDIFF_2: 13;

      end;

      then

       A6: ( sin * arccot ) is_differentiable_on Z by A1, FDIFF_1: 9;

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

      proof

        let x;

        assume

         A7: x in Z;

        

         A8: arccot is_differentiable_on Z by A2, SIN_COS9: 82;

        then

         A9: arccot is_differentiable_in x by A7, FDIFF_1: 9;

        

         A10: sin is_differentiable_in ( arccot . x) by SIN_COS: 64;

        ((( sin * arccot ) `| Z) . x) = ( diff (( sin * arccot ),x)) by A6, A7, FDIFF_1:def 7

        .= (( diff ( sin ,( arccot . x))) * ( diff ( arccot ,x))) by A9, A10, FDIFF_2: 13

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

        .= (( cos . ( arccot . x)) * (( arccot `| Z) . x)) by A7, A8, FDIFF_1:def 7

        .= (( cos . ( arccot . x)) * ( - (1 / (1 + (x ^2 ))))) by A2, A7, SIN_COS9: 82

        .= ( - (( cos . ( arccot . x)) / (1 + (x ^2 ))));

        hence thesis;

      end;

      hence thesis by A1, A3, FDIFF_1: 9;

    end;

    theorem :: FDIFF_11:15

    Z c= ( dom ( cos * arctan )) & Z c= ].( - 1), 1.[ implies ( cos * arctan ) is_differentiable_on Z & for x st x in Z holds ((( cos * arctan ) `| Z) . x) = ( - (( sin . ( arctan . x)) / (1 + (x ^2 ))))

    proof

      assume that

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

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

      

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

      proof

        let x;

        assume

         A4: x in Z;

        

         A5: cos is_differentiable_in ( arctan . x) by SIN_COS: 63;

         arctan is_differentiable_on Z by A2, SIN_COS9: 81;

        then arctan is_differentiable_in x by A4, FDIFF_1: 9;

        hence thesis by A5, FDIFF_2: 13;

      end;

      then

       A6: ( cos * arctan ) is_differentiable_on Z by A1, FDIFF_1: 9;

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

      proof

        let x;

        assume

         A7: x in Z;

        

         A8: arctan is_differentiable_on Z by A2, SIN_COS9: 81;

        then

         A9: arctan is_differentiable_in x by A7, FDIFF_1: 9;

        

         A10: cos is_differentiable_in ( arctan . x) by SIN_COS: 63;

        ((( cos * arctan ) `| Z) . x) = ( diff (( cos * arctan ),x)) by A6, A7, FDIFF_1:def 7

        .= (( diff ( cos ,( arctan . x))) * ( diff ( arctan ,x))) by A9, A10, FDIFF_2: 13

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

        .= ( - (( sin . ( arctan . x)) * ( diff ( arctan ,x))))

        .= ( - (( sin . ( arctan . x)) * (( arctan `| Z) . x))) by A7, A8, FDIFF_1:def 7

        .= ( - (( sin . ( arctan . x)) * (1 / (1 + (x ^2 ))))) by A2, A7, SIN_COS9: 81

        .= ( - (( sin . ( arctan . x)) / (1 + (x ^2 ))));

        hence thesis;

      end;

      hence thesis by A1, A3, FDIFF_1: 9;

    end;

    theorem :: FDIFF_11:16

    Z c= ( dom ( cos * arccot )) & Z c= ].( - 1), 1.[ implies ( cos * arccot ) is_differentiable_on Z & for x st x in Z holds ((( cos * arccot ) `| Z) . x) = (( sin . ( arccot . x)) / (1 + (x ^2 )))

    proof

      assume that

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

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

      

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

      proof

        let x;

        assume

         A4: x in Z;

        

         A5: cos is_differentiable_in ( arccot . x) by SIN_COS: 63;

         arccot is_differentiable_on Z by A2, SIN_COS9: 82;

        then arccot is_differentiable_in x by A4, FDIFF_1: 9;

        hence thesis by A5, FDIFF_2: 13;

      end;

      then

       A6: ( cos * arccot ) is_differentiable_on Z by A1, FDIFF_1: 9;

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

      proof

        let x;

        assume

         A7: x in Z;

        

         A8: arccot is_differentiable_on Z by A2, SIN_COS9: 82;

        then

         A9: arccot is_differentiable_in x by A7, FDIFF_1: 9;

        

         A10: cos is_differentiable_in ( arccot . x) by SIN_COS: 63;

        ((( cos * arccot ) `| Z) . x) = ( diff (( cos * arccot ),x)) by A6, A7, FDIFF_1:def 7

        .= (( diff ( cos ,( arccot . x))) * ( diff ( arccot ,x))) by A9, A10, FDIFF_2: 13

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

        .= ( - (( sin . ( arccot . x)) * ( diff ( arccot ,x))))

        .= ( - (( sin . ( arccot . x)) * (( arccot `| Z) . x))) by A7, A8, FDIFF_1:def 7

        .= ( - (( sin . ( arccot . x)) * ( - (1 / (1 + (x ^2 )))))) by A2, A7, SIN_COS9: 82

        .= (( sin . ( arccot . x)) / (1 + (x ^2 )));

        hence thesis;

      end;

      hence thesis by A1, A3, FDIFF_1: 9;

    end;

    theorem :: FDIFF_11:17

    Z c= ( dom ( tan * arctan )) & Z c= ].( - 1), 1.[ implies ( tan * arctan ) is_differentiable_on Z & for x st x in Z holds ((( tan * arctan ) `| Z) . x) = (1 / ((( cos . ( arctan . x)) ^2 ) * (1 + (x ^2 ))))

    proof

      assume that

       A1: Z c= ( dom ( tan * arctan )) and

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

      

       A3: for x st x in Z holds ( tan * arctan ) is_differentiable_in x

      proof

        let x;

        assume

         A4: x in Z;

        then ( arctan . x) in ( dom tan ) by A1, FUNCT_1: 11;

        then ( cos . ( arctan . x)) <> 0 by FDIFF_8: 1;

        then

         A5: tan is_differentiable_in ( arctan . x) by FDIFF_7: 46;

         arctan is_differentiable_on Z by A2, SIN_COS9: 81;

        then arctan is_differentiable_in x by A4, FDIFF_1: 9;

        hence thesis by A5, FDIFF_2: 13;

      end;

      then

       A6: ( tan * arctan ) is_differentiable_on Z by A1, FDIFF_1: 9;

      for x st x in Z holds ((( tan * arctan ) `| Z) . x) = (1 / ((( cos . ( arctan . x)) ^2 ) * (1 + (x ^2 ))))

      proof

        let x;

        assume

         A7: x in Z;

        then ( arctan . x) in ( dom tan ) by A1, FUNCT_1: 11;

        then

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

        then

         A9: tan is_differentiable_in ( arctan . x) by FDIFF_7: 46;

        

         A10: arctan is_differentiable_on Z by A2, SIN_COS9: 81;

        then

         A11: arctan is_differentiable_in x by A7, FDIFF_1: 9;

        ((( tan * arctan ) `| Z) . x) = ( diff (( tan * arctan ),x)) by A6, A7, FDIFF_1:def 7

        .= (( diff ( tan ,( arctan . x))) * ( diff ( arctan ,x))) by A11, A9, FDIFF_2: 13

        .= ((1 / (( cos . ( arctan . x)) ^2 )) * ( diff ( arctan ,x))) by A8, FDIFF_7: 46

        .= ((1 / (( cos . ( arctan . x)) ^2 )) * (( arctan `| Z) . x)) by A7, A10, FDIFF_1:def 7

        .= ((1 / (( cos . ( arctan . x)) ^2 )) * (1 / (1 + (x ^2 )))) by A2, A7, SIN_COS9: 81

        .= (1 / ((( cos . ( arctan . x)) ^2 ) * (1 + (x ^2 )))) by XCMPLX_1: 102;

        hence thesis;

      end;

      hence thesis by A1, A3, FDIFF_1: 9;

    end;

    theorem :: FDIFF_11:18

    Z c= ( dom ( tan * arccot )) & Z c= ].( - 1), 1.[ implies ( tan * arccot ) is_differentiable_on Z & for x st x in Z holds ((( tan * arccot ) `| Z) . x) = ( - (1 / ((( cos . ( arccot . x)) ^2 ) * (1 + (x ^2 )))))

    proof

      assume that

       A1: Z c= ( dom ( tan * arccot )) and

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

      

       A3: for x st x in Z holds ( tan * arccot ) is_differentiable_in x

      proof

        let x;

        assume

         A4: x in Z;

        then ( arccot . x) in ( dom tan ) by A1, FUNCT_1: 11;

        then ( cos . ( arccot . x)) <> 0 by FDIFF_8: 1;

        then

         A5: tan is_differentiable_in ( arccot . x) by FDIFF_7: 46;

         arccot is_differentiable_on Z by A2, SIN_COS9: 82;

        then arccot is_differentiable_in x by A4, FDIFF_1: 9;

        hence thesis by A5, FDIFF_2: 13;

      end;

      then

       A6: ( tan * arccot ) is_differentiable_on Z by A1, FDIFF_1: 9;

      for x st x in Z holds ((( tan * arccot ) `| Z) . x) = ( - (1 / ((( cos . ( arccot . x)) ^2 ) * (1 + (x ^2 )))))

      proof

        let x;

        assume

         A7: x in Z;

        then ( arccot . x) in ( dom tan ) by A1, FUNCT_1: 11;

        then

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

        then

         A9: tan is_differentiable_in ( arccot . x) by FDIFF_7: 46;

        

         A10: arccot is_differentiable_on Z by A2, SIN_COS9: 82;

        then

         A11: arccot is_differentiable_in x by A7, FDIFF_1: 9;

        ((( tan * arccot ) `| Z) . x) = ( diff (( tan * arccot ),x)) by A6, A7, FDIFF_1:def 7

        .= (( diff ( tan ,( arccot . x))) * ( diff ( arccot ,x))) by A11, A9, FDIFF_2: 13

        .= ((1 / (( cos . ( arccot . x)) ^2 )) * ( diff ( arccot ,x))) by A8, FDIFF_7: 46

        .= ((1 / (( cos . ( arccot . x)) ^2 )) * (( arccot `| Z) . x)) by A7, A10, FDIFF_1:def 7

        .= ((1 / (( cos . ( arccot . x)) ^2 )) * ( - (1 / (1 + (x ^2 ))))) by A2, A7, SIN_COS9: 82

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

        .= ( - (1 / ((( cos . ( arccot . x)) ^2 ) * (1 + (x ^2 ))))) by XCMPLX_1: 102;

        hence thesis;

      end;

      hence thesis by A1, A3, FDIFF_1: 9;

    end;

    theorem :: FDIFF_11:19

    Z c= ( dom ( cot * arctan )) & Z c= ].( - 1), 1.[ implies ( cot * arctan ) is_differentiable_on Z & for x st x in Z holds ((( cot * arctan ) `| Z) . x) = ( - (1 / ((( sin . ( arctan . x)) ^2 ) * (1 + (x ^2 )))))

    proof

      assume that

       A1: Z c= ( dom ( cot * arctan )) and

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

      

       A3: for x st x in Z holds ( cot * arctan ) is_differentiable_in x

      proof

        let x;

        assume

         A4: x in Z;

        then ( arctan . x) in ( dom cot ) by A1, FUNCT_1: 11;

        then ( sin . ( arctan . x)) <> 0 by FDIFF_8: 2;

        then

         A5: cot is_differentiable_in ( arctan . x) by FDIFF_7: 47;

         arctan is_differentiable_on Z by A2, SIN_COS9: 81;

        then arctan is_differentiable_in x by A4, FDIFF_1: 9;

        hence thesis by A5, FDIFF_2: 13;

      end;

      then

       A6: ( cot * arctan ) is_differentiable_on Z by A1, FDIFF_1: 9;

      for x st x in Z holds ((( cot * arctan ) `| Z) . x) = ( - (1 / ((( sin . ( arctan . x)) ^2 ) * (1 + (x ^2 )))))

      proof

        let x;

        assume

         A7: x in Z;

        then ( arctan . x) in ( dom cot ) by A1, FUNCT_1: 11;

        then

         A8: ( sin . ( arctan . x)) <> 0 by FDIFF_8: 2;

        then

         A9: cot is_differentiable_in ( arctan . x) by FDIFF_7: 47;

        

         A10: arctan is_differentiable_on Z by A2, SIN_COS9: 81;

        then

         A11: arctan is_differentiable_in x by A7, FDIFF_1: 9;

        ((( cot * arctan ) `| Z) . x) = ( diff (( cot * arctan ),x)) by A6, A7, FDIFF_1:def 7

        .= (( diff ( cot ,( arctan . x))) * ( diff ( arctan ,x))) by A11, A9, FDIFF_2: 13

        .= (( - (1 / (( sin . ( arctan . x)) ^2 ))) * ( diff ( arctan ,x))) by A8, FDIFF_7: 47

        .= ( - ((1 / (( sin . ( arctan . x)) ^2 )) * ( diff ( arctan ,x))))

        .= ( - ((1 / (( sin . ( arctan . x)) ^2 )) * (( arctan `| Z) . x))) by A7, A10, FDIFF_1:def 7

        .= ( - ((1 / (( sin . ( arctan . x)) ^2 )) * (1 / (1 + (x ^2 ))))) by A2, A7, SIN_COS9: 81

        .= ( - (1 / ((( sin . ( arctan . x)) ^2 ) * (1 + (x ^2 ))))) by XCMPLX_1: 102;

        hence thesis;

      end;

      hence thesis by A1, A3, FDIFF_1: 9;

    end;

    theorem :: FDIFF_11:20

    Z c= ( dom ( cot * arccot )) & Z c= ].( - 1), 1.[ implies ( cot * arccot ) is_differentiable_on Z & for x st x in Z holds ((( cot * arccot ) `| Z) . x) = (1 / ((( sin . ( arccot . x)) ^2 ) * (1 + (x ^2 ))))

    proof

      assume that

       A1: Z c= ( dom ( cot * arccot )) and

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

      

       A3: for x st x in Z holds ( cot * arccot ) is_differentiable_in x

      proof

        let x;

        assume

         A4: x in Z;

        then ( arccot . x) in ( dom cot ) by A1, FUNCT_1: 11;

        then ( sin . ( arccot . x)) <> 0 by FDIFF_8: 2;

        then

         A5: cot is_differentiable_in ( arccot . x) by FDIFF_7: 47;

         arccot is_differentiable_on Z by A2, SIN_COS9: 82;

        then arccot is_differentiable_in x by A4, FDIFF_1: 9;

        hence thesis by A5, FDIFF_2: 13;

      end;

      then

       A6: ( cot * arccot ) is_differentiable_on Z by A1, FDIFF_1: 9;

      for x st x in Z holds ((( cot * arccot ) `| Z) . x) = (1 / ((( sin . ( arccot . x)) ^2 ) * (1 + (x ^2 ))))

      proof

        let x;

        assume

         A7: x in Z;

        then ( arccot . x) in ( dom cot ) by A1, FUNCT_1: 11;

        then

         A8: ( sin . ( arccot . x)) <> 0 by FDIFF_8: 2;

        then

         A9: cot is_differentiable_in ( arccot . x) by FDIFF_7: 47;

        

         A10: arccot is_differentiable_on Z by A2, SIN_COS9: 82;

        then

         A11: arccot is_differentiable_in x by A7, FDIFF_1: 9;

        ((( cot * arccot ) `| Z) . x) = ( diff (( cot * arccot ),x)) by A6, A7, FDIFF_1:def 7

        .= (( diff ( cot ,( arccot . x))) * ( diff ( arccot ,x))) by A11, A9, FDIFF_2: 13

        .= (( - (1 / (( sin . ( arccot . x)) ^2 ))) * ( diff ( arccot ,x))) by A8, FDIFF_7: 47

        .= ( - ((1 / (( sin . ( arccot . x)) ^2 )) * ( diff ( arccot ,x))))

        .= ( - ((1 / (( sin . ( arccot . x)) ^2 )) * (( arccot `| Z) . x))) by A7, A10, FDIFF_1:def 7

        .= ( - ((1 / (( sin . ( arccot . x)) ^2 )) * ( - (1 / (1 + (x ^2 )))))) by A2, A7, SIN_COS9: 82

        .= ((1 / (( sin . ( arccot . x)) ^2 )) * (1 / (1 + (x ^2 ))))

        .= (1 / ((( sin . ( arccot . x)) ^2 ) * (1 + (x ^2 )))) by XCMPLX_1: 102;

        hence thesis;

      end;

      hence thesis by A1, A3, FDIFF_1: 9;

    end;

    theorem :: FDIFF_11:21

    Z c= ( dom ( sec * arctan )) & Z c= ].( - 1), 1.[ implies ( sec * arctan ) is_differentiable_on Z & for x st x in Z holds ((( sec * arctan ) `| Z) . x) = (( sin . ( arctan . x)) / ((( cos . ( arctan . x)) ^2 ) * (1 + (x ^2 ))))

    proof

      assume that

       A1: Z c= ( dom ( sec * arctan )) and

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

      

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

      proof

        let x;

        assume x in Z;

        then ( arctan . x) in ( dom sec ) by A1, FUNCT_1: 11;

        hence thesis by RFUNCT_1: 3;

      end;

      

       A4: for x st x in Z holds ( sec * arctan ) is_differentiable_in x

      proof

        let x;

        assume

         A5: x in Z;

        then ( cos . ( arctan . x)) <> 0 by A3;

        then

         A6: sec is_differentiable_in ( arctan . x) by FDIFF_9: 1;

         arctan is_differentiable_on Z by A2, SIN_COS9: 81;

        then arctan is_differentiable_in x by A5, FDIFF_1: 9;

        hence thesis by A6, FDIFF_2: 13;

      end;

      then

       A7: ( sec * arctan ) is_differentiable_on Z by A1, FDIFF_1: 9;

      for x st x in Z holds ((( sec * arctan ) `| Z) . x) = (( sin . ( arctan . x)) / ((( cos . ( arctan . x)) ^2 ) * (1 + (x ^2 ))))

      proof

        let x;

        assume

         A8: x in Z;

        then

         A9: ( cos . ( arctan . x)) <> 0 by A3;

        ( cos . ( arctan . x)) <> 0 by A3, A8;

        then

         A10: sec is_differentiable_in ( arctan . x) by FDIFF_9: 1;

        

         A11: arctan is_differentiable_on Z by A2, SIN_COS9: 81;

        then

         A12: arctan is_differentiable_in x by A8, FDIFF_1: 9;

        ((( sec * arctan ) `| Z) . x) = ( diff (( sec * arctan ),x)) by A7, A8, FDIFF_1:def 7

        .= (( diff ( sec ,( arctan . x))) * ( diff ( arctan ,x))) by A12, A10, FDIFF_2: 13

        .= ((( sin . ( arctan . x)) / (( cos . ( arctan . x)) ^2 )) * ( diff ( arctan ,x))) by A9, FDIFF_9: 1

        .= ((( sin . ( arctan . x)) / (( cos . ( arctan . x)) ^2 )) * (( arctan `| Z) . x)) by A8, A11, FDIFF_1:def 7

        .= ((( sin . ( arctan . x)) / (( cos . ( arctan . x)) ^2 )) * (1 / (1 + (x ^2 )))) by A2, A8, SIN_COS9: 81

        .= ((( sin . ( arctan . x)) * 1) / ((( cos . ( arctan . x)) ^2 ) * (1 + (x ^2 )))) by XCMPLX_1: 76

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

        hence thesis;

      end;

      hence thesis by A1, A4, FDIFF_1: 9;

    end;

    theorem :: FDIFF_11:22

    Z c= ( dom ( sec * arccot )) & Z c= ].( - 1), 1.[ implies ( sec * arccot ) is_differentiable_on Z & for x st x in Z holds ((( sec * arccot ) `| Z) . x) = ( - (( sin . ( arccot . x)) / ((( cos . ( arccot . x)) ^2 ) * (1 + (x ^2 )))))

    proof

      assume that

       A1: Z c= ( dom ( sec * arccot )) and

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

      

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

      proof

        let x;

        assume x in Z;

        then ( arccot . x) in ( dom sec ) by A1, FUNCT_1: 11;

        hence thesis by RFUNCT_1: 3;

      end;

      

       A4: for x st x in Z holds ( sec * arccot ) is_differentiable_in x

      proof

        let x;

        assume

         A5: x in Z;

        then ( cos . ( arccot . x)) <> 0 by A3;

        then

         A6: sec is_differentiable_in ( arccot . x) by FDIFF_9: 1;

         arccot is_differentiable_on Z by A2, SIN_COS9: 82;

        then arccot is_differentiable_in x by A5, FDIFF_1: 9;

        hence thesis by A6, FDIFF_2: 13;

      end;

      then

       A7: ( sec * arccot ) is_differentiable_on Z by A1, FDIFF_1: 9;

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

      proof

        let x;

        assume

         A8: x in Z;

        then

         A9: ( cos . ( arccot . x)) <> 0 by A3;

        ( cos . ( arccot . x)) <> 0 by A3, A8;

        then

         A10: sec is_differentiable_in ( arccot . x) by FDIFF_9: 1;

        

         A11: arccot is_differentiable_on Z by A2, SIN_COS9: 82;

        then

         A12: arccot is_differentiable_in x by A8, FDIFF_1: 9;

        ((( sec * arccot ) `| Z) . x) = ( diff (( sec * arccot ),x)) by A7, A8, FDIFF_1:def 7

        .= (( diff ( sec ,( arccot . x))) * ( diff ( arccot ,x))) by A12, A10, FDIFF_2: 13

        .= ((( sin . ( arccot . x)) / (( cos . ( arccot . x)) ^2 )) * ( diff ( arccot ,x))) by A9, FDIFF_9: 1

        .= ((( sin . ( arccot . x)) / (( cos . ( arccot . x)) ^2 )) * (( arccot `| Z) . x)) by A8, A11, FDIFF_1:def 7

        .= ((( sin . ( arccot . x)) / (( cos . ( arccot . x)) ^2 )) * ( - (1 / (1 + (x ^2 ))))) by A2, A8, SIN_COS9: 82

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

        .= ( - ((( sin . ( arccot . x)) * 1) / ((( cos . ( arccot . x)) ^2 ) * (1 + (x ^2 ))))) by XCMPLX_1: 76

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

        hence thesis;

      end;

      hence thesis by A1, A4, FDIFF_1: 9;

    end;

    theorem :: FDIFF_11:23

    Z c= ( dom ( cosec * arctan )) & Z c= ].( - 1), 1.[ implies ( cosec * arctan ) is_differentiable_on Z & for x st x in Z holds ((( cosec * arctan ) `| Z) . x) = ( - (( cos . ( arctan . x)) / ((( sin . ( arctan . x)) ^2 ) * (1 + (x ^2 )))))

    proof

      assume that

       A1: Z c= ( dom ( cosec * arctan )) and

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

      

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

      proof

        let x;

        assume x in Z;

        then ( arctan . x) in ( dom cosec ) by A1, FUNCT_1: 11;

        hence thesis by RFUNCT_1: 3;

      end;

      

       A4: for x st x in Z holds ( cosec * arctan ) is_differentiable_in x

      proof

        let x;

        assume

         A5: x in Z;

        then ( sin . ( arctan . x)) <> 0 by A3;

        then

         A6: cosec is_differentiable_in ( arctan . x) by FDIFF_9: 2;

         arctan is_differentiable_on Z by A2, SIN_COS9: 81;

        then arctan is_differentiable_in x by A5, FDIFF_1: 9;

        hence thesis by A6, FDIFF_2: 13;

      end;

      then

       A7: ( cosec * arctan ) is_differentiable_on Z by A1, FDIFF_1: 9;

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

      proof

        let x;

        assume

         A8: x in Z;

        then

         A9: ( sin . ( arctan . x)) <> 0 by A3;

        ( sin . ( arctan . x)) <> 0 by A3, A8;

        then

         A10: cosec is_differentiable_in ( arctan . x) by FDIFF_9: 2;

        

         A11: arctan is_differentiable_on Z by A2, SIN_COS9: 81;

        then

         A12: arctan is_differentiable_in x by A8, FDIFF_1: 9;

        ((( cosec * arctan ) `| Z) . x) = ( diff (( cosec * arctan ),x)) by A7, A8, FDIFF_1:def 7

        .= (( diff ( cosec ,( arctan . x))) * ( diff ( arctan ,x))) by A12, A10, FDIFF_2: 13

        .= (( - (( cos . ( arctan . x)) / (( sin . ( arctan . x)) ^2 ))) * ( diff ( arctan ,x))) by A9, FDIFF_9: 2

        .= ( - ((( cos . ( arctan . x)) / (( sin . ( arctan . x)) ^2 )) * ( diff ( arctan ,x))))

        .= ( - ((( cos . ( arctan . x)) / (( sin . ( arctan . x)) ^2 )) * (( arctan `| Z) . x))) by A8, A11, FDIFF_1:def 7

        .= ( - ((( cos . ( arctan . x)) / (( sin . ( arctan . x)) ^2 )) * (1 / (1 + (x ^2 ))))) by A2, A8, SIN_COS9: 81

        .= ( - ((( cos . ( arctan . x)) * 1) / ((( sin . ( arctan . x)) ^2 ) * (1 + (x ^2 ))))) by XCMPLX_1: 76

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

        hence thesis;

      end;

      hence thesis by A1, A4, FDIFF_1: 9;

    end;

    theorem :: FDIFF_11:24

    Z c= ( dom ( cosec * arccot )) & Z c= ].( - 1), 1.[ implies ( cosec * arccot ) is_differentiable_on Z & for x st x in Z holds ((( cosec * arccot ) `| Z) . x) = (( cos . ( arccot . x)) / ((( sin . ( arccot . x)) ^2 ) * (1 + (x ^2 ))))

    proof

      assume that

       A1: Z c= ( dom ( cosec * arccot )) and

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

      

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

      proof

        let x;

        assume x in Z;

        then ( arccot . x) in ( dom cosec ) by A1, FUNCT_1: 11;

        hence thesis by RFUNCT_1: 3;

      end;

      

       A4: for x st x in Z holds ( cosec * arccot ) is_differentiable_in x

      proof

        let x;

        assume

         A5: x in Z;

        then ( sin . ( arccot . x)) <> 0 by A3;

        then

         A6: cosec is_differentiable_in ( arccot . x) by FDIFF_9: 2;

         arccot is_differentiable_on Z by A2, SIN_COS9: 82;

        then arccot is_differentiable_in x by A5, FDIFF_1: 9;

        hence thesis by A6, FDIFF_2: 13;

      end;

      then

       A7: ( cosec * arccot ) is_differentiable_on Z by A1, FDIFF_1: 9;

      for x st x in Z holds ((( cosec * arccot ) `| Z) . x) = (( cos . ( arccot . x)) / ((( sin . ( arccot . x)) ^2 ) * (1 + (x ^2 ))))

      proof

        let x;

        assume

         A8: x in Z;

        then

         A9: ( sin . ( arccot . x)) <> 0 by A3;

        ( sin . ( arccot . x)) <> 0 by A3, A8;

        then

         A10: cosec is_differentiable_in ( arccot . x) by FDIFF_9: 2;

        

         A11: arccot is_differentiable_on Z by A2, SIN_COS9: 82;

        then

         A12: arccot is_differentiable_in x by A8, FDIFF_1: 9;

        ((( cosec * arccot ) `| Z) . x) = ( diff (( cosec * arccot ),x)) by A7, A8, FDIFF_1:def 7

        .= (( diff ( cosec ,( arccot . x))) * ( diff ( arccot ,x))) by A12, A10, FDIFF_2: 13

        .= (( - (( cos . ( arccot . x)) / (( sin . ( arccot . x)) ^2 ))) * ( diff ( arccot ,x))) by A9, FDIFF_9: 2

        .= ( - ((( cos . ( arccot . x)) / (( sin . ( arccot . x)) ^2 )) * ( diff ( arccot ,x))))

        .= ( - ((( cos . ( arccot . x)) / (( sin . ( arccot . x)) ^2 )) * (( arccot `| Z) . x))) by A8, A11, FDIFF_1:def 7

        .= ( - ((( cos . ( arccot . x)) / (( sin . ( arccot . x)) ^2 )) * ( - (1 / (1 + (x ^2 )))))) by A2, A8, SIN_COS9: 82

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

        .= ((( cos . ( arccot . x)) * 1) / ((( sin . ( arccot . x)) ^2 ) * (1 + (x ^2 )))) by XCMPLX_1: 76

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

        hence thesis;

      end;

      hence thesis by A1, A4, FDIFF_1: 9;

    end;

    theorem :: FDIFF_11:25

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

    proof

      assume that

       A1: Z c= ( dom ( sin (#) arctan )) and

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

      

       A3: arctan is_differentiable_on Z by A2, SIN_COS9: 81;

      

       A4: for x st x in Z holds sin is_differentiable_in x by SIN_COS: 64;

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

      then Z c= ( dom sin ) by XBOOLE_1: 18;

      then

       A5: sin is_differentiable_on Z by A4, FDIFF_1: 9;

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

      proof

        let x;

        assume

         A6: x in Z;

        

        then ((( sin (#) arctan ) `| Z) . x) = ((( arctan . x) * ( diff ( sin ,x))) + (( sin . x) * ( diff ( arctan ,x)))) by A1, A5, A3, FDIFF_1: 21

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

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

        .= ((( cos . x) * ( arctan . x)) + (( sin . x) * (1 / (1 + (x ^2 ))))) by A2, A6, SIN_COS9: 81

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

        hence thesis;

      end;

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

    end;

    theorem :: FDIFF_11:26

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

    proof

      assume that

       A1: Z c= ( dom ( sin (#) arccot )) and

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

      

       A3: arccot is_differentiable_on Z by A2, SIN_COS9: 82;

      

       A4: for x st x in Z holds sin is_differentiable_in x by SIN_COS: 64;

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

      then Z c= ( dom sin ) by XBOOLE_1: 18;

      then

       A5: sin is_differentiable_on Z by A4, FDIFF_1: 9;

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

      proof

        let x;

        assume

         A6: x in Z;

        

        then ((( sin (#) arccot ) `| Z) . x) = ((( arccot . x) * ( diff ( sin ,x))) + (( sin . x) * ( diff ( arccot ,x)))) by A1, A5, A3, FDIFF_1: 21

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

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

        .= ((( cos . x) * ( arccot . x)) + (( sin . x) * ( - (1 / (1 + (x ^2 )))))) by A2, A6, SIN_COS9: 82

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

        hence thesis;

      end;

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

    end;

    theorem :: FDIFF_11:27

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

    proof

      assume that

       A1: Z c= ( dom ( cos (#) arctan )) and

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

      

       A3: arctan is_differentiable_on Z by A2, SIN_COS9: 81;

      

       A4: for x st x in Z holds cos is_differentiable_in x by SIN_COS: 63;

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

      then Z c= ( dom cos ) by XBOOLE_1: 18;

      then

       A5: cos is_differentiable_on Z by A4, FDIFF_1: 9;

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

      proof

        let x;

        assume

         A6: x in Z;

        

        then ((( cos (#) arctan ) `| Z) . x) = ((( arctan . x) * ( diff ( cos ,x))) + (( cos . x) * ( diff ( arctan ,x)))) by A1, A5, A3, FDIFF_1: 21

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

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

        .= (( - (( sin . x) * ( arctan . x))) + (( cos . x) * (1 / (1 + (x ^2 ))))) by A2, A6, SIN_COS9: 81

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

        hence thesis;

      end;

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

    end;

    theorem :: FDIFF_11:28

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

    proof

      assume that

       A1: Z c= ( dom ( cos (#) arccot )) and

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

      

       A3: arccot is_differentiable_on Z by A2, SIN_COS9: 82;

      

       A4: for x st x in Z holds cos is_differentiable_in x by SIN_COS: 63;

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

      then Z c= ( dom cos ) by XBOOLE_1: 18;

      then

       A5: cos is_differentiable_on Z by A4, FDIFF_1: 9;

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

      proof

        let x;

        assume

         A6: x in Z;

        

        then ((( cos (#) arccot ) `| Z) . x) = ((( arccot . x) * ( diff ( cos ,x))) + (( cos . x) * ( diff ( arccot ,x)))) by A1, A5, A3, FDIFF_1: 21

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

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

        .= (( - (( sin . x) * ( arccot . x))) + (( cos . x) * ( - (1 / (1 + (x ^2 )))))) by A2, A6, SIN_COS9: 82

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

        hence thesis;

      end;

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

    end;

    theorem :: FDIFF_11:29

    Z c= ( dom ( tan (#) arctan )) & Z c= ].( - 1), 1.[ implies ( tan (#) arctan ) is_differentiable_on Z & for x st x in Z holds ((( tan (#) arctan ) `| Z) . x) = ((( arctan . x) / (( cos . x) ^2 )) + (( tan . x) / (1 + (x ^2 ))))

    proof

      assume that

       A1: Z c= ( dom ( tan (#) arctan )) and

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

      

       A3: arctan is_differentiable_on Z by A2, SIN_COS9: 81;

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

      then

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

      for x st x in Z holds tan is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then ( cos . x) <> 0 by A4, FDIFF_8: 1;

        hence thesis by FDIFF_7: 46;

      end;

      then

       A5: tan is_differentiable_on Z by A4, FDIFF_1: 9;

      for x st x in Z holds ((( tan (#) arctan ) `| Z) . x) = ((( arctan . x) / (( cos . x) ^2 )) + (( tan . x) / (1 + (x ^2 ))))

      proof

        let x;

        assume

         A6: x in Z;

        then

         A7: ( cos . x) <> 0 by A4, FDIFF_8: 1;

        ((( tan (#) arctan ) `| Z) . x) = ((( arctan . x) * ( diff ( tan ,x))) + (( tan . x) * ( diff ( arctan ,x)))) by A1, A5, A3, A6, FDIFF_1: 21

        .= ((( arctan . x) * (1 / (( cos . x) ^2 ))) + (( tan . x) * ( diff ( arctan ,x)))) by A7, FDIFF_7: 46

        .= ((( arctan . x) / (( cos . x) ^2 )) + (( tan . x) * (( arctan `| Z) . x))) by A3, A6, FDIFF_1:def 7

        .= ((( arctan . x) / (( cos . x) ^2 )) + (( tan . x) * (1 / (1 + (x ^2 ))))) by A2, A6, SIN_COS9: 81

        .= ((( arctan . x) / (( cos . x) ^2 )) + (( tan . x) / (1 + (x ^2 ))));

        hence thesis;

      end;

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

    end;

    theorem :: FDIFF_11:30

    Z c= ( dom ( tan (#) arccot )) & Z c= ].( - 1), 1.[ implies ( tan (#) arccot ) is_differentiable_on Z & for x st x in Z holds ((( tan (#) arccot ) `| Z) . x) = ((( arccot . x) / (( cos . x) ^2 )) - (( tan . x) / (1 + (x ^2 ))))

    proof

      assume that

       A1: Z c= ( dom ( tan (#) arccot )) and

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

      

       A3: arccot is_differentiable_on Z by A2, SIN_COS9: 82;

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

      then

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

      for x st x in Z holds tan is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then ( cos . x) <> 0 by A4, FDIFF_8: 1;

        hence thesis by FDIFF_7: 46;

      end;

      then

       A5: tan is_differentiable_on Z by A4, FDIFF_1: 9;

      for x st x in Z holds ((( tan (#) arccot ) `| Z) . x) = ((( arccot . x) / (( cos . x) ^2 )) - (( tan . x) / (1 + (x ^2 ))))

      proof

        let x;

        assume

         A6: x in Z;

        then

         A7: ( cos . x) <> 0 by A4, FDIFF_8: 1;

        ((( tan (#) arccot ) `| Z) . x) = ((( arccot . x) * ( diff ( tan ,x))) + (( tan . x) * ( diff ( arccot ,x)))) by A1, A5, A3, A6, FDIFF_1: 21

        .= ((( arccot . x) * (1 / (( cos . x) ^2 ))) + (( tan . x) * ( diff ( arccot ,x)))) by A7, FDIFF_7: 46

        .= ((( arccot . x) / (( cos . x) ^2 )) + (( tan . x) * (( arccot `| Z) . x))) by A3, A6, FDIFF_1:def 7

        .= ((( arccot . x) / (( cos . x) ^2 )) + (( tan . x) * ( - (1 / (1 + (x ^2 )))))) by A2, A6, SIN_COS9: 82

        .= ((( arccot . x) / (( cos . x) ^2 )) - (( tan . x) / (1 + (x ^2 ))));

        hence thesis;

      end;

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

    end;

    theorem :: FDIFF_11:31

    Z c= ( dom ( cot (#) arctan )) & Z c= ].( - 1), 1.[ implies ( cot (#) arctan ) is_differentiable_on Z & for x st x in Z holds ((( cot (#) arctan ) `| Z) . x) = (( - (( arctan . x) / (( sin . x) ^2 ))) + (( cot . x) / (1 + (x ^2 ))))

    proof

      assume that

       A1: Z c= ( dom ( cot (#) arctan )) and

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

      

       A3: arctan is_differentiable_on Z by A2, SIN_COS9: 81;

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

      then

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

      for x st x in Z holds cot is_differentiable_in x

      proof

        let x;

        assume x in Z;

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

        hence thesis by FDIFF_7: 47;

      end;

      then

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

      for x st x in Z holds ((( cot (#) arctan ) `| Z) . x) = (( - (( arctan . x) / (( sin . x) ^2 ))) + (( cot . x) / (1 + (x ^2 ))))

      proof

        let x;

        assume

         A6: x in Z;

        then

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

        ((( cot (#) arctan ) `| Z) . x) = ((( arctan . x) * ( diff ( cot ,x))) + (( cot . x) * ( diff ( arctan ,x)))) by A1, A5, A3, A6, FDIFF_1: 21

        .= ((( arctan . x) * ( - (1 / (( sin . x) ^2 )))) + (( cot . x) * ( diff ( arctan ,x)))) by A7, FDIFF_7: 47

        .= (( - (( arctan . x) / (( sin . x) ^2 ))) + (( cot . x) * (( arctan `| Z) . x))) by A3, A6, FDIFF_1:def 7

        .= (( - (( arctan . x) / (( sin . x) ^2 ))) + (( cot . x) * (1 / (1 + (x ^2 ))))) by A2, A6, SIN_COS9: 81

        .= (( - (( arctan . x) / (( sin . x) ^2 ))) + (( cot . x) / (1 + (x ^2 ))));

        hence thesis;

      end;

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

    end;

    theorem :: FDIFF_11:32

    Z c= ( dom ( cot (#) arccot )) & Z c= ].( - 1), 1.[ implies ( cot (#) arccot ) is_differentiable_on Z & for x st x in Z holds ((( cot (#) arccot ) `| Z) . x) = (( - (( arccot . x) / (( sin . x) ^2 ))) - (( cot . x) / (1 + (x ^2 ))))

    proof

      assume that

       A1: Z c= ( dom ( cot (#) arccot )) and

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

      

       A3: arccot is_differentiable_on Z by A2, SIN_COS9: 82;

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

      then

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

      for x st x in Z holds cot is_differentiable_in x

      proof

        let x;

        assume x in Z;

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

        hence thesis by FDIFF_7: 47;

      end;

      then

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

      for x st x in Z holds ((( cot (#) arccot ) `| Z) . x) = (( - (( arccot . x) / (( sin . x) ^2 ))) - (( cot . x) / (1 + (x ^2 ))))

      proof

        let x;

        assume

         A6: x in Z;

        then

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

        ((( cot (#) arccot ) `| Z) . x) = ((( arccot . x) * ( diff ( cot ,x))) + (( cot . x) * ( diff ( arccot ,x)))) by A1, A5, A3, A6, FDIFF_1: 21

        .= ((( arccot . x) * ( - (1 / (( sin . x) ^2 )))) + (( cot . x) * ( diff ( arccot ,x)))) by A7, FDIFF_7: 47

        .= (( - (( arccot . x) / (( sin . x) ^2 ))) + (( cot . x) * (( arccot `| Z) . x))) by A3, A6, FDIFF_1:def 7

        .= (( - (( arccot . x) / (( sin . x) ^2 ))) + (( cot . x) * ( - (1 / (1 + (x ^2 )))))) by A2, A6, SIN_COS9: 82

        .= (( - (( arccot . x) / (( sin . x) ^2 ))) - (( cot . x) / (1 + (x ^2 ))));

        hence thesis;

      end;

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

    end;

    theorem :: FDIFF_11:33

    Z c= ( dom ( sec (#) arctan )) & Z c= ].( - 1), 1.[ implies ( sec (#) arctan ) is_differentiable_on Z & for x st x in Z holds ((( sec (#) arctan ) `| Z) . x) = (((( sin . x) * ( arctan . x)) / (( cos . x) ^2 )) + (1 / (( cos . x) * (1 + (x ^2 )))))

    proof

      assume that

       A1: Z c= ( dom ( sec (#) arctan )) and

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

      

       A3: arctan is_differentiable_on Z by A2, SIN_COS9: 81;

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

      then

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

      for x st x in Z holds sec is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then ( cos . x) <> 0 by A4, RFUNCT_1: 3;

        hence thesis by FDIFF_9: 1;

      end;

      then

       A5: sec is_differentiable_on Z by A4, FDIFF_1: 9;

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

      proof

        let x;

        assume

         A6: x in Z;

        then

         A7: ( cos . x) <> 0 by A4, RFUNCT_1: 3;

        ((( sec (#) arctan ) `| Z) . x) = ((( arctan . x) * ( diff ( sec ,x))) + (( sec . x) * ( diff ( arctan ,x)))) by A1, A5, A3, A6, FDIFF_1: 21

        .= ((( arctan . x) * (( sin . x) / (( cos . x) ^2 ))) + (( sec . x) * ( diff ( arctan ,x)))) by A7, FDIFF_9: 1

        .= (((( sin . x) * ( arctan . x)) / (( cos . x) ^2 )) + (( sec . x) * (( arctan `| Z) . x))) by A3, A6, FDIFF_1:def 7

        .= (((( sin . x) * ( arctan . x)) / (( cos . x) ^2 )) + (( sec . x) * (1 / (1 + (x ^2 ))))) by A2, A6, SIN_COS9: 81

        .= (((( sin . x) * ( arctan . x)) / (( cos . x) ^2 )) + ((1 / ( cos . x)) * (1 / (1 + (x ^2 ))))) by A4, A6, RFUNCT_1:def 2

        .= (((( sin . x) * ( arctan . x)) / (( cos . x) ^2 )) + (1 / (( cos . x) * (1 + (x ^2 ))))) by XCMPLX_1: 102;

        hence thesis;

      end;

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

    end;

    theorem :: FDIFF_11:34

    Z c= ( dom ( sec (#) arccot )) & Z c= ].( - 1), 1.[ implies ( sec (#) arccot ) is_differentiable_on Z & for x st x in Z holds ((( sec (#) arccot ) `| Z) . x) = (((( sin . x) * ( arccot . x)) / (( cos . x) ^2 )) - (1 / (( cos . x) * (1 + (x ^2 )))))

    proof

      assume that

       A1: Z c= ( dom ( sec (#) arccot )) and

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

      

       A3: arccot is_differentiable_on Z by A2, SIN_COS9: 82;

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

      then

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

      for x st x in Z holds sec is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then ( cos . x) <> 0 by A4, RFUNCT_1: 3;

        hence thesis by FDIFF_9: 1;

      end;

      then

       A5: sec is_differentiable_on Z by A4, FDIFF_1: 9;

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

      proof

        let x;

        assume

         A6: x in Z;

        then

         A7: ( cos . x) <> 0 by A4, RFUNCT_1: 3;

        ((( sec (#) arccot ) `| Z) . x) = ((( arccot . x) * ( diff ( sec ,x))) + (( sec . x) * ( diff ( arccot ,x)))) by A1, A5, A3, A6, FDIFF_1: 21

        .= ((( arccot . x) * (( sin . x) / (( cos . x) ^2 ))) + (( sec . x) * ( diff ( arccot ,x)))) by A7, FDIFF_9: 1

        .= (((( sin . x) * ( arccot . x)) / (( cos . x) ^2 )) + (( sec . x) * (( arccot `| Z) . x))) by A3, A6, FDIFF_1:def 7

        .= (((( sin . x) * ( arccot . x)) / (( cos . x) ^2 )) + (( sec . x) * ( - (1 / (1 + (x ^2 )))))) by A2, A6, SIN_COS9: 82

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

        .= (((( sin . x) * ( arccot . x)) / (( cos . x) ^2 )) - ((1 / ( cos . x)) * (1 / (1 + (x ^2 ))))) by A4, A6, RFUNCT_1:def 2

        .= (((( sin . x) * ( arccot . x)) / (( cos . x) ^2 )) - (1 / (( cos . x) * (1 + (x ^2 ))))) by XCMPLX_1: 102;

        hence thesis;

      end;

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

    end;

    theorem :: FDIFF_11:35

    Z c= ( dom ( cosec (#) arctan )) & Z c= ].( - 1), 1.[ implies ( cosec (#) arctan ) is_differentiable_on Z & for x st x in Z holds ((( cosec (#) arctan ) `| Z) . x) = (( - ((( cos . x) * ( arctan . x)) / (( sin . x) ^2 ))) + (1 / (( sin . x) * (1 + (x ^2 )))))

    proof

      assume that

       A1: Z c= ( dom ( cosec (#) arctan )) and

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

      

       A3: arctan is_differentiable_on Z by A2, SIN_COS9: 81;

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

      then

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

      for x st x in Z holds cosec is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then ( sin . x) <> 0 by A4, RFUNCT_1: 3;

        hence thesis by FDIFF_9: 2;

      end;

      then

       A5: cosec is_differentiable_on Z by A4, FDIFF_1: 9;

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

      proof

        let x;

        assume

         A6: x in Z;

        then

         A7: ( sin . x) <> 0 by A4, RFUNCT_1: 3;

        ((( cosec (#) arctan ) `| Z) . x) = ((( arctan . x) * ( diff ( cosec ,x))) + (( cosec . x) * ( diff ( arctan ,x)))) by A1, A5, A3, A6, FDIFF_1: 21

        .= ((( arctan . x) * ( - (( cos . x) / (( sin . x) ^2 )))) + (( cosec . x) * ( diff ( arctan ,x)))) by A7, FDIFF_9: 2

        .= (( - ((( cos . x) * ( arctan . x)) / (( sin . x) ^2 ))) + (( cosec . x) * (( arctan `| Z) . x))) by A3, A6, FDIFF_1:def 7

        .= (( - ((( cos . x) * ( arctan . x)) / (( sin . x) ^2 ))) + (( cosec . x) * (1 / (1 + (x ^2 ))))) by A2, A6, SIN_COS9: 81

        .= (( - ((( cos . x) * ( arctan . x)) / (( sin . x) ^2 ))) + ((1 / ( sin . x)) * (1 / (1 + (x ^2 ))))) by A4, A6, RFUNCT_1:def 2

        .= (( - ((( cos . x) * ( arctan . x)) / (( sin . x) ^2 ))) + (1 / (( sin . x) * (1 + (x ^2 ))))) by XCMPLX_1: 102;

        hence thesis;

      end;

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

    end;

    theorem :: FDIFF_11:36

    Z c= ( dom ( cosec (#) arccot )) & Z c= ].( - 1), 1.[ implies ( cosec (#) arccot ) is_differentiable_on Z & for x st x in Z holds ((( cosec (#) arccot ) `| Z) . x) = (( - ((( cos . x) * ( arccot . x)) / (( sin . x) ^2 ))) - (1 / (( sin . x) * (1 + (x ^2 )))))

    proof

      assume that

       A1: Z c= ( dom ( cosec (#) arccot )) and

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

      

       A3: arccot is_differentiable_on Z by A2, SIN_COS9: 82;

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

      then

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

      for x st x in Z holds cosec is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then ( sin . x) <> 0 by A4, RFUNCT_1: 3;

        hence thesis by FDIFF_9: 2;

      end;

      then

       A5: cosec is_differentiable_on Z by A4, FDIFF_1: 9;

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

      proof

        let x;

        assume

         A6: x in Z;

        then

         A7: ( sin . x) <> 0 by A4, RFUNCT_1: 3;

        ((( cosec (#) arccot ) `| Z) . x) = ((( arccot . x) * ( diff ( cosec ,x))) + (( cosec . x) * ( diff ( arccot ,x)))) by A1, A5, A3, A6, FDIFF_1: 21

        .= ((( arccot . x) * ( - (( cos . x) / (( sin . x) ^2 )))) + (( cosec . x) * ( diff ( arccot ,x)))) by A7, FDIFF_9: 2

        .= (( - ((( cos . x) * ( arccot . x)) / (( sin . x) ^2 ))) + (( cosec . x) * (( arccot `| Z) . x))) by A3, A6, FDIFF_1:def 7

        .= (( - ((( cos . x) * ( arccot . x)) / (( sin . x) ^2 ))) + (( cosec . x) * ( - (1 / (1 + (x ^2 )))))) by A2, A6, SIN_COS9: 82

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

        .= (( - ((( cos . x) * ( arccot . x)) / (( sin . x) ^2 ))) - ((1 / ( sin . x)) * (1 / (1 + (x ^2 ))))) by A4, A6, RFUNCT_1:def 2

        .= (( - ((( cos . x) * ( arccot . x)) / (( sin . x) ^2 ))) - (1 / (( sin . x) * (1 + (x ^2 ))))) by XCMPLX_1: 102;

        hence thesis;

      end;

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

    end;

    theorem :: FDIFF_11:37

    

     Th37: Z c= ].( - 1), 1.[ implies ( arctan + arccot ) is_differentiable_on Z & for x st x in Z holds ((( arctan + arccot ) `| Z) . x) = 0

    proof

      assume

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

      then

       A2: arctan is_differentiable_on Z by SIN_COS9: 81;

      

       A3: ].( - 1), 1.[ c= [.( - 1), 1.] by XXREAL_1: 25;

      then ].( - 1), 1.[ c= ( dom arccot ) by SIN_COS9: 24, XBOOLE_1: 1;

      then

       A4: Z c= ( dom arccot ) by A1, XBOOLE_1: 1;

      

       A5: arccot is_differentiable_on Z by A1, SIN_COS9: 82;

       ].( - 1), 1.[ c= ( dom arctan ) by A3, SIN_COS9: 23, XBOOLE_1: 1;

      then Z c= ( dom arctan ) by A1, XBOOLE_1: 1;

      then Z c= (( dom arctan ) /\ ( dom arccot )) by A4, XBOOLE_1: 19;

      then

       A6: Z c= ( dom ( arctan + arccot )) by VALUED_1:def 1;

      for x st x in Z holds ((( arctan + arccot ) `| Z) . x) = 0

      proof

        let x;

        assume

         A7: x in Z;

        

        then ((( arctan + arccot ) `| Z) . x) = (( diff ( arctan ,x)) + ( diff ( arccot ,x))) by A6, A2, A5, FDIFF_1: 18

        .= ((( arctan `| Z) . x) + ( diff ( arccot ,x))) by A2, A7, FDIFF_1:def 7

        .= ((1 / (1 + (x ^2 ))) + ( diff ( arccot ,x))) by A1, A7, SIN_COS9: 81

        .= ((1 / (1 + (x ^2 ))) + (( arccot `| Z) . x)) by A5, A7, FDIFF_1:def 7

        .= ((1 / (1 + (x ^2 ))) + ( - (1 / (1 + (x ^2 ))))) by A1, A7, SIN_COS9: 82

        .= 0 ;

        hence thesis;

      end;

      hence thesis by A6, A2, A5, FDIFF_1: 18;

    end;

    theorem :: FDIFF_11:38

    

     Th38: Z c= ].( - 1), 1.[ implies ( arctan - arccot ) is_differentiable_on Z & for x st x in Z holds ((( arctan - arccot ) `| Z) . x) = (2 / (1 + (x ^2 )))

    proof

      assume

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

      then

       A2: arctan is_differentiable_on Z by SIN_COS9: 81;

      

       A3: ].( - 1), 1.[ c= [.( - 1), 1.] by XXREAL_1: 25;

      then ].( - 1), 1.[ c= ( dom arccot ) by SIN_COS9: 24, XBOOLE_1: 1;

      then

       A4: Z c= ( dom arccot ) by A1, XBOOLE_1: 1;

      

       A5: arccot is_differentiable_on Z by A1, SIN_COS9: 82;

       ].( - 1), 1.[ c= ( dom arctan ) by A3, SIN_COS9: 23, XBOOLE_1: 1;

      then Z c= ( dom arctan ) by A1, XBOOLE_1: 1;

      then Z c= (( dom arctan ) /\ ( dom arccot )) by A4, XBOOLE_1: 19;

      then

       A6: Z c= ( dom ( arctan - arccot )) by VALUED_1: 12;

      for x st x in Z holds ((( arctan - arccot ) `| Z) . x) = (2 / (1 + (x ^2 )))

      proof

        let x;

        assume

         A7: x in Z;

        

        then ((( arctan - arccot ) `| Z) . x) = (( diff ( arctan ,x)) - ( diff ( arccot ,x))) by A6, A2, A5, FDIFF_1: 19

        .= ((( arctan `| Z) . x) - ( diff ( arccot ,x))) by A2, A7, FDIFF_1:def 7

        .= ((1 / (1 + (x ^2 ))) - ( diff ( arccot ,x))) by A1, A7, SIN_COS9: 81

        .= ((1 / (1 + (x ^2 ))) - (( arccot `| Z) . x)) by A5, A7, FDIFF_1:def 7

        .= ((1 / (1 + (x ^2 ))) - ( - (1 / (1 + (x ^2 ))))) by A1, A7, SIN_COS9: 82

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

        hence thesis;

      end;

      hence thesis by A6, A2, A5, FDIFF_1: 19;

    end;

    theorem :: FDIFF_11:39

    Z c= ].( - 1), 1.[ implies ( sin (#) ( arctan + arccot )) is_differentiable_on Z & for x st x in Z holds ((( sin (#) ( arctan + arccot )) `| Z) . x) = (( cos . x) * (( arctan . x) + ( arccot . x)))

    proof

      for x st x in Z holds sin is_differentiable_in x by SIN_COS: 64;

      then

       A1: sin is_differentiable_on Z by FDIFF_1: 9, SIN_COS: 24;

      assume

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

      then

       A3: ( arctan + arccot ) is_differentiable_on Z by Th37;

      

       A4: ].( - 1), 1.[ c= [.( - 1), 1.] by XXREAL_1: 25;

      then ].( - 1), 1.[ c= ( dom arccot ) by SIN_COS9: 24, XBOOLE_1: 1;

      then

       A5: Z c= ( dom arccot ) by A2, XBOOLE_1: 1;

       ].( - 1), 1.[ c= ( dom arctan ) by A4, SIN_COS9: 23, XBOOLE_1: 1;

      then Z c= ( dom arctan ) by A2, XBOOLE_1: 1;

      then Z c= (( dom arctan ) /\ ( dom arccot )) by A5, XBOOLE_1: 19;

      then

       A6: Z c= ( dom ( arctan + arccot )) by VALUED_1:def 1;

      then Z c= (( dom sin ) /\ ( dom ( arctan + arccot ))) by SIN_COS: 24, XBOOLE_1: 19;

      then

       A7: Z c= ( dom ( sin (#) ( arctan + arccot ))) by VALUED_1:def 4;

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

      proof

        let x;

        assume

         A8: x in Z;

        

        then ((( sin (#) ( arctan + arccot )) `| Z) . x) = (((( arctan + arccot ) . x) * ( diff ( sin ,x))) + (( sin . x) * ( diff (( arctan + arccot ),x)))) by A7, A1, A3, FDIFF_1: 21

        .= (((( arctan . x) + ( arccot . x)) * ( diff ( sin ,x))) + (( sin . x) * ( diff (( arctan + arccot ),x)))) by A6, A8, VALUED_1:def 1

        .= (((( arctan . x) + ( arccot . x)) * ( cos . x)) + (( sin . x) * ( diff (( arctan + arccot ),x)))) by SIN_COS: 64

        .= (((( arctan . x) + ( arccot . x)) * ( cos . x)) + (( sin . x) * ((( arctan + arccot ) `| Z) . x))) by A3, A8, FDIFF_1:def 7

        .= (((( arctan . x) + ( arccot . x)) * ( cos . x)) + (( sin . x) * 0 )) by A2, A8, Th37

        .= (( cos . x) * (( arctan . x) + ( arccot . x)));

        hence thesis;

      end;

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

    end;

    theorem :: FDIFF_11:40

    Z c= ].( - 1), 1.[ implies ( sin (#) ( arctan - arccot )) is_differentiable_on Z & for x st x in Z holds ((( sin (#) ( arctan - arccot )) `| Z) . x) = ((( cos . x) * (( arctan . x) - ( arccot . x))) + ((2 * ( sin . x)) / (1 + (x ^2 ))))

    proof

      for x st x in Z holds sin is_differentiable_in x by SIN_COS: 64;

      then

       A1: sin is_differentiable_on Z by FDIFF_1: 9, SIN_COS: 24;

      assume

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

      then

       A3: ( arctan - arccot ) is_differentiable_on Z by Th38;

      

       A4: ].( - 1), 1.[ c= [.( - 1), 1.] by XXREAL_1: 25;

      then ].( - 1), 1.[ c= ( dom arccot ) by SIN_COS9: 24, XBOOLE_1: 1;

      then

       A5: Z c= ( dom arccot ) by A2, XBOOLE_1: 1;

       ].( - 1), 1.[ c= ( dom arctan ) by A4, SIN_COS9: 23, XBOOLE_1: 1;

      then Z c= ( dom arctan ) by A2, XBOOLE_1: 1;

      then Z c= (( dom arctan ) /\ ( dom arccot )) by A5, XBOOLE_1: 19;

      then

       A6: Z c= ( dom ( arctan - arccot )) by VALUED_1: 12;

      then Z c= (( dom sin ) /\ ( dom ( arctan - arccot ))) by SIN_COS: 24, XBOOLE_1: 19;

      then

       A7: Z c= ( dom ( sin (#) ( arctan - arccot ))) by VALUED_1:def 4;

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

      proof

        let x;

        assume

         A8: x in Z;

        

        then ((( sin (#) ( arctan - arccot )) `| Z) . x) = (((( arctan - arccot ) . x) * ( diff ( sin ,x))) + (( sin . x) * ( diff (( arctan - arccot ),x)))) by A7, A1, A3, FDIFF_1: 21

        .= (((( arctan . x) - ( arccot . x)) * ( diff ( sin ,x))) + (( sin . x) * ( diff (( arctan - arccot ),x)))) by A6, A8, VALUED_1: 13

        .= (((( arctan . x) - ( arccot . x)) * ( cos . x)) + (( sin . x) * ( diff (( arctan - arccot ),x)))) by SIN_COS: 64

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

        .= (((( arctan . x) - ( arccot . x)) * ( cos . x)) + (( sin . x) * (2 / (1 + (x ^2 ))))) by A2, A8, Th38

        .= ((( cos . x) * (( arctan . x) - ( arccot . x))) + ((2 * ( sin . x)) / (1 + (x ^2 ))));

        hence thesis;

      end;

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

    end;

    theorem :: FDIFF_11:41

    Z c= ].( - 1), 1.[ implies ( cos (#) ( arctan + arccot )) is_differentiable_on Z & for x st x in Z holds ((( cos (#) ( arctan + arccot )) `| Z) . x) = ( - (( sin . x) * (( arctan . x) + ( arccot . x))))

    proof

      for x st x in Z holds cos is_differentiable_in x by SIN_COS: 63;

      then

       A1: cos is_differentiable_on Z by FDIFF_1: 9, SIN_COS: 24;

      assume

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

      then

       A3: ( arctan + arccot ) is_differentiable_on Z by Th37;

      

       A4: ].( - 1), 1.[ c= [.( - 1), 1.] by XXREAL_1: 25;

      then ].( - 1), 1.[ c= ( dom arccot ) by SIN_COS9: 24, XBOOLE_1: 1;

      then

       A5: Z c= ( dom arccot ) by A2, XBOOLE_1: 1;

       ].( - 1), 1.[ c= ( dom arctan ) by A4, SIN_COS9: 23, XBOOLE_1: 1;

      then Z c= ( dom arctan ) by A2, XBOOLE_1: 1;

      then Z c= (( dom arctan ) /\ ( dom arccot )) by A5, XBOOLE_1: 19;

      then

       A6: Z c= ( dom ( arctan + arccot )) by VALUED_1:def 1;

      then Z c= (( dom cos ) /\ ( dom ( arctan + arccot ))) by SIN_COS: 24, XBOOLE_1: 19;

      then

       A7: Z c= ( dom ( cos (#) ( arctan + arccot ))) by VALUED_1:def 4;

      for x st x in Z holds ((( cos (#) ( arctan + arccot )) `| Z) . x) = ( - (( sin . x) * (( arctan . x) + ( arccot . x))))

      proof

        let x;

        assume

         A8: x in Z;

        

        then ((( cos (#) ( arctan + arccot )) `| Z) . x) = (((( arctan + arccot ) . x) * ( diff ( cos ,x))) + (( cos . x) * ( diff (( arctan + arccot ),x)))) by A7, A1, A3, FDIFF_1: 21

        .= (((( arctan . x) + ( arccot . x)) * ( diff ( cos ,x))) + (( cos . x) * ( diff (( arctan + arccot ),x)))) by A6, A8, VALUED_1:def 1

        .= (((( arctan . x) + ( arccot . x)) * ( - ( sin . x))) + (( cos . x) * ( diff (( arctan + arccot ),x)))) by SIN_COS: 63

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

        .= (( - ((( arctan . x) + ( arccot . x)) * ( sin . x))) + (( cos . x) * 0 )) by A2, A8, Th37

        .= ( - (( sin . x) * (( arctan . x) + ( arccot . x))));

        hence thesis;

      end;

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

    end;

    theorem :: FDIFF_11:42

    Z c= ].( - 1), 1.[ implies ( cos (#) ( arctan - arccot )) is_differentiable_on Z & for x st x in Z holds ((( cos (#) ( arctan - arccot )) `| Z) . x) = (( - (( sin . x) * (( arctan . x) - ( arccot . x)))) + ((2 * ( cos . x)) / (1 + (x ^2 ))))

    proof

      for x st x in Z holds cos is_differentiable_in x by SIN_COS: 63;

      then

       A1: cos is_differentiable_on Z by FDIFF_1: 9, SIN_COS: 24;

      assume

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

      then

       A3: ( arctan - arccot ) is_differentiable_on Z by Th38;

      

       A4: ].( - 1), 1.[ c= [.( - 1), 1.] by XXREAL_1: 25;

      then ].( - 1), 1.[ c= ( dom arccot ) by SIN_COS9: 24, XBOOLE_1: 1;

      then

       A5: Z c= ( dom arccot ) by A2, XBOOLE_1: 1;

       ].( - 1), 1.[ c= ( dom arctan ) by A4, SIN_COS9: 23, XBOOLE_1: 1;

      then Z c= ( dom arctan ) by A2, XBOOLE_1: 1;

      then Z c= (( dom arctan ) /\ ( dom arccot )) by A5, XBOOLE_1: 19;

      then

       A6: Z c= ( dom ( arctan - arccot )) by VALUED_1: 12;

      then Z c= (( dom cos ) /\ ( dom ( arctan - arccot ))) by SIN_COS: 24, XBOOLE_1: 19;

      then

       A7: Z c= ( dom ( cos (#) ( arctan - arccot ))) by VALUED_1:def 4;

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

      proof

        let x;

        assume

         A8: x in Z;

        

        then ((( cos (#) ( arctan - arccot )) `| Z) . x) = (((( arctan - arccot ) . x) * ( diff ( cos ,x))) + (( cos . x) * ( diff (( arctan - arccot ),x)))) by A7, A1, A3, FDIFF_1: 21

        .= (((( arctan . x) - ( arccot . x)) * ( diff ( cos ,x))) + (( cos . x) * ( diff (( arctan - arccot ),x)))) by A6, A8, VALUED_1: 13

        .= (((( arctan . x) - ( arccot . x)) * ( - ( sin . x))) + (( cos . x) * ( diff (( arctan - arccot ),x)))) by SIN_COS: 63

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

        .= (( - ((( arctan . x) - ( arccot . x)) * ( sin . x))) + (( cos . x) * (2 / (1 + (x ^2 ))))) by A2, A8, Th38

        .= (( - (( sin . x) * (( arctan . x) - ( arccot . x)))) + ((2 * ( cos . x)) / (1 + (x ^2 ))));

        hence thesis;

      end;

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

    end;

    theorem :: FDIFF_11:43

    Z c= ( dom tan ) & Z c= ].( - 1), 1.[ implies ( tan (#) ( arctan + arccot )) is_differentiable_on Z & for x st x in Z holds ((( tan (#) ( arctan + arccot )) `| Z) . x) = ((( arctan . x) + ( arccot . x)) / (( cos . x) ^2 ))

    proof

      assume that

       A1: Z c= ( dom tan ) and

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

      

       A3: ( arctan + arccot ) is_differentiable_on Z by A2, Th37;

      for x st x in Z holds tan is_differentiable_in x

      proof

        let x;

        assume x in Z;

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

        hence thesis by FDIFF_7: 46;

      end;

      then

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

      

       A5: ].( - 1), 1.[ c= [.( - 1), 1.] by XXREAL_1: 25;

      then ].( - 1), 1.[ c= ( dom arccot ) by SIN_COS9: 24, XBOOLE_1: 1;

      then

       A6: Z c= ( dom arccot ) by A2, XBOOLE_1: 1;

       ].( - 1), 1.[ c= ( dom arctan ) by A5, SIN_COS9: 23, XBOOLE_1: 1;

      then Z c= ( dom arctan ) by A2, XBOOLE_1: 1;

      then Z c= (( dom arctan ) /\ ( dom arccot )) by A6, XBOOLE_1: 19;

      then

       A7: Z c= ( dom ( arctan + arccot )) by VALUED_1:def 1;

      then Z c= (( dom tan ) /\ ( dom ( arctan + arccot ))) by A1, XBOOLE_1: 19;

      then

       A8: Z c= ( dom ( tan (#) ( arctan + arccot ))) by VALUED_1:def 4;

      for x st x in Z holds ((( tan (#) ( arctan + arccot )) `| Z) . x) = ((( arctan . x) + ( arccot . x)) / (( cos . x) ^2 ))

      proof

        let x;

        assume

         A9: x in Z;

        then

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

        ((( tan (#) ( arctan + arccot )) `| Z) . x) = (((( arctan + arccot ) . x) * ( diff ( tan ,x))) + (( tan . x) * ( diff (( arctan + arccot ),x)))) by A8, A4, A3, A9, FDIFF_1: 21

        .= (((( arctan . x) + ( arccot . x)) * ( diff ( tan ,x))) + (( tan . x) * ( diff (( arctan + arccot ),x)))) by A7, A9, VALUED_1:def 1

        .= (((( arctan . x) + ( arccot . x)) * (1 / (( cos . x) ^2 ))) + (( tan . x) * ( diff (( arctan + arccot ),x)))) by A10, FDIFF_7: 46

        .= (((( arctan . x) + ( arccot . x)) / (( cos . x) ^2 )) + (( tan . x) * ((( arctan + arccot ) `| Z) . x))) by A3, A9, FDIFF_1:def 7

        .= (((( arctan . x) + ( arccot . x)) / (( cos . x) ^2 )) + (( tan . x) * 0 )) by A2, A9, Th37

        .= ((( arctan . x) + ( arccot . x)) / (( cos . x) ^2 ));

        hence thesis;

      end;

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

    end;

    theorem :: FDIFF_11:44

    Z c= ( dom tan ) & Z c= ].( - 1), 1.[ implies ( tan (#) ( arctan - arccot )) is_differentiable_on Z & for x st x in Z holds ((( tan (#) ( arctan - arccot )) `| Z) . x) = (((( arctan . x) - ( arccot . x)) / (( cos . x) ^2 )) + ((2 * ( tan . x)) / (1 + (x ^2 ))))

    proof

      assume that

       A1: Z c= ( dom tan ) and

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

      

       A3: ( arctan - arccot ) is_differentiable_on Z by A2, Th38;

      for x st x in Z holds tan is_differentiable_in x

      proof

        let x;

        assume x in Z;

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

        hence thesis by FDIFF_7: 46;

      end;

      then

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

      

       A5: ].( - 1), 1.[ c= [.( - 1), 1.] by XXREAL_1: 25;

      then ].( - 1), 1.[ c= ( dom arccot ) by SIN_COS9: 24, XBOOLE_1: 1;

      then

       A6: Z c= ( dom arccot ) by A2, XBOOLE_1: 1;

       ].( - 1), 1.[ c= ( dom arctan ) by A5, SIN_COS9: 23, XBOOLE_1: 1;

      then Z c= ( dom arctan ) by A2, XBOOLE_1: 1;

      then Z c= (( dom arctan ) /\ ( dom arccot )) by A6, XBOOLE_1: 19;

      then

       A7: Z c= ( dom ( arctan - arccot )) by VALUED_1: 12;

      then Z c= (( dom tan ) /\ ( dom ( arctan - arccot ))) by A1, XBOOLE_1: 19;

      then

       A8: Z c= ( dom ( tan (#) ( arctan - arccot ))) by VALUED_1:def 4;

      for x st x in Z holds ((( tan (#) ( arctan - arccot )) `| Z) . x) = (((( arctan . x) - ( arccot . x)) / (( cos . x) ^2 )) + ((2 * ( tan . x)) / (1 + (x ^2 ))))

      proof

        let x;

        assume

         A9: x in Z;

        then

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

        ((( tan (#) ( arctan - arccot )) `| Z) . x) = (((( arctan - arccot ) . x) * ( diff ( tan ,x))) + (( tan . x) * ( diff (( arctan - arccot ),x)))) by A8, A4, A3, A9, FDIFF_1: 21

        .= (((( arctan . x) - ( arccot . x)) * ( diff ( tan ,x))) + (( tan . x) * ( diff (( arctan - arccot ),x)))) by A7, A9, VALUED_1: 13

        .= (((( arctan . x) - ( arccot . x)) * (1 / (( cos . x) ^2 ))) + (( tan . x) * ( diff (( arctan - arccot ),x)))) by A10, FDIFF_7: 46

        .= (((( arctan . x) - ( arccot . x)) / (( cos . x) ^2 )) + (( tan . x) * ((( arctan - arccot ) `| Z) . x))) by A3, A9, FDIFF_1:def 7

        .= (((( arctan . x) - ( arccot . x)) / (( cos . x) ^2 )) + (( tan . x) * (2 / (1 + (x ^2 ))))) by A2, A9, Th38

        .= (((( arctan . x) - ( arccot . x)) / (( cos . x) ^2 )) + ((2 * ( tan . x)) / (1 + (x ^2 ))));

        hence thesis;

      end;

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

    end;

    theorem :: FDIFF_11:45

    Z c= ( dom cot ) & Z c= ].( - 1), 1.[ implies ( cot (#) ( arctan + arccot )) is_differentiable_on Z & for x st x in Z holds ((( cot (#) ( arctan + arccot )) `| Z) . x) = ( - ((( arctan . x) + ( arccot . x)) / (( sin . x) ^2 )))

    proof

      assume that

       A1: Z c= ( dom cot ) and

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

      

       A3: ( arctan + arccot ) is_differentiable_on Z by A2, Th37;

      for x st x in Z holds cot is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then ( sin . x) <> 0 by A1, FDIFF_8: 2;

        hence thesis by FDIFF_7: 47;

      end;

      then

       A4: cot is_differentiable_on Z by A1, FDIFF_1: 9;

      

       A5: ].( - 1), 1.[ c= [.( - 1), 1.] by XXREAL_1: 25;

      then ].( - 1), 1.[ c= ( dom arccot ) by SIN_COS9: 24, XBOOLE_1: 1;

      then

       A6: Z c= ( dom arccot ) by A2, XBOOLE_1: 1;

       ].( - 1), 1.[ c= ( dom arctan ) by A5, SIN_COS9: 23, XBOOLE_1: 1;

      then Z c= ( dom arctan ) by A2, XBOOLE_1: 1;

      then Z c= (( dom arctan ) /\ ( dom arccot )) by A6, XBOOLE_1: 19;

      then

       A7: Z c= ( dom ( arctan + arccot )) by VALUED_1:def 1;

      then Z c= (( dom cot ) /\ ( dom ( arctan + arccot ))) by A1, XBOOLE_1: 19;

      then

       A8: Z c= ( dom ( cot (#) ( arctan + arccot ))) by VALUED_1:def 4;

      for x st x in Z holds ((( cot (#) ( arctan + arccot )) `| Z) . x) = ( - ((( arctan . x) + ( arccot . x)) / (( sin . x) ^2 )))

      proof

        let x;

        assume

         A9: x in Z;

        then

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

        ((( cot (#) ( arctan + arccot )) `| Z) . x) = (((( arctan + arccot ) . x) * ( diff ( cot ,x))) + (( cot . x) * ( diff (( arctan + arccot ),x)))) by A8, A4, A3, A9, FDIFF_1: 21

        .= (((( arctan . x) + ( arccot . x)) * ( diff ( cot ,x))) + (( cot . x) * ( diff (( arctan + arccot ),x)))) by A7, A9, VALUED_1:def 1

        .= (((( arctan . x) + ( arccot . x)) * ( - (1 / (( sin . x) ^2 )))) + (( cot . x) * ( diff (( arctan + arccot ),x)))) by A10, FDIFF_7: 47

        .= (( - ((( arctan . x) + ( arccot . x)) / (( sin . x) ^2 ))) + (( cot . x) * ((( arctan + arccot ) `| Z) . x))) by A3, A9, FDIFF_1:def 7

        .= (( - ((( arctan . x) + ( arccot . x)) / (( sin . x) ^2 ))) + (( cot . x) * 0 )) by A2, A9, Th37

        .= ( - ((( arctan . x) + ( arccot . x)) / (( sin . x) ^2 )));

        hence thesis;

      end;

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

    end;

    theorem :: FDIFF_11:46

    Z c= ( dom cot ) & Z c= ].( - 1), 1.[ implies ( cot (#) ( arctan - arccot )) is_differentiable_on Z & for x st x in Z holds ((( cot (#) ( arctan - arccot )) `| Z) . x) = (( - ((( arctan . x) - ( arccot . x)) / (( sin . x) ^2 ))) + ((2 * ( cot . x)) / (1 + (x ^2 ))))

    proof

      assume that

       A1: Z c= ( dom cot ) and

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

      

       A3: ( arctan - arccot ) is_differentiable_on Z by A2, Th38;

      for x st x in Z holds cot is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then ( sin . x) <> 0 by A1, FDIFF_8: 2;

        hence thesis by FDIFF_7: 47;

      end;

      then

       A4: cot is_differentiable_on Z by A1, FDIFF_1: 9;

      

       A5: ].( - 1), 1.[ c= [.( - 1), 1.] by XXREAL_1: 25;

      then ].( - 1), 1.[ c= ( dom arccot ) by SIN_COS9: 24, XBOOLE_1: 1;

      then

       A6: Z c= ( dom arccot ) by A2, XBOOLE_1: 1;

       ].( - 1), 1.[ c= ( dom arctan ) by A5, SIN_COS9: 23, XBOOLE_1: 1;

      then Z c= ( dom arctan ) by A2, XBOOLE_1: 1;

      then Z c= (( dom arctan ) /\ ( dom arccot )) by A6, XBOOLE_1: 19;

      then

       A7: Z c= ( dom ( arctan - arccot )) by VALUED_1: 12;

      then Z c= (( dom cot ) /\ ( dom ( arctan - arccot ))) by A1, XBOOLE_1: 19;

      then

       A8: Z c= ( dom ( cot (#) ( arctan - arccot ))) by VALUED_1:def 4;

      for x st x in Z holds ((( cot (#) ( arctan - arccot )) `| Z) . x) = (( - ((( arctan . x) - ( arccot . x)) / (( sin . x) ^2 ))) + ((2 * ( cot . x)) / (1 + (x ^2 ))))

      proof

        let x;

        assume

         A9: x in Z;

        then

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

        ((( cot (#) ( arctan - arccot )) `| Z) . x) = (((( arctan - arccot ) . x) * ( diff ( cot ,x))) + (( cot . x) * ( diff (( arctan - arccot ),x)))) by A8, A4, A3, A9, FDIFF_1: 21

        .= (((( arctan . x) - ( arccot . x)) * ( diff ( cot ,x))) + (( cot . x) * ( diff (( arctan - arccot ),x)))) by A7, A9, VALUED_1: 13

        .= (((( arctan . x) - ( arccot . x)) * ( - (1 / (( sin . x) ^2 )))) + (( cot . x) * ( diff (( arctan - arccot ),x)))) by A10, FDIFF_7: 47

        .= (( - ((( arctan . x) - ( arccot . x)) / (( sin . x) ^2 ))) + (( cot . x) * ((( arctan - arccot ) `| Z) . x))) by A3, A9, FDIFF_1:def 7

        .= (( - ((( arctan . x) - ( arccot . x)) / (( sin . x) ^2 ))) + (( cot . x) * (2 / (1 + (x ^2 ))))) by A2, A9, Th38

        .= (( - ((( arctan . x) - ( arccot . x)) / (( sin . x) ^2 ))) + ((2 * ( cot . x)) / (1 + (x ^2 ))));

        hence thesis;

      end;

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

    end;

    theorem :: FDIFF_11:47

    Z c= ( dom sec ) & Z c= ].( - 1), 1.[ implies ( sec (#) ( arctan + arccot )) is_differentiable_on Z & for x st x in Z holds ((( sec (#) ( arctan + arccot )) `| Z) . x) = (((( arctan . x) + ( arccot . x)) * ( sin . x)) / (( cos . x) ^2 ))

    proof

      assume that

       A1: Z c= ( dom sec ) and

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

      

       A3: ( arctan + arccot ) is_differentiable_on Z by A2, Th37;

      for x st x in Z holds sec is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then ( cos . x) <> 0 by A1, RFUNCT_1: 3;

        hence thesis by FDIFF_9: 1;

      end;

      then

       A4: sec is_differentiable_on Z by A1, FDIFF_1: 9;

      

       A5: ].( - 1), 1.[ c= [.( - 1), 1.] by XXREAL_1: 25;

      then ].( - 1), 1.[ c= ( dom arccot ) by SIN_COS9: 24, XBOOLE_1: 1;

      then

       A6: Z c= ( dom arccot ) by A2, XBOOLE_1: 1;

       ].( - 1), 1.[ c= ( dom arctan ) by A5, SIN_COS9: 23, XBOOLE_1: 1;

      then Z c= ( dom arctan ) by A2, XBOOLE_1: 1;

      then Z c= (( dom arctan ) /\ ( dom arccot )) by A6, XBOOLE_1: 19;

      then

       A7: Z c= ( dom ( arctan + arccot )) by VALUED_1:def 1;

      then Z c= (( dom sec ) /\ ( dom ( arctan + arccot ))) by A1, XBOOLE_1: 19;

      then

       A8: Z c= ( dom ( sec (#) ( arctan + arccot ))) by VALUED_1:def 4;

      for x st x in Z holds ((( sec (#) ( arctan + arccot )) `| Z) . x) = (((( arctan . x) + ( arccot . x)) * ( sin . x)) / (( cos . x) ^2 ))

      proof

        let x;

        assume

         A9: x in Z;

        then

         A10: ( cos . x) <> 0 by A1, RFUNCT_1: 3;

        ((( sec (#) ( arctan + arccot )) `| Z) . x) = (((( arctan + arccot ) . x) * ( diff ( sec ,x))) + (( sec . x) * ( diff (( arctan + arccot ),x)))) by A8, A4, A3, A9, FDIFF_1: 21

        .= (((( arctan . x) + ( arccot . x)) * ( diff ( sec ,x))) + (( sec . x) * ( diff (( arctan + arccot ),x)))) by A7, A9, VALUED_1:def 1

        .= (((( arctan . x) + ( arccot . x)) * (( sin . x) / (( cos . x) ^2 ))) + (( sec . x) * ( diff (( arctan + arccot ),x)))) by A10, FDIFF_9: 1

        .= ((((( arctan . x) + ( arccot . x)) * ( sin . x)) / (( cos . x) ^2 )) + (( sec . x) * ((( arctan + arccot ) `| Z) . x))) by A3, A9, FDIFF_1:def 7

        .= ((((( arctan . x) + ( arccot . x)) * ( sin . x)) / (( cos . x) ^2 )) + (( sec . x) * 0 )) by A2, A9, Th37

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

        hence thesis;

      end;

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

    end;

    theorem :: FDIFF_11:48

    Z c= ( dom sec ) & Z c= ].( - 1), 1.[ implies ( sec (#) ( arctan - arccot )) is_differentiable_on Z & for x st x in Z holds ((( sec (#) ( arctan - arccot )) `| Z) . x) = ((((( arctan . x) - ( arccot . x)) * ( sin . x)) / (( cos . x) ^2 )) + ((2 * ( sec . x)) / (1 + (x ^2 ))))

    proof

      assume that

       A1: Z c= ( dom sec ) and

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

      

       A3: ( arctan - arccot ) is_differentiable_on Z by A2, Th38;

      for x st x in Z holds sec is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then ( cos . x) <> 0 by A1, RFUNCT_1: 3;

        hence thesis by FDIFF_9: 1;

      end;

      then

       A4: sec is_differentiable_on Z by A1, FDIFF_1: 9;

      

       A5: ].( - 1), 1.[ c= [.( - 1), 1.] by XXREAL_1: 25;

      then ].( - 1), 1.[ c= ( dom arccot ) by SIN_COS9: 24, XBOOLE_1: 1;

      then

       A6: Z c= ( dom arccot ) by A2, XBOOLE_1: 1;

       ].( - 1), 1.[ c= ( dom arctan ) by A5, SIN_COS9: 23, XBOOLE_1: 1;

      then Z c= ( dom arctan ) by A2, XBOOLE_1: 1;

      then Z c= (( dom arctan ) /\ ( dom arccot )) by A6, XBOOLE_1: 19;

      then

       A7: Z c= ( dom ( arctan - arccot )) by VALUED_1: 12;

      then Z c= (( dom sec ) /\ ( dom ( arctan - arccot ))) by A1, XBOOLE_1: 19;

      then

       A8: Z c= ( dom ( sec (#) ( arctan - arccot ))) by VALUED_1:def 4;

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

      proof

        let x;

        assume

         A9: x in Z;

        then

         A10: ( cos . x) <> 0 by A1, RFUNCT_1: 3;

        ((( sec (#) ( arctan - arccot )) `| Z) . x) = (((( arctan - arccot ) . x) * ( diff ( sec ,x))) + (( sec . x) * ( diff (( arctan - arccot ),x)))) by A8, A4, A3, A9, FDIFF_1: 21

        .= (((( arctan . x) - ( arccot . x)) * ( diff ( sec ,x))) + (( sec . x) * ( diff (( arctan - arccot ),x)))) by A7, A9, VALUED_1: 13

        .= (((( arctan . x) - ( arccot . x)) * (( sin . x) / (( cos . x) ^2 ))) + (( sec . x) * ( diff (( arctan - arccot ),x)))) by A10, FDIFF_9: 1

        .= ((((( arctan . x) - ( arccot . x)) * ( sin . x)) / (( cos . x) ^2 )) + (( sec . x) * ((( arctan - arccot ) `| Z) . x))) by A3, A9, FDIFF_1:def 7

        .= ((((( arctan . x) - ( arccot . x)) * ( sin . x)) / (( cos . x) ^2 )) + (( sec . x) * (2 / (1 + (x ^2 ))))) by A2, A9, Th38

        .= ((((( arctan . x) - ( arccot . x)) * ( sin . x)) / (( cos . x) ^2 )) + ((2 * ( sec . x)) / (1 + (x ^2 ))));

        hence thesis;

      end;

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

    end;

    theorem :: FDIFF_11:49

    Z c= ( dom cosec ) & Z c= ].( - 1), 1.[ implies ( cosec (#) ( arctan + arccot )) is_differentiable_on Z & for x st x in Z holds ((( cosec (#) ( arctan + arccot )) `| Z) . x) = ( - (((( arctan . x) + ( arccot . x)) * ( cos . x)) / (( sin . x) ^2 )))

    proof

      assume that

       A1: Z c= ( dom cosec ) and

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

      

       A3: ( arctan + arccot ) is_differentiable_on Z by A2, Th37;

      for x st x in Z holds cosec is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then ( sin . x) <> 0 by A1, RFUNCT_1: 3;

        hence thesis by FDIFF_9: 2;

      end;

      then

       A4: cosec is_differentiable_on Z by A1, FDIFF_1: 9;

      

       A5: ].( - 1), 1.[ c= [.( - 1), 1.] by XXREAL_1: 25;

      then ].( - 1), 1.[ c= ( dom arccot ) by SIN_COS9: 24, XBOOLE_1: 1;

      then

       A6: Z c= ( dom arccot ) by A2, XBOOLE_1: 1;

       ].( - 1), 1.[ c= ( dom arctan ) by A5, SIN_COS9: 23, XBOOLE_1: 1;

      then Z c= ( dom arctan ) by A2, XBOOLE_1: 1;

      then Z c= (( dom arctan ) /\ ( dom arccot )) by A6, XBOOLE_1: 19;

      then

       A7: Z c= ( dom ( arctan + arccot )) by VALUED_1:def 1;

      then Z c= (( dom cosec ) /\ ( dom ( arctan + arccot ))) by A1, XBOOLE_1: 19;

      then

       A8: Z c= ( dom ( cosec (#) ( arctan + arccot ))) by VALUED_1:def 4;

      for x st x in Z holds ((( cosec (#) ( arctan + arccot )) `| Z) . x) = ( - (((( arctan . x) + ( arccot . x)) * ( cos . x)) / (( sin . x) ^2 )))

      proof

        let x;

        assume

         A9: x in Z;

        then

         A10: ( sin . x) <> 0 by A1, RFUNCT_1: 3;

        ((( cosec (#) ( arctan + arccot )) `| Z) . x) = (((( arctan + arccot ) . x) * ( diff ( cosec ,x))) + (( cosec . x) * ( diff (( arctan + arccot ),x)))) by A8, A4, A3, A9, FDIFF_1: 21

        .= (((( arctan . x) + ( arccot . x)) * ( diff ( cosec ,x))) + (( cosec . x) * ( diff (( arctan + arccot ),x)))) by A7, A9, VALUED_1:def 1

        .= (((( arctan . x) + ( arccot . x)) * ( - (( cos . x) / (( sin . x) ^2 )))) + (( cosec . x) * ( diff (( arctan + arccot ),x)))) by A10, FDIFF_9: 2

        .= (( - (((( arctan . x) + ( arccot . x)) * ( cos . x)) / (( sin . x) ^2 ))) + (( cosec . x) * ((( arctan + arccot ) `| Z) . x))) by A3, A9, FDIFF_1:def 7

        .= (( - (((( arctan . x) + ( arccot . x)) * ( cos . x)) / (( sin . x) ^2 ))) + (( cosec . x) * 0 )) by A2, A9, Th37

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

        hence thesis;

      end;

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

    end;

    theorem :: FDIFF_11:50

    Z c= ( dom cosec ) & Z c= ].( - 1), 1.[ implies ( cosec (#) ( arctan - arccot )) is_differentiable_on Z & for x st x in Z holds ((( cosec (#) ( arctan - arccot )) `| Z) . x) = (( - (((( arctan . x) - ( arccot . x)) * ( cos . x)) / (( sin . x) ^2 ))) + ((2 * ( cosec . x)) / (1 + (x ^2 ))))

    proof

      assume that

       A1: Z c= ( dom cosec ) and

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

      

       A3: ( arctan - arccot ) is_differentiable_on Z by A2, Th38;

      for x st x in Z holds cosec is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then ( sin . x) <> 0 by A1, RFUNCT_1: 3;

        hence thesis by FDIFF_9: 2;

      end;

      then

       A4: cosec is_differentiable_on Z by A1, FDIFF_1: 9;

      

       A5: ].( - 1), 1.[ c= [.( - 1), 1.] by XXREAL_1: 25;

      then ].( - 1), 1.[ c= ( dom arccot ) by SIN_COS9: 24, XBOOLE_1: 1;

      then

       A6: Z c= ( dom arccot ) by A2, XBOOLE_1: 1;

       ].( - 1), 1.[ c= ( dom arctan ) by A5, SIN_COS9: 23, XBOOLE_1: 1;

      then Z c= ( dom arctan ) by A2, XBOOLE_1: 1;

      then Z c= (( dom arctan ) /\ ( dom arccot )) by A6, XBOOLE_1: 19;

      then

       A7: Z c= ( dom ( arctan - arccot )) by VALUED_1: 12;

      then Z c= (( dom cosec ) /\ ( dom ( arctan - arccot ))) by A1, XBOOLE_1: 19;

      then

       A8: Z c= ( dom ( cosec (#) ( arctan - arccot ))) by VALUED_1:def 4;

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

      proof

        let x;

        assume

         A9: x in Z;

        then

         A10: ( sin . x) <> 0 by A1, RFUNCT_1: 3;

        ((( cosec (#) ( arctan - arccot )) `| Z) . x) = (((( arctan - arccot ) . x) * ( diff ( cosec ,x))) + (( cosec . x) * ( diff (( arctan - arccot ),x)))) by A8, A4, A3, A9, FDIFF_1: 21

        .= (((( arctan . x) - ( arccot . x)) * ( diff ( cosec ,x))) + (( cosec . x) * ( diff (( arctan - arccot ),x)))) by A7, A9, VALUED_1: 13

        .= (((( arctan . x) - ( arccot . x)) * ( - (( cos . x) / (( sin . x) ^2 )))) + (( cosec . x) * ( diff (( arctan - arccot ),x)))) by A10, FDIFF_9: 2

        .= (( - (((( arctan . x) - ( arccot . x)) * ( cos . x)) / (( sin . x) ^2 ))) + (( cosec . x) * ((( arctan - arccot ) `| Z) . x))) by A3, A9, FDIFF_1:def 7

        .= (( - (((( arctan . x) - ( arccot . x)) * ( cos . x)) / (( sin . x) ^2 ))) + (( cosec . x) * (2 / (1 + (x ^2 ))))) by A2, A9, Th38

        .= (( - (((( arctan . x) - ( arccot . x)) * ( cos . x)) / (( sin . x) ^2 ))) + ((2 * ( cosec . x)) / (1 + (x ^2 ))));

        hence thesis;

      end;

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

    end;

    theorem :: FDIFF_11:51

    Z c= ].( - 1), 1.[ implies ( exp_R (#) ( arctan + arccot )) is_differentiable_on Z & for x st x in Z holds ((( exp_R (#) ( arctan + arccot )) `| Z) . x) = (( exp_R . x) * (( arctan . x) + ( arccot . x)))

    proof

      assume

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

      then

       A2: ( arctan + arccot ) is_differentiable_on Z by Th37;

      

       A3: ].( - 1), 1.[ c= [.( - 1), 1.] by XXREAL_1: 25;

      then ].( - 1), 1.[ c= ( dom arccot ) by SIN_COS9: 24, XBOOLE_1: 1;

      then

       A4: Z c= ( dom arccot ) by A1, XBOOLE_1: 1;

       ].( - 1), 1.[ c= ( dom arctan ) by A3, SIN_COS9: 23, XBOOLE_1: 1;

      then Z c= ( dom arctan ) by A1, XBOOLE_1: 1;

      then Z c= (( dom arctan ) /\ ( dom arccot )) by A4, XBOOLE_1: 19;

      then

       A5: Z c= ( dom ( arctan + arccot )) by VALUED_1:def 1;

      then Z c= (( dom exp_R ) /\ ( dom ( arctan + arccot ))) by TAYLOR_1: 16, XBOOLE_1: 19;

      then

       A6: Z c= ( dom ( exp_R (#) ( arctan + arccot ))) by VALUED_1:def 4;

      

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

      for x st x in Z holds ((( exp_R (#) ( arctan + arccot )) `| Z) . x) = (( exp_R . x) * (( arctan . x) + ( arccot . x)))

      proof

        let x;

        assume

         A8: x in Z;

        

        then ((( exp_R (#) ( arctan + arccot )) `| Z) . x) = (((( arctan + arccot ) . x) * ( diff ( exp_R ,x))) + (( exp_R . x) * ( diff (( arctan + arccot ),x)))) by A6, A7, A2, FDIFF_1: 21

        .= (((( arctan . x) + ( arccot . x)) * ( diff ( exp_R ,x))) + (( exp_R . x) * ( diff (( arctan + arccot ),x)))) by A5, A8, VALUED_1:def 1

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

        .= (((( arctan . x) + ( arccot . x)) * ( exp_R . x)) + (( exp_R . x) * ((( arctan + arccot ) `| Z) . x))) by A2, A8, FDIFF_1:def 7

        .= (((( arctan . x) + ( arccot . x)) * ( exp_R . x)) + (( exp_R . x) * 0 )) by A1, A8, Th37

        .= (( exp_R . x) * (( arctan . x) + ( arccot . x)));

        hence thesis;

      end;

      hence thesis by A6, A7, A2, FDIFF_1: 21;

    end;

    theorem :: FDIFF_11:52

    Z c= ].( - 1), 1.[ implies ( exp_R (#) ( arctan - arccot )) is_differentiable_on Z & for x st x in Z holds ((( exp_R (#) ( arctan - arccot )) `| Z) . x) = ((( exp_R . x) * (( arctan . x) - ( arccot . x))) + ((2 * ( exp_R . x)) / (1 + (x ^2 ))))

    proof

      assume

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

      then

       A2: ( arctan - arccot ) is_differentiable_on Z by Th38;

      

       A3: ].( - 1), 1.[ c= [.( - 1), 1.] by XXREAL_1: 25;

      then ].( - 1), 1.[ c= ( dom arccot ) by SIN_COS9: 24, XBOOLE_1: 1;

      then

       A4: Z c= ( dom arccot ) by A1, XBOOLE_1: 1;

       ].( - 1), 1.[ c= ( dom arctan ) by A3, SIN_COS9: 23, XBOOLE_1: 1;

      then Z c= ( dom arctan ) by A1, XBOOLE_1: 1;

      then Z c= (( dom arctan ) /\ ( dom arccot )) by A4, XBOOLE_1: 19;

      then

       A5: Z c= ( dom ( arctan - arccot )) by VALUED_1: 12;

      then Z c= (( dom exp_R ) /\ ( dom ( arctan - arccot ))) by TAYLOR_1: 16, XBOOLE_1: 19;

      then

       A6: Z c= ( dom ( exp_R (#) ( arctan - arccot ))) by VALUED_1:def 4;

      

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

      for x st x in Z holds ((( exp_R (#) ( arctan - arccot )) `| Z) . x) = ((( exp_R . x) * (( arctan . x) - ( arccot . x))) + ((2 * ( exp_R . x)) / (1 + (x ^2 ))))

      proof

        let x;

        assume

         A8: x in Z;

        

        then ((( exp_R (#) ( arctan - arccot )) `| Z) . x) = (((( arctan - arccot ) . x) * ( diff ( exp_R ,x))) + (( exp_R . x) * ( diff (( arctan - arccot ),x)))) by A6, A7, A2, FDIFF_1: 21

        .= (((( arctan . x) - ( arccot . x)) * ( diff ( exp_R ,x))) + (( exp_R . x) * ( diff (( arctan - arccot ),x)))) by A5, A8, VALUED_1: 13

        .= (((( arctan . x) - ( arccot . x)) * ( exp_R . x)) + (( exp_R . x) * ( diff (( arctan - arccot ),x)))) by TAYLOR_1: 16

        .= (((( arctan . x) - ( arccot . x)) * ( exp_R . x)) + (( exp_R . x) * ((( arctan - arccot ) `| Z) . x))) by A2, A8, FDIFF_1:def 7

        .= (((( arctan . x) - ( arccot . x)) * ( exp_R . x)) + (( exp_R . x) * (2 / (1 + (x ^2 ))))) by A1, A8, Th38

        .= ((( exp_R . x) * (( arctan . x) - ( arccot . x))) + ((2 * ( exp_R . x)) / (1 + (x ^2 ))));

        hence thesis;

      end;

      hence thesis by A6, A7, A2, FDIFF_1: 21;

    end;

    theorem :: FDIFF_11:53

    Z c= ].( - 1), 1.[ implies (( arctan + arccot ) / exp_R ) is_differentiable_on Z & for x st x in Z holds (((( arctan + arccot ) / exp_R ) `| Z) . x) = ( - ((( arctan . x) + ( arccot . x)) / ( exp_R . x)))

    proof

      assume

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

      then

       A2: ( arctan + arccot ) is_differentiable_on Z by Th37;

      

       A3: ].( - 1), 1.[ c= [.( - 1), 1.] by XXREAL_1: 25;

      then ].( - 1), 1.[ c= ( dom arccot ) by SIN_COS9: 24, XBOOLE_1: 1;

      then

       A4: Z c= ( dom arccot ) by A1, XBOOLE_1: 1;

       ].( - 1), 1.[ c= ( dom arctan ) by A3, SIN_COS9: 23, XBOOLE_1: 1;

      then Z c= ( dom arctan ) by A1, XBOOLE_1: 1;

      then Z c= (( dom arctan ) /\ ( dom arccot )) by A4, XBOOLE_1: 19;

      then

       A5: Z c= ( dom ( arctan + arccot )) by VALUED_1:def 1;

      

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

       A7: (( arctan + arccot ) / exp_R ) is_differentiable_on Z by A2, FDIFF_2: 21;

      for x st x in Z holds (((( arctan + arccot ) / exp_R ) `| Z) . x) = ( - ((( arctan . x) + ( arccot . x)) / ( exp_R . x)))

      proof

        let x;

        

         A8: exp_R is_differentiable_in x by SIN_COS: 65;

        

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

        assume

         A10: x in Z;

        then

         A11: ( arctan + arccot ) is_differentiable_in x by A2, FDIFF_1: 9;

        (((( arctan + arccot ) / exp_R ) `| Z) . x) = ( diff ((( arctan + arccot ) / exp_R ),x)) by A7, A10, FDIFF_1:def 7

        .= (((( diff (( arctan + arccot ),x)) * ( exp_R . x)) - (( diff ( exp_R ,x)) * (( arctan + arccot ) . x))) / (( exp_R . x) ^2 )) by A11, A8, A9, FDIFF_2: 14

        .= (((((( arctan + arccot ) `| Z) . x) * ( exp_R . x)) - (( diff ( exp_R ,x)) * (( arctan + arccot ) . x))) / (( exp_R . x) ^2 )) by A2, A10, FDIFF_1:def 7

        .= ((( 0 * ( exp_R . x)) - (( diff ( exp_R ,x)) * (( arctan + arccot ) . x))) / (( exp_R . x) ^2 )) by A1, A10, Th37

        .= ( - ((( diff ( exp_R ,x)) * (( arctan + arccot ) . x)) / (( exp_R . x) ^2 )))

        .= ( - ((( exp_R . x) * (( arctan + arccot ) . x)) / (( exp_R . x) ^2 ))) by SIN_COS: 65

        .= ( - (((( arctan . x) + ( arccot . x)) * ( exp_R . x)) / (( exp_R . x) * ( exp_R . x)))) by A5, A10, VALUED_1:def 1

        .= ( - ((( arctan . x) + ( arccot . x)) * (( exp_R . x) / (( exp_R . x) * ( exp_R . x)))))

        .= ( - ((( arctan . x) + ( arccot . x)) * ((( exp_R . x) / ( exp_R . x)) / ( exp_R . x)))) by XCMPLX_1: 78

        .= ( - ((( arctan . x) + ( arccot . x)) * (1 / ( exp_R . x)))) by A9, XCMPLX_1: 60

        .= ( - ((( arctan . x) + ( arccot . x)) / ( exp_R . x)));

        hence thesis;

      end;

      hence thesis by A2, A6, FDIFF_2: 21;

    end;

    theorem :: FDIFF_11:54

    Z c= ].( - 1), 1.[ implies (( arctan - arccot ) / exp_R ) is_differentiable_on Z & for x st x in Z holds (((( arctan - arccot ) / exp_R ) `| Z) . x) = ((((2 / (1 + (x ^2 ))) - ( arctan . x)) + ( arccot . x)) / ( exp_R . x))

    proof

      assume

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

      then

       A2: ( arctan - arccot ) is_differentiable_on Z by Th38;

      

       A3: ].( - 1), 1.[ c= [.( - 1), 1.] by XXREAL_1: 25;

      then ].( - 1), 1.[ c= ( dom arccot ) by SIN_COS9: 24, XBOOLE_1: 1;

      then

       A4: Z c= ( dom arccot ) by A1, XBOOLE_1: 1;

       ].( - 1), 1.[ c= ( dom arctan ) by A3, SIN_COS9: 23, XBOOLE_1: 1;

      then Z c= ( dom arctan ) by A1, XBOOLE_1: 1;

      then Z c= (( dom arctan ) /\ ( dom arccot )) by A4, XBOOLE_1: 19;

      then

       A5: Z c= ( dom ( arctan - arccot )) by VALUED_1: 12;

      

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

       A7: (( arctan - arccot ) / exp_R ) is_differentiable_on Z by A2, FDIFF_2: 21;

      for x st x in Z holds (((( arctan - arccot ) / exp_R ) `| Z) . x) = ((((2 / (1 + (x ^2 ))) - ( arctan . x)) + ( arccot . x)) / ( exp_R . x))

      proof

        let x;

        

         A8: exp_R is_differentiable_in x by SIN_COS: 65;

        

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

        assume

         A10: x in Z;

        then

         A11: ( arctan - arccot ) is_differentiable_in x by A2, FDIFF_1: 9;

        (((( arctan - arccot ) / exp_R ) `| Z) . x) = ( diff ((( arctan - arccot ) / exp_R ),x)) by A7, A10, FDIFF_1:def 7

        .= (((( diff (( arctan - arccot ),x)) * ( exp_R . x)) - (( diff ( exp_R ,x)) * (( arctan - arccot ) . x))) / (( exp_R . x) ^2 )) by A11, A8, A9, FDIFF_2: 14

        .= (((((( arctan - arccot ) `| Z) . x) * ( exp_R . x)) - (( diff ( exp_R ,x)) * (( arctan - arccot ) . x))) / (( exp_R . x) ^2 )) by A2, A10, FDIFF_1:def 7

        .= ((((2 / (1 + (x ^2 ))) * ( exp_R . x)) - (( diff ( exp_R ,x)) * (( arctan - arccot ) . x))) / (( exp_R . x) ^2 )) by A1, A10, Th38

        .= ((((2 / (1 + (x ^2 ))) * ( exp_R . x)) - (( exp_R . x) * (( arctan - arccot ) . x))) / (( exp_R . x) ^2 )) by SIN_COS: 65

        .= ((((2 / (1 + (x ^2 ))) * ( exp_R . x)) - (( exp_R . x) * (( arctan . x) - ( arccot . x)))) / (( exp_R . x) ^2 )) by A5, A10, VALUED_1: 13

        .= (((2 / (1 + (x ^2 ))) - (( arctan . x) - ( arccot . x))) * (( exp_R . x) / (( exp_R . x) * ( exp_R . x))))

        .= (((2 / (1 + (x ^2 ))) - (( arctan . x) - ( arccot . x))) * ((( exp_R . x) / ( exp_R . x)) / ( exp_R . x))) by XCMPLX_1: 78

        .= (((2 / (1 + (x ^2 ))) - (( arctan . x) - ( arccot . x))) * (1 / ( exp_R . x))) by A9, XCMPLX_1: 60

        .= ((((2 / (1 + (x ^2 ))) - ( arctan . x)) + ( arccot . x)) / ( exp_R . x));

        hence thesis;

      end;

      hence thesis by A2, A6, FDIFF_2: 21;

    end;

    theorem :: FDIFF_11:55

    Z c= ( dom ( exp_R * ( arctan + arccot ))) & Z c= ].( - 1), 1.[ implies ( exp_R * ( arctan + arccot )) is_differentiable_on Z & for x st x in Z holds ((( exp_R * ( arctan + arccot )) `| Z) . x) = 0

    proof

      assume that

       A1: Z c= ( dom ( exp_R * ( arctan + arccot ))) and

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

      

       A3: ( arctan + arccot ) is_differentiable_on Z by A2, Th37;

      

       A4: for x st x in Z holds ( exp_R * ( arctan + arccot )) is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then

         A5: ( arctan + arccot ) is_differentiable_in x by A3, FDIFF_1: 9;

         exp_R is_differentiable_in (( arctan + arccot ) . x) by SIN_COS: 65;

        hence thesis by A5, FDIFF_2: 13;

      end;

      then

       A6: ( exp_R * ( arctan + arccot )) is_differentiable_on Z by A1, FDIFF_1: 9;

      for x st x in Z holds ((( exp_R * ( arctan + arccot )) `| Z) . x) = 0

      proof

        let x;

        

         A7: exp_R is_differentiable_in (( arctan + arccot ) . x) by SIN_COS: 65;

        assume

         A8: x in Z;

        then

         A9: ( arctan + arccot ) is_differentiable_in x by A3, FDIFF_1: 9;

        ((( exp_R * ( arctan + arccot )) `| Z) . x) = ( diff (( exp_R * ( arctan + arccot )),x)) by A6, A8, FDIFF_1:def 7

        .= (( diff ( exp_R ,(( arctan + arccot ) . x))) * ( diff (( arctan + arccot ),x))) by A9, A7, FDIFF_2: 13

        .= (( exp_R . (( arctan + arccot ) . x)) * ( diff (( arctan + arccot ),x))) by SIN_COS: 65

        .= (( exp_R . (( arctan + arccot ) . x)) * ((( arctan + arccot ) `| Z) . x)) by A3, A8, FDIFF_1:def 7

        .= (( exp_R . (( arctan + arccot ) . x)) * 0 ) by A2, A8, Th37

        .= 0 ;

        hence thesis;

      end;

      hence thesis by A1, A4, FDIFF_1: 9;

    end;

    theorem :: FDIFF_11:56

    Z c= ( dom ( exp_R * ( arctan - arccot ))) & Z c= ].( - 1), 1.[ implies ( exp_R * ( arctan - arccot )) is_differentiable_on Z & for x st x in Z holds ((( exp_R * ( arctan - arccot )) `| Z) . x) = ((2 * ( exp_R . (( arctan . x) - ( arccot . x)))) / (1 + (x ^2 )))

    proof

      assume that

       A1: Z c= ( dom ( exp_R * ( arctan - arccot ))) and

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

      

       A3: ].( - 1), 1.[ c= [.( - 1), 1.] by XXREAL_1: 25;

      then ].( - 1), 1.[ c= ( dom arccot ) by SIN_COS9: 24, XBOOLE_1: 1;

      then

       A4: Z c= ( dom arccot ) by A2, XBOOLE_1: 1;

       ].( - 1), 1.[ c= ( dom arctan ) by A3, SIN_COS9: 23, XBOOLE_1: 1;

      then Z c= ( dom arctan ) by A2, XBOOLE_1: 1;

      then Z c= (( dom arctan ) /\ ( dom arccot )) by A4, XBOOLE_1: 19;

      then

       A5: Z c= ( dom ( arctan - arccot )) by VALUED_1: 12;

      

       A6: ( arctan - arccot ) is_differentiable_on Z by A2, Th38;

      

       A7: for x st x in Z holds ( exp_R * ( arctan - arccot )) is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then

         A8: ( arctan - arccot ) is_differentiable_in x by A6, FDIFF_1: 9;

         exp_R is_differentiable_in (( arctan - arccot ) . x) by SIN_COS: 65;

        hence thesis by A8, FDIFF_2: 13;

      end;

      then

       A9: ( exp_R * ( arctan - arccot )) is_differentiable_on Z by A1, FDIFF_1: 9;

      for x st x in Z holds ((( exp_R * ( arctan - arccot )) `| Z) . x) = ((2 * ( exp_R . (( arctan . x) - ( arccot . x)))) / (1 + (x ^2 )))

      proof

        let x;

        

         A10: exp_R is_differentiable_in (( arctan - arccot ) . x) by SIN_COS: 65;

        assume

         A11: x in Z;

        then

         A12: ( arctan - arccot ) is_differentiable_in x by A6, FDIFF_1: 9;

        ((( exp_R * ( arctan - arccot )) `| Z) . x) = ( diff (( exp_R * ( arctan - arccot )),x)) by A9, A11, FDIFF_1:def 7

        .= (( diff ( exp_R ,(( arctan - arccot ) . x))) * ( diff (( arctan - arccot ),x))) by A12, A10, FDIFF_2: 13

        .= (( exp_R . (( arctan - arccot ) . x)) * ( diff (( arctan - arccot ),x))) by SIN_COS: 65

        .= (( exp_R . (( arctan - arccot ) . x)) * ((( arctan - arccot ) `| Z) . x)) by A6, A11, FDIFF_1:def 7

        .= (( exp_R . (( arctan - arccot ) . x)) * (2 / (1 + (x ^2 )))) by A2, A11, Th38

        .= (( exp_R . (( arctan . x) - ( arccot . x))) * (2 / (1 + (x ^2 )))) by A5, A11, VALUED_1: 13

        .= ((2 * ( exp_R . (( arctan . x) - ( arccot . x)))) / (1 + (x ^2 )));

        hence thesis;

      end;

      hence thesis by A1, A7, FDIFF_1: 9;

    end;

    theorem :: FDIFF_11:57

    Z c= ( dom ( sin * ( arctan + arccot ))) & Z c= ].( - 1), 1.[ implies ( sin * ( arctan + arccot )) is_differentiable_on Z & for x st x in Z holds ((( sin * ( arctan + arccot )) `| Z) . x) = 0

    proof

      assume that

       A1: Z c= ( dom ( sin * ( arctan + arccot ))) and

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

      

       A3: ( arctan + arccot ) is_differentiable_on Z by A2, Th37;

      

       A4: for x st x in Z holds ( sin * ( arctan + arccot )) is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then

         A5: ( arctan + arccot ) is_differentiable_in x by A3, FDIFF_1: 9;

         sin is_differentiable_in (( arctan + arccot ) . x) by SIN_COS: 64;

        hence thesis by A5, FDIFF_2: 13;

      end;

      then

       A6: ( sin * ( arctan + arccot )) is_differentiable_on Z by A1, FDIFF_1: 9;

      for x st x in Z holds ((( sin * ( arctan + arccot )) `| Z) . x) = 0

      proof

        let x;

        

         A7: sin is_differentiable_in (( arctan + arccot ) . x) by SIN_COS: 64;

        assume

         A8: x in Z;

        then

         A9: ( arctan + arccot ) is_differentiable_in x by A3, FDIFF_1: 9;

        ((( sin * ( arctan + arccot )) `| Z) . x) = ( diff (( sin * ( arctan + arccot )),x)) by A6, A8, FDIFF_1:def 7

        .= (( diff ( sin ,(( arctan + arccot ) . x))) * ( diff (( arctan + arccot ),x))) by A9, A7, FDIFF_2: 13

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

        .= (( cos . (( arctan + arccot ) . x)) * ((( arctan + arccot ) `| Z) . x)) by A3, A8, FDIFF_1:def 7

        .= (( cos . (( arctan + arccot ) . x)) * 0 ) by A2, A8, Th37

        .= 0 ;

        hence thesis;

      end;

      hence thesis by A1, A4, FDIFF_1: 9;

    end;

    theorem :: FDIFF_11:58

    Z c= ( dom ( sin * ( arctan - arccot ))) & Z c= ].( - 1), 1.[ implies ( sin * ( arctan - arccot )) is_differentiable_on Z & for x st x in Z holds ((( sin * ( arctan - arccot )) `| Z) . x) = ((2 * ( cos . (( arctan . x) - ( arccot . x)))) / (1 + (x ^2 )))

    proof

      assume that

       A1: Z c= ( dom ( sin * ( arctan - arccot ))) and

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

      

       A3: ].( - 1), 1.[ c= [.( - 1), 1.] by XXREAL_1: 25;

      then ].( - 1), 1.[ c= ( dom arccot ) by SIN_COS9: 24, XBOOLE_1: 1;

      then

       A4: Z c= ( dom arccot ) by A2, XBOOLE_1: 1;

       ].( - 1), 1.[ c= ( dom arctan ) by A3, SIN_COS9: 23, XBOOLE_1: 1;

      then Z c= ( dom arctan ) by A2, XBOOLE_1: 1;

      then Z c= (( dom arctan ) /\ ( dom arccot )) by A4, XBOOLE_1: 19;

      then

       A5: Z c= ( dom ( arctan - arccot )) by VALUED_1: 12;

      

       A6: ( arctan - arccot ) is_differentiable_on Z by A2, Th38;

      

       A7: for x st x in Z holds ( sin * ( arctan - arccot )) is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then

         A8: ( arctan - arccot ) is_differentiable_in x by A6, FDIFF_1: 9;

         sin is_differentiable_in (( arctan - arccot ) . x) by SIN_COS: 64;

        hence thesis by A8, FDIFF_2: 13;

      end;

      then

       A9: ( sin * ( arctan - arccot )) is_differentiable_on Z by A1, FDIFF_1: 9;

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

      proof

        let x;

        

         A10: sin is_differentiable_in (( arctan - arccot ) . x) by SIN_COS: 64;

        assume

         A11: x in Z;

        then

         A12: ( arctan - arccot ) is_differentiable_in x by A6, FDIFF_1: 9;

        ((( sin * ( arctan - arccot )) `| Z) . x) = ( diff (( sin * ( arctan - arccot )),x)) by A9, A11, FDIFF_1:def 7

        .= (( diff ( sin ,(( arctan - arccot ) . x))) * ( diff (( arctan - arccot ),x))) by A12, A10, FDIFF_2: 13

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

        .= (( cos . (( arctan - arccot ) . x)) * ((( arctan - arccot ) `| Z) . x)) by A6, A11, FDIFF_1:def 7

        .= (( cos . (( arctan - arccot ) . x)) * (2 / (1 + (x ^2 )))) by A2, A11, Th38

        .= (( cos . (( arctan . x) - ( arccot . x))) * (2 / (1 + (x ^2 )))) by A5, A11, VALUED_1: 13

        .= ((2 * ( cos . (( arctan . x) - ( arccot . x)))) / (1 + (x ^2 )));

        hence thesis;

      end;

      hence thesis by A1, A7, FDIFF_1: 9;

    end;

    theorem :: FDIFF_11:59

    Z c= ( dom ( cos * ( arctan + arccot ))) & Z c= ].( - 1), 1.[ implies ( cos * ( arctan + arccot )) is_differentiable_on Z & for x st x in Z holds ((( cos * ( arctan + arccot )) `| Z) . x) = 0

    proof

      assume that

       A1: Z c= ( dom ( cos * ( arctan + arccot ))) and

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

      

       A3: ( arctan + arccot ) is_differentiable_on Z by A2, Th37;

      

       A4: for x st x in Z holds ( cos * ( arctan + arccot )) is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then

         A5: ( arctan + arccot ) is_differentiable_in x by A3, FDIFF_1: 9;

         cos is_differentiable_in (( arctan + arccot ) . x) by SIN_COS: 63;

        hence thesis by A5, FDIFF_2: 13;

      end;

      then

       A6: ( cos * ( arctan + arccot )) is_differentiable_on Z by A1, FDIFF_1: 9;

      for x st x in Z holds ((( cos * ( arctan + arccot )) `| Z) . x) = 0

      proof

        let x;

        

         A7: cos is_differentiable_in (( arctan + arccot ) . x) by SIN_COS: 63;

        assume

         A8: x in Z;

        then

         A9: ( arctan + arccot ) is_differentiable_in x by A3, FDIFF_1: 9;

        ((( cos * ( arctan + arccot )) `| Z) . x) = ( diff (( cos * ( arctan + arccot )),x)) by A6, A8, FDIFF_1:def 7

        .= (( diff ( cos ,(( arctan + arccot ) . x))) * ( diff (( arctan + arccot ),x))) by A9, A7, FDIFF_2: 13

        .= (( - ( sin . (( arctan + arccot ) . x))) * ( diff (( arctan + arccot ),x))) by SIN_COS: 63

        .= (( - ( sin . (( arctan + arccot ) . x))) * ((( arctan + arccot ) `| Z) . x)) by A3, A8, FDIFF_1:def 7

        .= (( - ( sin . (( arctan + arccot ) . x))) * 0 ) by A2, A8, Th37

        .= 0 ;

        hence thesis;

      end;

      hence thesis by A1, A4, FDIFF_1: 9;

    end;

    theorem :: FDIFF_11:60

    Z c= ( dom ( cos * ( arctan - arccot ))) & Z c= ].( - 1), 1.[ implies ( cos * ( arctan - arccot )) is_differentiable_on Z & for x st x in Z holds ((( cos * ( arctan - arccot )) `| Z) . x) = ( - ((2 * ( sin . (( arctan . x) - ( arccot . x)))) / (1 + (x ^2 ))))

    proof

      assume that

       A1: Z c= ( dom ( cos * ( arctan - arccot ))) and

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

      

       A3: ].( - 1), 1.[ c= [.( - 1), 1.] by XXREAL_1: 25;

      then ].( - 1), 1.[ c= ( dom arccot ) by SIN_COS9: 24, XBOOLE_1: 1;

      then

       A4: Z c= ( dom arccot ) by A2, XBOOLE_1: 1;

       ].( - 1), 1.[ c= ( dom arctan ) by A3, SIN_COS9: 23, XBOOLE_1: 1;

      then Z c= ( dom arctan ) by A2, XBOOLE_1: 1;

      then Z c= (( dom arctan ) /\ ( dom arccot )) by A4, XBOOLE_1: 19;

      then

       A5: Z c= ( dom ( arctan - arccot )) by VALUED_1: 12;

      

       A6: ( arctan - arccot ) is_differentiable_on Z by A2, Th38;

      

       A7: for x st x in Z holds ( cos * ( arctan - arccot )) is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then

         A8: ( arctan - arccot ) is_differentiable_in x by A6, FDIFF_1: 9;

         cos is_differentiable_in (( arctan - arccot ) . x) by SIN_COS: 63;

        hence thesis by A8, FDIFF_2: 13;

      end;

      then

       A9: ( cos * ( arctan - arccot )) is_differentiable_on Z by A1, FDIFF_1: 9;

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

      proof

        let x;

        

         A10: cos is_differentiable_in (( arctan - arccot ) . x) by SIN_COS: 63;

        assume

         A11: x in Z;

        then

         A12: ( arctan - arccot ) is_differentiable_in x by A6, FDIFF_1: 9;

        ((( cos * ( arctan - arccot )) `| Z) . x) = ( diff (( cos * ( arctan - arccot )),x)) by A9, A11, FDIFF_1:def 7

        .= (( diff ( cos ,(( arctan - arccot ) . x))) * ( diff (( arctan - arccot ),x))) by A12, A10, FDIFF_2: 13

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

        .= (( - ( sin . (( arctan - arccot ) . x))) * ((( arctan - arccot ) `| Z) . x)) by A6, A11, FDIFF_1:def 7

        .= (( - ( sin . (( arctan - arccot ) . x))) * (2 / (1 + (x ^2 )))) by A2, A11, Th38

        .= (( - ( sin . (( arctan . x) - ( arccot . x)))) * (2 / (1 + (x ^2 )))) by A5, A11, VALUED_1: 13

        .= ( - ((2 * ( sin . (( arctan . x) - ( arccot . x)))) / (1 + (x ^2 ))));

        hence thesis;

      end;

      hence thesis by A1, A7, FDIFF_1: 9;

    end;

    theorem :: FDIFF_11:61

    Z c= ].( - 1), 1.[ implies ( arctan (#) arccot ) is_differentiable_on Z & for x st x in Z holds ((( arctan (#) arccot ) `| Z) . x) = ((( arccot . x) - ( arctan . x)) / (1 + (x ^2 )))

    proof

      assume

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

      then

       A2: arctan is_differentiable_on Z by SIN_COS9: 81;

      

       A3: ].( - 1), 1.[ c= [.( - 1), 1.] by XXREAL_1: 25;

      then ].( - 1), 1.[ c= ( dom arccot ) by SIN_COS9: 24, XBOOLE_1: 1;

      then

       A4: Z c= ( dom arccot ) by A1, XBOOLE_1: 1;

      

       A5: arccot is_differentiable_on Z by A1, SIN_COS9: 82;

       ].( - 1), 1.[ c= ( dom arctan ) by A3, SIN_COS9: 23, XBOOLE_1: 1;

      then Z c= ( dom arctan ) by A1, XBOOLE_1: 1;

      then Z c= (( dom arctan ) /\ ( dom arccot )) by A4, XBOOLE_1: 19;

      then

       A6: Z c= ( dom ( arctan (#) arccot )) by VALUED_1:def 4;

      for x st x in Z holds ((( arctan (#) arccot ) `| Z) . x) = ((( arccot . x) - ( arctan . x)) / (1 + (x ^2 )))

      proof

        let x;

        assume

         A7: x in Z;

        

        then ((( arctan (#) arccot ) `| Z) . x) = ((( arccot . x) * ( diff ( arctan ,x))) + (( arctan . x) * ( diff ( arccot ,x)))) by A6, A2, A5, FDIFF_1: 21

        .= ((( arccot . x) * (( arctan `| Z) . x)) + (( arctan . x) * ( diff ( arccot ,x)))) by A2, A7, FDIFF_1:def 7

        .= ((( arccot . x) * (1 / (1 + (x ^2 )))) + (( arctan . x) * ( diff ( arccot ,x)))) by A1, A7, SIN_COS9: 81

        .= ((( arccot . x) * (1 / (1 + (x ^2 )))) + (( arctan . x) * (( arccot `| Z) . x))) by A5, A7, FDIFF_1:def 7

        .= ((( arccot . x) * (1 / (1 + (x ^2 )))) + (( arctan . x) * ( - (1 / (1 + (x ^2 )))))) by A1, A7, SIN_COS9: 82

        .= ((( arccot . x) - ( arctan . x)) / (1 + (x ^2 )));

        hence thesis;

      end;

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

    end;

    theorem :: FDIFF_11:62

     not 0 in Z & Z c= ( dom (( arctan * (( id Z) ^ )) (#) ( arccot * (( id Z) ^ )))) & (for x st x in Z holds ((( id Z) ^ ) . x) > ( - 1) & ((( id Z) ^ ) . x) < 1) implies (( arctan * (( id Z) ^ )) (#) ( arccot * (( id Z) ^ ))) is_differentiable_on Z & for x st x in Z holds (((( arctan * (( id Z) ^ )) (#) ( arccot * (( id Z) ^ ))) `| Z) . x) = ((( arctan . (1 / x)) - ( arccot . (1 / x))) / (1 + (x ^2 )))

    proof

      set f = ( id Z);

      assume that

       A1: not 0 in Z and

       A2: Z c= ( dom (( arctan * (f ^ )) (#) ( arccot * (f ^ )))) and

       A3: for x st x in Z holds ((f ^ ) . x) > ( - 1) & ((f ^ ) . x) < 1;

      

       A4: Z c= (( dom ( arctan * (f ^ ))) /\ ( dom ( arccot * (f ^ )))) by A2, VALUED_1:def 4;

      then

       A5: Z c= ( dom ( arctan * (f ^ ))) by XBOOLE_1: 18;

      then

       A6: ( arctan * (f ^ )) is_differentiable_on Z by A1, A3, SIN_COS9: 111;

      

       A7: Z c= ( dom ( arccot * (f ^ ))) by A4, XBOOLE_1: 18;

      then

       A8: ( arccot * (f ^ )) is_differentiable_on Z by A1, A3, SIN_COS9: 112;

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

      then

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

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

      proof

        let x;

        assume

         A10: x in Z;

        

        then (((( arctan * (f ^ )) (#) ( arccot * (f ^ ))) `| Z) . x) = (((( arccot * (f ^ )) . x) * ( diff (( arctan * (f ^ )),x))) + ((( arctan * (f ^ )) . x) * ( diff (( arccot * (f ^ )),x)))) by A2, A6, A8, FDIFF_1: 21

        .= (((( arccot * (f ^ )) . x) * ((( arctan * (f ^ )) `| Z) . x)) + ((( arctan * (f ^ )) . x) * ( diff (( arccot * (f ^ )),x)))) by A6, A10, FDIFF_1:def 7

        .= (((( arccot * (f ^ )) . x) * ( - (1 / (1 + (x ^2 ))))) + ((( arctan * (f ^ )) . x) * ( diff (( arccot * (f ^ )),x)))) by A1, A3, A5, A10, SIN_COS9: 111

        .= (((( arccot * (f ^ )) . x) * ( - (1 / (1 + (x ^2 ))))) + ((( arctan * (f ^ )) . x) * ((( arccot * (f ^ )) `| Z) . x))) by A8, A10, FDIFF_1:def 7

        .= (((( arccot * (f ^ )) . x) * ( - (1 / (1 + (x ^2 ))))) + ((( arctan * (f ^ )) . x) * (1 / (1 + (x ^2 ))))) by A1, A3, A7, A10, SIN_COS9: 112

        .= ((( arccot . ((f ^ ) . x)) * ( - (1 / (1 + (x ^2 ))))) + ((( arctan * (f ^ )) . x) * (1 / (1 + (x ^2 ))))) by A7, A10, FUNCT_1: 12

        .= ((( arccot . ((f . x) " )) * ( - (1 / (1 + (x ^2 ))))) + ((( arctan * (f ^ )) . x) * (1 / (1 + (x ^2 ))))) by A9, A10, RFUNCT_1:def 2

        .= ((( arccot . (1 / x)) * ( - (1 / (1 + (x ^2 ))))) + ((( arctan * (f ^ )) . x) * (1 / (1 + (x ^2 ))))) by A10, FUNCT_1: 18

        .= ((( arccot . (1 / x)) * ( - (1 / (1 + (x ^2 ))))) + (( arctan . ((f ^ ) . x)) * (1 / (1 + (x ^2 ))))) by A5, A10, FUNCT_1: 12

        .= ((( arccot . (1 / x)) * ( - (1 / (1 + (x ^2 ))))) + (( arctan . ((f . x) " )) * (1 / (1 + (x ^2 ))))) by A9, A10, RFUNCT_1:def 2

        .= (( - (( arccot . (1 / x)) * (1 / (1 + (x ^2 ))))) + (( arctan . (1 / x)) * (1 / (1 + (x ^2 ))))) by A10, FUNCT_1: 18

        .= ((( arctan . (1 / x)) - ( arccot . (1 / x))) / (1 + (x ^2 )));

        hence thesis;

      end;

      hence thesis by A2, A6, A8, FDIFF_1: 21;

    end;

    theorem :: FDIFF_11:63

     not 0 in Z & Z c= ( dom (( id Z) (#) ( arctan * (( id Z) ^ )))) & (for x st x in Z holds ((( id Z) ^ ) . x) > ( - 1) & ((( id Z) ^ ) . x) < 1) implies (( id Z) (#) ( arctan * (( id Z) ^ ))) is_differentiable_on Z & for x st x in Z holds (((( id Z) (#) ( arctan * (( id Z) ^ ))) `| Z) . x) = (( arctan . (1 / x)) - (x / (1 + (x ^2 ))))

    proof

      set f = ( id Z);

      assume that

       A1: not 0 in Z and

       A2: Z c= ( dom (( id Z) (#) ( arctan * (f ^ )))) and

       A3: for x st x in Z holds ((f ^ ) . x) > ( - 1) & ((f ^ ) . x) < 1;

      

       A4: Z c= (( dom ( id Z)) /\ ( dom ( arctan * (f ^ )))) by A2, VALUED_1:def 4;

      then

       A5: Z c= ( dom ( arctan * (f ^ ))) by XBOOLE_1: 18;

      then

       A6: ( arctan * (f ^ )) is_differentiable_on Z by A1, A3, SIN_COS9: 111;

      

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

      

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

      then

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

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

      then

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

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

      proof

        let x;

        assume

         A11: x in Z;

        

        then (((( id Z) (#) ( arctan * (f ^ ))) `| Z) . x) = (((( arctan * (f ^ )) . x) * ( diff (( id Z),x))) + ((( id Z) . x) * ( diff (( arctan * (f ^ )),x)))) by A2, A6, A9, FDIFF_1: 21

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

        .= (((( arctan * (f ^ )) . x) * 1) + ((( id Z) . x) * ( diff (( arctan * (f ^ )),x)))) by A8, A7, A11, FDIFF_1: 23

        .= (((( arctan * (f ^ )) . x) * 1) + (x * ( diff (( arctan * (f ^ )),x)))) by A11, FUNCT_1: 18

        .= ((( arctan * (f ^ )) . x) + (x * ((( arctan * (f ^ )) `| Z) . x))) by A6, A11, FDIFF_1:def 7

        .= ((( arctan * (f ^ )) . x) + (x * ( - (1 / (1 + (x ^2 )))))) by A1, A3, A5, A11, SIN_COS9: 111

        .= (( arctan . ((f ^ ) . x)) - (x / (1 + (x ^2 )))) by A5, A11, FUNCT_1: 12

        .= (( arctan . ((f . x) " )) - (x / (1 + (x ^2 )))) by A10, A11, RFUNCT_1:def 2

        .= (( arctan . (1 / x)) - (x / (1 + (x ^2 )))) by A11, FUNCT_1: 18;

        hence thesis;

      end;

      hence thesis by A2, A6, A9, FDIFF_1: 21;

    end;

    theorem :: FDIFF_11:64

     not 0 in Z & Z c= ( dom (( id Z) (#) ( arccot * (( id Z) ^ )))) & (for x st x in Z holds ((( id Z) ^ ) . x) > ( - 1) & ((( id Z) ^ ) . x) < 1) implies (( id Z) (#) ( arccot * (( id Z) ^ ))) is_differentiable_on Z & for x st x in Z holds (((( id Z) (#) ( arccot * (( id Z) ^ ))) `| Z) . x) = (( arccot . (1 / x)) + (x / (1 + (x ^2 ))))

    proof

      set f = ( id Z);

      assume that

       A1: not 0 in Z and

       A2: Z c= ( dom (( id Z) (#) ( arccot * (f ^ )))) and

       A3: for x st x in Z holds ((f ^ ) . x) > ( - 1) & ((f ^ ) . x) < 1;

      

       A4: Z c= (( dom ( id Z)) /\ ( dom ( arccot * (f ^ )))) by A2, VALUED_1:def 4;

      then

       A5: Z c= ( dom ( arccot * (f ^ ))) by XBOOLE_1: 18;

      then

       A6: ( arccot * (f ^ )) is_differentiable_on Z by A1, A3, SIN_COS9: 112;

      

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

      

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

      then

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

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

      then

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

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

      proof

        let x;

        assume

         A11: x in Z;

        

        then (((( id Z) (#) ( arccot * (f ^ ))) `| Z) . x) = (((( arccot * (f ^ )) . x) * ( diff (( id Z),x))) + ((( id Z) . x) * ( diff (( arccot * (f ^ )),x)))) by A2, A6, A9, FDIFF_1: 21

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

        .= (((( arccot * (f ^ )) . x) * 1) + ((( id Z) . x) * ( diff (( arccot * (f ^ )),x)))) by A8, A7, A11, FDIFF_1: 23

        .= (((( arccot * (f ^ )) . x) * 1) + (x * ( diff (( arccot * (f ^ )),x)))) by A11, FUNCT_1: 18

        .= ((( arccot * (f ^ )) . x) + (x * ((( arccot * (f ^ )) `| Z) . x))) by A6, A11, FDIFF_1:def 7

        .= ((( arccot * (f ^ )) . x) + (x * (1 / (1 + (x ^2 ))))) by A1, A3, A5, A11, SIN_COS9: 112

        .= (( arccot . ((f ^ ) . x)) + (x / (1 + (x ^2 )))) by A5, A11, FUNCT_1: 12

        .= (( arccot . ((f . x) " )) + (x / (1 + (x ^2 )))) by A10, A11, RFUNCT_1:def 2

        .= (( arccot . (1 / x)) + (x / (1 + (x ^2 )))) by A11, FUNCT_1: 18;

        hence thesis;

      end;

      hence thesis by A2, A6, A9, FDIFF_1: 21;

    end;

    theorem :: FDIFF_11:65

     not 0 in Z & Z c= ( dom (g (#) ( arctan * (( id Z) ^ )))) & g = ( #Z 2) & (for x st x in Z holds ((( id Z) ^ ) . x) > ( - 1) & ((( id Z) ^ ) . x) < 1) implies (g (#) ( arctan * (( id Z) ^ ))) is_differentiable_on Z & for x st x in Z holds (((g (#) ( arctan * (( id Z) ^ ))) `| Z) . x) = (((2 * x) * ( arctan . (1 / x))) - ((x ^2 ) / (1 + (x ^2 ))))

    proof

      set f = ( id Z);

      assume that

       A1: not 0 in Z and

       A2: Z c= ( dom (g (#) ( arctan * (f ^ )))) and

       A3: g = ( #Z 2) and

       A4: for x st x in Z holds ((f ^ ) . x) > ( - 1) & ((f ^ ) . x) < 1;

      

       A5: for x st x in Z holds g is_differentiable_in x by A3, TAYLOR_1: 2;

      

       A6: Z c= (( dom g) /\ ( dom ( arctan * (f ^ )))) by A2, VALUED_1:def 4;

      then

       A7: Z c= ( dom ( arctan * (f ^ ))) by XBOOLE_1: 18;

      then

       A8: ( arctan * (f ^ )) is_differentiable_on Z by A1, A4, SIN_COS9: 111;

      Z c= ( dom g) by A6, XBOOLE_1: 18;

      then

       A9: g is_differentiable_on Z by A5, FDIFF_1: 9;

      

       A10: for x st x in Z holds ((g `| Z) . x) = (2 * x)

      proof

        let x;

        assume x in Z;

        

        then ((g `| Z) . x) = ( diff (g,x)) by A9, FDIFF_1:def 7

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

        .= (2 * x) by PREPOWER: 35;

        hence thesis;

      end;

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

      then

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

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

      proof

        let x;

        assume

         A12: x in Z;

        

        then (((g (#) ( arctan * (f ^ ))) `| Z) . x) = (((( arctan * (f ^ )) . x) * ( diff (g,x))) + ((g . x) * ( diff (( arctan * (f ^ )),x)))) by A2, A8, A9, FDIFF_1: 21

        .= (((( arctan * (f ^ )) . x) * ((g `| Z) . x)) + ((g . x) * ( diff (( arctan * (f ^ )),x)))) by A9, A12, FDIFF_1:def 7

        .= (((( arctan * (f ^ )) . x) * (2 * x)) + ((g . x) * ( diff (( arctan * (f ^ )),x)))) by A10, A12

        .= (((( arctan * (f ^ )) . x) * (2 * x)) + ((x #Z 2) * ( diff (( arctan * (f ^ )),x)))) by A3, TAYLOR_1:def 1

        .= (((( arctan * (f ^ )) . x) * (2 * x)) + ((x #Z 2) * ((( arctan * (f ^ )) `| Z) . x))) by A8, A12, FDIFF_1:def 7

        .= (((( arctan * (f ^ )) . x) * (2 * x)) + ((x #Z (1 + 1)) * ( - (1 / (1 + (x ^2 )))))) by A1, A4, A7, A12, SIN_COS9: 111

        .= (((( arctan * (f ^ )) . x) * (2 * x)) + (((x #Z 1) * (x #Z 1)) * ( - (1 / (1 + (x ^2 )))))) by TAYLOR_1: 1

        .= (((( arctan * (f ^ )) . x) * (2 * x)) + ((x * (x #Z 1)) * ( - (1 / (1 + (x ^2 )))))) by PREPOWER: 35

        .= (((( arctan * (f ^ )) . x) * (2 * x)) + ((x ^2 ) * ( - (1 / (1 + (x ^2 )))))) by PREPOWER: 35

        .= ((( arctan . ((f ^ ) . x)) * (2 * x)) - ((x ^2 ) / (1 + (x ^2 )))) by A7, A12, FUNCT_1: 12

        .= ((( arctan . ((f . x) " )) * (2 * x)) - ((x ^2 ) / (1 + (x ^2 )))) by A11, A12, RFUNCT_1:def 2

        .= (((2 * x) * ( arctan . (1 / x))) - ((x ^2 ) / (1 + (x ^2 )))) by A12, FUNCT_1: 18;

        hence thesis;

      end;

      hence thesis by A2, A8, A9, FDIFF_1: 21;

    end;

    theorem :: FDIFF_11:66

     not 0 in Z & Z c= ( dom (g (#) ( arccot * (( id Z) ^ )))) & g = ( #Z 2) & (for x st x in Z holds ((( id Z) ^ ) . x) > ( - 1) & ((( id Z) ^ ) . x) < 1) implies (g (#) ( arccot * (( id Z) ^ ))) is_differentiable_on Z & for x st x in Z holds (((g (#) ( arccot * (( id Z) ^ ))) `| Z) . x) = (((2 * x) * ( arccot . (1 / x))) + ((x ^2 ) / (1 + (x ^2 ))))

    proof

      set f = ( id Z);

      assume that

       A1: not 0 in Z and

       A2: Z c= ( dom (g (#) ( arccot * (f ^ )))) and

       A3: g = ( #Z 2) and

       A4: for x st x in Z holds ((f ^ ) . x) > ( - 1) & ((f ^ ) . x) < 1;

      

       A5: for x st x in Z holds g is_differentiable_in x by A3, TAYLOR_1: 2;

      

       A6: Z c= (( dom g) /\ ( dom ( arccot * (f ^ )))) by A2, VALUED_1:def 4;

      then

       A7: Z c= ( dom ( arccot * (f ^ ))) by XBOOLE_1: 18;

      then

       A8: ( arccot * (f ^ )) is_differentiable_on Z by A1, A4, SIN_COS9: 112;

      Z c= ( dom g) by A6, XBOOLE_1: 18;

      then

       A9: g is_differentiable_on Z by A5, FDIFF_1: 9;

      

       A10: for x st x in Z holds ((g `| Z) . x) = (2 * x)

      proof

        let x;

        assume x in Z;

        

        then ((g `| Z) . x) = ( diff (g,x)) by A9, FDIFF_1:def 7

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

        .= (2 * x) by PREPOWER: 35;

        hence thesis;

      end;

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

      then

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

      for x st x in Z holds (((g (#) ( arccot * (f ^ ))) `| Z) . x) = (((2 * x) * ( arccot . (1 / x))) + ((x ^2 ) / (1 + (x ^2 ))))

      proof

        let x;

        assume

         A12: x in Z;

        

        then (((g (#) ( arccot * (f ^ ))) `| Z) . x) = (((( arccot * (f ^ )) . x) * ( diff (g,x))) + ((g . x) * ( diff (( arccot * (f ^ )),x)))) by A2, A8, A9, FDIFF_1: 21

        .= (((( arccot * (f ^ )) . x) * ((g `| Z) . x)) + ((g . x) * ( diff (( arccot * (f ^ )),x)))) by A9, A12, FDIFF_1:def 7

        .= (((( arccot * (f ^ )) . x) * (2 * x)) + ((g . x) * ( diff (( arccot * (f ^ )),x)))) by A10, A12

        .= (((( arccot * (f ^ )) . x) * (2 * x)) + ((x #Z 2) * ( diff (( arccot * (f ^ )),x)))) by A3, TAYLOR_1:def 1

        .= (((( arccot * (f ^ )) . x) * (2 * x)) + ((x #Z 2) * ((( arccot * (f ^ )) `| Z) . x))) by A8, A12, FDIFF_1:def 7

        .= (((( arccot * (f ^ )) . x) * (2 * x)) + ((x #Z (1 + 1)) * (1 / (1 + (x ^2 ))))) by A1, A4, A7, A12, SIN_COS9: 112

        .= (((( arccot * (f ^ )) . x) * (2 * x)) + (((x #Z 1) * (x #Z 1)) * (1 / (1 + (x ^2 ))))) by TAYLOR_1: 1

        .= (((( arccot * (f ^ )) . x) * (2 * x)) + ((x * (x #Z 1)) * (1 / (1 + (x ^2 ))))) by PREPOWER: 35

        .= (((( arccot * (f ^ )) . x) * (2 * x)) + ((x ^2 ) / (1 + (x ^2 )))) by PREPOWER: 35

        .= ((( arccot . ((f ^ ) . x)) * (2 * x)) + ((x ^2 ) / (1 + (x ^2 )))) by A7, A12, FUNCT_1: 12

        .= ((( arccot . ((f . x) " )) * (2 * x)) + ((x ^2 ) / (1 + (x ^2 )))) by A11, A12, RFUNCT_1:def 2

        .= (((2 * x) * ( arccot . (1 / x))) + ((x ^2 ) / (1 + (x ^2 )))) by A12, FUNCT_1: 18;

        hence thesis;

      end;

      hence thesis by A2, A8, A9, FDIFF_1: 21;

    end;

    theorem :: FDIFF_11:67

    

     Th67: Z c= ].( - 1), 1.[ & (for x st x in Z holds ( arctan . x) <> 0 ) implies ( arctan ^ ) is_differentiable_on Z & for x st x in Z holds ((( arctan ^ ) `| Z) . x) = ( - (1 / ((( arctan . x) ^2 ) * (1 + (x ^2 )))))

    proof

      assume that

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

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

      

       A3: arctan is_differentiable_on Z by A1, SIN_COS9: 81;

      then

       A4: ( arctan ^ ) is_differentiable_on Z by A2, FDIFF_2: 22;

      for x st x in Z holds ((( arctan ^ ) `| Z) . x) = ( - (1 / ((( arctan . x) ^2 ) * (1 + (x ^2 )))))

      proof

        let x;

        assume

         A5: x in Z;

        then

         A6: ( arctan . x) <> 0 & arctan is_differentiable_in x by A2, A3, FDIFF_1: 9;

        ((( arctan ^ ) `| Z) . x) = ( diff (( arctan ^ ),x)) by A4, A5, FDIFF_1:def 7

        .= ( - (( diff ( arctan ,x)) / (( arctan . x) ^2 ))) by A6, FDIFF_2: 15

        .= ( - ((( arctan `| Z) . x) / (( arctan . x) ^2 ))) by A3, A5, FDIFF_1:def 7

        .= ( - ((1 / (1 + (x ^2 ))) / (( arctan . x) ^2 ))) by A1, A5, SIN_COS9: 81

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

        hence thesis;

      end;

      hence thesis by A2, A3, FDIFF_2: 22;

    end;

    theorem :: FDIFF_11:68

    

     Th68: Z c= ].( - 1), 1.[ implies ( arccot ^ ) is_differentiable_on Z & for x st x in Z holds ((( arccot ^ ) `| Z) . x) = (1 / ((( arccot . x) ^2 ) * (1 + (x ^2 ))))

    proof

      assume

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

      then

       A2: arccot is_differentiable_on Z by SIN_COS9: 82;

      

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

      proof

         PI in ]. 0 , 4.[ by SIN_COS:def 28;

        then PI > 0 by XXREAL_1: 4;

        then

         A4: ( PI / 4) > ( 0 / 4) by XREAL_1: 74;

        let x;

        assume

         A5: x in Z;

        assume

         A6: ( arccot . x) = 0 ;

         ].( - 1), 1.[ c= [.( - 1), 1.] by XXREAL_1: 25;

        then Z c= [.( - 1), 1.] by A1, XBOOLE_1: 1;

        then x in [.( - 1), 1.] by A5;

        then 0 in ( arccot .: [.( - 1), 1.]) by A6, FUNCT_1:def 6, SIN_COS9: 24;

        then 0 in [.( PI / 4), ((3 / 4) * PI ).] by RELAT_1: 115, SIN_COS9: 56;

        hence contradiction by A4, XXREAL_1: 1;

      end;

      then

       A7: ( arccot ^ ) is_differentiable_on Z by A2, FDIFF_2: 22;

      for x st x in Z holds ((( arccot ^ ) `| Z) . x) = (1 / ((( arccot . x) ^2 ) * (1 + (x ^2 ))))

      proof

        let x;

        assume

         A8: x in Z;

        then

         A9: ( arccot . x) <> 0 & arccot is_differentiable_in x by A3, A2, FDIFF_1: 9;

        ((( arccot ^ ) `| Z) . x) = ( diff (( arccot ^ ),x)) by A7, A8, FDIFF_1:def 7

        .= ( - (( diff ( arccot ,x)) / (( arccot . x) ^2 ))) by A9, FDIFF_2: 15

        .= ( - ((( arccot `| Z) . x) / (( arccot . x) ^2 ))) by A2, A8, FDIFF_1:def 7

        .= ( - (( - (1 / (1 + (x ^2 )))) / (( arccot . x) ^2 ))) by A1, A8, SIN_COS9: 82

        .= ((1 / (1 + (x ^2 ))) / (( arccot . x) ^2 ))

        .= (1 / ((( arccot . x) ^2 ) * (1 + (x ^2 )))) by XCMPLX_1: 78;

        hence thesis;

      end;

      hence thesis by A3, A2, FDIFF_2: 22;

    end;

    theorem :: FDIFF_11:69

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

    proof

      assume that

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

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

       A3: n > 0 and

       A4: for x st x in Z holds ( arctan . x) <> 0 ;

      

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

      

       A6: ( arctan ^ ) is_differentiable_on Z by A2, A4, Th67;

      for x st x in Z holds (( #Z n) * ( arctan ^ )) is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then ( arctan ^ ) is_differentiable_in x by A6, FDIFF_1: 9;

        hence thesis by TAYLOR_1: 3;

      end;

      then

       A7: (( #Z n) * ( arctan ^ )) is_differentiable_on Z by A5, FDIFF_1: 9;

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

      then

       A8: Z c= ( dom ( arctan ^ )) by TARSKI:def 3;

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

      proof

        let x;

        assume

         A9: x in Z;

        then

         A10: ( arctan ^ ) is_differentiable_in x by A6, FDIFF_1: 9;

        

         A11: (( arctan ^ ) . x) = (1 / ( arctan . x)) by A8, A9, RFUNCT_1:def 2;

        ((((1 / n) (#) (( #Z n) * ( arctan ^ ))) `| Z) . x) = ((1 / n) * ( diff ((( #Z n) * ( arctan ^ )),x))) by A1, A7, A9, FDIFF_1: 20

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

        .= ((1 / n) * ((n * ((( arctan ^ ) . x) #Z (n - 1))) * ((( arctan ^ ) `| Z) . x))) by A6, A9, FDIFF_1:def 7

        .= ((1 / n) * ((n * ((( arctan ^ ) . x) #Z (n - 1))) * ( - (1 / ((( arctan . x) ^2 ) * (1 + (x ^2 ))))))) by A2, A4, A9, Th67

        .= ( - ((((1 / n) * n) * ((( arctan ^ ) . x) #Z (n - 1))) * (1 / ((( arctan . x) ^2 ) * (1 + (x ^2 ))))))

        .= ( - ((1 * ((( arctan ^ ) . x) #Z (n - 1))) * (1 / ((( arctan . x) ^2 ) * (1 + (x ^2 )))))) by A3, XCMPLX_1: 106

        .= ( - (((1 / ( arctan . x)) #Z (n - 1)) * (1 / ((( arctan . x) #Z 2) * (1 + (x ^2 )))))) by A11, FDIFF_7: 1

        .= ( - ((1 / (( arctan . x) #Z (n - 1))) / ((( arctan . x) #Z 2) * (1 + (x ^2 ))))) by PREPOWER: 42

        .= ( - (1 / ((( arctan . x) #Z (n - 1)) * ((( arctan . x) #Z 2) * (1 + (x ^2 )))))) by XCMPLX_1: 78

        .= ( - (1 / (((( arctan . x) #Z (n - 1)) * (( arctan . x) #Z 2)) * (1 + (x ^2 )))))

        .= ( - (1 / ((( arctan . x) #Z ((n - 1) + 2)) * (1 + (x ^2 ))))) by A4, A9, PREPOWER: 44

        .= ( - (1 / ((( arctan . x) #Z (n + 1)) * (1 + (x ^2 )))));

        hence thesis;

      end;

      hence thesis by A1, A7, FDIFF_1: 20;

    end;

    theorem :: FDIFF_11:70

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

    proof

      assume that

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

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

       A3: n > 0 ;

      

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

      

       A5: for x st x in Z holds ( arccot . x) <> 0

      proof

         PI in ]. 0 , 4.[ by SIN_COS:def 28;

        then PI > 0 by XXREAL_1: 4;

        then

         A6: ( PI / 4) > ( 0 / 4) by XREAL_1: 74;

        let x;

        assume

         A7: x in Z;

        assume

         A8: ( arccot . x) = 0 ;

         ].( - 1), 1.[ c= [.( - 1), 1.] by XXREAL_1: 25;

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

        then x in [.( - 1), 1.] by A7;

        then 0 in ( arccot .: [.( - 1), 1.]) by A8, FUNCT_1:def 6, SIN_COS9: 24;

        then 0 in [.( PI / 4), ((3 / 4) * PI ).] by RELAT_1: 115, SIN_COS9: 56;

        hence contradiction by A6, XXREAL_1: 1;

      end;

      

       A9: ( arccot ^ ) is_differentiable_on Z by A2, Th68;

      for x st x in Z holds (( #Z n) * ( arccot ^ )) is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then ( arccot ^ ) is_differentiable_in x by A9, FDIFF_1: 9;

        hence thesis by TAYLOR_1: 3;

      end;

      then

       A10: (( #Z n) * ( arccot ^ )) is_differentiable_on Z by A4, FDIFF_1: 9;

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

      then

       A11: Z c= ( dom ( arccot ^ )) by TARSKI:def 3;

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

      proof

        let x;

        assume

         A12: x in Z;

        then

         A13: ( arccot ^ ) is_differentiable_in x by A9, FDIFF_1: 9;

        

         A14: (( arccot ^ ) . x) = (1 / ( arccot . x)) by A11, A12, RFUNCT_1:def 2;

        ((((1 / n) (#) (( #Z n) * ( arccot ^ ))) `| Z) . x) = ((1 / n) * ( diff ((( #Z n) * ( arccot ^ )),x))) by A1, A10, A12, FDIFF_1: 20

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

        .= ((1 / n) * ((n * ((( arccot ^ ) . x) #Z (n - 1))) * ((( arccot ^ ) `| Z) . x))) by A9, A12, FDIFF_1:def 7

        .= ((1 / n) * ((n * ((( arccot ^ ) . x) #Z (n - 1))) * (1 / ((( arccot . x) ^2 ) * (1 + (x ^2 )))))) by A2, A12, Th68

        .= ((((1 / n) * n) * ((( arccot ^ ) . x) #Z (n - 1))) * (1 / ((( arccot . x) ^2 ) * (1 + (x ^2 )))))

        .= ((1 * ((( arccot ^ ) . x) #Z (n - 1))) * (1 / ((( arccot . x) ^2 ) * (1 + (x ^2 ))))) by A3, XCMPLX_1: 106

        .= (((1 / ( arccot . x)) #Z (n - 1)) * (1 / ((( arccot . x) #Z 2) * (1 + (x ^2 ))))) by A14, FDIFF_7: 1

        .= ((1 / (( arccot . x) #Z (n - 1))) / ((( arccot . x) #Z 2) * (1 + (x ^2 )))) by PREPOWER: 42

        .= (1 / ((( arccot . x) #Z (n - 1)) * ((( arccot . x) #Z 2) * (1 + (x ^2 ))))) by XCMPLX_1: 78

        .= (1 / (((( arccot . x) #Z (n - 1)) * (( arccot . x) #Z 2)) * (1 + (x ^2 ))))

        .= (1 / ((( arccot . x) #Z ((n - 1) + 2)) * (1 + (x ^2 )))) by A5, A12, PREPOWER: 44

        .= (1 / ((( arccot . x) #Z (n + 1)) * (1 + (x ^2 ))));

        hence thesis;

      end;

      hence thesis by A1, A10, FDIFF_1: 20;

    end;

    theorem :: FDIFF_11:71

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

    proof

      assume that

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

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

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

      

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

      proof

        let x;

        assume

         A5: x in Z;

        then

         A6: ( arctan . x) > 0 by A3;

         arctan is_differentiable_on Z by A2, SIN_COS9: 81;

        then arctan is_differentiable_in x by A5, FDIFF_1: 9;

        hence thesis by A6, TAYLOR_1: 22;

      end;

      Z c= ( dom (( #R (1 / 2)) * arctan )) by A1, VALUED_1:def 5;

      then

       A7: (( #R (1 / 2)) * arctan ) is_differentiable_on Z by A4, FDIFF_1: 9;

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

      proof

        let x;

        assume

         A8: x in Z;

        then

         A9: ( arctan . x) > 0 by A3;

        

         A10: arctan is_differentiable_on Z by A2, SIN_COS9: 81;

        then

         A11: arctan is_differentiable_in x by A8, FDIFF_1: 9;

        (((2 (#) (( #R (1 / 2)) * arctan )) `| Z) . x) = (2 * ( diff ((( #R (1 / 2)) * arctan ),x))) by A1, A7, A8, FDIFF_1: 20

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

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

        .= (2 * (((1 / 2) * (( arctan . x) #R ((1 / 2) - 1))) * (1 / (1 + (x ^2 ))))) by A2, A8, SIN_COS9: 81

        .= ((( arctan . x) #R ( - (1 / 2))) / (1 + (x ^2 )));

        hence thesis;

      end;

      hence thesis by A1, A7, FDIFF_1: 20;

    end;

    theorem :: FDIFF_11:72

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

    proof

      assume that

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

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

      

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

      proof

        let x;

         ].( - 1), 1.[ c= [.( - 1), 1.] by XXREAL_1: 25;

        then

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

        assume x in Z;

        then x in [.( - 1), 1.] by A4;

        then ( arccot . x) in ( arccot .: [.( - 1), 1.]) by FUNCT_1:def 6, SIN_COS9: 24;

        then ( arccot . x) in [.( PI / 4), ((3 / 4) * PI ).] by RELAT_1: 115, SIN_COS9: 56;

        then ( arccot . x) >= ( PI / 4) by XXREAL_1: 1;

        then

         A5: (( arccot . x) + 0 ) > (( PI / 4) + ( - ( PI / 4))) by XREAL_1: 8;

        assume ( arccot . x) <= 0 ;

        hence contradiction by A5;

      end;

      

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

      proof

        let x;

        assume

         A7: x in Z;

        then

         A8: ( arccot . x) > 0 by A3;

         arccot is_differentiable_on Z by A2, SIN_COS9: 82;

        then arccot is_differentiable_in x by A7, FDIFF_1: 9;

        hence thesis by A8, TAYLOR_1: 22;

      end;

      Z c= ( dom (( #R (1 / 2)) * arccot )) by A1, VALUED_1:def 5;

      then

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

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

      proof

        let x;

        assume

         A10: x in Z;

        then

         A11: ( arccot . x) > 0 by A3;

        

         A12: arccot is_differentiable_on Z by A2, SIN_COS9: 82;

        then

         A13: arccot is_differentiable_in x by A10, FDIFF_1: 9;

        (((2 (#) (( #R (1 / 2)) * arccot )) `| Z) . x) = (2 * ( diff ((( #R (1 / 2)) * arccot ),x))) by A1, A9, A10, FDIFF_1: 20

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

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

        .= (2 * (((1 / 2) * (( arccot . x) #R ((1 / 2) - 1))) * ( - (1 / (1 + (x ^2 )))))) by A2, A10, SIN_COS9: 82

        .= ( - ((( arccot . x) #R ( - (1 / 2))) / (1 + (x ^2 ))));

        hence thesis;

      end;

      hence thesis by A1, A9, FDIFF_1: 20;

    end;

    theorem :: FDIFF_11:73

    Z c= ( dom ((2 / 3) (#) (( #R (3 / 2)) * arctan ))) & Z c= ].( - 1), 1.[ & (for x st x in Z holds ( arctan . x) > 0 ) implies ((2 / 3) (#) (( #R (3 / 2)) * arctan )) is_differentiable_on Z & for x st x in Z holds ((((2 / 3) (#) (( #R (3 / 2)) * arctan )) `| Z) . x) = ((( arctan . x) #R (1 / 2)) / (1 + (x ^2 )))

    proof

      assume that

       A1: Z c= ( dom ((2 / 3) (#) (( #R (3 / 2)) * arctan ))) and

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

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

      

       A4: for x st x in Z holds (( #R (3 / 2)) * arctan ) is_differentiable_in x

      proof

        let x;

        assume

         A5: x in Z;

        then

         A6: ( arctan . x) > 0 by A3;

         arctan is_differentiable_on Z by A2, SIN_COS9: 81;

        then arctan is_differentiable_in x by A5, FDIFF_1: 9;

        hence thesis by A6, TAYLOR_1: 22;

      end;

      Z c= ( dom (( #R (3 / 2)) * arctan )) by A1, VALUED_1:def 5;

      then

       A7: (( #R (3 / 2)) * arctan ) is_differentiable_on Z by A4, FDIFF_1: 9;

      for x st x in Z holds ((((2 / 3) (#) (( #R (3 / 2)) * arctan )) `| Z) . x) = ((( arctan . x) #R (1 / 2)) / (1 + (x ^2 )))

      proof

        let x;

        assume

         A8: x in Z;

        then

         A9: ( arctan . x) > 0 by A3;

        

         A10: arctan is_differentiable_on Z by A2, SIN_COS9: 81;

        then

         A11: arctan is_differentiable_in x by A8, FDIFF_1: 9;

        ((((2 / 3) (#) (( #R (3 / 2)) * arctan )) `| Z) . x) = ((2 / 3) * ( diff ((( #R (3 / 2)) * arctan ),x))) by A1, A7, A8, FDIFF_1: 20

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

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

        .= ((2 / 3) * (((3 / 2) * (( arctan . x) #R ((3 / 2) - 1))) * (1 / (1 + (x ^2 ))))) by A2, A8, SIN_COS9: 81

        .= ((( arctan . x) #R (1 / 2)) / (1 + (x ^2 )));

        hence thesis;

      end;

      hence thesis by A1, A7, FDIFF_1: 20;

    end;

    theorem :: FDIFF_11:74

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

    proof

      assume that

       A1: Z c= ( dom ((2 / 3) (#) (( #R (3 / 2)) * arccot ))) and

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

      

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

      proof

        let x;

         ].( - 1), 1.[ c= [.( - 1), 1.] by XXREAL_1: 25;

        then

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

        assume x in Z;

        then x in [.( - 1), 1.] by A4;

        then ( arccot . x) in ( arccot .: [.( - 1), 1.]) by FUNCT_1:def 6, SIN_COS9: 24;

        then ( arccot . x) in [.( PI / 4), ((3 / 4) * PI ).] by RELAT_1: 115, SIN_COS9: 56;

        then ( arccot . x) >= ( PI / 4) by XXREAL_1: 1;

        then

         A5: (( arccot . x) + 0 ) > (( PI / 4) + ( - ( PI / 4))) by XREAL_1: 8;

        assume ( arccot . x) <= 0 ;

        hence contradiction by A5;

      end;

      

       A6: for x st x in Z holds (( #R (3 / 2)) * arccot ) is_differentiable_in x

      proof

        let x;

        assume

         A7: x in Z;

        then

         A8: ( arccot . x) > 0 by A3;

         arccot is_differentiable_on Z by A2, SIN_COS9: 82;

        then arccot is_differentiable_in x by A7, FDIFF_1: 9;

        hence thesis by A8, TAYLOR_1: 22;

      end;

      Z c= ( dom (( #R (3 / 2)) * arccot )) by A1, VALUED_1:def 5;

      then

       A9: (( #R (3 / 2)) * arccot ) is_differentiable_on Z by A6, FDIFF_1: 9;

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

      proof

        let x;

        assume

         A10: x in Z;

        then

         A11: ( arccot . x) > 0 by A3;

        

         A12: arccot is_differentiable_on Z by A2, SIN_COS9: 82;

        then

         A13: arccot is_differentiable_in x by A10, FDIFF_1: 9;

        ((((2 / 3) (#) (( #R (3 / 2)) * arccot )) `| Z) . x) = ((2 / 3) * ( diff ((( #R (3 / 2)) * arccot ),x))) by A1, A9, A10, FDIFF_1: 20

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

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

        .= ((2 / 3) * (((3 / 2) * (( arccot . x) #R ((3 / 2) - 1))) * ( - (1 / (1 + (x ^2 )))))) by A2, A10, SIN_COS9: 82

        .= ( - ((( arccot . x) #R (1 / 2)) / (1 + (x ^2 ))));

        hence thesis;

      end;

      hence thesis by A1, A9, FDIFF_1: 20;

    end;