integr14.miz



    begin

    reserve a,x for Real;

    reserve n for Nat;

    reserve A for non empty closed_interval Subset of REAL ;

    reserve f,f1 for PartFunc of REAL , REAL ;

    reserve Z for open Subset of REAL ;

    

     Lm1: 0 in Z implies (( id Z) " { 0 }) = { 0 }

    proof

      assume

       A1: 0 in Z;

      thus (( id Z) " { 0 }) c= { 0 }

      proof

        let x be object;

        assume

         A2: x in (( id Z) " { 0 });

        then x in ( dom ( id Z)) by FUNCT_1:def 7;

        then

         A3: x in Z;

        (( id Z) . x) in { 0 } by A2, FUNCT_1:def 7;

        hence thesis by A3, FUNCT_1: 18;

      end;

      let x be object;

      assume x in { 0 };

      then

       A4: x = 0 by TARSKI:def 1;

      then (( id Z) . x) = 0 by A1, FUNCT_1: 18;

      then

       A5: (( id Z) . x) in { 0 } by TARSKI:def 1;

      x in ( dom ( id Z)) by A1, A4;

      hence thesis by A5, FUNCT_1:def 7;

    end;

    theorem :: INTEGR14:1

    

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

      assume

       A1: Z c= ( dom ( sec * (( id Z) ^ )));

      then

       A2: Z c= ( dom ( - ( sec * (( id Z) ^ )))) by VALUED_1:def 5;

      

       A3: Z c= ( dom (( id Z) ^ )) by A1, FUNCT_1: 101;

      

       A4: not 0 in Z

      proof

        assume

         A5: 0 in Z;

        ( dom (( id Z) ^ )) = (( dom ( id Z)) \ (( id Z) " { 0 })) by RFUNCT_1:def 2

        .= (( dom ( id Z)) \ { 0 }) by Lm1, A5;

        then not 0 in { 0 } by A5, A3, XBOOLE_0:def 5;

        hence thesis by TARSKI:def 1;

      end;

      then

       A6: ( sec * (( id Z) ^ )) is_differentiable_on Z by A1, FDIFF_9: 8;

      then

       A7: (( - 1) (#) ( sec * (( id Z) ^ ))) is_differentiable_on Z by A2, FDIFF_1: 20;

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

      proof

        let x;

        assume

         A8: x in Z;

        ((( - ( sec * (( id Z) ^ ))) `| Z) . x) = ((( - 1) (#) (( sec * (( id Z) ^ )) `| Z)) . x) by A6, FDIFF_2: 19

        .= (( - 1) * ((( sec * (( id Z) ^ )) `| Z) . x)) by VALUED_1: 6

        .= (( - 1) * ( - (( sin . (1 / x)) / ((x ^2 ) * (( cos . (1 / x)) ^2 ))))) by A1, A4, A8, FDIFF_9: 8

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

        hence thesis;

      end;

      hence thesis by A7;

    end;

    theorem :: INTEGR14:2

    

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

      then

       A2: Z c= ( dom ( - ( cosec * exp_R ))) by VALUED_1: 8;

      

       A3: ( cosec * exp_R ) is_differentiable_on Z by A1, FDIFF_9: 13;

      then

       A4: (( - 1) (#) ( cosec * exp_R )) is_differentiable_on Z by A2, FDIFF_1: 20;

      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;

        ((( - ( cosec * exp_R )) `| Z) . x) = ((( - 1) (#) (( cosec * exp_R ) `| Z)) . x) by A3, FDIFF_2: 19

        .= (( - 1) * ((( cosec * exp_R ) `| Z) . x)) by VALUED_1: 6

        .= (( - 1) * ( - ((( exp_R . x) * ( cos . ( exp_R . x))) / (( sin . ( exp_R . x)) ^2 )))) by A1, A5, FDIFF_9: 13

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

        hence thesis;

      end;

      hence thesis by A4;

    end;

    theorem :: INTEGR14:3

    

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

      then

       A2: Z c= ( dom ( - ( cosec * ln ))) by VALUED_1: 8;

      

       A3: ( cosec * ln ) is_differentiable_on Z by A1, FDIFF_9: 15;

      then

       A4: (( - 1) (#) ( cosec * ln )) is_differentiable_on Z by A2, FDIFF_1: 20;

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

      proof

        let x;

        assume

         A5: x in Z;

        ((( - ( cosec * ln )) `| Z) . x) = ((( - 1) (#) (( cosec * ln ) `| Z)) . x) by A3, FDIFF_2: 19

        .= (( - 1) * ((( cosec * ln ) `| Z) . x)) by VALUED_1: 6

        .= (( - 1) * ( - (( cos . ( ln . x)) / (x * (( sin . ( ln . x)) ^2 ))))) by A1, A5, FDIFF_9: 15

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

        hence thesis;

      end;

      hence thesis by A4;

    end;

    theorem :: INTEGR14:4

    

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

      then

       A2: Z c= ( dom ( - ( exp_R * cosec ))) by VALUED_1: 8;

      

       A3: ( exp_R * cosec ) is_differentiable_on Z by A1, FDIFF_9: 17;

      then

       A4: (( - 1) (#) ( exp_R * cosec )) is_differentiable_on Z by A2, FDIFF_1: 20;

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

      proof

        let x;

        assume

         A5: x in Z;

        ((( - ( exp_R * cosec )) `| Z) . x) = ((( - 1) (#) (( exp_R * cosec ) `| Z)) . x) by A3, FDIFF_2: 19

        .= (( - 1) * ((( exp_R * cosec ) `| Z) . x)) by VALUED_1: 6

        .= (( - 1) * ( - ((( exp_R . ( cosec . x)) * ( cos . x)) / (( sin . x) ^2 )))) by A1, A5, FDIFF_9: 17

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

        hence thesis;

      end;

      hence thesis by A4;

    end;

    theorem :: INTEGR14:5

    

     Th5: Z c= ( dom ( ln * cosec )) implies ( - ( ln * cosec )) is_differentiable_on Z & for x st x in Z holds ((( - ( ln * cosec )) `| Z) . x) = ( cot . x)

    proof

      assume

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

      then

       A2: Z c= ( dom ( - ( ln * cosec ))) by VALUED_1: 8;

      

       A3: ( ln * cosec ) is_differentiable_on Z by A1, FDIFF_9: 19;

      then

       A4: (( - 1) (#) ( ln * cosec )) is_differentiable_on Z by A2, FDIFF_1: 20;

      

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

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

      proof

        let x;

        assume

         A6: x in Z;

        ((( - ( ln * cosec )) `| Z) . x) = ((( - 1) (#) (( ln * cosec ) `| Z)) . x) by A3, FDIFF_2: 19

        .= (( - 1) * ((( ln * cosec ) `| Z) . x)) by VALUED_1: 6

        .= (( - 1) * ( - (( cos . x) / ( sin . x)))) by A1, A6, FDIFF_9: 19

        .= ( cot x)

        .= ( cot . x) by A5, A6, SIN_COS9: 16;

        hence thesis;

      end;

      hence thesis by A4;

    end;

    theorem :: INTEGR14:6

    

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

       A1: Z c= ( dom (( #Z n) * cosec )) & 1 <= n;

      then

       A2: Z c= ( dom ( - (( #Z n) * cosec ))) & 1 <= n by VALUED_1: 8;

      

       A3: (( #Z n) * cosec ) is_differentiable_on Z by A1, FDIFF_9: 21;

      then

       A4: (( - 1) (#) (( #Z n) * cosec )) is_differentiable_on Z by A2, FDIFF_1: 20;

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

      proof

        let x;

        assume

         A5: x in Z;

        ((( - (( #Z n) * cosec )) `| Z) . x) = ((( - 1) (#) ((( #Z n) * cosec ) `| Z)) . x) by A3, FDIFF_2: 19

        .= (( - 1) * (((( #Z n) * cosec ) `| Z) . x)) by VALUED_1: 6

        .= (( - 1) * ( - ((n * ( cos . x)) / (( sin . x) #Z (n + 1))))) by A1, A5, FDIFF_9: 21

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

        hence thesis;

      end;

      hence thesis by A4;

    end;

    theorem :: INTEGR14:7

    

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

      assume

       A1: Z c= ( dom ((( id Z) ^ ) (#) sec ));

      then

       A2: Z c= ( dom ( - ((( id Z) ^ ) (#) sec ))) by VALUED_1: 8;

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

      then

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

      

       A4: not 0 in Z

      proof

        assume

         A5: 0 in Z;

        ( dom (( id Z) ^ )) = (( dom ( id Z)) \ (( id Z) " { 0 })) by RFUNCT_1:def 2

        .= (( dom ( id Z)) \ { 0 }) by Lm1, A5;

        then not 0 in { 0 } by A5, A3, XBOOLE_0:def 5;

        hence thesis by TARSKI:def 1;

      end;

      then

       A6: ((( id Z) ^ ) (#) sec ) is_differentiable_on Z by A1, FDIFF_9: 32;

      then

       A7: (( - 1) (#) ((( id Z) ^ ) (#) sec )) is_differentiable_on Z by A2, FDIFF_1: 20;

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

      proof

        let x;

        assume

         A8: x in Z;

        ((( - ((( id Z) ^ ) (#) sec )) `| Z) . x) = ((( - 1) (#) (((( id Z) ^ ) (#) sec ) `| Z)) . x) by A6, FDIFF_2: 19

        .= (( - 1) * ((((( id Z) ^ ) (#) sec ) `| Z) . x)) by VALUED_1: 6

        .= (( - 1) * (( - ((1 / ( cos . x)) / (x ^2 ))) + ((( sin . x) / x) / (( cos . x) ^2 )))) by A1, A4, A8, FDIFF_9: 32

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

        hence thesis;

      end;

      hence thesis by A7;

    end;

    theorem :: INTEGR14:8

    

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

      assume

       A1: Z c= ( dom ((( id Z) ^ ) (#) cosec ));

      then

       A2: Z c= ( dom ( - ((( id Z) ^ ) (#) cosec ))) by VALUED_1: 8;

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

      then

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

      

       A4: not 0 in Z

      proof

        assume

         A5: 0 in Z;

        ( dom (( id Z) ^ )) = (( dom ( id Z)) \ (( id Z) " { 0 })) by RFUNCT_1:def 2

        .= (( dom ( id Z)) \ { 0 }) by Lm1, A5;

        then not 0 in { 0 } by A5, A3, XBOOLE_0:def 5;

        hence thesis by TARSKI:def 1;

      end;

      then

       A6: ((( id Z) ^ ) (#) cosec ) is_differentiable_on Z by A1, FDIFF_9: 33;

      then

       A7: (( - 1) (#) ((( id Z) ^ ) (#) cosec )) is_differentiable_on Z by A2, FDIFF_1: 20;

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

      proof

        let x;

        assume

         A8: x in Z;

        ((( - ((( id Z) ^ ) (#) cosec )) `| Z) . x) = ((( - 1) (#) (((( id Z) ^ ) (#) cosec ) `| Z)) . x) by A6, FDIFF_2: 19

        .= (( - 1) * ((((( id Z) ^ ) (#) cosec ) `| Z) . x)) by VALUED_1: 6

        .= (( - 1) * (( - ((1 / ( sin . x)) / (x ^2 ))) - ((( cos . x) / x) / (( sin . x) ^2 )))) by A1, A4, A8, FDIFF_9: 33

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

        hence thesis;

      end;

      hence thesis by A7;

    end;

    theorem :: INTEGR14:9

    

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

      then

       A2: Z c= ( dom ( - ( cosec * sin ))) by VALUED_1: 8;

      

       A3: ( cosec * sin ) is_differentiable_on Z by A1, FDIFF_9: 36;

      then

       A4: (( - 1) (#) ( cosec * sin )) is_differentiable_on Z by A2, FDIFF_1: 20;

      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;

        ((( - ( cosec * sin )) `| Z) . x) = ((( - 1) (#) (( cosec * sin ) `| Z)) . x) by A3, FDIFF_2: 19

        .= (( - 1) * ((( cosec * sin ) `| Z) . x)) by VALUED_1: 6

        .= (( - 1) * ( - ((( cos . x) * ( cos . ( sin . x))) / (( sin . ( sin . x)) ^2 )))) by A1, A5, FDIFF_9: 36

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

        hence thesis;

      end;

      hence thesis by A4;

    end;

    theorem :: INTEGR14:10

    

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

      then

       A2: Z c= ( dom ( - ( sec * cot ))) by VALUED_1: 8;

      

       A3: ( sec * cot ) is_differentiable_on Z by A1, FDIFF_9: 39;

      then

       A4: (( - 1) (#) ( sec * cot )) is_differentiable_on Z by A2, FDIFF_1: 20;

      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

         A5: x in Z;

        ((( - ( sec * cot )) `| Z) . x) = ((( - 1) (#) (( sec * cot ) `| Z)) . x) by A3, FDIFF_2: 19

        .= (( - 1) * ((( sec * cot ) `| Z) . x)) by VALUED_1: 6

        .= (( - 1) * ( - ((( sin . ( cot . x)) / (( sin . x) ^2 )) / (( cos . ( cot . x)) ^2 )))) by A1, A5, FDIFF_9: 39

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

        hence thesis;

      end;

      hence thesis by A4;

    end;

    theorem :: INTEGR14:11

    

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

      then

       A2: Z c= ( dom ( - ( cosec * tan ))) by VALUED_1: 8;

      

       A3: ( cosec * tan ) is_differentiable_on Z by A1, FDIFF_9: 40;

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

      then

       A4: Z c= ( dom tan ) by A1;

      

       A5: (( - 1) (#) ( cosec * tan )) is_differentiable_on Z by A2, A3, FDIFF_1: 20;

      

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

      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

         A7: x in Z;

        then

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

        then

         A9: tan is_differentiable_in x by FDIFF_7: 46;

        

         A10: ( sin . ( tan . x)) <> 0 by A6, A7;

        then

         A11: cosec is_differentiable_in ( tan . x) by FDIFF_9: 2;

        

         A12: ( cosec * tan ) is_differentiable_in x by A3, A7, FDIFF_1: 9;

        ((( - ( cosec * tan )) `| Z) . x) = ( diff (( - ( cosec * tan )),x)) by A5, A7, FDIFF_1:def 7

        .= (( - 1) * ( diff (( cosec * tan ),x))) by A12, FDIFF_1: 15

        .= (( - 1) * (( diff ( cosec ,( tan . x))) * ( diff ( tan ,x)))) by A9, A11, FDIFF_2: 13

        .= (( - 1) * (( - (( cos . ( tan . x)) / (( sin . ( tan . x)) ^2 ))) * ( diff ( tan ,x)))) by A10, FDIFF_9: 2

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

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

        hence thesis;

      end;

      hence thesis by A5;

    end;

    theorem :: INTEGR14:12

    

     Th12: 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 (#) sec ))) by VALUED_1: 8;

      

       A3: ( cot (#) sec ) is_differentiable_on Z by A1, FDIFF_9: 43;

      then

       A4: (( - 1) (#) ( cot (#) sec )) is_differentiable_on Z by A2, FDIFF_1: 20;

      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

         A5: x in Z;

        ((( - ( cot (#) sec )) `| Z) . x) = ((( - 1) (#) (( cot (#) sec ) `| Z)) . x) by A3, FDIFF_2: 19

        .= (( - 1) * ((( cot (#) sec ) `| Z) . x)) by VALUED_1: 6

        .= (( - 1) * (( - ((1 / (( sin . x) ^2 )) / ( cos . x))) + ((( cot . x) * ( sin . x)) / (( cos . x) ^2 )))) by A1, A5, FDIFF_9: 43

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

        hence thesis;

      end;

      hence thesis by A4;

    end;

    theorem :: INTEGR14:13

    

     Th13: 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 (#) cosec ))) by VALUED_1: 8;

      

       A3: ( cot (#) cosec ) is_differentiable_on Z by A1, FDIFF_9: 45;

      then

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

      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

         A5: x in Z;

        ((( - ( cot (#) cosec )) `| Z) . x) = ((( - 1) (#) (( cot (#) cosec ) `| Z)) . x) by A3, FDIFF_2: 19

        .= (( - 1) * ((( cot (#) cosec ) `| Z) . x)) by VALUED_1: 6

        .= (( - 1) * (( - ((1 / (( sin . x) ^2 )) / ( sin . x))) - ((( cot . x) * ( cos . x)) / (( sin . x) ^2 )))) by A1, A5, FDIFF_9: 45

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

        hence thesis;

      end;

      hence thesis by A4;

    end;

    theorem :: INTEGR14:14

    

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

    proof

      assume

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

      then

       A2: Z c= ( dom ( - ( cos (#) cot ))) by VALUED_1: 8;

      

       A3: ( cos (#) cot ) is_differentiable_on Z by A1, FDIFF_10: 11;

      then

       A4: (( - 1) (#) ( cos (#) cot )) is_differentiable_on Z by A2, FDIFF_1: 20;

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

      proof

        let x;

        assume

         A5: x in Z;

        ((( - ( cos (#) cot )) `| Z) . x) = ((( - 1) (#) (( cos (#) cot ) `| Z)) . x) by A3, FDIFF_2: 19

        .= (( - 1) * ((( cos (#) cot ) `| Z) . x)) by VALUED_1: 6

        .= (( - 1) * (( - ( cos . x)) - (( cos . x) / (( sin . x) ^2 )))) by A1, A5, FDIFF_10: 11

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

        hence thesis;

      end;

      hence thesis by A4;

    end;

    begin

    theorem :: INTEGR14:15

    A c= Z & (for x st x in Z holds (f . x) = (( sin . (1 / x)) / ((x ^2 ) * (( cos . (1 / x)) ^2 )))) & Z c= ( dom ( sec * (( id Z) ^ ))) & Z = ( dom f) & (f | A) is continuous implies ( integral (f,A)) = ((( - ( sec * (( id Z) ^ ))) . ( upper_bound A)) - (( - ( sec * (( id Z) ^ ))) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & (for x st x in Z holds (f . x) = (( sin . (1 / x)) / ((x ^2 ) * (( cos . (1 / x)) ^2 )))) & Z c= ( dom ( sec * (( id Z) ^ ))) & Z = ( dom f) & (f | A) is continuous;

      then

       A2: f is_integrable_on A & (f | A) is bounded by INTEGRA5: 10, INTEGRA5: 11;

      

       A3: ( - ( sec * (( id Z) ^ ))) is_differentiable_on Z by A1, Th1;

      

       A4: for x be Element of REAL st x in ( dom (( - ( sec * (( id Z) ^ ))) `| Z)) holds ((( - ( sec * (( id Z) ^ ))) `| Z) . x) = (f . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom (( - ( sec * (( id Z) ^ ))) `| Z));

        then

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

        

        then ((( - ( sec * (( id Z) ^ ))) `| Z) . x) = (( sin . (1 / x)) / ((x ^2 ) * (( cos . (1 / x)) ^2 ))) by A1, Th1

        .= (f . x) by A1, A5;

        hence thesis;

      end;

      ( dom (( - ( sec * (( id Z) ^ ))) `| Z)) = ( dom f) by A1, A3, FDIFF_1:def 7;

      then (( - ( sec * (( id Z) ^ ))) `| Z) = f by A4, PARTFUN1: 5;

      hence thesis by A1, A2, A3, INTEGRA5: 13;

    end;

    theorem :: INTEGR14:16

    A c= Z & (for x st x in Z holds (f . x) = (( cos . (1 / x)) / ((x ^2 ) * (( sin . (1 / x)) ^2 )))) & Z c= ( dom ( cosec * (( id Z) ^ ))) & Z = ( dom f) & (f | A) is continuous implies ( integral (f,A)) = ((( cosec * (( id Z) ^ )) . ( upper_bound A)) - (( cosec * (( id Z) ^ )) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & (for x st x in Z holds (f . x) = (( cos . (1 / x)) / ((x ^2 ) * (( sin . (1 / x)) ^2 )))) & Z c= ( dom ( cosec * (( id Z) ^ ))) & Z = ( dom f) & (f | A) is continuous;

      then

       A2: f is_integrable_on A & (f | A) is bounded by INTEGRA5: 10, INTEGRA5: 11;

      

       A3: Z c= ( dom (( id Z) ^ )) by A1, FUNCT_1: 101;

      

       A4: not 0 in Z

      proof

        assume

         A5: 0 in Z;

        ( dom (( id Z) ^ )) = (( dom ( id Z)) \ (( id Z) " { 0 })) by RFUNCT_1:def 2

        .= (( dom ( id Z)) \ { 0 }) by Lm1, A5;

        then not 0 in { 0 } by A5, A3, XBOOLE_0:def 5;

        hence thesis by TARSKI:def 1;

      end;

      then

       A6: ( cosec * (( id Z) ^ )) is_differentiable_on Z by A1, FDIFF_9: 9;

      

       A7: for x be Element of REAL st x in ( dom (( cosec * (( id Z) ^ )) `| Z)) holds ((( cosec * (( id Z) ^ )) `| Z) . x) = (f . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom (( cosec * (( id Z) ^ )) `| Z));

        then

         A8: x in Z by A6, FDIFF_1:def 7;

        

        then ((( cosec * (( id Z) ^ )) `| Z) . x) = (( cos . (1 / x)) / ((x ^2 ) * (( sin . (1 / x)) ^2 ))) by A1, A4, FDIFF_9: 9

        .= (f . x) by A1, A8;

        hence thesis;

      end;

      ( dom (( cosec * (( id Z) ^ )) `| Z)) = ( dom f) by A1, A6, FDIFF_1:def 7;

      then (( cosec * (( id Z) ^ )) `| Z) = f by A7, PARTFUN1: 5;

      hence thesis by A1, A2, A6, INTEGRA5: 13;

    end;

    theorem :: INTEGR14:17

    A c= Z & (for x st x in Z holds (f . x) = ((( exp_R . x) * ( sin . ( exp_R . x))) / (( cos . ( exp_R . x)) ^2 ))) & Z c= ( dom ( sec * exp_R )) & Z = ( dom f) & (f | A) is continuous implies ( integral (f,A)) = ((( sec * exp_R ) . ( upper_bound A)) - (( sec * exp_R ) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & (for x st x in Z holds (f . x) = ((( exp_R . x) * ( sin . ( exp_R . x))) / (( cos . ( exp_R . x)) ^2 ))) & Z c= ( dom ( sec * exp_R )) & Z = ( dom f) & (f | A) is continuous;

      then

       A2: f is_integrable_on A & (f | A) is bounded by INTEGRA5: 10, INTEGRA5: 11;

      

       A3: ( sec * exp_R ) is_differentiable_on Z by A1, FDIFF_9: 12;

      

       A4: for x be Element of REAL st x in ( dom (( sec * exp_R ) `| Z)) holds ((( sec * exp_R ) `| Z) . x) = (f . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom (( sec * exp_R ) `| Z));

        then

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

        

        then ((( sec * exp_R ) `| Z) . x) = ((( exp_R . x) * ( sin . ( exp_R . x))) / (( cos . ( exp_R . x)) ^2 )) by A1, FDIFF_9: 12

        .= (f . x) by A1, A5;

        hence thesis;

      end;

      ( dom (( sec * exp_R ) `| Z)) = ( dom f) by A1, A3, FDIFF_1:def 7;

      then (( sec * exp_R ) `| Z) = f by A4, PARTFUN1: 5;

      hence thesis by A1, A2, A3, INTEGRA5: 13;

    end;

    theorem :: INTEGR14:18

    A c= Z & (for x st x in Z holds (f . x) = ((( exp_R . x) * ( cos . ( exp_R . x))) / (( sin . ( exp_R . x)) ^2 ))) & Z c= ( dom ( cosec * exp_R )) & Z = ( dom f) & (f | A) is continuous implies ( integral (f,A)) = ((( - ( cosec * exp_R )) . ( upper_bound A)) - (( - ( cosec * exp_R )) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & (for x st x in Z holds (f . x) = ((( exp_R . x) * ( cos . ( exp_R . x))) / (( sin . ( exp_R . x)) ^2 ))) & Z c= ( dom ( cosec * exp_R )) & Z = ( dom f) & (f | A) is continuous;

      then

       A2: f is_integrable_on A & (f | A) is bounded by INTEGRA5: 10, INTEGRA5: 11;

      

       A3: ( - ( cosec * exp_R )) is_differentiable_on Z by A1, Th2;

      

       A4: for x be Element of REAL st x in ( dom (( - ( cosec * exp_R )) `| Z)) holds ((( - ( cosec * exp_R )) `| Z) . x) = (f . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom (( - ( cosec * exp_R )) `| Z));

        then

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

        

        then ((( - ( cosec * exp_R )) `| Z) . x) = ((( exp_R . x) * ( cos . ( exp_R . x))) / (( sin . ( exp_R . x)) ^2 )) by A1, Th2

        .= (f . x) by A1, A5;

        hence thesis;

      end;

      ( dom (( - ( cosec * exp_R )) `| Z)) = ( dom f) by A1, A3, FDIFF_1:def 7;

      then (( - ( cosec * exp_R )) `| Z) = f by A4, PARTFUN1: 5;

      hence thesis by A1, A2, A3, INTEGRA5: 13;

    end;

    theorem :: INTEGR14:19

    A c= Z & (for x st x in Z holds (f . x) = (( sin . ( ln . x)) / (x * (( cos . ( ln . x)) ^2 )))) & Z c= ( dom ( sec * ln )) & Z = ( dom f) & (f | A) is continuous implies ( integral (f,A)) = ((( sec * ln ) . ( upper_bound A)) - (( sec * ln ) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & (for x st x in Z holds (f . x) = (( sin . ( ln . x)) / (x * (( cos . ( ln . x)) ^2 )))) & Z c= ( dom ( sec * ln )) & Z = ( dom f) & (f | A) is continuous;

      then

       A2: f is_integrable_on A & (f | A) is bounded by INTEGRA5: 10, INTEGRA5: 11;

      

       A3: ( sec * ln ) is_differentiable_on Z by A1, FDIFF_9: 14;

      

       A4: for x be Element of REAL st x in ( dom (( sec * ln ) `| Z)) holds ((( sec * ln ) `| Z) . x) = (f . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom (( sec * ln ) `| Z));

        then

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

        

        then ((( sec * ln ) `| Z) . x) = (( sin . ( ln . x)) / (x * (( cos . ( ln . x)) ^2 ))) by A1, FDIFF_9: 14

        .= (f . x) by A1, A5;

        hence thesis;

      end;

      ( dom (( sec * ln ) `| Z)) = ( dom f) by A1, A3, FDIFF_1:def 7;

      then (( sec * ln ) `| Z) = f by A4, PARTFUN1: 5;

      hence thesis by A1, A2, A3, INTEGRA5: 13;

    end;

    theorem :: INTEGR14:20

    A c= Z & (for x st x in Z holds (f . x) = (( cos . ( ln . x)) / (x * (( sin . ( ln . x)) ^2 )))) & Z c= ( dom ( cosec * ln )) & Z = ( dom f) & (f | A) is continuous implies ( integral (f,A)) = ((( - ( cosec * ln )) . ( upper_bound A)) - (( - ( cosec * ln )) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & (for x st x in Z holds (f . x) = (( cos . ( ln . x)) / (x * (( sin . ( ln . x)) ^2 )))) & Z c= ( dom ( cosec * ln )) & Z = ( dom f) & (f | A) is continuous;

      then

       A2: f is_integrable_on A & (f | A) is bounded by INTEGRA5: 10, INTEGRA5: 11;

      

       A3: ( - ( cosec * ln )) is_differentiable_on Z by A1, Th3;

      

       A4: for x be Element of REAL st x in ( dom (( - ( cosec * ln )) `| Z)) holds ((( - ( cosec * ln )) `| Z) . x) = (f . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom (( - ( cosec * ln )) `| Z));

        then

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

        

        then ((( - ( cosec * ln )) `| Z) . x) = (( cos . ( ln . x)) / (x * (( sin . ( ln . x)) ^2 ))) by A1, Th3

        .= (f . x) by A1, A5;

        hence thesis;

      end;

      ( dom (( - ( cosec * ln )) `| Z)) = ( dom f) by A1, A3, FDIFF_1:def 7;

      then (( - ( cosec * ln )) `| Z) = f by A4, PARTFUN1: 5;

      hence thesis by A1, A2, A3, INTEGRA5: 13;

    end;

    theorem :: INTEGR14:21

    A c= Z & f = (( exp_R * sec ) (#) ( sin / ( cos ^2 ))) & Z = ( dom f) & (f | A) is continuous implies ( integral (f,A)) = ((( exp_R * sec ) . ( upper_bound A)) - (( exp_R * sec ) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & f = (( exp_R * sec ) (#) ( sin / ( cos ^2 ))) & Z = ( dom f) & (f | A) is continuous;

      then

       A2: f is_integrable_on A & (f | A) is bounded by INTEGRA5: 10, INTEGRA5: 11;

      Z = (( dom ( exp_R * sec )) /\ ( dom ( sin / ( cos ^2 )))) by A1, VALUED_1:def 4;

      then

       A3: Z c= ( dom ( exp_R * sec )) & Z c= ( dom ( sin / ( cos ^2 ))) by XBOOLE_1: 18;

      then

       A4: ( exp_R * sec ) is_differentiable_on Z by FDIFF_9: 16;

      

       A5: for x st x in Z holds (f . x) = ((( exp_R . ( sec . x)) * ( sin . x)) / (( cos . x) ^2 ))

      proof

        let x;

        assume

         A6: x in Z;

        ((( exp_R * sec ) (#) ( sin / ( cos ^2 ))) . x) = ((( exp_R * sec ) . x) * (( sin / ( cos ^2 )) . x)) by VALUED_1: 5

        .= (( exp_R . ( sec . x)) * (( sin / ( cos ^2 )) . x)) by A6, A3, FUNCT_1: 12

        .= (( exp_R . ( sec . x)) * (( sin . x) / (( cos ^2 ) . x))) by A3, A6, RFUNCT_1:def 1

        .= (( exp_R . ( sec . x)) * (( sin . x) / (( cos . x) ^2 ))) by VALUED_1: 11

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

        hence thesis by A1;

      end;

      

       A7: for x be Element of REAL st x in ( dom (( exp_R * sec ) `| Z)) holds ((( exp_R * sec ) `| Z) . x) = (f . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom (( exp_R * sec ) `| Z));

        then

         A8: x in Z by A4, FDIFF_1:def 7;

        

        then ((( exp_R * sec ) `| Z) . x) = ((( exp_R . ( sec . x)) * ( sin . x)) / (( cos . x) ^2 )) by A3, FDIFF_9: 16

        .= (f . x) by A5, A8;

        hence thesis;

      end;

      ( dom (( exp_R * sec ) `| Z)) = ( dom f) by A1, A4, FDIFF_1:def 7;

      then (( exp_R * sec ) `| Z) = f by A7, PARTFUN1: 5;

      hence thesis by A1, A2, A4, INTEGRA5: 13;

    end;

    theorem :: INTEGR14:22

    A c= Z & f = (( exp_R * cosec ) (#) ( cos / ( sin ^2 ))) & Z = ( dom f) & (f | A) is continuous implies ( integral (f,A)) = ((( - ( exp_R * cosec )) . ( upper_bound A)) - (( - ( exp_R * cosec )) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & f = (( exp_R * cosec ) (#) ( cos / ( sin ^2 ))) & Z = ( dom f) & (f | A) is continuous;

      then

       A2: f is_integrable_on A & (f | A) is bounded by INTEGRA5: 10, INTEGRA5: 11;

      Z = (( dom ( exp_R * cosec )) /\ ( dom ( cos / ( sin ^2 )))) by A1, VALUED_1:def 4;

      then

       A3: Z c= ( dom ( exp_R * cosec )) & Z c= ( dom ( cos / ( sin ^2 ))) by XBOOLE_1: 18;

      then

       A4: ( - ( exp_R * cosec )) is_differentiable_on Z by Th4;

      

       A5: for x st x in Z holds (f . x) = ((( exp_R . ( cosec . x)) * ( cos . x)) / (( sin . x) ^2 ))

      proof

        let x;

        assume

         A6: x in Z;

        ((( exp_R * cosec ) (#) ( cos / ( sin ^2 ))) . x) = ((( exp_R * cosec ) . x) * (( cos / ( sin ^2 )) . x)) by VALUED_1: 5

        .= (( exp_R . ( cosec . x)) * (( cos / ( sin ^2 )) . x)) by A6, A3, FUNCT_1: 12

        .= (( exp_R . ( cosec . x)) * (( cos . x) / (( sin ^2 ) . x))) by A3, A6, RFUNCT_1:def 1

        .= (( exp_R . ( cosec . x)) * (( cos . x) / (( sin . x) ^2 ))) by VALUED_1: 11

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

        hence thesis by A1;

      end;

      

       A7: for x be Element of REAL st x in ( dom (( - ( exp_R * cosec )) `| Z)) holds ((( - ( exp_R * cosec )) `| Z) . x) = (f . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom (( - ( exp_R * cosec )) `| Z));

        then

         A8: x in Z by A4, FDIFF_1:def 7;

        

        then ((( - ( exp_R * cosec )) `| Z) . x) = ((( exp_R . ( cosec . x)) * ( cos . x)) / (( sin . x) ^2 )) by A3, Th4

        .= (f . x) by A5, A8;

        hence thesis;

      end;

      ( dom (( - ( exp_R * cosec )) `| Z)) = ( dom f) by A1, A4, FDIFF_1:def 7;

      then (( - ( exp_R * cosec )) `| Z) = f by A7, PARTFUN1: 5;

      hence thesis by A1, A2, A4, INTEGRA5: 13;

    end;

    theorem :: INTEGR14:23

    A c= Z & Z c= ( dom ( ln * sec )) & Z = ( dom tan ) & ( tan | A) is continuous implies ( integral ( tan ,A)) = ((( ln * sec ) . ( upper_bound A)) - (( ln * sec ) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & Z c= ( dom ( ln * sec )) & Z = ( dom tan ) & ( tan | A) is continuous;

      then

       A2: tan is_integrable_on A & ( tan | A) is bounded by INTEGRA5: 10, INTEGRA5: 11;

      

       A3: ( ln * sec ) is_differentiable_on Z by A1, FDIFF_9: 18;

      

       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 be Element of REAL st x in ( dom (( ln * sec ) `| Z)) holds ((( ln * sec ) `| Z) . x) = ( tan . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom (( ln * sec ) `| Z));

        then

         A6: x in Z by A3, FDIFF_1:def 7;

        then

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

        ((( ln * sec ) `| Z) . x) = ( tan x) by A1, A6, FDIFF_9: 18

        .= ( tan . x) by A7, SIN_COS9: 15;

        hence thesis;

      end;

      ( dom (( ln * sec ) `| Z)) = ( dom tan ) by A1, A3, FDIFF_1:def 7;

      then (( ln * sec ) `| Z) = tan by A5, PARTFUN1: 5;

      hence thesis by A1, A2, A3, INTEGRA5: 13;

    end;

    theorem :: INTEGR14:24

    A c= Z & Z c= ( dom ( ln * cosec )) & Z = ( dom cot ) & (( - cot ) | A) is continuous implies ( integral (( - cot ),A)) = ((( ln * cosec ) . ( upper_bound A)) - (( ln * cosec ) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & Z c= ( dom ( ln * cosec )) & Z = ( dom cot ) & (( - cot ) | A) is continuous;

      then

       A2: Z = ( dom ( - cot )) by VALUED_1: 8;

      then

       A3: ( - cot ) is_integrable_on A & (( - cot ) | A) is bounded by A1, INTEGRA5: 10, INTEGRA5: 11;

      

       A4: ( ln * cosec ) is_differentiable_on Z by A1, FDIFF_9: 19;

      

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

      

       A6: for x be Element of REAL st x in ( dom (( ln * cosec ) `| Z)) holds ((( ln * cosec ) `| Z) . x) = (( - cot ) . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom (( ln * cosec ) `| Z));

        then

         A7: x in Z by A4, FDIFF_1:def 7;

        then

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

        ((( ln * cosec ) `| Z) . x) = ( - ( cot x)) by A1, A7, FDIFF_9: 19

        .= ( - ( cot . x)) by A8, SIN_COS9: 16

        .= (( - cot ) . x) by VALUED_1: 8;

        hence thesis;

      end;

      ( dom (( ln * cosec ) `| Z)) = ( dom ( - cot )) by A2, A4, FDIFF_1:def 7;

      then (( ln * cosec ) `| Z) = ( - cot ) by A6, PARTFUN1: 5;

      hence thesis by A1, A3, A4, INTEGRA5: 13;

    end;

    theorem :: INTEGR14:25

    A c= Z & Z c= ( dom ( ln * cosec )) & Z = ( dom cot ) & ( cot | A) is continuous implies ( integral ( cot ,A)) = ((( - ( ln * cosec )) . ( upper_bound A)) - (( - ( ln * cosec )) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & Z c= ( dom ( ln * cosec )) & Z = ( dom cot ) & ( cot | A) is continuous;

      then

       A2: cot is_integrable_on A & ( cot | A) is bounded by INTEGRA5: 10, INTEGRA5: 11;

      

       A3: ( - ( ln * cosec )) is_differentiable_on Z by A1, Th5;

      

       A4: for x be Element of REAL st x in ( dom (( - ( ln * cosec )) `| Z)) holds ((( - ( ln * cosec )) `| Z) . x) = ( cot . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom (( - ( ln * cosec )) `| Z));

        then x in Z by A3, FDIFF_1:def 7;

        then ((( - ( ln * cosec )) `| Z) . x) = ( cot . x) by A1, Th5;

        hence thesis;

      end;

      ( dom (( - ( ln * cosec )) `| Z)) = ( dom cot ) by A1, A3, FDIFF_1:def 7;

      then (( - ( ln * cosec )) `| Z) = cot by A4, PARTFUN1: 5;

      hence thesis by A1, A2, A3, INTEGRA5: 13;

    end;

    theorem :: INTEGR14:26

    A c= Z & (for x st x in Z holds (f . x) = ((n * ( sin . x)) / (( cos . x) #Z (n + 1)))) & Z c= ( dom (( #Z n) * sec )) & 1 <= n & Z = ( dom f) & (f | A) is continuous implies ( integral (f,A)) = (((( #Z n) * sec ) . ( upper_bound A)) - ((( #Z n) * sec ) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & (for x st x in Z holds (f . x) = ((n * ( sin . x)) / (( cos . x) #Z (n + 1)))) & Z c= ( dom (( #Z n) * sec )) & 1 <= n & Z = ( dom f) & (f | A) is continuous;

      then

       A2: f is_integrable_on A & (f | A) is bounded by INTEGRA5: 10, INTEGRA5: 11;

      

       A3: (( #Z n) * sec ) is_differentiable_on Z by A1, FDIFF_9: 20;

      

       A4: for x be Element of REAL st x in ( dom ((( #Z n) * sec ) `| Z)) holds (((( #Z n) * sec ) `| Z) . x) = (f . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom ((( #Z n) * sec ) `| Z));

        then

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

        

        then (((( #Z n) * sec ) `| Z) . x) = ((n * ( sin . x)) / (( cos . x) #Z (n + 1))) by A1, FDIFF_9: 20

        .= (f . x) by A1, A5;

        hence thesis;

      end;

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

      then ((( #Z n) * sec ) `| Z) = f by A4, PARTFUN1: 5;

      hence thesis by A1, A2, A3, INTEGRA5: 13;

    end;

    theorem :: INTEGR14:27

    A c= Z & (for x st x in Z holds (f . x) = ((n * ( cos . x)) / (( sin . x) #Z (n + 1)))) & Z c= ( dom (( #Z n) * cosec )) & 1 <= n & Z = ( dom f) & (f | A) is continuous implies ( integral (f,A)) = ((( - (( #Z n) * cosec )) . ( upper_bound A)) - (( - (( #Z n) * cosec )) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & (for x st x in Z holds (f . x) = ((n * ( cos . x)) / (( sin . x) #Z (n + 1)))) & Z c= ( dom (( #Z n) * cosec )) & 1 <= n & Z = ( dom f) & (f | A) is continuous;

      then

       A2: f is_integrable_on A & (f | A) is bounded by INTEGRA5: 10, INTEGRA5: 11;

      

       A3: ( - (( #Z n) * cosec )) is_differentiable_on Z by A1, Th6;

      

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

      proof

        let x be Element of REAL ;

        assume x in ( dom (( - (( #Z n) * cosec )) `| Z));

        then

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

        

        then ((( - (( #Z n) * cosec )) `| Z) . x) = ((n * ( cos . x)) / (( sin . x) #Z (n + 1))) by A1, Th6

        .= (f . x) by A1, A5;

        hence thesis;

      end;

      ( dom (( - (( #Z n) * cosec )) `| Z)) = ( dom f) by A1, A3, FDIFF_1:def 7;

      then (( - (( #Z n) * cosec )) `| Z) = f by A4, PARTFUN1: 5;

      hence thesis by A1, A2, A3, INTEGRA5: 13;

    end;

    theorem :: INTEGR14:28

    A c= Z & (for x st x in Z holds (f . x) = ((( exp_R . x) / ( cos . x)) + ((( exp_R . x) * ( sin . x)) / (( cos . x) ^2 )))) & Z c= ( dom ( exp_R (#) sec )) & Z = ( dom f) & (f | A) is continuous implies ( integral (f,A)) = ((( exp_R (#) sec ) . ( upper_bound A)) - (( exp_R (#) sec ) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & (for x st x in Z holds (f . x) = ((( exp_R . x) / ( cos . x)) + ((( exp_R . x) * ( sin . x)) / (( cos . x) ^2 )))) & Z c= ( dom ( exp_R (#) sec )) & Z = ( dom f) & (f | A) is continuous;

      then

       A2: f is_integrable_on A & (f | A) is bounded by INTEGRA5: 10, INTEGRA5: 11;

      

       A3: ( exp_R (#) sec ) is_differentiable_on Z by A1, FDIFF_9: 24;

      

       A4: for x be Element of REAL st x in ( dom (( exp_R (#) sec ) `| Z)) holds ((( exp_R (#) sec ) `| Z) . x) = (f . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom (( exp_R (#) sec ) `| Z));

        then

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

        

        then ((( exp_R (#) sec ) `| Z) . x) = ((( exp_R . x) / ( cos . x)) + ((( exp_R . x) * ( sin . x)) / (( cos . x) ^2 ))) by A1, FDIFF_9: 24

        .= (f . x) by A1, A5;

        hence thesis;

      end;

      ( dom (( exp_R (#) sec ) `| Z)) = ( dom f) by A1, A3, FDIFF_1:def 7;

      then (( exp_R (#) sec ) `| Z) = f by A4, PARTFUN1: 5;

      hence thesis by A1, A2, A3, INTEGRA5: 13;

    end;

    theorem :: INTEGR14:29

    A c= Z & (for x st x in Z holds (f . x) = ((( exp_R . x) / ( sin . x)) - ((( exp_R . x) * ( cos . x)) / (( sin . x) ^2 )))) & Z c= ( dom ( exp_R (#) cosec )) & Z = ( dom f) & (f | A) is continuous implies ( integral (f,A)) = ((( exp_R (#) cosec ) . ( upper_bound A)) - (( exp_R (#) cosec ) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & (for x st x in Z holds (f . x) = ((( exp_R . x) / ( sin . x)) - ((( exp_R . x) * ( cos . x)) / (( sin . x) ^2 )))) & Z c= ( dom ( exp_R (#) cosec )) & Z = ( dom f) & (f | A) is continuous;

      then

       A2: f is_integrable_on A & (f | A) is bounded by INTEGRA5: 10, INTEGRA5: 11;

      

       A3: ( exp_R (#) cosec ) is_differentiable_on Z by A1, FDIFF_9: 25;

      

       A4: for x be Element of REAL st x in ( dom (( exp_R (#) cosec ) `| Z)) holds ((( exp_R (#) cosec ) `| Z) . x) = (f . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom (( exp_R (#) cosec ) `| Z));

        then

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

        

        then ((( exp_R (#) cosec ) `| Z) . x) = ((( exp_R . x) / ( sin . x)) - ((( exp_R . x) * ( cos . x)) / (( sin . x) ^2 ))) by A1, FDIFF_9: 25

        .= (f . x) by A1, A5;

        hence thesis;

      end;

      ( dom (( exp_R (#) cosec ) `| Z)) = ( dom f) by A1, A3, FDIFF_1:def 7;

      then (( exp_R (#) cosec ) `| Z) = f by A4, PARTFUN1: 5;

      hence thesis by A1, A2, A3, INTEGRA5: 13;

    end;

    theorem :: INTEGR14:30

    A c= Z & (for x st x in Z holds (f . x) = ((( sin . (a * x)) - (( cos . (a * x)) ^2 )) / (( cos . (a * x)) ^2 ))) & (Z c= ( dom (((1 / a) (#) ( sec * f1)) - ( id Z))) & for x st x in Z holds (f1 . x) = (a * x) & a <> 0 ) & Z = ( dom f) & (f | A) is continuous implies ( integral (f,A)) = (((((1 / a) (#) ( sec * f1)) - ( id Z)) . ( upper_bound A)) - ((((1 / a) (#) ( sec * f1)) - ( id Z)) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & (for x st x in Z holds (f . x) = ((( sin . (a * x)) - (( cos . (a * x)) ^2 )) / (( cos . (a * x)) ^2 ))) & (Z c= ( dom (((1 / a) (#) ( sec * f1)) - ( id Z))) & for x st x in Z holds (f1 . x) = (a * x) & a <> 0 ) & Z = ( dom f) & (f | A) is continuous;

      then

       A2: f is_integrable_on A & (f | A) is bounded by INTEGRA5: 10, INTEGRA5: 11;

      

       A3: (((1 / a) (#) ( sec * f1)) - ( id Z)) is_differentiable_on Z by A1, FDIFF_9: 26;

      

       A4: for x be Element of REAL st x in ( dom ((((1 / a) (#) ( sec * f1)) - ( id Z)) `| Z)) holds (((((1 / a) (#) ( sec * f1)) - ( id Z)) `| Z) . x) = (f . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom ((((1 / a) (#) ( sec * f1)) - ( id Z)) `| Z));

        then

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

        

        then (((((1 / a) (#) ( sec * f1)) - ( id Z)) `| Z) . x) = ((( sin . (a * x)) - (( cos . (a * x)) ^2 )) / (( cos . (a * x)) ^2 )) by A1, FDIFF_9: 26

        .= (f . x) by A1, A5;

        hence thesis;

      end;

      ( dom ((((1 / a) (#) ( sec * f1)) - ( id Z)) `| Z)) = ( dom f) by A1, A3, FDIFF_1:def 7;

      then ((((1 / a) (#) ( sec * f1)) - ( id Z)) `| Z) = f by A4, PARTFUN1: 5;

      hence thesis by A1, A2, A3, INTEGRA5: 13;

    end;

    theorem :: INTEGR14:31

    A c= Z & (for x st x in Z holds (f . x) = ((( cos . (a * x)) - (( sin . (a * x)) ^2 )) / (( sin . (a * x)) ^2 ))) & (Z c= ( dom ((( - (1 / a)) (#) ( cosec * f1)) - ( id Z))) & for x st x in Z holds (f1 . x) = (a * x) & a <> 0 ) & Z = ( dom f) & (f | A) is continuous implies ( integral (f,A)) = ((((( - (1 / a)) (#) ( cosec * f1)) - ( id Z)) . ( upper_bound A)) - (((( - (1 / a)) (#) ( cosec * f1)) - ( id Z)) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & (for x st x in Z holds (f . x) = ((( cos . (a * x)) - (( sin . (a * x)) ^2 )) / (( sin . (a * x)) ^2 ))) & (Z c= ( dom ((( - (1 / a)) (#) ( cosec * f1)) - ( id Z))) & for x st x in Z holds (f1 . x) = (a * x) & a <> 0 ) & Z = ( dom f) & (f | A) is continuous;

      then

       A2: f is_integrable_on A & (f | A) is bounded by INTEGRA5: 10, INTEGRA5: 11;

      

       A3: ((( - (1 / a)) (#) ( cosec * f1)) - ( id Z)) is_differentiable_on Z by A1, FDIFF_9: 27;

      

       A4: for x be Element of REAL st x in ( dom (((( - (1 / a)) (#) ( cosec * f1)) - ( id Z)) `| Z)) holds ((((( - (1 / a)) (#) ( cosec * f1)) - ( id Z)) `| Z) . x) = (f . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom (((( - (1 / a)) (#) ( cosec * f1)) - ( id Z)) `| Z));

        then

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

        

        then ((((( - (1 / a)) (#) ( cosec * f1)) - ( id Z)) `| Z) . x) = ((( cos . (a * x)) - (( sin . (a * x)) ^2 )) / (( sin . (a * x)) ^2 )) by A1, FDIFF_9: 27

        .= (f . x) by A1, A5;

        hence thesis;

      end;

      ( dom (((( - (1 / a)) (#) ( cosec * f1)) - ( id Z)) `| Z)) = ( dom f) by A1, A3, FDIFF_1:def 7;

      then (((( - (1 / a)) (#) ( cosec * f1)) - ( id Z)) `| Z) = f by A4, PARTFUN1: 5;

      hence thesis by A1, A2, A3, INTEGRA5: 13;

    end;

    theorem :: INTEGR14:32

    A c= Z & (for x st x in Z holds (f . x) = (((1 / ( cos . x)) / x) + ((( ln . x) * ( sin . x)) / (( cos . x) ^2 )))) & Z c= ( dom ( ln (#) sec )) & Z = ( dom f) & (f | A) is continuous implies ( integral (f,A)) = ((( ln (#) sec ) . ( upper_bound A)) - (( ln (#) sec ) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & (for x st x in Z holds (f . x) = (((1 / ( cos . x)) / x) + ((( ln . x) * ( sin . x)) / (( cos . x) ^2 )))) & Z c= ( dom ( ln (#) sec )) & Z = ( dom f) & (f | A) is continuous;

      then

       A2: f is_integrable_on A & (f | A) is bounded by INTEGRA5: 10, INTEGRA5: 11;

      

       A3: ( ln (#) sec ) is_differentiable_on Z by A1, FDIFF_9: 30;

      

       A4: for x be Element of REAL st x in ( dom (( ln (#) sec ) `| Z)) holds ((( ln (#) sec ) `| Z) . x) = (f . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom (( ln (#) sec ) `| Z));

        then

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

        

        then ((( ln (#) sec ) `| Z) . x) = (((1 / ( cos . x)) / x) + ((( ln . x) * ( sin . x)) / (( cos . x) ^2 ))) by A1, FDIFF_9: 30

        .= (f . x) by A1, A5;

        hence thesis;

      end;

      ( dom (( ln (#) sec ) `| Z)) = ( dom f) by A1, A3, FDIFF_1:def 7;

      then (( ln (#) sec ) `| Z) = f by A4, PARTFUN1: 5;

      hence thesis by A1, A2, A3, INTEGRA5: 13;

    end;

    theorem :: INTEGR14:33

    A c= Z & (for x st x in Z holds (f . x) = (((1 / ( sin . x)) / x) - ((( ln . x) * ( cos . x)) / (( sin . x) ^2 )))) & Z c= ( dom ( ln (#) cosec )) & Z = ( dom f) & (f | A) is continuous implies ( integral (f,A)) = ((( ln (#) cosec ) . ( upper_bound A)) - (( ln (#) cosec ) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & (for x st x in Z holds (f . x) = (((1 / ( sin . x)) / x) - ((( ln . x) * ( cos . x)) / (( sin . x) ^2 )))) & Z c= ( dom ( ln (#) cosec )) & Z = ( dom f) & (f | A) is continuous;

      then

       A2: f is_integrable_on A & (f | A) is bounded by INTEGRA5: 10, INTEGRA5: 11;

      

       A3: ( ln (#) cosec ) is_differentiable_on Z by A1, FDIFF_9: 31;

      

       A4: for x be Element of REAL st x in ( dom (( ln (#) cosec ) `| Z)) holds ((( ln (#) cosec ) `| Z) . x) = (f . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom (( ln (#) cosec ) `| Z));

        then

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

        

        then ((( ln (#) cosec ) `| Z) . x) = (((1 / ( sin . x)) / x) - ((( ln . x) * ( cos . x)) / (( sin . x) ^2 ))) by A1, FDIFF_9: 31

        .= (f . x) by A1, A5;

        hence thesis;

      end;

      ( dom (( ln (#) cosec ) `| Z)) = ( dom f) by A1, A3, FDIFF_1:def 7;

      then (( ln (#) cosec ) `| Z) = f by A4, PARTFUN1: 5;

      hence thesis by A1, A2, A3, INTEGRA5: 13;

    end;

    theorem :: INTEGR14:34

    A c= Z & (for x st x in Z holds (f . x) = (((1 / ( cos . x)) / (x ^2 )) - ((( sin . x) / x) / (( cos . x) ^2 )))) & Z c= ( dom ((( id Z) ^ ) (#) sec )) & Z = ( dom f) & (f | A) is continuous implies ( integral (f,A)) = ((( - ((( id Z) ^ ) (#) sec )) . ( upper_bound A)) - (( - ((( id Z) ^ ) (#) sec )) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & (for x st x in Z holds (f . x) = (((1 / ( cos . x)) / (x ^2 )) - ((( sin . x) / x) / (( cos . x) ^2 )))) & Z c= ( dom ((( id Z) ^ ) (#) sec )) & Z = ( dom f) & (f | A) is continuous;

      then

       A2: f is_integrable_on A & (f | A) is bounded by INTEGRA5: 10, INTEGRA5: 11;

      

       A3: ( - ((( id Z) ^ ) (#) sec )) is_differentiable_on Z by A1, Th7;

      

       A4: for x be Element of REAL st x in ( dom (( - ((( id Z) ^ ) (#) sec )) `| Z)) holds ((( - ((( id Z) ^ ) (#) sec )) `| Z) . x) = (f . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom (( - ((( id Z) ^ ) (#) sec )) `| Z));

        then

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

        

        then ((( - ((( id Z) ^ ) (#) sec )) `| Z) . x) = (((1 / ( cos . x)) / (x ^2 )) - ((( sin . x) / x) / (( cos . x) ^2 ))) by A1, Th7

        .= (f . x) by A1, A5;

        hence thesis;

      end;

      ( dom (( - ((( id Z) ^ ) (#) sec )) `| Z)) = ( dom f) by A1, A3, FDIFF_1:def 7;

      then (( - ((( id Z) ^ ) (#) sec )) `| Z) = f by A4, PARTFUN1: 5;

      hence thesis by A1, A2, A3, INTEGRA5: 13;

    end;

    theorem :: INTEGR14:35

    A c= Z & (for x st x in Z holds (f . x) = (((1 / ( sin . x)) / (x ^2 )) + ((( cos . x) / x) / (( sin . x) ^2 )))) & Z c= ( dom ((( id Z) ^ ) (#) cosec )) & Z = ( dom f) & (f | A) is continuous implies ( integral (f,A)) = ((( - ((( id Z) ^ ) (#) cosec )) . ( upper_bound A)) - (( - ((( id Z) ^ ) (#) cosec )) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & (for x st x in Z holds (f . x) = (((1 / ( sin . x)) / (x ^2 )) + ((( cos . x) / x) / (( sin . x) ^2 )))) & Z c= ( dom ((( id Z) ^ ) (#) cosec )) & Z = ( dom f) & (f | A) is continuous;

      then

       A2: f is_integrable_on A & (f | A) is bounded by INTEGRA5: 10, INTEGRA5: 11;

      

       A3: ( - ((( id Z) ^ ) (#) cosec )) is_differentiable_on Z by A1, Th8;

      

       A4: for x be Element of REAL st x in ( dom (( - ((( id Z) ^ ) (#) cosec )) `| Z)) holds ((( - ((( id Z) ^ ) (#) cosec )) `| Z) . x) = (f . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom (( - ((( id Z) ^ ) (#) cosec )) `| Z));

        then

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

        

        then ((( - ((( id Z) ^ ) (#) cosec )) `| Z) . x) = (((1 / ( sin . x)) / (x ^2 )) + ((( cos . x) / x) / (( sin . x) ^2 ))) by A1, Th8

        .= (f . x) by A1, A5;

        hence thesis;

      end;

      ( dom (( - ((( id Z) ^ ) (#) cosec )) `| Z)) = ( dom f) by A1, A3, FDIFF_1:def 7;

      then (( - ((( id Z) ^ ) (#) cosec )) `| Z) = f by A4, PARTFUN1: 5;

      hence thesis by A1, A2, A3, INTEGRA5: 13;

    end;

    theorem :: INTEGR14:36

    A c= Z & (for x st x in Z holds (f . x) = ((( cos . x) * ( sin . ( sin . x))) / (( cos . ( sin . x)) ^2 ))) & Z c= ( dom ( sec * sin )) & Z = ( dom f) & (f | A) is continuous implies ( integral (f,A)) = ((( sec * sin ) . ( upper_bound A)) - (( sec * sin ) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & (for x st x in Z holds (f . x) = ((( cos . x) * ( sin . ( sin . x))) / (( cos . ( sin . x)) ^2 ))) & Z c= ( dom ( sec * sin )) & Z = ( dom f) & (f | A) is continuous;

      then

       A2: f is_integrable_on A & (f | A) is bounded by INTEGRA5: 10, INTEGRA5: 11;

      

       A3: ( sec * sin ) is_differentiable_on Z by A1, FDIFF_9: 34;

      

       A4: for x be Element of REAL st x in ( dom (( sec * sin ) `| Z)) holds ((( sec * sin ) `| Z) . x) = (f . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom (( sec * sin ) `| Z));

        then

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

        

        then ((( sec * sin ) `| Z) . x) = ((( cos . x) * ( sin . ( sin . x))) / (( cos . ( sin . x)) ^2 )) by A1, FDIFF_9: 34

        .= (f . x) by A1, A5;

        hence thesis;

      end;

      ( dom (( sec * sin ) `| Z)) = ( dom f) by A1, A3, FDIFF_1:def 7;

      then (( sec * sin ) `| Z) = f by A4, PARTFUN1: 5;

      hence thesis by A1, A2, A3, INTEGRA5: 13;

    end;

    theorem :: INTEGR14:37

    A c= Z & (for x st x in Z holds (f . x) = ((( sin . x) * ( sin . ( cos . x))) / (( cos . ( cos . x)) ^2 ))) & Z c= ( dom ( sec * cos )) & Z = ( dom f) & (f | A) is continuous implies ( integral (f,A)) = ((( - ( sec * cos )) . ( upper_bound A)) - (( - ( sec * cos )) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & (for x st x in Z holds (f . x) = ((( sin . x) * ( sin . ( cos . x))) / (( cos . ( cos . x)) ^2 ))) & Z c= ( dom ( sec * cos )) & Z = ( dom f) & (f | A) is continuous;

      then

       A2: f is_integrable_on A & (f | A) is bounded by INTEGRA5: 10, INTEGRA5: 11;

      

       A3: Z c= ( dom ( - ( sec * cos ))) by A1, VALUED_1: 8;

      

       A4: ( sec * cos ) is_differentiable_on Z by A1, FDIFF_9: 35;

      then

       A5: (( - 1) (#) ( sec * cos )) is_differentiable_on Z by A3, FDIFF_1: 20;

      

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

      proof

        let x;

        assume

         A7: x in Z;

        ((( - ( sec * cos )) `| Z) . x) = ((( - 1) (#) (( sec * cos ) `| Z)) . x) by A4, FDIFF_2: 19

        .= (( - 1) * ((( sec * cos ) `| Z) . x)) by VALUED_1: 6

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

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

        hence thesis;

      end;

      

       A8: for x be Element of REAL st x in ( dom (( - ( sec * cos )) `| Z)) holds ((( - ( sec * cos )) `| Z) . x) = (f . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom (( - ( sec * cos )) `| Z));

        then

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

        

        then ((( - ( sec * cos )) `| Z) . x) = ((( sin . x) * ( sin . ( cos . x))) / (( cos . ( cos . x)) ^2 )) by A6

        .= (f . x) by A1, A9;

        hence thesis;

      end;

      ( dom (( - ( sec * cos )) `| Z)) = ( dom f) by A1, A5, FDIFF_1:def 7;

      then (( - ( sec * cos )) `| Z) = f by A8, PARTFUN1: 5;

      hence thesis by A1, A2, A5, INTEGRA5: 13;

    end;

    theorem :: INTEGR14:38

    A c= Z & (for x st x in Z holds (f . x) = ((( cos . x) * ( cos . ( sin . x))) / (( sin . ( sin . x)) ^2 ))) & Z c= ( dom ( cosec * sin )) & Z = ( dom f) & (f | A) is continuous implies ( integral (f,A)) = ((( - ( cosec * sin )) . ( upper_bound A)) - (( - ( cosec * sin )) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & (for x st x in Z holds (f . x) = ((( cos . x) * ( cos . ( sin . x))) / (( sin . ( sin . x)) ^2 ))) & Z c= ( dom ( cosec * sin )) & Z = ( dom f) & (f | A) is continuous;

      then

       A2: f is_integrable_on A & (f | A) is bounded by INTEGRA5: 10, INTEGRA5: 11;

      

       A3: ( - ( cosec * sin )) is_differentiable_on Z by A1, Th9;

      

       A4: for x be Element of REAL st x in ( dom (( - ( cosec * sin )) `| Z)) holds ((( - ( cosec * sin )) `| Z) . x) = (f . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom (( - ( cosec * sin )) `| Z));

        then

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

        

        then ((( - ( cosec * sin )) `| Z) . x) = ((( cos . x) * ( cos . ( sin . x))) / (( sin . ( sin . x)) ^2 )) by A1, Th9

        .= (f . x) by A1, A5;

        hence thesis;

      end;

      ( dom (( - ( cosec * sin )) `| Z)) = ( dom f) by A1, A3, FDIFF_1:def 7;

      then (( - ( cosec * sin )) `| Z) = f by A4, PARTFUN1: 5;

      hence thesis by A1, A2, A3, INTEGRA5: 13;

    end;

    theorem :: INTEGR14:39

    A c= Z & (for x st x in Z holds (f . x) = ((( sin . x) * ( cos . ( cos . x))) / (( sin . ( cos . x)) ^2 ))) & Z c= ( dom ( cosec * cos )) & Z = ( dom f) & (f | A) is continuous implies ( integral (f,A)) = ((( cosec * cos ) . ( upper_bound A)) - (( cosec * cos ) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & (for x st x in Z holds (f . x) = ((( sin . x) * ( cos . ( cos . x))) / (( sin . ( cos . x)) ^2 ))) & Z c= ( dom ( cosec * cos )) & Z = ( dom f) & (f | A) is continuous;

      then

       A2: f is_integrable_on A & (f | A) is bounded by INTEGRA5: 10, INTEGRA5: 11;

      

       A3: ( cosec * cos ) is_differentiable_on Z by A1, FDIFF_9: 37;

      

       A4: for x be Element of REAL st x in ( dom (( cosec * cos ) `| Z)) holds ((( cosec * cos ) `| Z) . x) = (f . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom (( cosec * cos ) `| Z));

        then

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

        

        then ((( cosec * cos ) `| Z) . x) = ((( sin . x) * ( cos . ( cos . x))) / (( sin . ( cos . x)) ^2 )) by A1, FDIFF_9: 37

        .= (f . x) by A1, A5;

        hence thesis;

      end;

      ( dom (( cosec * cos ) `| Z)) = ( dom f) by A1, A3, FDIFF_1:def 7;

      then (( cosec * cos ) `| Z) = f by A4, PARTFUN1: 5;

      hence thesis by A1, A2, A3, INTEGRA5: 13;

    end;

    theorem :: INTEGR14:40

    A c= Z & (for x st x in Z holds (f . x) = ((( sin . ( tan . x)) / (( cos . x) ^2 )) / (( cos . ( tan . x)) ^2 ))) & Z c= ( dom ( sec * tan )) & Z = ( dom f) & (f | A) is continuous implies ( integral (f,A)) = ((( sec * tan ) . ( upper_bound A)) - (( sec * tan ) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & (for x st x in Z holds (f . x) = ((( sin . ( tan . x)) / (( cos . x) ^2 )) / (( cos . ( tan . x)) ^2 ))) & Z c= ( dom ( sec * tan )) & Z = ( dom f) & (f | A) is continuous;

      then

       A2: f is_integrable_on A & (f | A) is bounded by INTEGRA5: 10, INTEGRA5: 11;

      

       A3: ( sec * tan ) is_differentiable_on Z by A1, FDIFF_9: 38;

      

       A4: for x be Element of REAL st x in ( dom (( sec * tan ) `| Z)) holds ((( sec * tan ) `| Z) . x) = (f . x)

      proof

        let x be Element of REAL ;

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

        then

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

        

        then ((( sec * tan ) `| Z) . x) = ((( sin . ( tan . x)) / (( cos . x) ^2 )) / (( cos . ( tan . x)) ^2 )) by A1, FDIFF_9: 38

        .= (f . x) by A1, A5;

        hence thesis;

      end;

      ( dom (( sec * tan ) `| Z)) = ( dom f) by A1, A3, FDIFF_1:def 7;

      then (( sec * tan ) `| Z) = f by A4, PARTFUN1: 5;

      hence thesis by A1, A2, A3, INTEGRA5: 13;

    end;

    theorem :: INTEGR14:41

    A c= Z & (for x st x in Z holds (f . x) = ((( sin . ( cot . x)) / (( sin . x) ^2 )) / (( cos . ( cot . x)) ^2 ))) & Z c= ( dom ( sec * cot )) & Z = ( dom f) & (f | A) is continuous implies ( integral (f,A)) = ((( - ( sec * cot )) . ( upper_bound A)) - (( - ( sec * cot )) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & (for x st x in Z holds (f . x) = ((( sin . ( cot . x)) / (( sin . x) ^2 )) / (( cos . ( cot . x)) ^2 ))) & Z c= ( dom ( sec * cot )) & Z = ( dom f) & (f | A) is continuous;

      then

       A2: f is_integrable_on A & (f | A) is bounded by INTEGRA5: 10, INTEGRA5: 11;

      

       A3: ( - ( sec * cot )) is_differentiable_on Z by A1, Th10;

      

       A4: for x be Element of REAL st x in ( dom (( - ( sec * cot )) `| Z)) holds ((( - ( sec * cot )) `| Z) . x) = (f . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom (( - ( sec * cot )) `| Z));

        then

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

        

        then ((( - ( sec * cot )) `| Z) . x) = ((( sin . ( cot . x)) / (( sin . x) ^2 )) / (( cos . ( cot . x)) ^2 )) by A1, Th10

        .= (f . x) by A1, A5;

        hence thesis;

      end;

      ( dom (( - ( sec * cot )) `| Z)) = ( dom f) by A1, A3, FDIFF_1:def 7;

      then (( - ( sec * cot )) `| Z) = f by A4, PARTFUN1: 5;

      hence thesis by A1, A2, A3, INTEGRA5: 13;

    end;

    theorem :: INTEGR14:42

    A c= Z & (for x st x in Z holds (f . x) = ((( cos . ( tan . x)) / (( cos . x) ^2 )) / (( sin . ( tan . x)) ^2 ))) & Z c= ( dom ( cosec * tan )) & Z = ( dom f) & (f | A) is continuous implies ( integral (f,A)) = ((( - ( cosec * tan )) . ( upper_bound A)) - (( - ( cosec * tan )) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & (for x st x in Z holds (f . x) = ((( cos . ( tan . x)) / (( cos . x) ^2 )) / (( sin . ( tan . x)) ^2 ))) & Z c= ( dom ( cosec * tan )) & Z = ( dom f) & (f | A) is continuous;

      then

       A2: f is_integrable_on A & (f | A) is bounded by INTEGRA5: 10, INTEGRA5: 11;

      

       A3: ( - ( cosec * tan )) is_differentiable_on Z by A1, Th11;

      

       A4: for x be Element of REAL st x in ( dom (( - ( cosec * tan )) `| Z)) holds ((( - ( cosec * tan )) `| Z) . x) = (f . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom (( - ( cosec * tan )) `| Z));

        then

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

        

        then ((( - ( cosec * tan )) `| Z) . x) = ((( cos . ( tan . x)) / (( cos . x) ^2 )) / (( sin . ( tan . x)) ^2 )) by A1, Th11

        .= (f . x) by A1, A5;

        hence thesis;

      end;

      ( dom (( - ( cosec * tan )) `| Z)) = ( dom f) by A1, A3, FDIFF_1:def 7;

      then (( - ( cosec * tan )) `| Z) = f by A4, PARTFUN1: 5;

      hence thesis by A1, A2, A3, INTEGRA5: 13;

    end;

    theorem :: INTEGR14:43

    A c= Z & (for x st x in Z holds (f . x) = ((( cos . ( cot . x)) / (( sin . x) ^2 )) / (( sin . ( cot . x)) ^2 ))) & Z c= ( dom ( cosec * cot )) & Z = ( dom f) & (f | A) is continuous implies ( integral (f,A)) = ((( cosec * cot ) . ( upper_bound A)) - (( cosec * cot ) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & (for x st x in Z holds (f . x) = ((( cos . ( cot . x)) / (( sin . x) ^2 )) / (( sin . ( cot . x)) ^2 ))) & Z c= ( dom ( cosec * cot )) & Z = ( dom f) & (f | A) is continuous;

      then

       A2: f is_integrable_on A & (f | A) is bounded by INTEGRA5: 10, INTEGRA5: 11;

      

       A3: ( cosec * cot ) is_differentiable_on Z by A1, FDIFF_9: 41;

      

       A4: for x be Element of REAL st x in ( dom (( cosec * cot ) `| Z)) holds ((( cosec * cot ) `| Z) . x) = (f . x)

      proof

        let x be Element of REAL ;

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

        then

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

        

        then ((( cosec * cot ) `| Z) . x) = ((( cos . ( cot . x)) / (( sin . x) ^2 )) / (( sin . ( cot . x)) ^2 )) by A1, FDIFF_9: 41

        .= (f . x) by A1, A5;

        hence thesis;

      end;

      ( dom (( cosec * cot ) `| Z)) = ( dom f) by A1, A3, FDIFF_1:def 7;

      then (( cosec * cot ) `| Z) = f by A4, PARTFUN1: 5;

      hence thesis by A1, A2, A3, INTEGRA5: 13;

    end;

    theorem :: INTEGR14:44

    A c= Z & (for x st x in Z holds (f . x) = (((1 / (( cos . x) ^2 )) / ( cos . x)) + ((( tan . x) * ( sin . x)) / (( cos . x) ^2 )))) & Z c= ( dom ( tan (#) sec )) & Z = ( dom f) & (f | A) is continuous implies ( integral (f,A)) = ((( tan (#) sec ) . ( upper_bound A)) - (( tan (#) sec ) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & (for x st x in Z holds (f . x) = (((1 / (( cos . x) ^2 )) / ( cos . x)) + ((( tan . x) * ( sin . x)) / (( cos . x) ^2 )))) & Z c= ( dom ( tan (#) sec )) & Z = ( dom f) & (f | A) is continuous;

      then

       A2: f is_integrable_on A & (f | A) is bounded by INTEGRA5: 10, INTEGRA5: 11;

      

       A3: ( tan (#) sec ) is_differentiable_on Z by A1, FDIFF_9: 42;

      

       A4: for x be Element of REAL st x in ( dom (( tan (#) sec ) `| Z)) holds ((( tan (#) sec ) `| Z) . x) = (f . x)

      proof

        let x be Element of REAL ;

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

        then

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

        

        then ((( tan (#) sec ) `| Z) . x) = (((1 / (( cos . x) ^2 )) / ( cos . x)) + ((( tan . x) * ( sin . x)) / (( cos . x) ^2 ))) by A1, FDIFF_9: 42

        .= (f . x) by A1, A5;

        hence thesis;

      end;

      ( dom (( tan (#) sec ) `| Z)) = ( dom f) by A1, A3, FDIFF_1:def 7;

      then (( tan (#) sec ) `| Z) = f by A4, PARTFUN1: 5;

      hence thesis by A1, A2, A3, INTEGRA5: 13;

    end;

    theorem :: INTEGR14:45

    A c= Z & (for x st x in Z holds (f . x) = (((1 / (( sin . x) ^2 )) / ( cos . x)) - ((( cot . x) * ( sin . x)) / (( cos . x) ^2 )))) & Z c= ( dom ( cot (#) sec )) & Z = ( dom f) & (f | A) is continuous implies ( integral (f,A)) = ((( - ( cot (#) sec )) . ( upper_bound A)) - (( - ( cot (#) sec )) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & (for x st x in Z holds (f . x) = (((1 / (( sin . x) ^2 )) / ( cos . x)) - ((( cot . x) * ( sin . x)) / (( cos . x) ^2 )))) & Z c= ( dom ( cot (#) sec )) & Z = ( dom f) & (f | A) is continuous;

      then

       A2: f is_integrable_on A & (f | A) is bounded by INTEGRA5: 10, INTEGRA5: 11;

      

       A3: ( - ( cot (#) sec )) is_differentiable_on Z by A1, Th12;

      

       A4: for x be Element of REAL st x in ( dom (( - ( cot (#) sec )) `| Z)) holds ((( - ( cot (#) sec )) `| Z) . x) = (f . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom (( - ( cot (#) sec )) `| Z));

        then

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

        

        then ((( - ( cot (#) sec )) `| Z) . x) = (((1 / (( sin . x) ^2 )) / ( cos . x)) - ((( cot . x) * ( sin . x)) / (( cos . x) ^2 ))) by A1, Th12

        .= (f . x) by A1, A5;

        hence thesis;

      end;

      ( dom (( - ( cot (#) sec )) `| Z)) = ( dom f) by A1, A3, FDIFF_1:def 7;

      then (( - ( cot (#) sec )) `| Z) = f by A4, PARTFUN1: 5;

      hence thesis by A1, A2, A3, INTEGRA5: 13;

    end;

    theorem :: INTEGR14:46

    A c= Z & (for x st x in Z holds (f . x) = (((1 / (( cos . x) ^2 )) / ( sin . x)) - ((( tan . x) * ( cos . x)) / (( sin . x) ^2 )))) & Z c= ( dom ( tan (#) cosec )) & Z = ( dom f) & (f | A) is continuous implies ( integral (f,A)) = ((( tan (#) cosec ) . ( upper_bound A)) - (( tan (#) cosec ) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & (for x st x in Z holds (f . x) = (((1 / (( cos . x) ^2 )) / ( sin . x)) - ((( tan . x) * ( cos . x)) / (( sin . x) ^2 )))) & Z c= ( dom ( tan (#) cosec )) & Z = ( dom f) & (f | A) is continuous;

      then

       A2: f is_integrable_on A & (f | A) is bounded by INTEGRA5: 10, INTEGRA5: 11;

      

       A3: ( tan (#) cosec ) is_differentiable_on Z by A1, FDIFF_9: 44;

      

       A4: for x be Element of REAL st x in ( dom (( tan (#) cosec ) `| Z)) holds ((( tan (#) cosec ) `| Z) . x) = (f . x)

      proof

        let x be Element of REAL ;

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

        then

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

        

        then ((( tan (#) cosec ) `| Z) . x) = (((1 / (( cos . x) ^2 )) / ( sin . x)) - ((( tan . x) * ( cos . x)) / (( sin . x) ^2 ))) by A1, FDIFF_9: 44

        .= (f . x) by A1, A5;

        hence thesis;

      end;

      ( dom (( tan (#) cosec ) `| Z)) = ( dom f) by A1, A3, FDIFF_1:def 7;

      then (( tan (#) cosec ) `| Z) = f by A4, PARTFUN1: 5;

      hence thesis by A1, A2, A3, INTEGRA5: 13;

    end;

    theorem :: INTEGR14:47

    A c= Z & (for x st x in Z holds (f . x) = (((1 / (( sin . x) ^2 )) / ( sin . x)) + ((( cot . x) * ( cos . x)) / (( sin . x) ^2 )))) & Z c= ( dom ( cot (#) cosec )) & Z = ( dom f) & (f | A) is continuous implies ( integral (f,A)) = ((( - ( cot (#) cosec )) . ( upper_bound A)) - (( - ( cot (#) cosec )) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & (for x st x in Z holds (f . x) = (((1 / (( sin . x) ^2 )) / ( sin . x)) + ((( cot . x) * ( cos . x)) / (( sin . x) ^2 )))) & Z c= ( dom ( cot (#) cosec )) & Z = ( dom f) & (f | A) is continuous;

      then

       A2: f is_integrable_on A & (f | A) is bounded by INTEGRA5: 10, INTEGRA5: 11;

      

       A3: ( - ( cot (#) cosec )) is_differentiable_on Z by A1, Th13;

      

       A4: for x be Element of REAL st x in ( dom (( - ( cot (#) cosec )) `| Z)) holds ((( - ( cot (#) cosec )) `| Z) . x) = (f . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom (( - ( cot (#) cosec )) `| Z));

        then

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

        

        then ((( - ( cot (#) cosec )) `| Z) . x) = (((1 / (( sin . x) ^2 )) / ( sin . x)) + ((( cot . x) * ( cos . x)) / (( sin . x) ^2 ))) by A1, Th13

        .= (f . x) by A1, A5;

        hence thesis;

      end;

      ( dom (( - ( cot (#) cosec )) `| Z)) = ( dom f) by A1, A3, FDIFF_1:def 7;

      then (( - ( cot (#) cosec )) `| Z) = f by A4, PARTFUN1: 5;

      hence thesis by A1, A2, A3, INTEGRA5: 13;

    end;

    theorem :: INTEGR14:48

    A c= Z & (for x st x in Z holds (f . x) = ((1 / (( cos . ( cot . x)) ^2 )) * (1 / (( sin . x) ^2 )))) & Z c= ( dom ( tan * cot )) & Z = ( dom f) & (f | A) is continuous implies ( integral (f,A)) = ((( - ( tan * cot )) . ( upper_bound A)) - (( - ( tan * cot )) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & (for x st x in Z holds (f . x) = ((1 / (( cos . ( cot . x)) ^2 )) * (1 / (( sin . x) ^2 )))) & Z c= ( dom ( tan * cot )) & Z = ( dom f) & (f | A) is continuous;

      then

       A2: f is_integrable_on A & (f | A) is bounded by INTEGRA5: 10, INTEGRA5: 11;

      

       A3: Z c= ( dom ( - ( tan * cot ))) by A1, VALUED_1: 8;

      

       A4: ( tan * cot ) is_differentiable_on Z by A1, FDIFF_10: 1;

      then

       A5: (( - 1) (#) ( tan * cot )) is_differentiable_on Z by A3, FDIFF_1: 20;

      

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

      proof

        let x;

        assume

         A7: x in Z;

        ((( - ( tan * cot )) `| Z) . x) = ((( - 1) (#) (( tan * cot ) `| Z)) . x) by A4, FDIFF_2: 19

        .= (( - 1) * ((( tan * cot ) `| Z) . x)) by VALUED_1: 6

        .= (( - 1) * ((1 / (( cos . ( cot . x)) ^2 )) * ( - (1 / (( sin . x) ^2 ))))) by A1, A7, FDIFF_10: 1

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

        hence thesis;

      end;

      

       A8: for x be Element of REAL st x in ( dom (( - ( tan * cot )) `| Z)) holds ((( - ( tan * cot )) `| Z) . x) = (f . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom (( - ( tan * cot )) `| Z));

        then

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

        

        then ((( - ( tan * cot )) `| Z) . x) = ((1 / (( cos . ( cot . x)) ^2 )) * (1 / (( sin . x) ^2 ))) by A6

        .= (f . x) by A1, A9;

        hence thesis;

      end;

      ( dom (( - ( tan * cot )) `| Z)) = ( dom f) by A1, A5, FDIFF_1:def 7;

      then (( - ( tan * cot )) `| Z) = f by A8, PARTFUN1: 5;

      hence thesis by A1, A2, A5, INTEGRA5: 13;

    end;

    theorem :: INTEGR14:49

    A c= Z & (for x st x in Z holds (f . x) = ((1 / (( cos . ( tan . x)) ^2 )) * (1 / (( cos . x) ^2 )))) & Z c= ( dom ( tan * tan )) & Z = ( dom f) & (f | A) is continuous implies ( integral (f,A)) = ((( tan * tan ) . ( upper_bound A)) - (( tan * tan ) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & (for x st x in Z holds (f . x) = ((1 / (( cos . ( tan . x)) ^2 )) * (1 / (( cos . x) ^2 )))) & Z c= ( dom ( tan * tan )) & Z = ( dom f) & (f | A) is continuous;

      then

       A2: f is_integrable_on A & (f | A) is bounded by INTEGRA5: 10, INTEGRA5: 11;

      

       A3: ( tan * tan ) is_differentiable_on Z by A1, FDIFF_10: 2;

      

       A4: for x be Element of REAL st x in ( dom (( tan * tan ) `| Z)) holds ((( tan * tan ) `| Z) . x) = (f . x)

      proof

        let x be Element of REAL ;

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

        then

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

        

        then ((( tan * tan ) `| Z) . x) = ((1 / (( cos . ( tan . x)) ^2 )) * (1 / (( cos . x) ^2 ))) by A1, FDIFF_10: 2

        .= (f . x) by A1, A5;

        hence thesis;

      end;

      ( dom (( tan * tan ) `| Z)) = ( dom f) by A1, A3, FDIFF_1:def 7;

      then (( tan * tan ) `| Z) = f by A4, PARTFUN1: 5;

      hence thesis by A1, A2, A3, INTEGRA5: 13;

    end;

    theorem :: INTEGR14:50

    A c= Z & (for x st x in Z holds (f . x) = ((1 / (( sin . ( cot . x)) ^2 )) * (1 / (( sin . x) ^2 )))) & Z c= ( dom ( cot * cot )) & Z = ( dom f) & (f | A) is continuous implies ( integral (f,A)) = ((( cot * cot ) . ( upper_bound A)) - (( cot * cot ) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & (for x st x in Z holds (f . x) = ((1 / (( sin . ( cot . x)) ^2 )) * (1 / (( sin . x) ^2 )))) & Z c= ( dom ( cot * cot )) & Z = ( dom f) & (f | A) is continuous;

      then

       A2: f is_integrable_on A & (f | A) is bounded by INTEGRA5: 10, INTEGRA5: 11;

      

       A3: ( cot * cot ) is_differentiable_on Z by A1, FDIFF_10: 3;

      

       A4: for x be Element of REAL st x in ( dom (( cot * cot ) `| Z)) holds ((( cot * cot ) `| Z) . x) = (f . x)

      proof

        let x be Element of REAL ;

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

        then

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

        

        then ((( cot * cot ) `| Z) . x) = ((1 / (( sin . ( cot . x)) ^2 )) * (1 / (( sin . x) ^2 ))) by A1, FDIFF_10: 3

        .= (f . x) by A1, A5;

        hence thesis;

      end;

      ( dom (( cot * cot ) `| Z)) = ( dom f) by A1, A3, FDIFF_1:def 7;

      then (( cot * cot ) `| Z) = f by A4, PARTFUN1: 5;

      hence thesis by A1, A2, A3, INTEGRA5: 13;

    end;

    theorem :: INTEGR14:51

    A c= Z & (for x st x in Z holds (f . x) = ((1 / (( sin . ( tan . x)) ^2 )) * (1 / (( cos . x) ^2 )))) & Z c= ( dom ( cot * tan )) & Z = ( dom f) & (f | A) is continuous implies ( integral (f,A)) = ((( - ( cot * tan )) . ( upper_bound A)) - (( - ( cot * tan )) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & (for x st x in Z holds (f . x) = ((1 / (( sin . ( tan . x)) ^2 )) * (1 / (( cos . x) ^2 )))) & Z c= ( dom ( cot * tan )) & Z = ( dom f) & (f | A) is continuous;

      then

       A2: f is_integrable_on A & (f | A) is bounded by INTEGRA5: 10, INTEGRA5: 11;

      

       A3: Z c= ( dom ( - ( cot * tan ))) by A1, VALUED_1: 8;

      

       A4: ( cot * tan ) is_differentiable_on Z by A1, FDIFF_10: 4;

      then

       A5: (( - 1) (#) ( cot * tan )) is_differentiable_on Z by A3, FDIFF_1: 20;

      

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

      proof

        let x;

        assume

         A7: x in Z;

        ((( - ( cot * tan )) `| Z) . x) = ((( - 1) (#) (( cot * tan ) `| Z)) . x) by A4, FDIFF_2: 19

        .= (( - 1) * ((( cot * tan ) `| Z) . x)) by VALUED_1: 6

        .= (( - 1) * (( - (1 / (( sin . ( tan . x)) ^2 ))) * (1 / (( cos . x) ^2 )))) by A1, A7, FDIFF_10: 4

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

        hence thesis;

      end;

      

       A8: for x be Element of REAL st x in ( dom (( - ( cot * tan )) `| Z)) holds ((( - ( cot * tan )) `| Z) . x) = (f . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom (( - ( cot * tan )) `| Z));

        then

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

        

        then ((( - ( cot * tan )) `| Z) . x) = ((1 / (( sin . ( tan . x)) ^2 )) * (1 / (( cos . x) ^2 ))) by A6

        .= (f . x) by A1, A9;

        hence thesis;

      end;

      ( dom (( - ( cot * tan )) `| Z)) = ( dom f) by A1, A5, FDIFF_1:def 7;

      then (( - ( cot * tan )) `| Z) = f by A8, PARTFUN1: 5;

      hence thesis by A1, A2, A5, INTEGRA5: 13;

    end;

    theorem :: INTEGR14:52

    A c= Z & (for x st x in Z holds (f . x) = ((1 / (( cos . x) ^2 )) + (1 / (( sin . x) ^2 )))) & Z c= ( dom ( tan - cot )) & Z = ( dom f) & (f | A) is continuous implies ( integral (f,A)) = ((( tan - cot ) . ( upper_bound A)) - (( tan - cot ) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & (for x st x in Z holds (f . x) = ((1 / (( cos . x) ^2 )) + (1 / (( sin . x) ^2 )))) & Z c= ( dom ( tan - cot )) & Z = ( dom f) & (f | A) is continuous;

      then

       A2: f is_integrable_on A & (f | A) is bounded by INTEGRA5: 10, INTEGRA5: 11;

      

       A3: ( tan - cot ) is_differentiable_on Z by A1, FDIFF_10: 5;

      

       A4: for x be Element of REAL st x in ( dom (( tan - cot ) `| Z)) holds ((( tan - cot ) `| Z) . x) = (f . x)

      proof

        let x be Element of REAL ;

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

        then

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

        

        then ((( tan - cot ) `| Z) . x) = ((1 / (( cos . x) ^2 )) + (1 / (( sin . x) ^2 ))) by A1, FDIFF_10: 5

        .= (f . x) by A1, A5;

        hence thesis;

      end;

      ( dom (( tan - cot ) `| Z)) = ( dom f) by A1, A3, FDIFF_1:def 7;

      then (( tan - cot ) `| Z) = f by A4, PARTFUN1: 5;

      hence thesis by A1, A2, A3, INTEGRA5: 13;

    end;

    theorem :: INTEGR14:53

    A c= Z & (for x st x in Z holds (f . x) = ((1 / (( cos . x) ^2 )) - (1 / (( sin . x) ^2 )))) & Z c= ( dom ( tan + cot )) & Z = ( dom f) & (f | A) is continuous implies ( integral (f,A)) = ((( tan + cot ) . ( upper_bound A)) - (( tan + cot ) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & (for x st x in Z holds (f . x) = ((1 / (( cos . x) ^2 )) - (1 / (( sin . x) ^2 )))) & Z c= ( dom ( tan + cot )) & Z = ( dom f) & (f | A) is continuous;

      then

       A2: f is_integrable_on A & (f | A) is bounded by INTEGRA5: 10, INTEGRA5: 11;

      

       A3: ( tan + cot ) is_differentiable_on Z by A1, FDIFF_10: 6;

      

       A4: for x be Element of REAL st x in ( dom (( tan + cot ) `| Z)) holds ((( tan + cot ) `| Z) . x) = (f . x)

      proof

        let x be Element of REAL ;

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

        then

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

        

        then ((( tan + cot ) `| Z) . x) = ((1 / (( cos . x) ^2 )) - (1 / (( sin . x) ^2 ))) by A1, FDIFF_10: 6

        .= (f . x) by A1, A5;

        hence thesis;

      end;

      ( dom (( tan + cot ) `| Z)) = ( dom f) by A1, A3, FDIFF_1:def 7;

      then (( tan + cot ) `| Z) = f by A4, PARTFUN1: 5;

      hence thesis by A1, A2, A3, INTEGRA5: 13;

    end;

    theorem :: INTEGR14:54

    A c= Z & (for x st x in Z holds (f . x) = (( cos . ( sin . x)) * ( cos . x))) & Z = ( dom f) & (f | A) is continuous implies ( integral (f,A)) = ((( sin * sin ) . ( upper_bound A)) - (( sin * sin ) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & (for x st x in Z holds (f . x) = (( cos . ( sin . x)) * ( cos . x))) & Z = ( dom f) & (f | A) is continuous;

      then

       A2: f is_integrable_on A & (f | A) is bounded by INTEGRA5: 10, INTEGRA5: 11;

      

       A3: ( sin * sin ) is_differentiable_on Z by FDIFF_10: 7;

      

       A4: for x be Element of REAL st x in ( dom (( sin * sin ) `| Z)) holds ((( sin * sin ) `| Z) . x) = (f . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom (( sin * sin ) `| Z));

        then

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

        

        then ((( sin * sin ) `| Z) . x) = (( cos . ( sin . x)) * ( cos . x)) by FDIFF_10: 7

        .= (f . x) by A1, A5;

        hence thesis;

      end;

      ( dom (( sin * sin ) `| Z)) = ( dom f) by A1, A3, FDIFF_1:def 7;

      then (( sin * sin ) `| Z) = f by A4, PARTFUN1: 5;

      hence thesis by A1, A2, A3, INTEGRA5: 13;

    end;

    theorem :: INTEGR14:55

    A c= Z & (for x st x in Z holds (f . x) = (( cos . ( cos . x)) * ( sin . x))) & Z = ( dom f) & (f | A) is continuous implies ( integral (f,A)) = ((( - ( sin * cos )) . ( upper_bound A)) - (( - ( sin * cos )) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & (for x st x in Z holds (f . x) = (( cos . ( cos . x)) * ( sin . x))) & Z = ( dom f) & (f | A) is continuous;

      then

       A2: f is_integrable_on A & (f | A) is bounded by INTEGRA5: 10, INTEGRA5: 11;

      ( dom cos ) = REAL & ( rng cos ) c= ( dom cos ) & ( dom sin ) = ( dom cos ) by SIN_COS: 24;

      then ( dom ( sin * cos )) = REAL by RELAT_1: 27;

      then

       A3: ( dom ( - ( sin * cos ))) = REAL by VALUED_1: 8;

      

       A4: ( sin * cos ) is_differentiable_on Z by FDIFF_10: 8;

      then

       A5: (( - 1) (#) ( sin * cos )) is_differentiable_on Z by A3, FDIFF_1: 20;

      

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

      proof

        let x;

        assume

         A7: x in Z;

        ((( - ( sin * cos )) `| Z) . x) = ((( - 1) (#) (( sin * cos ) `| Z)) . x) by A4, FDIFF_2: 19

        .= (( - 1) * ((( sin * cos ) `| Z) . x)) by VALUED_1: 6

        .= (( - 1) * ( - (( cos . ( cos . x)) * ( sin . x)))) by A7, FDIFF_10: 8

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

        hence thesis;

      end;

      

       A8: for x be Element of REAL st x in ( dom (( - ( sin * cos )) `| Z)) holds ((( - ( sin * cos )) `| Z) . x) = (f . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom (( - ( sin * cos )) `| Z));

        then

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

        

        then ((( - ( sin * cos )) `| Z) . x) = (( cos . ( cos . x)) * ( sin . x)) by A6

        .= (f . x) by A1, A9;

        hence thesis;

      end;

      ( dom (( - ( sin * cos )) `| Z)) = ( dom f) by A1, A5, FDIFF_1:def 7;

      then (( - ( sin * cos )) `| Z) = f by A8, PARTFUN1: 5;

      hence thesis by A1, A2, A5, INTEGRA5: 13;

    end;

    theorem :: INTEGR14:56

    A c= Z & (for x st x in Z holds (f . x) = (( sin . ( sin . x)) * ( cos . x))) & Z = ( dom f) & (f | A) is continuous implies ( integral (f,A)) = ((( - ( cos * sin )) . ( upper_bound A)) - (( - ( cos * sin )) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & (for x st x in Z holds (f . x) = (( sin . ( sin . x)) * ( cos . x))) & Z = ( dom f) & (f | A) is continuous;

      then

       A2: f is_integrable_on A & (f | A) is bounded by INTEGRA5: 10, INTEGRA5: 11;

      

       A3: ( dom sin ) = REAL by SIN_COS: 24;

      ( rng sin ) c= ( dom sin ) & ( dom sin ) = ( dom cos ) by SIN_COS: 24;

      then ( dom ( cos * sin )) = REAL by A3, RELAT_1: 27;

      then

       A4: ( dom ( - ( cos * sin ))) = REAL by VALUED_1: 8;

      

       A5: ( cos * sin ) is_differentiable_on Z by FDIFF_10: 9;

      then

       A6: (( - 1) (#) ( cos * sin )) is_differentiable_on Z by A4, FDIFF_1: 20;

      

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

      proof

        let x;

        assume

         A8: x in Z;

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

        .= (( - 1) * ((( cos * sin ) `| Z) . x)) by VALUED_1: 6

        .= (( - 1) * ( - (( sin . ( sin . x)) * ( cos . x)))) by A8, FDIFF_10: 9

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

        hence thesis;

      end;

      

       A9: for x be Element of REAL st x in ( dom (( - ( cos * sin )) `| Z)) holds ((( - ( cos * sin )) `| Z) . x) = (f . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom (( - ( cos * sin )) `| Z));

        then

         A10: x in Z by A6, FDIFF_1:def 7;

        

        then ((( - ( cos * sin )) `| Z) . x) = (( sin . ( sin . x)) * ( cos . x)) by A7

        .= (f . x) by A1, A10;

        hence thesis;

      end;

      ( dom (( - ( cos * sin )) `| Z)) = ( dom f) by A1, A6, FDIFF_1:def 7;

      then (( - ( cos * sin )) `| Z) = f by A9, PARTFUN1: 5;

      hence thesis by A1, A2, A6, INTEGRA5: 13;

    end;

    theorem :: INTEGR14:57

    A c= Z & (for x st x in Z holds (f . x) = (( sin . ( cos . x)) * ( sin . x))) & Z = ( dom f) & (f | A) is continuous implies ( integral (f,A)) = ((( cos * cos ) . ( upper_bound A)) - (( cos * cos ) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & (for x st x in Z holds (f . x) = (( sin . ( cos . x)) * ( sin . x))) & Z = ( dom f) & (f | A) is continuous;

      then

       A2: f is_integrable_on A & (f | A) is bounded by INTEGRA5: 10, INTEGRA5: 11;

      

       A3: ( cos * cos ) is_differentiable_on Z by FDIFF_10: 10;

      

       A4: for x be Element of REAL st x in ( dom (( cos * cos ) `| Z)) holds ((( cos * cos ) `| Z) . x) = (f . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom (( cos * cos ) `| Z));

        then

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

        

        then ((( cos * cos ) `| Z) . x) = (( sin . ( cos . x)) * ( sin . x)) by FDIFF_10: 10

        .= (f . x) by A1, A5;

        hence thesis;

      end;

      ( dom (( cos * cos ) `| Z)) = ( dom f) by A1, A3, FDIFF_1:def 7;

      then (( cos * cos ) `| Z) = f by A4, PARTFUN1: 5;

      hence thesis by A1, A2, A3, INTEGRA5: 13;

    end;

    theorem :: INTEGR14:58

    A c= Z & (for x st x in Z holds (f . x) = (( cos . x) + (( cos . x) / (( sin . x) ^2 )))) & Z c= ( dom ( cos (#) cot )) & Z = ( dom f) & (f | A) is continuous implies ( integral (f,A)) = ((( - ( cos (#) cot )) . ( upper_bound A)) - (( - ( cos (#) cot )) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & (for x st x in Z holds (f . x) = (( cos . x) + (( cos . x) / (( sin . x) ^2 )))) & Z c= ( dom ( cos (#) cot )) & Z = ( dom f) & (f | A) is continuous;

      then

       A2: f is_integrable_on A & (f | A) is bounded by INTEGRA5: 10, INTEGRA5: 11;

      

       A3: ( - ( cos (#) cot )) is_differentiable_on Z by A1, Th14;

      

       A4: for x be Element of REAL st x in ( dom (( - ( cos (#) cot )) `| Z)) holds ((( - ( cos (#) cot )) `| Z) . x) = (f . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom (( - ( cos (#) cot )) `| Z));

        then

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

        

        then ((( - ( cos (#) cot )) `| Z) . x) = (( cos . x) + (( cos . x) / (( sin . x) ^2 ))) by A1, Th14

        .= (f . x) by A1, A5;

        hence thesis;

      end;

      ( dom (( - ( cos (#) cot )) `| Z)) = ( dom f) by A1, A3, FDIFF_1:def 7;

      then (( - ( cos (#) cot )) `| Z) = f by A4, PARTFUN1: 5;

      hence thesis by A1, A2, A3, INTEGRA5: 13;

    end;

    theorem :: INTEGR14:59

    A c= Z & (for x st x in Z holds (f . x) = (( sin . x) + (( sin . x) / (( cos . x) ^2 )))) & Z c= ( dom ( sin (#) tan )) & Z = ( dom f) & (f | A) is continuous implies ( integral (f,A)) = ((( sin (#) tan ) . ( upper_bound A)) - (( sin (#) tan ) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & (for x st x in Z holds (f . x) = (( sin . x) + (( sin . x) / (( cos . x) ^2 )))) & Z c= ( dom ( sin (#) tan )) & Z = ( dom f) & (f | A) is continuous;

      then

       A2: f is_integrable_on A & (f | A) is bounded by INTEGRA5: 10, INTEGRA5: 11;

      

       A3: ( sin (#) tan ) is_differentiable_on Z by A1, FDIFF_10: 12;

      

       A4: for x be Element of REAL st x in ( dom (( sin (#) tan ) `| Z)) holds ((( sin (#) tan ) `| Z) . x) = (f . x)

      proof

        let x be Element of REAL ;

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

        then

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

        

        then ((( sin (#) tan ) `| Z) . x) = (( sin . x) + (( sin . x) / (( cos . x) ^2 ))) by A1, FDIFF_10: 12

        .= (f . x) by A1, A5;

        hence thesis;

      end;

      ( dom (( sin (#) tan ) `| Z)) = ( dom f) by A1, A3, FDIFF_1:def 7;

      then (( sin (#) tan ) `| Z) = f by A4, PARTFUN1: 5;

      hence thesis by A1, A2, A3, INTEGRA5: 13;

    end;