fdiff_9.miz



    begin

    definition

      :: FDIFF_9:def1

      func sec -> PartFunc of REAL , REAL equals ( cos ^ );

      coherence ;

      :: FDIFF_9:def2

      func cosec -> PartFunc of REAL , REAL equals ( sin ^ );

      coherence ;

    end

    reserve x,a,b,c for Real,

n for Nat,

Z for open Subset of REAL ,

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

    theorem :: FDIFF_9:1

    

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

    proof

      

       A1: cos is_differentiable_in x by SIN_COS: 63;

      assume

       A2: ( cos . x) <> 0 ;

      

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

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

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

      hence thesis by A2, A1, FDIFF_2: 15;

    end;

    theorem :: FDIFF_9:2

    

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

    proof

      

       A1: sin is_differentiable_in x by SIN_COS: 64;

      assume

       A2: ( sin . x) <> 0 ;

      

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

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

      hence thesis by A2, A1, FDIFF_2: 15;

    end;

    theorem :: FDIFF_9:3

    

     Th3: ((1 / x) #Z n) = (1 / (x #Z n))

    proof

      ((1 / x) #Z n) = ((1 / x) |^ n) by PREPOWER: 36

      .= (1 / (x |^ n)) by PREPOWER: 7;

      hence thesis by PREPOWER: 36;

    end;

    theorem :: FDIFF_9:4

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

    proof

      assume Z c= ( dom sec );

      then for x st x in Z holds ( cos . x) <> 0 by RFUNCT_1: 3;

      hence thesis by FDIFF_4: 39;

    end;

    theorem :: FDIFF_9:5

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

    proof

      assume Z c= ( dom cosec );

      then for x st x in Z holds ( sin . x) <> 0 by RFUNCT_1: 3;

      hence thesis by FDIFF_4: 40;

    end;

    theorem :: FDIFF_9:6

    

     Th6: Z c= ( dom ( sec * f)) & (for x st x in Z holds (f . x) = ((a * x) + b)) implies ( sec * f) is_differentiable_on Z & for x st x in Z holds ((( sec * f) `| Z) . x) = ((a * ( sin . ((a * x) + b))) / (( cos . ((a * x) + b)) ^2 ))

    proof

      assume that

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

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

      ( dom ( sec * f)) c= ( dom f) by RELAT_1: 25;

      then

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

      then

       A4: f is_differentiable_on Z by A2, FDIFF_1: 23;

      

       A5: for x st x in Z holds ( cos . (f . x)) <> 0

      proof

        let x;

        assume x in Z;

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

        hence thesis by RFUNCT_1: 3;

      end;

      

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

      proof

        let x;

        assume

         A7: x in Z;

        then ( cos . (f . x)) <> 0 by A5;

        then

         A8: sec is_differentiable_in (f . x) by Th1;

        f is_differentiable_in x by A4, A7, FDIFF_1: 9;

        hence thesis by A8, FDIFF_2: 13;

      end;

      then

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

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

      proof

        let x;

        assume

         A10: x in Z;

        then

         A11: f is_differentiable_in x by A4, FDIFF_1: 9;

        

         A12: ( cos . (f . x)) <> 0 by A5, A10;

        then sec is_differentiable_in (f . x) by Th1;

        

        then ( diff (( sec * f),x)) = (( diff ( sec ,(f . x))) * ( diff (f,x))) by A11, FDIFF_2: 13

        .= ((( sin . (f . x)) / (( cos . (f . x)) ^2 )) * ( diff (f,x))) by A12, Th1

        .= (( diff (f,x)) * (( sin . (f . x)) / (( cos . ((a * x) + b)) ^2 ))) by A2, A10

        .= (((f `| Z) . x) * (( sin . (f . x)) / (( cos . ((a * x) + b)) ^2 ))) by A4, A10, FDIFF_1:def 7

        .= (a * (( sin . (f . x)) / (( cos . ((a * x) + b)) ^2 ))) by A2, A3, A10, FDIFF_1: 23

        .= (a * (( sin . ((a * x) + b)) / (( cos . ((a * x) + b)) ^2 ))) by A2, A10;

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

      end;

      hence thesis by A1, A6, FDIFF_1: 9;

    end;

    theorem :: FDIFF_9:7

    

     Th7: Z c= ( dom ( cosec * f)) & (for x st x in Z holds (f . x) = ((a * x) + b)) implies ( cosec * f) is_differentiable_on Z & for x st x in Z holds ((( cosec * f) `| Z) . x) = ( - ((a * ( cos . ((a * x) + b))) / (( sin . ((a * x) + b)) ^2 )))

    proof

      assume that

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

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

      ( dom ( cosec * f)) c= ( dom f) by RELAT_1: 25;

      then

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

      then

       A4: f is_differentiable_on Z by A2, FDIFF_1: 23;

      

       A5: for x st x in Z holds ( sin . (f . x)) <> 0

      proof

        let x;

        assume x in Z;

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

        hence thesis by RFUNCT_1: 3;

      end;

      

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

      proof

        let x;

        assume

         A7: x in Z;

        then ( sin . (f . x)) <> 0 by A5;

        then

         A8: cosec is_differentiable_in (f . x) by Th2;

        f is_differentiable_in x by A4, A7, FDIFF_1: 9;

        hence thesis by A8, FDIFF_2: 13;

      end;

      then

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

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

      proof

        let x;

        assume

         A10: x in Z;

        then

         A11: f is_differentiable_in x by A4, FDIFF_1: 9;

        

         A12: ( sin . (f . x)) <> 0 by A5, A10;

        then cosec is_differentiable_in (f . x) by Th2;

        

        then ( diff (( cosec * f),x)) = (( diff ( cosec ,(f . x))) * ( diff (f,x))) by A11, FDIFF_2: 13

        .= (( - (( cos . (f . x)) / (( sin . (f . x)) ^2 ))) * ( diff (f,x))) by A12, Th2

        .= (( diff (f,x)) * ( - (( cos . (f . x)) / (( sin . ((a * x) + b)) ^2 )))) by A2, A10

        .= (((f `| Z) . x) * ( - (( cos . (f . x)) / (( sin . ((a * x) + b)) ^2 )))) by A4, A10, FDIFF_1:def 7

        .= (a * ( - (( cos . (f . x)) / (( sin . ((a * x) + b)) ^2 )))) by A2, A3, A10, FDIFF_1: 23

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

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

      end;

      hence thesis by A1, A6, FDIFF_1: 9;

    end;

    theorem :: FDIFF_9:8

     not 0 in Z & Z c= ( dom ( sec * (( id Z) ^ ))) implies ( sec * (( id Z) ^ )) is_differentiable_on Z & for x st x in Z holds ((( sec * (( id Z) ^ )) `| Z) . x) = ( - (( sin . (1 / x)) / ((x ^2 ) * (( cos . (1 / x)) ^2 ))))

    proof

      set f = ( id Z);

      assume that

       A1: not 0 in Z and

       A2: Z c= ( dom ( sec * (f ^ )));

      

       A3: (f ^ ) is_differentiable_on Z by A1, FDIFF_5: 4;

      ( dom ( sec * (f ^ ))) c= ( dom (f ^ )) by RELAT_1: 25;

      then

       A4: Z c= ( dom (f ^ )) by A2, XBOOLE_1: 1;

      

       A5: for x st x in Z holds ( cos . ((f ^ ) . x)) <> 0

      proof

        let x;

        assume x in Z;

        then ((f ^ ) . x) in ( dom sec ) by A2, FUNCT_1: 11;

        hence thesis by RFUNCT_1: 3;

      end;

      

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

      proof

        let x;

        assume

         A7: x in Z;

        then ( cos . ((f ^ ) . x)) <> 0 by A5;

        then

         A8: sec is_differentiable_in ((f ^ ) . x) by Th1;

        (f ^ ) is_differentiable_in x by A3, A7, FDIFF_1: 9;

        hence thesis by A8, FDIFF_2: 13;

      end;

      then

       A9: ( sec * (f ^ )) is_differentiable_on Z by A2, FDIFF_1: 9;

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

      proof

        let x;

        assume

         A10: x in Z;

        then

         A11: (f ^ ) is_differentiable_in x by A3, FDIFF_1: 9;

        

         A12: ( cos . ((f ^ ) . x)) <> 0 by A5, A10;

        then sec is_differentiable_in ((f ^ ) . x) by Th1;

        

        then ( diff (( sec * (f ^ )),x)) = (( diff ( sec ,((f ^ ) . x))) * ( diff ((f ^ ),x))) by A11, FDIFF_2: 13

        .= ((( sin . ((f ^ ) . x)) / (( cos . ((f ^ ) . x)) ^2 )) * ( diff ((f ^ ),x))) by A12, Th1

        .= (( diff ((f ^ ),x)) * (( sin . ((f ^ ) . x)) / (( cos . ((f . x) " )) ^2 ))) by A4, A10, RFUNCT_1:def 2

        .= (( diff ((f ^ ),x)) * (( sin . ((f . x) " )) / (( cos . ((f . x) " )) ^2 ))) by A4, A10, RFUNCT_1:def 2

        .= (( diff ((f ^ ),x)) * (( sin . ((f . x) " )) / (( cos . (1 * (x " ))) ^2 ))) by A10, FUNCT_1: 18

        .= (( diff ((f ^ ),x)) * (( sin . (1 * (x " ))) / (( cos . (1 * (x " ))) ^2 ))) by A10, FUNCT_1: 18

        .= ((((f ^ ) `| Z) . x) * (( sin . (1 * (x " ))) / (( cos . (1 * (x " ))) ^2 ))) by A3, A10, FDIFF_1:def 7

        .= (( - (1 / (x ^2 ))) * (( sin . (1 * (x " ))) / (( cos . (1 * (x " ))) ^2 ))) by A1, A10, FDIFF_5: 4

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

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

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

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

      end;

      hence thesis by A2, A6, FDIFF_1: 9;

    end;

    theorem :: FDIFF_9:9

     not 0 in Z & Z c= ( dom ( cosec * (( id Z) ^ ))) implies ( cosec * (( id Z) ^ )) is_differentiable_on Z & for x st x in Z holds ((( cosec * (( id Z) ^ )) `| Z) . x) = (( cos . (1 / x)) / ((x ^2 ) * (( sin . (1 / x)) ^2 )))

    proof

      set f = ( id Z);

      assume that

       A1: not 0 in Z and

       A2: Z c= ( dom ( cosec * (f ^ )));

      

       A3: (f ^ ) is_differentiable_on Z by A1, FDIFF_5: 4;

      ( dom ( cosec * (f ^ ))) c= ( dom (f ^ )) by RELAT_1: 25;

      then

       A4: Z c= ( dom (f ^ )) by A2, XBOOLE_1: 1;

      

       A5: for x st x in Z holds ( sin . ((f ^ ) . x)) <> 0

      proof

        let x;

        assume x in Z;

        then ((f ^ ) . x) in ( dom cosec ) by A2, FUNCT_1: 11;

        hence thesis by RFUNCT_1: 3;

      end;

      

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

      proof

        let x;

        assume

         A7: x in Z;

        then ( sin . ((f ^ ) . x)) <> 0 by A5;

        then

         A8: cosec is_differentiable_in ((f ^ ) . x) by Th2;

        (f ^ ) is_differentiable_in x by A3, A7, FDIFF_1: 9;

        hence thesis by A8, FDIFF_2: 13;

      end;

      then

       A9: ( cosec * (f ^ )) is_differentiable_on Z by A2, FDIFF_1: 9;

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

      proof

        let x;

        assume

         A10: x in Z;

        then

         A11: (f ^ ) is_differentiable_in x by A3, FDIFF_1: 9;

        

         A12: ( sin . ((f ^ ) . x)) <> 0 by A5, A10;

        then cosec is_differentiable_in ((f ^ ) . x) by Th2;

        

        then ( diff (( cosec * (f ^ )),x)) = (( diff ( cosec ,((f ^ ) . x))) * ( diff ((f ^ ),x))) by A11, FDIFF_2: 13

        .= (( - (( cos . ((f ^ ) . x)) / (( sin . ((f ^ ) . x)) ^2 ))) * ( diff ((f ^ ),x))) by A12, Th2

        .= (( diff ((f ^ ),x)) * ( - (( cos . ((f ^ ) . x)) / (( sin . ((f . x) " )) ^2 )))) by A4, A10, RFUNCT_1:def 2

        .= (( diff ((f ^ ),x)) * ( - (( cos . ((f . x) " )) / (( sin . ((f . x) " )) ^2 )))) by A4, A10, RFUNCT_1:def 2

        .= (( diff ((f ^ ),x)) * ( - (( cos . ((f . x) " )) / (( sin . (1 * (x " ))) ^2 )))) by A10, FUNCT_1: 18

        .= (( diff ((f ^ ),x)) * ( - (( cos . (1 * (x " ))) / (( sin . (1 * (x " ))) ^2 )))) by A10, FUNCT_1: 18

        .= ((((f ^ ) `| Z) . x) * ( - (( cos . (1 * (x " ))) / (( sin . (1 * (x " ))) ^2 )))) by A3, A10, FDIFF_1:def 7

        .= (( - (1 / (x ^2 ))) * ( - (( cos . (1 * (x " ))) / (( sin . (1 * (x " ))) ^2 )))) by A1, A10, FDIFF_5: 4

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

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

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

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

      end;

      hence thesis by A2, A6, FDIFF_1: 9;

    end;

    theorem :: FDIFF_9:10

    Z c= ( dom ( sec * (f1 + (c (#) f2)))) & f2 = ( #Z 2) & (for x st x in Z holds (f1 . x) = (a + (b * x))) implies ( sec * (f1 + (c (#) f2))) is_differentiable_on Z & for x st x in Z holds ((( sec * (f1 + (c (#) f2))) `| Z) . x) = (((b + ((2 * c) * x)) * ( sin . ((a + (b * x)) + (c * (x ^2 ))))) / (( cos . ((a + (b * x)) + (c * (x ^2 )))) ^2 ))

    proof

      assume that

       A1: Z c= ( dom ( sec * (f1 + (c (#) f2)))) and

       A2: f2 = ( #Z 2) and

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

      ( dom ( sec * (f1 + (c (#) f2)))) c= ( dom (f1 + (c (#) f2))) by RELAT_1: 25;

      then

       A4: Z c= ( dom (f1 + (c (#) f2))) by A1, XBOOLE_1: 1;

      then

       A5: (f1 + (c (#) f2)) is_differentiable_on Z by A2, A3, FDIFF_4: 12;

      Z c= (( dom f1) /\ ( dom (c (#) f2))) by A4, VALUED_1:def 1;

      then

       A6: Z c= ( dom (c (#) f2)) by XBOOLE_1: 18;

      

       A7: for x st x in Z holds ( cos . ((f1 + (c (#) f2)) . x)) <> 0

      proof

        let x;

        assume x in Z;

        then ((f1 + (c (#) f2)) . x) in ( dom sec ) by A1, FUNCT_1: 11;

        hence thesis by RFUNCT_1: 3;

      end;

      

       A8: for x st x in Z holds ( sec * (f1 + (c (#) f2))) is_differentiable_in x

      proof

        let x;

        assume

         A9: x in Z;

        then ( cos . ((f1 + (c (#) f2)) . x)) <> 0 by A7;

        then

         A10: sec is_differentiable_in ((f1 + (c (#) f2)) . x) by Th1;

        (f1 + (c (#) f2)) is_differentiable_in x by A5, A9, FDIFF_1: 9;

        hence thesis by A10, FDIFF_2: 13;

      end;

      then

       A11: ( sec * (f1 + (c (#) f2))) is_differentiable_on Z by A1, FDIFF_1: 9;

      for x st x in Z holds ((( sec * (f1 + (c (#) f2))) `| Z) . x) = (((b + ((2 * c) * x)) * ( sin . ((a + (b * x)) + (c * (x ^2 ))))) / (( cos . ((a + (b * x)) + (c * (x ^2 )))) ^2 ))

      proof

        let x;

        assume

         A12: x in Z;

        

        then

         A13: ((f1 + (c (#) f2)) . x) = ((f1 . x) + ((c (#) f2) . x)) by A4, VALUED_1:def 1

        .= ((f1 . x) + (c * (f2 . x))) by A6, A12, VALUED_1:def 5

        .= ((a + (b * x)) + (c * (f2 . x))) by A3, A12

        .= ((a + (b * x)) + (c * (x #Z 2))) by A2, TAYLOR_1:def 1

        .= ((a + (b * x)) + (c * (x |^ 2))) by PREPOWER: 36

        .= ((a + (b * x)) + (c * (x ^2 ))) by NEWTON: 81;

        

         A14: (f1 + (c (#) f2)) is_differentiable_in x by A5, A12, FDIFF_1: 9;

        

         A15: ( cos . ((f1 + (c (#) f2)) . x)) <> 0 by A7, A12;

        then sec is_differentiable_in ((f1 + (c (#) f2)) . x) by Th1;

        

        then ( diff (( sec * (f1 + (c (#) f2))),x)) = (( diff ( sec ,((f1 + (c (#) f2)) . x))) * ( diff ((f1 + (c (#) f2)),x))) by A14, FDIFF_2: 13

        .= ((( sin . ((f1 + (c (#) f2)) . x)) / (( cos . ((f1 + (c (#) f2)) . x)) ^2 )) * ( diff ((f1 + (c (#) f2)),x))) by A15, Th1

        .= ((((f1 + (c (#) f2)) `| Z) . x) * (( sin . ((a + (b * x)) + (c * (x ^2 )))) / (( cos . ((a + (b * x)) + (c * (x ^2 )))) ^2 ))) by A5, A12, A13, FDIFF_1:def 7

        .= ((b + ((2 * c) * x)) * (( sin . ((a + (b * x)) + (c * (x ^2 )))) / (( cos . ((a + (b * x)) + (c * (x ^2 )))) ^2 ))) by A2, A3, A4, A12, FDIFF_4: 12;

        hence thesis by A11, A12, FDIFF_1:def 7;

      end;

      hence thesis by A1, A8, FDIFF_1: 9;

    end;

    theorem :: FDIFF_9:11

    Z c= ( dom ( cosec * (f1 + (c (#) f2)))) & f2 = ( #Z 2) & (for x st x in Z holds (f1 . x) = (a + (b * x))) implies ( cosec * (f1 + (c (#) f2))) is_differentiable_on Z & for x st x in Z holds ((( cosec * (f1 + (c (#) f2))) `| Z) . x) = ( - (((b + ((2 * c) * x)) * ( cos . ((a + (b * x)) + (c * (x ^2 ))))) / (( sin . ((a + (b * x)) + (c * (x ^2 )))) ^2 )))

    proof

      assume that

       A1: Z c= ( dom ( cosec * (f1 + (c (#) f2)))) and

       A2: f2 = ( #Z 2) and

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

      ( dom ( cosec * (f1 + (c (#) f2)))) c= ( dom (f1 + (c (#) f2))) by RELAT_1: 25;

      then

       A4: Z c= ( dom (f1 + (c (#) f2))) by A1, XBOOLE_1: 1;

      then

       A5: (f1 + (c (#) f2)) is_differentiable_on Z by A2, A3, FDIFF_4: 12;

      Z c= (( dom f1) /\ ( dom (c (#) f2))) by A4, VALUED_1:def 1;

      then

       A6: Z c= ( dom (c (#) f2)) by XBOOLE_1: 18;

      

       A7: for x st x in Z holds ( sin . ((f1 + (c (#) f2)) . x)) <> 0

      proof

        let x;

        assume x in Z;

        then ((f1 + (c (#) f2)) . x) in ( dom cosec ) by A1, FUNCT_1: 11;

        hence thesis by RFUNCT_1: 3;

      end;

      

       A8: for x st x in Z holds ( cosec * (f1 + (c (#) f2))) is_differentiable_in x

      proof

        let x;

        assume

         A9: x in Z;

        then ( sin . ((f1 + (c (#) f2)) . x)) <> 0 by A7;

        then

         A10: cosec is_differentiable_in ((f1 + (c (#) f2)) . x) by Th2;

        (f1 + (c (#) f2)) is_differentiable_in x by A5, A9, FDIFF_1: 9;

        hence thesis by A10, FDIFF_2: 13;

      end;

      then

       A11: ( cosec * (f1 + (c (#) f2))) is_differentiable_on Z by A1, FDIFF_1: 9;

      for x st x in Z holds ((( cosec * (f1 + (c (#) f2))) `| Z) . x) = ( - (((b + ((2 * c) * x)) * ( cos . ((a + (b * x)) + (c * (x ^2 ))))) / (( sin . ((a + (b * x)) + (c * (x ^2 )))) ^2 )))

      proof

        let x;

        assume

         A12: x in Z;

        

        then

         A13: ((f1 + (c (#) f2)) . x) = ((f1 . x) + ((c (#) f2) . x)) by A4, VALUED_1:def 1

        .= ((f1 . x) + (c * (f2 . x))) by A6, A12, VALUED_1:def 5

        .= ((a + (b * x)) + (c * (f2 . x))) by A3, A12

        .= ((a + (b * x)) + (c * (x #Z 2))) by A2, TAYLOR_1:def 1

        .= ((a + (b * x)) + (c * (x |^ 2))) by PREPOWER: 36

        .= ((a + (b * x)) + (c * (x ^2 ))) by NEWTON: 81;

        

         A14: (f1 + (c (#) f2)) is_differentiable_in x by A5, A12, FDIFF_1: 9;

        

         A15: ( sin . ((f1 + (c (#) f2)) . x)) <> 0 by A7, A12;

        then cosec is_differentiable_in ((f1 + (c (#) f2)) . x) by Th2;

        

        then ( diff (( cosec * (f1 + (c (#) f2))),x)) = (( diff ( cosec ,((f1 + (c (#) f2)) . x))) * ( diff ((f1 + (c (#) f2)),x))) by A14, FDIFF_2: 13

        .= (( - (( cos . ((f1 + (c (#) f2)) . x)) / (( sin . ((f1 + (c (#) f2)) . x)) ^2 ))) * ( diff ((f1 + (c (#) f2)),x))) by A15, Th2

        .= ((((f1 + (c (#) f2)) `| Z) . x) * ( - (( cos . ((a + (b * x)) + (c * (x ^2 )))) / (( sin . ((a + (b * x)) + (c * (x ^2 )))) ^2 )))) by A5, A12, A13, FDIFF_1:def 7

        .= ((b + ((2 * c) * x)) * ( - (( cos . ((a + (b * x)) + (c * (x ^2 )))) / (( sin . ((a + (b * x)) + (c * (x ^2 )))) ^2 )))) by A2, A3, A4, A12, FDIFF_4: 12;

        hence thesis by A11, A12, FDIFF_1:def 7;

      end;

      hence thesis by A1, A8, FDIFF_1: 9;

    end;

    theorem :: FDIFF_9:12

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

    proof

      assume

       A1: Z c= ( dom ( sec * exp_R ));

      

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

      proof

        let x;

        assume x in Z;

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

        hence thesis by RFUNCT_1: 3;

      end;

      

       A3: for x st x in Z holds ( sec * exp_R ) is_differentiable_in x

      proof

        let x;

        assume x in Z;

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

        then exp_R is_differentiable_in x & sec is_differentiable_in ( exp_R . x) by Th1, SIN_COS: 65;

        hence thesis by FDIFF_2: 13;

      end;

      then

       A4: ( sec * exp_R ) is_differentiable_on Z by A1, FDIFF_1: 9;

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

      proof

        let x;

        assume

         A5: x in Z;

        then

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

        then exp_R is_differentiable_in x & sec is_differentiable_in ( exp_R . x) by Th1, SIN_COS: 65;

        

        then ( diff (( sec * exp_R ),x)) = (( diff ( sec ,( exp_R . x))) * ( diff ( exp_R ,x))) by FDIFF_2: 13

        .= ((( sin . ( exp_R . x)) / (( cos . ( exp_R . x)) ^2 )) * ( diff ( exp_R ,x))) by A6, Th1

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

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

      end;

      hence thesis by A1, A3, FDIFF_1: 9;

    end;

    theorem :: FDIFF_9:13

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

    proof

      assume

       A1: Z c= ( dom ( cosec * exp_R ));

      

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

      proof

        let x;

        assume x in Z;

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

        hence thesis by RFUNCT_1: 3;

      end;

      

       A3: for x st x in Z holds ( cosec * exp_R ) is_differentiable_in x

      proof

        let x;

        assume x in Z;

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

        then exp_R is_differentiable_in x & cosec is_differentiable_in ( exp_R . x) by Th2, SIN_COS: 65;

        hence thesis by FDIFF_2: 13;

      end;

      then

       A4: ( cosec * exp_R ) is_differentiable_on Z by A1, FDIFF_1: 9;

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

      proof

        let x;

        assume

         A5: x in Z;

        then

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

        then exp_R is_differentiable_in x & cosec is_differentiable_in ( exp_R . x) by Th2, SIN_COS: 65;

        

        then ( diff (( cosec * exp_R ),x)) = (( diff ( cosec ,( exp_R . x))) * ( diff ( exp_R ,x))) by FDIFF_2: 13

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

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

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

      end;

      hence thesis by A1, A3, FDIFF_1: 9;

    end;

    

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

    theorem :: FDIFF_9:14

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

    proof

      assume

       A1: Z c= ( dom ( sec * ln ));

      ( dom ( sec * ln )) c= ( dom ln ) by RELAT_1: 25;

      then

       A2: Z c= ( dom ln ) by A1, XBOOLE_1: 1;

      

       A3: for x st x in Z holds x > 0

      proof

        let x;

        assume x in Z;

        then x in ( right_open_halfline 0 ) by A2, TAYLOR_1: 18;

        then ex g be Real st x = g & 0 < g by Lm1;

        hence thesis;

      end;

      

       A4: for x st x in Z holds ( diff ( ln ,x)) = (1 / x)

      proof

        let x;

        assume x in Z;

        then x > 0 by A3;

        then x in ( right_open_halfline 0 ) by Lm1;

        hence thesis by TAYLOR_1: 18;

      end;

      

       A5: for x st x in Z holds ( cos . ( ln . x)) <> 0

      proof

        let x;

        assume x in Z;

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

        hence thesis by RFUNCT_1: 3;

      end;

      

       A6: for x st x in Z holds ( sec * ln ) is_differentiable_in x

      proof

        let x;

        assume

         A7: x in Z;

        then ( cos . ( ln . x)) <> 0 by A5;

        then

         A8: sec is_differentiable_in ( ln . x) by Th1;

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

        hence thesis by A8, FDIFF_2: 13;

      end;

      then

       A9: ( sec * ln ) is_differentiable_on Z by A1, FDIFF_1: 9;

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

      proof

        let x;

        assume

         A10: x in Z;

        then

         A11: ln is_differentiable_in x by A3, TAYLOR_1: 18;

        

         A12: ( cos . ( ln . x)) <> 0 by A5, A10;

        then sec is_differentiable_in ( ln . x) by Th1;

        

        then ( diff (( sec * ln ),x)) = (( diff ( sec ,( ln . x))) * ( diff ( ln ,x))) by A11, FDIFF_2: 13

        .= ((( sin . ( ln . x)) / (( cos . ( ln . x)) ^2 )) * ( diff ( ln ,x))) by A12, Th1

        .= ((1 / x) * (( sin . ( ln . x)) / (( cos . ( ln . x)) ^2 ))) by A4, A10

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

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

      end;

      hence thesis by A1, A6, FDIFF_1: 9;

    end;

    theorem :: FDIFF_9:15

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

    proof

      assume

       A1: Z c= ( dom ( cosec * ln ));

      ( dom ( cosec * ln )) c= ( dom ln ) by RELAT_1: 25;

      then

       A2: Z c= ( dom ln ) by A1, XBOOLE_1: 1;

      

       A3: for x st x in Z holds x > 0

      proof

        let x;

        assume x in Z;

        then x in ( right_open_halfline 0 ) by A2, TAYLOR_1: 18;

        then ex g be Real st x = g & 0 < g by Lm1;

        hence thesis;

      end;

      

       A4: for x st x in Z holds ( diff ( ln ,x)) = (1 / x)

      proof

        let x;

        assume x in Z;

        then x > 0 by A3;

        then x in ( right_open_halfline 0 ) by Lm1;

        hence thesis by TAYLOR_1: 18;

      end;

      

       A5: for x st x in Z holds ( sin . ( ln . x)) <> 0

      proof

        let x;

        assume x in Z;

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

        hence thesis by RFUNCT_1: 3;

      end;

      

       A6: for x st x in Z holds ( cosec * ln ) is_differentiable_in x

      proof

        let x;

        assume

         A7: x in Z;

        then ( sin . ( ln . x)) <> 0 by A5;

        then

         A8: cosec is_differentiable_in ( ln . x) by Th2;

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

        hence thesis by A8, FDIFF_2: 13;

      end;

      then

       A9: ( cosec * ln ) is_differentiable_on Z by A1, FDIFF_1: 9;

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

      proof

        let x;

        assume

         A10: x in Z;

        then

         A11: ln is_differentiable_in x by A3, TAYLOR_1: 18;

        

         A12: ( sin . ( ln . x)) <> 0 by A5, A10;

        then cosec is_differentiable_in ( ln . x) by Th2;

        

        then ( diff (( cosec * ln ),x)) = (( diff ( cosec ,( ln . x))) * ( diff ( ln ,x))) by A11, FDIFF_2: 13

        .= (( - (( cos . ( ln . x)) / (( sin . ( ln . x)) ^2 ))) * ( diff ( ln ,x))) by A12, Th2

        .= ((1 / x) * (( - ( cos . ( ln . x))) / (( sin . ( ln . x)) ^2 ))) by A4, A10

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

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

      end;

      hence thesis by A1, A6, FDIFF_1: 9;

    end;

    theorem :: FDIFF_9:16

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

    proof

      assume

       A1: Z c= ( dom ( exp_R * sec ));

      

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

      proof

        let x;

        assume x in Z;

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

        hence thesis by RFUNCT_1: 3;

      end;

      

       A3: for x st x in Z holds ( exp_R * sec ) is_differentiable_in x

      proof

        let x;

        assume x in Z;

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

        then

         A4: sec is_differentiable_in x by Th1;

         exp_R is_differentiable_in ( sec . x) by SIN_COS: 65;

        hence thesis by A4, FDIFF_2: 13;

      end;

      then

       A5: ( exp_R * sec ) is_differentiable_on Z by A1, FDIFF_1: 9;

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

      proof

        let x;

        

         A6: exp_R is_differentiable_in ( sec . x) by SIN_COS: 65;

        assume

         A7: x in Z;

        then

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

        then sec is_differentiable_in x by Th1;

        

        then ( diff (( exp_R * sec ),x)) = (( diff ( exp_R ,( sec . x))) * ( diff ( sec ,x))) by A6, FDIFF_2: 13

        .= (( diff ( exp_R ,( sec . x))) * (( sin . x) / (( cos . x) ^2 ))) by A8, Th1

        .= (( exp_R . ( sec . x)) * (( sin . x) / (( cos . x) ^2 ))) by SIN_COS: 65;

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

      end;

      hence thesis by A1, A3, FDIFF_1: 9;

    end;

    theorem :: FDIFF_9:17

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

    proof

      assume

       A1: Z c= ( dom ( exp_R * cosec ));

      

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

      proof

        let x;

        assume x in Z;

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

        hence thesis by RFUNCT_1: 3;

      end;

      

       A3: for x st x in Z holds ( exp_R * cosec ) is_differentiable_in x

      proof

        let x;

        assume x in Z;

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

        then

         A4: cosec is_differentiable_in x by Th2;

         exp_R is_differentiable_in ( cosec . x) by SIN_COS: 65;

        hence thesis by A4, FDIFF_2: 13;

      end;

      then

       A5: ( exp_R * cosec ) is_differentiable_on Z by A1, FDIFF_1: 9;

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

      proof

        let x;

        

         A6: exp_R is_differentiable_in ( cosec . x) by SIN_COS: 65;

        assume

         A7: x in Z;

        then

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

        then cosec is_differentiable_in x by Th2;

        

        then ( diff (( exp_R * cosec ),x)) = (( diff ( exp_R ,( cosec . x))) * ( diff ( cosec ,x))) by A6, FDIFF_2: 13

        .= (( diff ( exp_R ,( cosec . x))) * ( - (( cos . x) / (( sin . x) ^2 )))) by A8, Th2

        .= (( exp_R . ( cosec . x)) * ( - (( cos . x) / (( sin . x) ^2 )))) by SIN_COS: 65;

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

      end;

      hence thesis by A1, A3, FDIFF_1: 9;

    end;

    theorem :: FDIFF_9:18

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

    proof

      assume

       A1: Z c= ( dom ( ln * sec ));

      

       A2: for x st x in Z holds ( sec . x) > 0

      proof

        let x;

        assume x in Z;

        then ( sec . x) in ( right_open_halfline 0 ) by A1, FUNCT_1: 11, TAYLOR_1: 18;

        then ex g be Real st ( sec . x) = g & 0 < g by Lm1;

        hence thesis;

      end;

      ( dom ( ln * sec )) c= ( dom sec ) by RELAT_1: 25;

      then

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

      

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

      proof

        let x;

        assume x in Z;

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

        hence thesis by RFUNCT_1: 3;

      end;

      

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

        hence thesis by Th1;

      end;

      

       A6: for x st x in Z holds ( ln * sec ) is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then sec is_differentiable_in x & ( sec . x) > 0 by A2, A5;

        hence thesis by TAYLOR_1: 20;

      end;

      then

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

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

      proof

        let x;

        assume

         A8: x in Z;

        then

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

         sec is_differentiable_in x & ( sec . x) > 0 by A2, A5, A8;

        

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

        .= ((( sin . x) / (( cos . x) ^2 )) / ( sec . x)) by A9, Th1

        .= ((( sin . x) / (( cos . x) ^2 )) / (( cos . x) " )) by A3, A8, RFUNCT_1:def 2

        .= ((( sin . x) * ( cos . x)) / (( cos . x) * ( cos . x)))

        .= (( sin . x) / ( cos . x)) by A4, A8, XCMPLX_1: 91;

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

      end;

      hence thesis by A1, A6, FDIFF_1: 9;

    end;

    theorem :: FDIFF_9:19

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

    proof

      assume

       A1: Z c= ( dom ( ln * cosec ));

      

       A2: for x st x in Z holds ( cosec . x) > 0

      proof

        let x;

        assume x in Z;

        then ( cosec . x) in ( right_open_halfline 0 ) by A1, FUNCT_1: 11, TAYLOR_1: 18;

        then ex g be Real st ( cosec . x) = g & 0 < g by Lm1;

        hence thesis;

      end;

      ( dom ( ln * cosec )) c= ( dom cosec ) by RELAT_1: 25;

      then

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

      

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

      proof

        let x;

        assume x in Z;

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

        hence thesis by RFUNCT_1: 3;

      end;

      

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

        hence thesis by Th2;

      end;

      

       A6: for x st x in Z holds ( ln * cosec ) is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then cosec is_differentiable_in x & ( cosec . x) > 0 by A2, A5;

        hence thesis by TAYLOR_1: 20;

      end;

      then

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

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

      proof

        let x;

        assume

         A8: x in Z;

        then

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

         cosec is_differentiable_in x & ( cosec . x) > 0 by A2, A5, A8;

        

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

        .= (( - (( cos . x) / (( sin . x) ^2 ))) / ( cosec . x)) by A9, Th2

        .= (( - (( cos . x) / (( sin . x) ^2 ))) / (( sin . x) " )) by A3, A8, RFUNCT_1:def 2

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

        .= (( - ( cos . x)) / ( sin . x)) by A4, A8, XCMPLX_1: 91;

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

      end;

      hence thesis by A1, A6, FDIFF_1: 9;

    end;

    theorem :: FDIFF_9:20

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

    proof

      assume that

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

       A2: 1 <= n;

      ( dom (( #Z n) * sec )) c= ( dom sec ) by RELAT_1: 25;

      then

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

      

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

      proof

        let x;

        assume x in Z;

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

        hence thesis by RFUNCT_1: 3;

      end;

      

       A5: for x st x in Z holds (( #Z n) * sec ) is_differentiable_in x

      proof

        let x;

        assume x in Z;

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

        then sec is_differentiable_in x by Th1;

        hence thesis by TAYLOR_1: 3;

      end;

      then

       A6: (( #Z n) * sec ) is_differentiable_on Z by A1, FDIFF_1: 9;

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

      proof

        set m = (n - 1);

        let x;

        

         A7: ex m be Nat st n = (m + 1) by A2, NAT_1: 6;

        assume

         A8: x in Z;

        then

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

        then

         A10: sec is_differentiable_in x by Th1;

        (((( #Z n) * sec ) `| Z) . x) = ( diff ((( #Z n) * sec ),x)) by A6, A8, FDIFF_1:def 7

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

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

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

        .= ((n * (1 / (( cos . x) #Z m))) * (( sin . x) / (( cos . x) ^2 ))) by A7, Th3

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

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

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

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

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

        hence thesis;

      end;

      hence thesis by A1, A5, FDIFF_1: 9;

    end;

    theorem :: FDIFF_9:21

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

    proof

      assume that

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

       A2: 1 <= n;

      ( dom (( #Z n) * cosec )) c= ( dom cosec ) by RELAT_1: 25;

      then

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

      

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

      proof

        let x;

        assume x in Z;

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

        hence thesis by RFUNCT_1: 3;

      end;

      

       A5: for x st x in Z holds (( #Z n) * cosec ) is_differentiable_in x

      proof

        let x;

        assume x in Z;

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

        then cosec is_differentiable_in x by Th2;

        hence thesis by TAYLOR_1: 3;

      end;

      then

       A6: (( #Z n) * cosec ) is_differentiable_on Z by A1, FDIFF_1: 9;

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

      proof

        set m = (n - 1);

        let x;

        

         A7: ex m be Nat st n = (m + 1) by A2, NAT_1: 6;

        assume

         A8: x in Z;

        then

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

        then

         A10: cosec is_differentiable_in x by Th2;

        (((( #Z n) * cosec ) `| Z) . x) = ( diff ((( #Z n) * cosec ),x)) by A6, A8, FDIFF_1:def 7

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

        .= ((n * (( cosec . x) #Z (n - 1))) * ( - (( cos . x) / (( sin . x) ^2 )))) by A9, Th2

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

        .= ((n * (1 / (( sin . x) #Z m))) * ( - (( cos . x) / (( sin . x) ^2 )))) by A7, Th3

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

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

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

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

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

        hence thesis;

      end;

      hence thesis by A1, A5, FDIFF_1: 9;

    end;

    theorem :: FDIFF_9:22

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

    proof

      

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

      assume

       A2: Z c= ( dom ( sec - ( id Z)));

      then

       A3: Z c= (( dom sec ) /\ ( dom ( id Z))) by VALUED_1: 12;

      then

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

      

       A5: Z c= ( dom ( id Z)) by A3, XBOOLE_1: 18;

      then

       A6: ( id Z) is_differentiable_on Z by A1, FDIFF_1: 23;

      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 Th1;

      end;

      then

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

      for x st x in Z holds ((( sec - ( id Z)) `| Z) . x) = ((( sin . x) - (( cos . x) ^2 )) / (( cos . x) ^2 ))

      proof

        let x;

        assume

         A8: x in Z;

        then

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

        then

         A10: (( cos . x) ^2 ) > 0 by SQUARE_1: 12;

        ((( sec - ( id Z)) `| Z) . x) = (( diff ( sec ,x)) - ( diff (( id Z),x))) by A2, A6, A7, A8, FDIFF_1: 19

        .= ((( sin . x) / (( cos . x) ^2 )) - ( diff (( id Z),x))) by A9, Th1

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

        .= ((( sin . x) / (( cos . x) ^2 )) - 1) by A5, A1, A8, FDIFF_1: 23

        .= ((( sin . x) / (( cos . x) ^2 )) - ((( cos . x) ^2 ) / (( cos . x) ^2 ))) by A10, XCMPLX_1: 60

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

        hence thesis;

      end;

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

    end;

    theorem :: FDIFF_9:23

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

    proof

      set f = ( - cosec );

      

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

      assume

       A2: Z c= ( dom (( - cosec ) - ( id Z)));

      then

       A3: Z c= (( dom ( - cosec )) /\ ( dom ( id Z))) by VALUED_1: 12;

      then

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

      then

       A5: Z c= ( dom cosec ) by VALUED_1: 8;

      for x st x in Z holds cosec is_differentiable_in x

      proof

        let x;

        assume x in Z;

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

        hence thesis by Th2;

      end;

      then

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

      then

       A7: (( - 1) (#) cosec ) is_differentiable_on Z by A4, FDIFF_1: 20;

      

       A8: Z c= ( dom ( id Z)) by A3, XBOOLE_1: 18;

      then

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

      for x st x in Z holds (((( - cosec ) - ( id Z)) `| Z) . x) = ((( cos . x) - (( sin . x) ^2 )) / (( sin . x) ^2 ))

      proof

        let x;

        assume

         A10: x in Z;

        then

         A11: ( sin . x) <> 0 by A5, RFUNCT_1: 3;

        then

         A12: (( sin . x) ^2 ) > 0 by SQUARE_1: 12;

        (((f - ( id Z)) `| Z) . x) = (( diff (f,x)) - ( diff (( id Z),x))) by A2, A9, A7, A10, FDIFF_1: 19

        .= ((((( - 1) (#) cosec ) `| Z) . x) - ( diff (( id Z),x))) by A7, A10, FDIFF_1:def 7

        .= ((( - 1) * ( diff ( cosec ,x))) - ( diff (( id Z),x))) by A4, A6, A10, FDIFF_1: 20

        .= ((( - 1) * ( - (( cos . x) / (( sin . x) ^2 )))) - ( diff (( id Z),x))) by A11, Th2

        .= ((( cos . x) / (( sin . x) ^2 )) - ((( id Z) `| Z) . x)) by A9, A10, FDIFF_1:def 7

        .= ((( cos . x) / (( sin . x) ^2 )) - 1) by A8, A1, A10, FDIFF_1: 23

        .= ((( cos . x) / (( sin . x) ^2 )) - ((( sin . x) ^2 ) / (( sin . x) ^2 ))) by A12, XCMPLX_1: 60

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

        hence thesis;

      end;

      hence thesis by A2, A9, A7, FDIFF_1: 19;

    end;

    theorem :: FDIFF_9:24

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

    proof

      

       A1: for x st x in Z holds exp_R is_differentiable_in x by SIN_COS: 65;

      assume

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

      then

       A3: Z c= (( dom exp_R ) /\ ( dom sec )) by VALUED_1:def 4;

      then

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

      Z c= ( dom exp_R ) by A3, XBOOLE_1: 18;

      then

       A5: exp_R is_differentiable_on Z by A1, FDIFF_1: 9;

      

       A6: for x st x in Z holds sec is_differentiable_in x & ( diff ( sec ,x)) = (( sin . x) / (( cos . x) ^2 ))

      proof

        let x;

        assume x in Z;

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

        hence thesis by Th1;

      end;

      then for x st x in Z holds sec is_differentiable_in x;

      then

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

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

      proof

        let x;

        assume

         A8: x in Z;

        

        then ((( exp_R (#) sec ) `| Z) . x) = ((( sec . x) * ( diff ( exp_R ,x))) + (( exp_R . x) * ( diff ( sec ,x)))) by A2, A5, A7, FDIFF_1: 21

        .= ((( sec . x) * ( exp_R . x)) + (( exp_R . x) * ( diff ( sec ,x)))) by SIN_COS: 65

        .= ((( sec . x) * ( exp_R . x)) + (( exp_R . x) * (( sin . x) / (( cos . x) ^2 )))) by A6, A8

        .= ((( exp_R . x) / ( cos . x)) + ((( exp_R . x) * ( sin . x)) / (( cos . x) ^2 ))) by A4, A8, RFUNCT_1:def 2;

        hence thesis;

      end;

      hence thesis by A2, A5, A7, FDIFF_1: 21;

    end;

    theorem :: FDIFF_9:25

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

    proof

      

       A1: for x st x in Z holds exp_R is_differentiable_in x by SIN_COS: 65;

      assume

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

      then

       A3: Z c= (( dom exp_R ) /\ ( dom cosec )) by VALUED_1:def 4;

      then

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

      Z c= ( dom exp_R ) by A3, XBOOLE_1: 18;

      then

       A5: exp_R is_differentiable_on Z by A1, FDIFF_1: 9;

      

       A6: for x st x in Z holds cosec is_differentiable_in x & ( diff ( cosec ,x)) = ( - (( cos . x) / (( sin . x) ^2 )))

      proof

        let x;

        assume x in Z;

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

        hence thesis by Th2;

      end;

      then for x st x in Z holds cosec is_differentiable_in x;

      then

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

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

      proof

        let x;

        assume

         A8: x in Z;

        

        then ((( exp_R (#) cosec ) `| Z) . x) = ((( cosec . x) * ( diff ( exp_R ,x))) + (( exp_R . x) * ( diff ( cosec ,x)))) by A2, A5, A7, FDIFF_1: 21

        .= ((( cosec . x) * ( exp_R . x)) + (( exp_R . x) * ( diff ( cosec ,x)))) by SIN_COS: 65

        .= ((( cosec . x) * ( exp_R . x)) + (( exp_R . x) * ( - (( cos . x) / (( sin . x) ^2 ))))) by A6, A8

        .= ((( exp_R . x) / ( sin . x)) + ((( exp_R . x) * ( - ( cos . x))) / (( sin . x) ^2 ))) by A4, A8, RFUNCT_1:def 2;

        hence thesis;

      end;

      hence thesis by A2, A5, A7, FDIFF_1: 21;

    end;

    theorem :: FDIFF_9:26

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

    proof

      assume that

       A1: Z c= ( dom (((1 / a) (#) ( sec * f)) - ( id Z))) and

       A2: for x st x in Z holds (f . x) = (a * x) & a <> 0 ;

      

       A3: Z c= (( dom ((1 / a) (#) ( sec * f))) /\ ( dom ( id Z))) by A1, VALUED_1: 12;

      then

       A4: Z c= ( dom ((1 / a) (#) ( sec * f))) by XBOOLE_1: 18;

      then

       A5: Z c= ( dom ( sec * f)) by VALUED_1:def 5;

      

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

      then

       A7: ( sec * f) is_differentiable_on Z by A5, Th6;

      then

       A8: ((1 / a) (#) ( sec * f)) is_differentiable_on Z by A4, FDIFF_1: 20;

      set g = ((1 / a) (#) ( sec * f));

      

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

      

       A10: Z c= ( dom ( id Z)) by A3, XBOOLE_1: 18;

      then

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

      

       A12: for x st x in Z holds ( cos . (f . x)) <> 0

      proof

        let x;

        assume x in Z;

        then (f . x) in ( dom sec ) by A5, FUNCT_1: 11;

        hence thesis by RFUNCT_1: 3;

      end;

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

      proof

        let x;

        assume

         A13: x in Z;

        then

         A14: (f . x) = ((a * x) + 0 ) by A2;

        ( cos . (f . x)) <> 0 by A12, A13;

        then

         A15: (( cos . (a * x)) ^2 ) > 0 by A14, SQUARE_1: 12;

        (((g - ( id Z)) `| Z) . x) = (( diff (g,x)) - ( diff (( id Z),x))) by A1, A8, A11, A13, FDIFF_1: 19

        .= (((g `| Z) . x) - ( diff (( id Z),x))) by A8, A13, FDIFF_1:def 7

        .= (((1 / a) * ( diff (( sec * f),x))) - ( diff (( id Z),x))) by A4, A7, A13, FDIFF_1: 20

        .= (((1 / a) * ((( sec * f) `| Z) . x)) - ( diff (( id Z),x))) by A7, A13, FDIFF_1:def 7

        .= (((1 / a) * ((( sec * f) `| Z) . x)) - ((( id Z) `| Z) . x)) by A11, A13, FDIFF_1:def 7

        .= (((1 / a) * ((a * ( sin . (a * x))) / (( cos . (a * x)) ^2 ))) - ((( id Z) `| Z) . x)) by A5, A6, A13, A14, Th6

        .= (((1 / a) * ((a * ( sin . (a * x))) / (( cos . (a * x)) ^2 ))) - 1) by A10, A9, A13, FDIFF_1: 23

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

        .= ((( sin . (a * x)) / (( cos . (a * x)) ^2 )) - 1) by A2, A13, XCMPLX_1: 91

        .= ((( sin . (a * x)) / (( cos . (a * x)) ^2 )) - ((( cos . (a * x)) ^2 ) / (( cos . (a * x)) ^2 ))) by A15, XCMPLX_1: 60

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

        hence thesis;

      end;

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

    end;

    theorem :: FDIFF_9:27

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

    proof

      assume that

       A1: Z c= ( dom ((( - (1 / a)) (#) ( cosec * f)) - ( id Z))) and

       A2: for x st x in Z holds (f . x) = (a * x) & a <> 0 ;

      

       A3: Z c= (( dom (( - (1 / a)) (#) ( cosec * f))) /\ ( dom ( id Z))) by A1, VALUED_1: 12;

      then

       A4: Z c= ( dom (( - (1 / a)) (#) ( cosec * f))) by XBOOLE_1: 18;

      then

       A5: Z c= ( dom ( cosec * f)) by VALUED_1:def 5;

      

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

      then

       A7: ( cosec * f) is_differentiable_on Z by A5, Th7;

      then

       A8: (( - (1 / a)) (#) ( cosec * f)) is_differentiable_on Z by A4, FDIFF_1: 20;

      set g = (( - (1 / a)) (#) ( cosec * f));

      

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

      

       A10: Z c= ( dom ( id Z)) by A3, XBOOLE_1: 18;

      then

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

      

       A12: for x st x in Z holds ( sin . (f . x)) <> 0

      proof

        let x;

        assume x in Z;

        then (f . x) in ( dom cosec ) by A5, FUNCT_1: 11;

        hence thesis by RFUNCT_1: 3;

      end;

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

      proof

        let x;

        assume

         A13: x in Z;

        then

         A14: (f . x) = ((a * x) + 0 ) by A2;

        ( sin . (f . x)) <> 0 by A12, A13;

        then

         A15: (( sin . (a * x)) ^2 ) > 0 by A14, SQUARE_1: 12;

        (((g - ( id Z)) `| Z) . x) = (( diff (g,x)) - ( diff (( id Z),x))) by A1, A8, A11, A13, FDIFF_1: 19

        .= (((g `| Z) . x) - ( diff (( id Z),x))) by A8, A13, FDIFF_1:def 7

        .= ((( - (1 / a)) * ( diff (( cosec * f),x))) - ( diff (( id Z),x))) by A4, A7, A13, FDIFF_1: 20

        .= ((( - (1 / a)) * ((( cosec * f) `| Z) . x)) - ( diff (( id Z),x))) by A7, A13, FDIFF_1:def 7

        .= ((( - (1 / a)) * ((( cosec * f) `| Z) . x)) - ((( id Z) `| Z) . x)) by A11, A13, FDIFF_1:def 7

        .= ((( - (1 / a)) * ( - ((a * ( cos . (a * x))) / (( sin . (a * x)) ^2 )))) - ((( id Z) `| Z) . x)) by A5, A6, A13, A14, Th7

        .= (((( - 1) / a) * ((a * ( - ( cos . (a * x)))) / (( sin . (a * x)) ^2 ))) - 1) by A10, A9, A13, FDIFF_1: 23

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

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

        .= ((( cos . (a * x)) / (( sin . (a * x)) ^2 )) - 1) by A2, A13, XCMPLX_1: 91

        .= ((( cos . (a * x)) / (( sin . (a * x)) ^2 )) - ((( sin . (a * x)) ^2 ) / (( sin . (a * x)) ^2 ))) by A15, XCMPLX_1: 60

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

        hence thesis;

      end;

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

    end;

    theorem :: FDIFF_9:28

    (Z c= ( dom (f (#) sec )) & for x st x in Z holds (f . x) = ((a * x) + b)) implies (f (#) sec ) is_differentiable_on Z & for x st x in Z holds (((f (#) sec ) `| Z) . x) = ((a / ( cos . x)) + ((((a * x) + b) * ( sin . x)) / (( cos . x) ^2 )))

    proof

      assume that

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

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

      

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

      then

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

      

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

      then

       A6: f is_differentiable_on Z by A2, FDIFF_1: 23;

      

       A7: for x st x in Z holds sec is_differentiable_in x & ( diff ( sec ,x)) = (( sin . x) / (( cos . x) ^2 ))

      proof

        let x;

        assume x in Z;

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

        hence thesis by Th1;

      end;

      then for x st x in Z holds sec is_differentiable_in x;

      then

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

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

      proof

        let x;

        assume

         A9: x in Z;

        

        then (((f (#) sec ) `| Z) . x) = ((( sec . x) * ( diff (f,x))) + ((f . x) * ( diff ( sec ,x)))) by A1, A6, A8, FDIFF_1: 21

        .= ((( sec . x) * ((f `| Z) . x)) + ((f . x) * ( diff ( sec ,x)))) by A6, A9, FDIFF_1:def 7

        .= ((( sec . x) * a) + ((f . x) * ( diff ( sec ,x)))) by A2, A5, A9, FDIFF_1: 23

        .= ((( sec . x) * a) + (((a * x) + b) * ( diff ( sec ,x)))) by A2, A9

        .= ((( sec . x) * a) + (((a * x) + b) * (( sin . x) / (( cos . x) ^2 )))) by A7, A9

        .= ((a / ( cos . x)) + ((((a * x) + b) * ( sin . x)) / (( cos . x) ^2 ))) by A4, A9, RFUNCT_1:def 2;

        hence thesis;

      end;

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

    end;

    theorem :: FDIFF_9:29

    (Z c= ( dom (f (#) cosec )) & for x st x in Z holds (f . x) = ((a * x) + b)) implies (f (#) cosec ) is_differentiable_on Z & for x st x in Z holds (((f (#) cosec ) `| Z) . x) = ((a / ( sin . x)) - ((((a * x) + b) * ( cos . x)) / (( sin . x) ^2 )))

    proof

      assume that

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

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

      

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

      then

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

      

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

      then

       A6: f is_differentiable_on Z by A2, FDIFF_1: 23;

      

       A7: for x st x in Z holds cosec is_differentiable_in x & ( diff ( cosec ,x)) = ( - (( cos . x) / (( sin . x) ^2 )))

      proof

        let x;

        assume x in Z;

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

        hence thesis by Th2;

      end;

      then for x st x in Z holds cosec is_differentiable_in x;

      then

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

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

      proof

        let x;

        assume

         A9: x in Z;

        

        then (((f (#) cosec ) `| Z) . x) = ((( cosec . x) * ( diff (f,x))) + ((f . x) * ( diff ( cosec ,x)))) by A1, A6, A8, FDIFF_1: 21

        .= ((( cosec . x) * ((f `| Z) . x)) + ((f . x) * ( diff ( cosec ,x)))) by A6, A9, FDIFF_1:def 7

        .= ((( cosec . x) * a) + ((f . x) * ( diff ( cosec ,x)))) by A2, A5, A9, FDIFF_1: 23

        .= ((( cosec . x) * a) + (((a * x) + b) * ( diff ( cosec ,x)))) by A2, A9

        .= ((( cosec . x) * a) + (((a * x) + b) * ( - (( cos . x) / (( sin . x) ^2 ))))) by A7, A9

        .= ((a / ( sin . x)) - ((((a * x) + b) * ( cos . x)) / (( sin . x) ^2 ))) by A4, A9, RFUNCT_1:def 2;

        hence thesis;

      end;

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

    end;

    theorem :: FDIFF_9:30

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

    proof

      assume

       A1: Z c= ( dom ( ln (#) sec ));

      then

       A2: Z c= (( dom ln ) /\ ( dom sec )) by VALUED_1:def 4;

      then

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

      

       A4: for x st x in Z holds sec is_differentiable_in x & ( diff ( sec ,x)) = (( sin . x) / (( cos . x) ^2 ))

      proof

        let x;

        assume x in Z;

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

        hence thesis by Th1;

      end;

      then for x st x in Z holds sec is_differentiable_in x;

      then

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

      

       A6: Z c= ( dom ln ) by A2, XBOOLE_1: 18;

      

       A7: for x st x in Z holds x > 0

      proof

        let x;

        assume x in Z;

        then x in ( right_open_halfline 0 ) by A6, TAYLOR_1: 18;

        then ex g be Real st x = g & 0 < g by Lm1;

        hence thesis;

      end;

      then for x st x in Z holds ln is_differentiable_in x by TAYLOR_1: 18;

      then

       A8: ln is_differentiable_on Z by A6, FDIFF_1: 9;

      

       A9: for x st x in Z holds ( diff ( ln ,x)) = (1 / x)

      proof

        let x;

        assume x in Z;

        then x > 0 by A7;

        then x in ( right_open_halfline 0 ) by Lm1;

        hence thesis by TAYLOR_1: 18;

      end;

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

      proof

        let x;

        assume

         A10: x in Z;

        

        then ((( ln (#) sec ) `| Z) . x) = ((( sec . x) * ( diff ( ln ,x))) + (( ln . x) * ( diff ( sec ,x)))) by A1, A8, A5, FDIFF_1: 21

        .= ((( sec . x) * (1 / x)) + (( ln . x) * ( diff ( sec ,x)))) by A9, A10

        .= ((( sec . x) * (1 / x)) + (( ln . x) * (( sin . x) / (( cos . x) ^2 )))) by A4, A10

        .= (((1 / ( cos . x)) / x) + ((( ln . x) * ( sin . x)) / (( cos . x) ^2 ))) by A3, A10, RFUNCT_1:def 2;

        hence thesis;

      end;

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

    end;

    theorem :: FDIFF_9:31

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

    proof

      assume

       A1: Z c= ( dom ( ln (#) cosec ));

      then

       A2: Z c= (( dom ln ) /\ ( dom cosec )) by VALUED_1:def 4;

      then

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

      

       A4: for x st x in Z holds cosec is_differentiable_in x & ( diff ( cosec ,x)) = ( - (( cos . x) / (( sin . x) ^2 )))

      proof

        let x;

        assume x in Z;

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

        hence thesis by Th2;

      end;

      then for x st x in Z holds cosec is_differentiable_in x;

      then

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

      

       A6: Z c= ( dom ln ) by A2, XBOOLE_1: 18;

      

       A7: for x st x in Z holds x > 0

      proof

        let x;

        assume x in Z;

        then x in ( right_open_halfline 0 ) by A6, TAYLOR_1: 18;

        then ex g be Real st x = g & 0 < g by Lm1;

        hence thesis;

      end;

      then for x st x in Z holds ln is_differentiable_in x by TAYLOR_1: 18;

      then

       A8: ln is_differentiable_on Z by A6, FDIFF_1: 9;

      

       A9: for x st x in Z holds ( diff ( ln ,x)) = (1 / x)

      proof

        let x;

        assume x in Z;

        then x > 0 by A7;

        then x in ( right_open_halfline 0 ) by Lm1;

        hence thesis by TAYLOR_1: 18;

      end;

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

      proof

        let x;

        assume

         A10: x in Z;

        

        then ((( ln (#) cosec ) `| Z) . x) = ((( cosec . x) * ( diff ( ln ,x))) + (( ln . x) * ( diff ( cosec ,x)))) by A1, A8, A5, FDIFF_1: 21

        .= ((( cosec . x) * (1 / x)) + (( ln . x) * ( diff ( cosec ,x)))) by A9, A10

        .= ((( cosec . x) * (1 / x)) + (( ln . x) * ( - (( cos . x) / (( sin . x) ^2 ))))) by A4, A10

        .= (((1 / ( sin . x)) / x) - ((( ln . x) * ( cos . x)) / (( sin . x) ^2 ))) by A3, A10, RFUNCT_1:def 2;

        hence thesis;

      end;

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

    end;

    theorem :: FDIFF_9:32

     not 0 in Z & Z c= ( dom ((( id Z) ^ ) (#) sec )) implies ((( id Z) ^ ) (#) sec ) is_differentiable_on Z & for x st x in Z holds ((((( id Z) ^ ) (#) sec ) `| Z) . x) = (( - ((1 / ( cos . x)) / (x ^2 ))) + ((( sin . x) / x) / (( cos . x) ^2 )))

    proof

      set f = ( id Z);

      assume that

       A1: not 0 in Z and

       A2: Z c= ( dom ((f ^ ) (#) sec ));

      

       A3: (f ^ ) is_differentiable_on Z by A1, FDIFF_5: 4;

      

       A4: Z c= (( dom (f ^ )) /\ ( dom sec )) by A2, VALUED_1:def 4;

      then

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

      

       A6: for x st x in Z holds sec is_differentiable_in x & ( diff ( sec ,x)) = (( sin . x) / (( cos . x) ^2 ))

      proof

        let x;

        assume x in Z;

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

        hence thesis by Th1;

      end;

      then for x st x in Z holds sec is_differentiable_in x;

      then

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

      

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

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

      proof

        let x;

        assume

         A9: x in Z;

        

        then ((((f ^ ) (#) sec ) `| Z) . x) = ((( sec . x) * ( diff ((f ^ ),x))) + (((f ^ ) . x) * ( diff ( sec ,x)))) by A2, A3, A7, FDIFF_1: 21

        .= ((( sec . x) * (((f ^ ) `| Z) . x)) + (((f ^ ) . x) * ( diff ( sec ,x)))) by A3, A9, FDIFF_1:def 7

        .= ((( sec . x) * ( - (1 / (x ^2 )))) + (((f ^ ) . x) * ( diff ( sec ,x)))) by A1, A9, FDIFF_5: 4

        .= (( - (( sec . x) * (1 / (x ^2 )))) + (((f ^ ) . x) * (( sin . x) / (( cos . x) ^2 )))) by A6, A9

        .= (( - ((( cos . x) " ) * (1 / (x ^2 )))) + (((f ^ ) . x) * (( sin . x) / (( cos . x) ^2 )))) by A5, A9, RFUNCT_1:def 2

        .= (( - ((1 / ( cos . x)) / (x ^2 ))) + (((f . x) " ) * (( sin . x) / (( cos . x) ^2 )))) by A8, A9, RFUNCT_1:def 2

        .= (( - ((1 / ( cos . x)) / (x ^2 ))) + ((1 / x) * (( sin . x) / (( cos . x) ^2 )))) by A9, FUNCT_1: 18

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

        hence thesis;

      end;

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

    end;

    theorem :: FDIFF_9:33

     not 0 in Z & Z c= ( dom ((( id Z) ^ ) (#) cosec )) implies ((( id Z) ^ ) (#) cosec ) is_differentiable_on Z & for x st x in Z holds ((((( id Z) ^ ) (#) cosec ) `| Z) . x) = (( - ((1 / ( sin . x)) / (x ^2 ))) - ((( cos . x) / x) / (( sin . x) ^2 )))

    proof

      set f = ( id Z);

      assume that

       A1: not 0 in Z and

       A2: Z c= ( dom ((f ^ ) (#) cosec ));

      

       A3: (f ^ ) is_differentiable_on Z by A1, FDIFF_5: 4;

      

       A4: Z c= (( dom (f ^ )) /\ ( dom cosec )) by A2, VALUED_1:def 4;

      then

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

      

       A6: for x st x in Z holds cosec is_differentiable_in x & ( diff ( cosec ,x)) = ( - (( cos . x) / (( sin . x) ^2 )))

      proof

        let x;

        assume x in Z;

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

        hence thesis by Th2;

      end;

      then for x st x in Z holds cosec is_differentiable_in x;

      then

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

      

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

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

      proof

        let x;

        assume

         A9: x in Z;

        

        then ((((f ^ ) (#) cosec ) `| Z) . x) = ((( cosec . x) * ( diff ((f ^ ),x))) + (((f ^ ) . x) * ( diff ( cosec ,x)))) by A2, A3, A7, FDIFF_1: 21

        .= ((( cosec . x) * (((f ^ ) `| Z) . x)) + (((f ^ ) . x) * ( diff ( cosec ,x)))) by A3, A9, FDIFF_1:def 7

        .= ((( cosec . x) * ( - (1 / (x ^2 )))) + (((f ^ ) . x) * ( diff ( cosec ,x)))) by A1, A9, FDIFF_5: 4

        .= (( - (( cosec . x) * (1 / (x ^2 )))) + (((f ^ ) . x) * ( - (( cos . x) / (( sin . x) ^2 ))))) by A6, A9

        .= (( - ((( sin . x) " ) * (1 / (x ^2 )))) + (((f ^ ) . x) * (( - ( cos . x)) / (( sin . x) ^2 )))) by A5, A9, RFUNCT_1:def 2

        .= (( - ((1 / ( sin . x)) / (x ^2 ))) + (((f . x) " ) * (( - ( cos . x)) / (( sin . x) ^2 )))) by A8, A9, RFUNCT_1:def 2

        .= (( - ((1 / ( sin . x)) / (x ^2 ))) + ((1 / x) * (( - ( cos . x)) / (( sin . x) ^2 )))) by A9, FUNCT_1: 18

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

        hence thesis;

      end;

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

    end;

    theorem :: FDIFF_9:34

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

    proof

      assume

       A1: Z c= ( dom ( sec * sin ));

      

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

      proof

        let x;

        assume x in Z;

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

        hence thesis by RFUNCT_1: 3;

      end;

      

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

      proof

        let x;

        assume x in Z;

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

        then sin is_differentiable_in x & sec is_differentiable_in ( sin . x) by Th1, SIN_COS: 64;

        hence thesis by FDIFF_2: 13;

      end;

      then

       A4: ( sec * sin ) is_differentiable_on Z by A1, FDIFF_1: 9;

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

      proof

        let x;

        assume

         A5: x in Z;

        then

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

        then sin is_differentiable_in x & sec is_differentiable_in ( sin . x) by Th1, SIN_COS: 64;

        

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

        .= ((( sin . ( sin . x)) / (( cos . ( sin . x)) ^2 )) * ( diff ( sin ,x))) by A6, Th1

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

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

      end;

      hence thesis by A1, A3, FDIFF_1: 9;

    end;

    theorem :: FDIFF_9:35

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

    proof

      assume

       A1: Z c= ( dom ( sec * cos ));

      

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

      proof

        let x;

        assume x in Z;

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

        hence thesis by RFUNCT_1: 3;

      end;

      

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

      proof

        let x;

        assume x in Z;

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

        then cos is_differentiable_in x & sec is_differentiable_in ( cos . x) by Th1, SIN_COS: 63;

        hence thesis by FDIFF_2: 13;

      end;

      then

       A4: ( sec * cos ) is_differentiable_on Z by A1, FDIFF_1: 9;

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

      proof

        let x;

        assume

         A5: x in Z;

        then

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

        then cos is_differentiable_in x & sec is_differentiable_in ( cos . x) by Th1, SIN_COS: 63;

        

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

        .= ((( sin . ( cos . x)) / (( cos . ( cos . x)) ^2 )) * ( diff ( cos ,x))) by A6, Th1

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

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

      end;

      hence thesis by A1, A3, FDIFF_1: 9;

    end;

    theorem :: FDIFF_9:36

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

    proof

      assume

       A1: Z c= ( dom ( cosec * sin ));

      

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

      proof

        let x;

        assume x in Z;

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

        hence thesis by RFUNCT_1: 3;

      end;

      

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

      proof

        let x;

        assume x in Z;

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

        then sin is_differentiable_in x & cosec is_differentiable_in ( sin . x) by Th2, SIN_COS: 64;

        hence thesis by FDIFF_2: 13;

      end;

      then

       A4: ( cosec * sin ) is_differentiable_on Z by A1, FDIFF_1: 9;

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

      proof

        let x;

        assume

         A5: x in Z;

        then

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

        then sin is_differentiable_in x & cosec is_differentiable_in ( sin . x) by Th2, SIN_COS: 64;

        

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

        .= (( - (( cos . ( sin . x)) / (( sin . ( sin . x)) ^2 ))) * ( diff ( sin ,x))) by A6, Th2

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

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

      end;

      hence thesis by A1, A3, FDIFF_1: 9;

    end;

    theorem :: FDIFF_9:37

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

    proof

      assume

       A1: Z c= ( dom ( cosec * cos ));

      

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

      proof

        let x;

        assume x in Z;

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

        hence thesis by RFUNCT_1: 3;

      end;

      

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

      proof

        let x;

        assume x in Z;

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

        then cos is_differentiable_in x & cosec is_differentiable_in ( cos . x) by Th2, SIN_COS: 63;

        hence thesis by FDIFF_2: 13;

      end;

      then

       A4: ( cosec * cos ) is_differentiable_on Z by A1, FDIFF_1: 9;

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

      proof

        let x;

        assume

         A5: x in Z;

        then

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

        then cos is_differentiable_in x & cosec is_differentiable_in ( cos . x) by Th2, SIN_COS: 63;

        

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

        .= (( - (( cos . ( cos . x)) / (( sin . ( cos . x)) ^2 ))) * ( diff ( cos ,x))) by A6, Th2

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

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

      end;

      hence thesis by A1, A3, FDIFF_1: 9;

    end;

    theorem :: FDIFF_9:38

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

    proof

      assume

       A1: Z c= ( dom ( sec * tan ));

      

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

      proof

        let x;

        assume x in Z;

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

        hence thesis by RFUNCT_1: 3;

      end;

      ( dom ( sec * 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 ( sec * 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;

        ( cos . ( tan . x)) <> 0 by A2, A5;

        then sec is_differentiable_in ( tan . x) by Th1;

        hence thesis by A6, FDIFF_2: 13;

      end;

      then

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

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

      proof

        let x;

        assume

         A8: x in Z;

        then

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

        then

         A10: tan is_differentiable_in x by FDIFF_7: 46;

        

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

        then sec is_differentiable_in ( tan . x) by Th1;

        

        then ( diff (( sec * tan ),x)) = (( diff ( sec ,( tan . x))) * ( diff ( tan ,x))) by A10, FDIFF_2: 13

        .= ((( sin . ( tan . x)) / (( cos . ( tan . x)) ^2 )) * ( diff ( tan ,x))) by A11, Th1

        .= ((1 / (( cos . x) ^2 )) * (( sin . ( tan . x)) / (( cos . ( tan . x)) ^2 ))) by A9, FDIFF_7: 46

        .= ((( sin . ( tan . x)) / (( cos . x) ^2 )) / (( cos . ( tan . x)) ^2 ));

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

      end;

      hence thesis by A1, A4, FDIFF_1: 9;

    end;

    theorem :: FDIFF_9:39

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

    proof

      assume

       A1: Z c= ( dom ( sec * cot ));

      

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

      proof

        let x;

        assume x in Z;

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

        hence thesis by RFUNCT_1: 3;

      end;

      ( dom ( sec * 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 ( sec * 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;

        ( cos . ( cot . x)) <> 0 by A2, A5;

        then sec is_differentiable_in ( cot . x) by Th1;

        hence thesis by A6, FDIFF_2: 13;

      end;

      then

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

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

      proof

        let x;

        assume

         A8: x in Z;

        then

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

        then

         A10: cot is_differentiable_in x by FDIFF_7: 47;

        

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

        then sec is_differentiable_in ( cot . x) by Th1;

        

        then ( diff (( sec * cot ),x)) = (( diff ( sec ,( cot . x))) * ( diff ( cot ,x))) by A10, FDIFF_2: 13

        .= ((( sin . ( cot . x)) / (( cos . ( cot . x)) ^2 )) * ( diff ( cot ,x))) by A11, Th1

        .= (( - (1 / (( sin . x) ^2 ))) * (( sin . ( cot . x)) / (( cos . ( cot . x)) ^2 ))) by A9, FDIFF_7: 47

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

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

      end;

      hence thesis by A1, A4, FDIFF_1: 9;

    end;

    theorem :: FDIFF_9:40

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

    proof

      assume

       A1: Z c= ( dom ( cosec * tan ));

      

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

      proof

        let x;

        assume x in Z;

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

        hence thesis by RFUNCT_1: 3;

      end;

      ( dom ( cosec * 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 ( cosec * 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;

        ( sin . ( tan . x)) <> 0 by A2, A5;

        then cosec is_differentiable_in ( tan . x) by Th2;

        hence thesis by A6, FDIFF_2: 13;

      end;

      then

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

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

      proof

        let x;

        assume

         A8: x in Z;

        then

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

        then

         A10: tan is_differentiable_in x by FDIFF_7: 46;

        

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

        then cosec is_differentiable_in ( tan . x) by Th2;

        

        then ( diff (( cosec * tan ),x)) = (( diff ( cosec ,( tan . x))) * ( diff ( tan ,x))) by A10, FDIFF_2: 13

        .= (( - (( cos . ( tan . x)) / (( sin . ( tan . x)) ^2 ))) * ( diff ( tan ,x))) by A11, Th2

        .= ((1 / (( cos . x) ^2 )) * ( - (( cos . ( tan . x)) / (( sin . ( tan . x)) ^2 )))) by A9, FDIFF_7: 46

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

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

      end;

      hence thesis by A1, A4, FDIFF_1: 9;

    end;

    theorem :: FDIFF_9:41

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

    proof

      assume

       A1: Z c= ( dom ( cosec * cot ));

      

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

      proof

        let x;

        assume x in Z;

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

        hence thesis by RFUNCT_1: 3;

      end;

      ( dom ( cosec * 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 ( cosec * 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;

        ( sin . ( cot . x)) <> 0 by A2, A5;

        then cosec is_differentiable_in ( cot . x) by Th2;

        hence thesis by A6, FDIFF_2: 13;

      end;

      then

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

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

      proof

        let x;

        assume

         A8: x in Z;

        then

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

        then

         A10: cot is_differentiable_in x by FDIFF_7: 47;

        

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

        then cosec is_differentiable_in ( cot . x) by Th2;

        

        then ( diff (( cosec * cot ),x)) = (( diff ( cosec ,( cot . x))) * ( diff ( cot ,x))) by A10, FDIFF_2: 13

        .= (( - (( cos . ( cot . x)) / (( sin . ( cot . x)) ^2 ))) * ( diff ( cot ,x))) by A11, Th2

        .= (( - (1 / (( sin . x) ^2 ))) * ( - (( cos . ( cot . x)) / (( sin . ( cot . x)) ^2 )))) by A9, FDIFF_7: 47

        .= ((( cos . ( cot . x)) / (( sin . x) ^2 )) / (( sin . ( cot . x)) ^2 ));

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

      end;

      hence thesis by A1, A4, FDIFF_1: 9;

    end;

    theorem :: FDIFF_9:42

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

    proof

      assume

       A1: Z c= ( dom ( tan (#) sec ));

      then

       A2: Z c= (( dom tan ) /\ ( dom sec )) by VALUED_1:def 4;

      then

       A3: 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 A3, FDIFF_8: 1;

        hence thesis by FDIFF_7: 46;

      end;

      then

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

      

       A5: Z c= ( dom sec ) by A2, XBOOLE_1: 18;

      

       A6: for x st x in Z holds sec is_differentiable_in x & ( diff ( sec ,x)) = (( sin . x) / (( cos . x) ^2 ))

      proof

        let x;

        assume x in Z;

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

        hence thesis by Th1;

      end;

      then for x st x in Z holds sec is_differentiable_in x;

      then

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

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

      proof

        let x;

        assume

         A8: x in Z;

        then

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

        ((( tan (#) sec ) `| Z) . x) = ((( sec . x) * ( diff ( tan ,x))) + (( tan . x) * ( diff ( sec ,x)))) by A1, A4, A7, A8, FDIFF_1: 21

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

        .= ((( sec . x) * (1 / (( cos . x) ^2 ))) + (( tan . x) * (( sin . x) / (( cos . x) ^2 )))) by A6, A8

        .= (((1 / (( cos . x) ^2 )) / ( cos . x)) + ((( tan . x) * ( sin . x)) / (( cos . x) ^2 ))) by A5, A8, RFUNCT_1:def 2;

        hence thesis;

      end;

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

    end;

    theorem :: FDIFF_9:43

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

    proof

      assume

       A1: Z c= ( dom ( cot (#) sec ));

      then

       A2: Z c= (( dom cot ) /\ ( dom sec )) by VALUED_1:def 4;

      then

       A3: 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 A3, FDIFF_8: 2;

        hence thesis by FDIFF_7: 47;

      end;

      then

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

      

       A5: Z c= ( dom sec ) by A2, XBOOLE_1: 18;

      

       A6: for x st x in Z holds sec is_differentiable_in x & ( diff ( sec ,x)) = (( sin . x) / (( cos . x) ^2 ))

      proof

        let x;

        assume x in Z;

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

        hence thesis by Th1;

      end;

      then for x st x in Z holds sec is_differentiable_in x;

      then

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

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

      proof

        let x;

        assume

         A8: x in Z;

        then

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

        ((( cot (#) sec ) `| Z) . x) = ((( sec . x) * ( diff ( cot ,x))) + (( cot . x) * ( diff ( sec ,x)))) by A1, A4, A7, A8, FDIFF_1: 21

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

        .= ((( sec . x) * ( - (1 / (( sin . x) ^2 )))) + (( cot . x) * (( sin . x) / (( cos . x) ^2 )))) by A6, A8

        .= ((( - (1 / (( sin . x) ^2 ))) / ( cos . x)) + ((( cot . x) * ( sin . x)) / (( cos . x) ^2 ))) by A5, A8, RFUNCT_1:def 2;

        hence thesis;

      end;

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

    end;

    theorem :: FDIFF_9:44

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

    proof

      assume

       A1: Z c= ( dom ( tan (#) cosec ));

      then

       A2: Z c= (( dom tan ) /\ ( dom cosec )) by VALUED_1:def 4;

      then

       A3: 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 A3, FDIFF_8: 1;

        hence thesis by FDIFF_7: 46;

      end;

      then

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

      

       A5: Z c= ( dom cosec ) by A2, XBOOLE_1: 18;

      

       A6: for x st x in Z holds cosec is_differentiable_in x & ( diff ( cosec ,x)) = ( - (( cos . x) / (( sin . x) ^2 )))

      proof

        let x;

        assume x in Z;

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

        hence thesis by Th2;

      end;

      then for x st x in Z holds cosec is_differentiable_in x;

      then

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

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

      proof

        let x;

        assume

         A8: x in Z;

        then

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

        ((( tan (#) cosec ) `| Z) . x) = ((( cosec . x) * ( diff ( tan ,x))) + (( tan . x) * ( diff ( cosec ,x)))) by A1, A4, A7, A8, FDIFF_1: 21

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

        .= ((( cosec . x) * (1 / (( cos . x) ^2 ))) + (( tan . x) * ( - (( cos . x) / (( sin . x) ^2 ))))) by A6, A8

        .= (((1 / (( cos . x) ^2 )) / ( sin . x)) + (( tan . x) * ( - (( cos . x) / (( sin . x) ^2 ))))) by A5, A8, RFUNCT_1:def 2;

        hence thesis;

      end;

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

    end;

    theorem :: FDIFF_9:45

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

    proof

      assume

       A1: Z c= ( dom ( cot (#) cosec ));

      then

       A2: Z c= (( dom cot ) /\ ( dom cosec )) by VALUED_1:def 4;

      then

       A3: 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 A3, FDIFF_8: 2;

        hence thesis by FDIFF_7: 47;

      end;

      then

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

      

       A5: Z c= ( dom cosec ) by A2, XBOOLE_1: 18;

      

       A6: for x st x in Z holds cosec is_differentiable_in x & ( diff ( cosec ,x)) = ( - (( cos . x) / (( sin . x) ^2 )))

      proof

        let x;

        assume x in Z;

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

        hence thesis by Th2;

      end;

      then for x st x in Z holds cosec is_differentiable_in x;

      then

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

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

      proof

        let x;

        assume

         A8: x in Z;

        then

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

        ((( cot (#) cosec ) `| Z) . x) = ((( cosec . x) * ( diff ( cot ,x))) + (( cot . x) * ( diff ( cosec ,x)))) by A1, A4, A7, A8, FDIFF_1: 21

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

        .= ((( cosec . x) * ( - (1 / (( sin . x) ^2 )))) + (( cot . x) * ( - (( cos . x) / (( sin . x) ^2 ))))) by A6, A8

        .= ((( - (1 / (( sin . x) ^2 ))) / ( sin . x)) + (( cot . x) * ( - (( cos . x) / (( sin . x) ^2 ))))) by A5, A8, RFUNCT_1:def 2;

        hence thesis;

      end;

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

    end;