integr13.miz



    begin

    reserve a,x for Real;

    reserve n for Element of NAT ;

    reserve A for non empty closed_interval Subset of REAL ;

    reserve f,h,f1,f2 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;

    

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

    theorem :: INTEGR13:1

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

    proof

      assume

       A1: A c= Z & f = (( sin (#) cos ) ^ ) & Z c= ( dom ( ln * 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: ( ln * tan ) is_differentiable_on Z by A1, FDIFF_8: 18;

      

       A4: for x st x in Z holds (f . x) = (1 / (( sin . x) * ( cos . x)))

      proof

        let x;

        assume x in Z;

        

        then ((( sin (#) cos ) ^ ) . x) = (1 / (( sin (#) cos ) . x)) by A1, RFUNCT_1:def 2

        .= (1 / (( sin . x) * ( cos . x))) by VALUED_1: 5;

        hence thesis by A1;

      end;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

        then ((( ln * tan ) `| Z) . x) = (1 / (( sin . x) * ( cos . x))) by A1, FDIFF_8: 18

        .= (f . x) by A4, A6;

        hence thesis;

      end;

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

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

      hence thesis by A1, A2, FDIFF_8: 18, INTEGRA5: 13;

    end;

    theorem :: INTEGR13:2

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

    proof

      assume

       A1: A c= Z & f = ( - (( sin (#) cos ) ^ )) & Z c= ( dom ( ln * 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: ( ln * cot ) is_differentiable_on Z by A1, FDIFF_8: 19;

      

       A4: Z = ( dom (( sin (#) cos ) ^ )) by A1, VALUED_1: 8;

      

       A5: for x st x in Z holds (f . x) = ( - (1 / (( sin . x) * ( cos . x))))

      proof

        let x;

        assume

         A6: x in Z;

        (( - (( sin (#) cos ) ^ )) . x) = ( - ((( sin (#) cos ) ^ ) . x)) by VALUED_1: 8

        .= ( - (1 / (( sin (#) cos ) . x))) by A4, A6, RFUNCT_1:def 2

        .= ( - (1 / (( sin . x) * ( cos . x)))) by VALUED_1: 5;

        hence thesis by A1;

      end;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

        then ((( ln * cot ) `| Z) . x) = ( - (1 / (( sin . x) * ( cos . x)))) by A1, FDIFF_8: 19

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

        hence thesis;

      end;

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

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

      hence thesis by A1, A2, FDIFF_8: 19, INTEGRA5: 13;

    end;

    theorem :: INTEGR13:3

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

    proof

      assume

       A1: A c= Z & f = (2 (#) ( exp_R (#) sin )) & Z c= ( dom ( exp_R (#) ( sin - 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: ( exp_R (#) ( sin - cos )) is_differentiable_on Z by A1, FDIFF_7: 40;

      

       A4: for x st x in Z holds (f . x) = ((2 * ( exp_R . x)) * ( sin . x))

      proof

        let x;

        assume x in Z;

        ((2 (#) ( exp_R (#) sin )) . x) = (2 * (( exp_R (#) sin ) . x)) by VALUED_1: 6

        .= (2 * (( exp_R . x) * ( sin . x))) by VALUED_1: 5;

        hence thesis by A1;

      end;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

        then ((( exp_R (#) ( sin - cos )) `| Z) . x) = ((2 * ( exp_R . x)) * ( sin . x)) by A1, FDIFF_7: 40

        .= (f . x) by A4, A6;

        hence thesis;

      end;

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

      then (( exp_R (#) ( sin - cos )) `| Z) = f by A5, PARTFUN1: 5;

      hence thesis by A1, A2, FDIFF_7: 40, INTEGRA5: 13;

    end;

    theorem :: INTEGR13:4

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

    proof

      assume

       A1: A c= Z & f = (2 (#) ( exp_R (#) cos )) & Z c= ( dom ( exp_R (#) ( sin + 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: ( exp_R (#) ( sin + cos )) is_differentiable_on Z by A1, FDIFF_7: 41;

      

       A4: for x st x in Z holds (f . x) = ((2 * ( exp_R . x)) * ( cos . x))

      proof

        let x;

        assume x in Z;

        ((2 (#) ( exp_R (#) cos )) . x) = (2 * (( exp_R (#) cos ) . x)) by VALUED_1: 6

        .= (2 * (( exp_R . x) * ( cos . x))) by VALUED_1: 5;

        hence thesis by A1;

      end;

      

       A5: for x be Element of REAL st x in ( dom (( exp_R (#) ( sin + cos )) `| Z)) holds ((( exp_R (#) ( sin + cos )) `| Z) . x) = (f . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom (( exp_R (#) ( sin + cos )) `| Z));

        then

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

        

        then ((( exp_R (#) ( sin + cos )) `| Z) . x) = ((2 * ( exp_R . x)) * ( cos . x)) by A1, FDIFF_7: 41

        .= (f . x) by A6, A4;

        hence thesis;

      end;

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

      then (( exp_R (#) ( sin + cos )) `| Z) = f by A5, PARTFUN1: 5;

      hence thesis by A1, A2, FDIFF_7: 41, INTEGRA5: 13;

    end;

    theorem :: INTEGR13:5

    A c= Z & Z = ( dom ( cos - sin )) & (( cos - sin ) | A) is continuous implies ( integral (( cos - sin ),A)) = ((( sin + cos ) . ( upper_bound A)) - (( sin + cos ) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & Z = ( dom ( cos - sin )) & (( cos - sin ) | A) is continuous;

      then

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

      Z = (( dom cos ) /\ ( dom sin )) by A1, VALUED_1: 12;

      then

       A3: Z c= ( dom ( sin + cos )) by VALUED_1:def 1;

      then

       A4: ( sin + cos ) is_differentiable_on Z by FDIFF_7: 38;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

        then ((( sin + cos ) `| Z) . x) = (( cos . x) - ( sin . x)) by A3, FDIFF_7: 38

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

        hence thesis;

      end;

      ( dom (( sin + cos ) `| Z)) = ( dom ( cos - sin )) by A1, A4, FDIFF_1:def 7;

      then (( sin + cos ) `| Z) = ( cos - sin ) by A5, PARTFUN1: 5;

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

    end;

    theorem :: INTEGR13:6

    A c= Z & Z = ( dom ( cos + sin )) & (( cos + sin ) | A) is continuous implies ( integral (( cos + sin ),A)) = ((( sin - cos ) . ( upper_bound A)) - (( sin - cos ) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & Z = ( dom ( cos + sin )) & (( cos + sin ) | A) is continuous;

      then

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

      Z = (( dom cos ) /\ ( dom sin )) by A1, VALUED_1:def 1;

      then

       A3: Z c= ( dom ( sin - cos )) by VALUED_1: 12;

      then

       A4: ( sin - cos ) is_differentiable_on Z by FDIFF_7: 39;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

        then ((( sin - cos ) `| Z) . x) = (( cos . x) + ( sin . x)) by A3, FDIFF_7: 39

        .= (( cos + sin ) . x) by A1, A6, VALUED_1:def 1;

        hence thesis;

      end;

      ( dom (( sin - cos ) `| Z)) = ( dom ( cos + sin )) by A1, A4, FDIFF_1:def 7;

      then (( sin - cos ) `| Z) = ( cos + sin ) by A5, PARTFUN1: 5;

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

    end;

    theorem :: INTEGR13:7

    

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

    proof

      assume

       A1: Z c= ( dom (( - (1 / 2)) (#) (( sin + cos ) / exp_R )));

      then

       A2: Z c= ( dom (( sin + cos ) / exp_R )) by VALUED_1:def 5;

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

      then

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

      then

       A4: ( sin + cos ) is_differentiable_on Z & for x st x in Z holds ((( sin + cos ) `| Z) . x) = (( cos . x) - ( sin . x)) by FDIFF_7: 38;

      

       A5: (( sin + cos ) / exp_R ) is_differentiable_on Z by A2, FDIFF_7: 42;

      then

       A6: (( - (1 / 2)) (#) (( sin + cos ) / exp_R )) is_differentiable_on Z by FDIFF_2: 19;

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

      proof

        let x;

        

         A7: x in REAL by XREAL_0:def 1;

        assume

         A8: x in Z;

        

         A9: exp_R is_differentiable_in x by SIN_COS: 65;

        

         A10: ( sin + cos ) is_differentiable_in x by A4, A8, FDIFF_1: 9;

        

         A11: (( sin + cos ) . x) = (( sin . x) + ( cos . x)) by VALUED_1: 1, A7;

        

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

        (((( - (1 / 2)) (#) (( sin + cos ) / exp_R )) `| Z) . x) = (( - (1 / 2)) * ( diff ((( sin + cos ) / exp_R ),x))) by A1, A5, A8, FDIFF_1: 20

        .= (( - (1 / 2)) * (((( diff (( sin + cos ),x)) * ( exp_R . x)) - (( diff ( exp_R ,x)) * (( sin + cos ) . x))) / (( exp_R . x) ^2 ))) by A9, A10, A12, FDIFF_2: 14

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

        .= (( - (1 / 2)) * ((((( cos . x) - ( sin . x)) * ( exp_R . x)) - (( diff ( exp_R ,x)) * (( sin + cos ) . x))) / (( exp_R . x) ^2 ))) by A3, A8, FDIFF_7: 38

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

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

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

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

        .= (( sin . x) / ( exp_R . x));

        hence thesis;

      end;

      hence thesis by A6;

    end;

    theorem :: INTEGR13:8

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

    proof

      assume

       A1: A c= Z & f = ( sin / exp_R ) & Z c= ( dom (( - (1 / 2)) (#) (( sin + cos ) / 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: (( - (1 / 2)) (#) (( sin + cos ) / exp_R )) is_differentiable_on Z by A1, Th7;

      

       A4: for x st x in Z holds (f . x) = (( sin . x) / ( exp_R . x)) by A1, RFUNCT_1:def 1;

      

       A5: for x be Element of REAL st x in ( dom ((( - (1 / 2)) (#) (( sin + cos ) / exp_R )) `| Z)) holds (((( - (1 / 2)) (#) (( sin + cos ) / exp_R )) `| Z) . x) = (f . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom ((( - (1 / 2)) (#) (( sin + cos ) / exp_R )) `| Z));

        then

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

        

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

        .= (f . x) by A6, A4;

        hence thesis;

      end;

      ( dom ((( - (1 / 2)) (#) (( sin + cos ) / exp_R )) `| Z)) = ( dom f) by A1, A3, FDIFF_1:def 7;

      then ((( - (1 / 2)) (#) (( sin + cos ) / exp_R )) `| Z) = f by A5, PARTFUN1: 5;

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

    end;

    theorem :: INTEGR13:9

    

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

    proof

      assume

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

      then

       A2: Z c= ( dom (( sin - cos ) / exp_R )) by VALUED_1:def 5;

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

      then

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

      then

       A4: ( sin - cos ) is_differentiable_on Z & for x st x in Z holds ((( sin - cos ) `| Z) . x) = (( cos . x) + ( sin . x)) by FDIFF_7: 39;

      

       A5: (( sin - cos ) / exp_R ) is_differentiable_on Z by A2, FDIFF_7: 43;

      then

       A6: ((1 / 2) (#) (( sin - cos ) / exp_R )) is_differentiable_on Z by FDIFF_2: 19;

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

      proof

        let x;

        assume

         A7: x in Z;

        

         A8: exp_R is_differentiable_in x by SIN_COS: 65;

        

         A9: ( sin - cos ) is_differentiable_in x by A4, A7, FDIFF_1: 9;

        

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

        

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

        ((((1 / 2) (#) (( sin - cos ) / exp_R )) `| Z) . x) = ((1 / 2) * ( diff ((( sin - cos ) / exp_R ),x))) by A1, A5, A7, FDIFF_1: 20

        .= ((1 / 2) * (((( diff (( sin - cos ),x)) * ( exp_R . x)) - (( diff ( exp_R ,x)) * (( sin - cos ) . x))) / (( exp_R . x) ^2 ))) by A8, A9, A11, FDIFF_2: 14

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

        .= ((1 / 2) * ((((( cos . x) + ( sin . x)) * ( exp_R . x)) - (( diff ( exp_R ,x)) * (( sin - cos ) . x))) / (( exp_R . x) ^2 ))) by A3, A7, FDIFF_7: 39

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

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

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

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

        .= (( cos . x) / ( exp_R . x));

        hence thesis;

      end;

      hence thesis by A6;

    end;

    theorem :: INTEGR13:10

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

    proof

      assume

       A1: A c= Z & f = ( cos / exp_R ) & Z c= ( dom ((1 / 2) (#) (( sin - cos ) / 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: ((1 / 2) (#) (( sin - cos ) / exp_R )) is_differentiable_on Z by A1, Th9;

      

       A4: for x st x in Z holds (f . x) = (( cos . x) / ( exp_R . x)) by A1, RFUNCT_1:def 1;

      

       A5: for x be Element of REAL st x in ( dom (((1 / 2) (#) (( sin - cos ) / exp_R )) `| Z)) holds ((((1 / 2) (#) (( sin - cos ) / exp_R )) `| Z) . x) = (f . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom (((1 / 2) (#) (( sin - cos ) / exp_R )) `| Z));

        then

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

        

        then ((((1 / 2) (#) (( sin - cos ) / exp_R )) `| Z) . x) = (( cos . x) / ( exp_R . x)) by A1, Th9

        .= (f . x) by A4, A6;

        hence thesis;

      end;

      ( dom (((1 / 2) (#) (( sin - cos ) / exp_R )) `| Z)) = ( dom f) by A1, A3, FDIFF_1:def 7;

      then (((1 / 2) (#) (( sin - cos ) / exp_R )) `| Z) = f by A5, PARTFUN1: 5;

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

    end;

    theorem :: INTEGR13:11

    A c= Z & f = ( exp_R (#) ( sin + cos )) & Z c= ( dom ( exp_R (#) sin )) & Z = ( dom f) & (f | A) is continuous implies ( integral (f,A)) = ((( exp_R (#) sin ) . ( upper_bound A)) - (( exp_R (#) sin ) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & f = ( exp_R (#) ( sin + cos )) & Z c= ( dom ( exp_R (#) 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: ( exp_R (#) sin ) is_differentiable_on Z by A1, FDIFF_7: 44;

      ( dom f) = (( dom exp_R ) /\ ( dom ( sin + cos ))) by A1, VALUED_1:def 4;

      then

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

      

       A5: for x st x in Z holds (f . x) = (( exp_R . x) * (( sin . x) + ( cos . x)))

      proof

        let x;

        assume

         A6: x in Z;

        (( exp_R (#) ( sin + cos )) . x) = (( exp_R . x) * (( sin + cos ) . x)) by VALUED_1: 5

        .= (( exp_R . x) * (( sin . x) + ( cos . x))) by A4, A6, VALUED_1:def 1;

        hence thesis by A1;

      end;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

        then ((( exp_R (#) sin ) `| Z) . x) = (( exp_R . x) * (( sin . x) + ( cos . x))) by A1, FDIFF_7: 44

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

        hence thesis;

      end;

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

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

      hence thesis by A1, A2, FDIFF_7: 44, INTEGRA5: 13;

    end;

    theorem :: INTEGR13:12

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

    proof

      assume

       A1: A c= Z & f = ( exp_R (#) ( cos - sin )) & Z c= ( dom ( exp_R (#) 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: ( exp_R (#) cos ) is_differentiable_on Z by A1, FDIFF_7: 45;

      ( dom f) = (( dom exp_R ) /\ ( dom ( cos - sin ))) by A1, VALUED_1:def 4;

      then

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

      

       A5: for x st x in Z holds (f . x) = (( exp_R . x) * (( cos . x) - ( sin . x)))

      proof

        let x;

        assume

         A6: x in Z;

        (( exp_R (#) ( cos - sin )) . x) = (( exp_R . x) * (( cos - sin ) . x)) by VALUED_1: 5

        .= (( exp_R . x) * (( cos . x) - ( sin . x))) by A4, A6, VALUED_1: 13;

        hence thesis by A1;

      end;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

        then ((( exp_R (#) cos ) `| Z) . x) = (( exp_R . x) * (( cos . x) - ( sin . x))) by A1, FDIFF_7: 45

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

        hence thesis;

      end;

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

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

      hence thesis by A1, A2, FDIFF_7: 45, INTEGRA5: 13;

    end;

    theorem :: INTEGR13:13

    A c= Z & f1 = ( #Z 2) & f = (( - (( sin / cos ) / f1)) + ((( id Z) ^ ) / ( cos ^2 ))) & Z c= ( dom ((( id Z) ^ ) (#) tan )) & Z = ( dom f) & (f | A) is continuous implies ( integral (f,A)) = ((((( id Z) ^ ) (#) tan ) . ( upper_bound A)) - (((( id Z) ^ ) (#) tan ) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & f1 = ( #Z 2) & f = (( - (( sin / cos ) / f1)) + ((( id Z) ^ ) / ( cos ^2 ))) & Z c= ( dom ((( id Z) ^ ) (#) tan )) & Z = ( dom f) & (f | A) is continuous;

      then

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

      set g = ( id Z);

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

      then

       A3: Z c= ( dom (g ^ )) 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) ^ ) (#) tan ) is_differentiable_on Z by A1, FDIFF_8: 34;

      ( dom f) = (( dom ( - (( sin / cos ) / f1))) /\ ( dom ((( id Z) ^ ) / ( cos ^2 )))) by A1, VALUED_1:def 1;

      then ( dom f) c= ( dom ( - (( sin / cos ) / f1))) & ( dom f) c= ( dom ((( id Z) ^ ) / ( cos ^2 ))) by XBOOLE_1: 18;

      then

       A7: Z c= ( dom (( sin / cos ) / f1)) & Z c= ( dom ((( id Z) ^ ) / ( cos ^2 ))) by A1, VALUED_1: 8;

      ( dom (( sin / cos ) / f1)) = (( dom ( sin / cos )) /\ (( dom f1) \ (f1 " { 0 }))) by RFUNCT_1:def 1;

      then

       A8: Z c= ( dom ( sin / cos )) by A7, XBOOLE_1: 18;

      ( dom ((( id Z) ^ ) / ( cos ^2 ))) c= (( dom (( id Z) ^ )) /\ (( dom ( cos ^2 )) \ (( cos ^2 ) " { 0 }))) by RFUNCT_1:def 1;

      then ( dom ((( id Z) ^ ) / ( cos ^2 ))) c= ( dom (( id Z) ^ )) & ( dom ((( id Z) ^ ) / ( cos ^2 ))) c= (( dom ( cos ^2 )) \ (( cos ^2 ) " { 0 })) by XBOOLE_1: 18;

      then

       A9: Z c= ( dom (( id Z) ^ )) & Z c= (( dom ( cos ^2 )) \ (( cos ^2 ) " { 0 })) by A7;

      

       A10: for x st x in Z holds (f . x) = (( - ((( sin . x) / ( cos . x)) / (x ^2 ))) + ((1 / x) / (( cos . x) ^2 )))

      proof

        let x;

        assume

         A11: x in Z;

        

        then ((( - (( sin / cos ) / f1)) + ((( id Z) ^ ) / ( cos ^2 ))) . x) = ((( - (( sin / cos ) / f1)) . x) + (((( id Z) ^ ) / ( cos ^2 )) . x)) by A1, VALUED_1:def 1

        .= (( - ((( sin / cos ) / f1) . x)) + (((( id Z) ^ ) / ( cos ^2 )) . x)) by VALUED_1: 8

        .= (( - ((( sin / cos ) . x) / (f1 . x))) + (((( id Z) ^ ) / ( cos ^2 )) . x)) by A11, A7, RFUNCT_1:def 1

        .= (( - ((( sin . x) * (( cos . x) " )) / (f1 . x))) + (((( id Z) ^ ) / ( cos ^2 )) . x)) by A8, A11, RFUNCT_1:def 1

        .= (( - ((( sin . x) / ( cos . x)) / (f1 . x))) + (((( id Z) ^ ) . x) / (( cos ^2 ) . x))) by A7, A11, RFUNCT_1:def 1

        .= (( - ((( sin . x) / ( cos . x)) / (f1 . x))) + (((( id Z) . x) " ) / (( cos ^2 ) . x))) by A9, A11, RFUNCT_1:def 2

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

        .= (( - ((( sin . x) / ( cos . x)) / (f1 . x))) + ((1 / x) / (( cos . x) ^2 ))) by VALUED_1: 11

        .= (( - ((( sin . x) / ( cos . x)) / (x #Z 2))) + ((1 / x) / (( cos . x) ^2 ))) by A1, TAYLOR_1:def 1

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

        hence thesis by A1;

      end;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

        then ((((( id Z) ^ ) (#) tan ) `| Z) . x) = (( - ((( sin . x) / ( cos . x)) / (x ^2 ))) + ((1 / x) / (( cos . x) ^2 ))) by A4, A1, FDIFF_8: 34

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

        hence thesis;

      end;

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

      then (((( id Z) ^ ) (#) tan ) `| Z) = f by A12, PARTFUN1: 5;

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

    end;

    theorem :: INTEGR13:14

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

    proof

      assume

       A1: A c= Z & f = (( - (( cos / sin ) / f1)) - ((( id Z) ^ ) / ( sin ^2 ))) & f1 = ( #Z 2) & Z c= ( dom ((( id Z) ^ ) (#) cot )) & Z = ( dom f) & (f | A) is continuous;

      then

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

      set g = ( id Z);

      Z c= ( dom ((g ^ ) (#) cot )) by A1;

      then Z c= (( dom (g ^ )) /\ ( dom cot )) by VALUED_1:def 4;

      then

       A3: Z c= ( dom (g ^ )) 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) ^ ) (#) cot ) is_differentiable_on Z by A1, FDIFF_8: 35;

      ( dom f) = (( dom ( - (( cos / sin ) / f1))) /\ ( dom ((( id Z) ^ ) / ( sin ^2 )))) by A1, VALUED_1: 12;

      then

       A7: ( dom f) c= ( dom ( - (( cos / sin ) / f1))) & ( dom f) c= ( dom ((( id Z) ^ ) / ( sin ^2 ))) by XBOOLE_1: 18;

      then ( dom f) c= ( dom (( cos / sin ) / f1)) by VALUED_1: 8;

      then

       A8: Z c= ( dom (( cos / sin ) / f1)) & Z c= ( dom ((( id Z) ^ ) / ( sin ^2 ))) by A1, A7;

      ( dom (( cos / sin ) / f1)) = (( dom ( cos / sin )) /\ (( dom f1) \ (f1 " { 0 }))) by RFUNCT_1:def 1;

      then

       A9: Z c= ( dom ( cos / sin )) by A8, XBOOLE_1: 18;

      ( dom ((( id Z) ^ ) / ( sin ^2 ))) c= (( dom (( id Z) ^ )) /\ (( dom ( sin ^2 )) \ (( sin ^2 ) " { 0 }))) by RFUNCT_1:def 1;

      then ( dom ((( id Z) ^ ) / ( sin ^2 ))) c= ( dom (( id Z) ^ )) & ( dom ((( id Z) ^ ) / ( sin ^2 ))) c= (( dom ( sin ^2 )) \ (( sin ^2 ) " { 0 })) by XBOOLE_1: 18;

      then

       A10: Z c= ( dom (( id Z) ^ )) & Z c= (( dom ( sin ^2 )) \ (( sin ^2 ) " { 0 })) by A8;

      

       A11: for x st x in Z holds (f . x) = (( - ((( cos . x) / ( sin . x)) / (x ^2 ))) - ((1 / x) / (( sin . x) ^2 )))

      proof

        let x;

        assume

         A12: x in Z;

        

        then ((( - (( cos / sin ) / f1)) - ((( id Z) ^ ) / ( sin ^2 ))) . x) = ((( - (( cos / sin ) / f1)) . x) - (((( id Z) ^ ) / ( sin ^2 )) . x)) by A1, VALUED_1: 13

        .= (( - ((( cos / sin ) / f1) . x)) - (((( id Z) ^ ) / ( sin ^2 )) . x)) by VALUED_1: 8

        .= (( - ((( cos / sin ) . x) / (f1 . x))) - (((( id Z) ^ ) / ( sin ^2 )) . x)) by A12, A8, RFUNCT_1:def 1

        .= (( - ((( cos . x) / ( sin . x)) / (f1 . x))) - (((( id Z) ^ ) / ( sin ^2 )) . x)) by A9, A12, RFUNCT_1:def 1

        .= (( - ((( cos . x) / ( sin . x)) / (f1 . x))) - (((( id Z) ^ ) . x) / (( sin ^2 ) . x))) by A8, A12, RFUNCT_1:def 1

        .= (( - ((( cos . x) / ( sin . x)) / (f1 . x))) - (((( id Z) . x) " ) / (( sin ^2 ) . x))) by A10, A12, RFUNCT_1:def 2

        .= (( - ((( cos . x) / ( sin . x)) / (f1 . x))) - ((1 / x) / (( sin ^2 ) . x))) by A12, FUNCT_1: 18

        .= (( - ((( cos . x) / ( sin . x)) / (f1 . x))) - ((1 / x) / (( sin . x) ^2 ))) by VALUED_1: 11

        .= (( - ((( cos . x) / ( sin . x)) / (x #Z 2))) - ((1 / x) / (( sin . x) ^2 ))) by A1, TAYLOR_1:def 1

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

        hence thesis by A1;

      end;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

        then ((((( id Z) ^ ) (#) cot ) `| Z) . x) = (( - ((( cos . x) / ( sin . x)) / (x ^2 ))) - ((1 / x) / (( sin . x) ^2 ))) by A1, A4, FDIFF_8: 35

        .= (f . x) by A11, A14;

        hence thesis;

      end;

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

      then (((( id Z) ^ ) (#) cot ) `| Z) = f by A13, PARTFUN1: 5;

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

    end;

    theorem :: INTEGR13:15

    A c= Z & f = ((( sin / cos ) / ( id Z)) + ( ln / ( cos ^2 ))) & Z c= ( dom ( ln (#) tan )) & Z = ( dom f) & (f | A) is continuous implies ( integral (f,A)) = ((( ln (#) tan ) . ( upper_bound A)) - (( ln (#) tan ) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & f = ((( sin / cos ) / ( id Z)) + ( ln / ( cos ^2 ))) & Z c= ( dom ( ln (#) 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: ( ln (#) tan ) is_differentiable_on Z by A1, FDIFF_8: 32;

      Z = (( dom (( sin / cos ) / ( id Z))) /\ ( dom ( ln / ( cos ^2 )))) by A1, VALUED_1:def 1;

      then

       A4: Z c= ( dom (( sin / cos ) / ( id Z))) & Z c= ( dom ( ln / ( cos ^2 ))) by XBOOLE_1: 18;

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

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

      then

       A5: Z c= ( dom ( sin / cos )) by A4;

      

       A6: for x st x in Z holds (f . x) = (((( sin . x) / ( cos . x)) / x) + (( ln . x) / (( cos . x) ^2 )))

      proof

        let x;

        assume

         A7: x in Z;

        

        then (((( sin / cos ) / ( id Z)) + ( ln / ( cos ^2 ))) . x) = (((( sin / cos ) / ( id Z)) . x) + (( ln / ( cos ^2 )) . x)) by A1, VALUED_1:def 1

        .= (((( sin / cos ) . x) / (( id Z) . x)) + (( ln / ( cos ^2 )) . x)) by A7, A4, RFUNCT_1:def 1

        .= (((( sin . x) / ( cos . x)) / (( id Z) . x)) + (( ln / ( cos ^2 )) . x)) by A5, A7, RFUNCT_1:def 1

        .= (((( sin . x) / ( cos . x)) / x) + (( ln / ( cos ^2 )) . x)) by A7, FUNCT_1: 18

        .= (((( sin . x) / ( cos . x)) / x) + (( ln . x) / (( cos ^2 ) . x))) by A7, A4, RFUNCT_1:def 1

        .= (((( sin . x) / ( cos . x)) / x) + (( ln . x) / (( cos . x) ^2 ))) by VALUED_1: 11;

        hence thesis by A1;

      end;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

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

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

        hence thesis;

      end;

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

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

      hence thesis by A1, A2, FDIFF_8: 32, INTEGRA5: 13;

    end;

    theorem :: INTEGR13:16

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

    proof

      assume

       A1: A c= Z & f = ((( cos / sin ) / ( id Z)) - ( ln / ( sin ^2 ))) & Z c= ( dom ( ln (#) 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: ( ln (#) cot ) is_differentiable_on Z by A1, FDIFF_8: 33;

      Z = (( dom (( cos / sin ) / ( id Z))) /\ ( dom ( ln / ( sin ^2 )))) by A1, VALUED_1: 12;

      then

       A4: Z c= ( dom (( cos / sin ) / ( id Z))) & Z c= ( dom ( ln / ( sin ^2 ))) by XBOOLE_1: 18;

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

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

      then

       A5: Z c= ( dom ( cos / sin )) by A4;

      

       A6: for x st x in Z holds (f . x) = (((( cos . x) / ( sin . x)) / x) - (( ln . x) / (( sin . x) ^2 )))

      proof

        let x;

        assume

         A7: x in Z;

        

        then (((( cos / sin ) / ( id Z)) - ( ln / ( sin ^2 ))) . x) = (((( cos / sin ) / ( id Z)) . x) - (( ln / ( sin ^2 )) . x)) by A1, VALUED_1: 13

        .= (((( cos / sin ) . x) / (( id Z) . x)) - (( ln / ( sin ^2 )) . x)) by A7, A4, RFUNCT_1:def 1

        .= (((( cos . x) / ( sin . x)) / (( id Z) . x)) - (( ln / ( sin ^2 )) . x)) by A5, A7, RFUNCT_1:def 1

        .= (((( cos . x) / ( sin . x)) / x) - (( ln / ( sin ^2 )) . x)) by A7, FUNCT_1: 18

        .= (((( cos . x) / ( sin . x)) / x) - (( ln . x) / (( sin ^2 ) . x))) by A7, A4, RFUNCT_1:def 1

        .= (((( cos . x) / ( sin . x)) / x) - (( ln . x) / (( sin . x) ^2 ))) by VALUED_1: 11;

        hence thesis by A1;

      end;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

        then ((( ln (#) cot ) `| Z) . x) = (((( cos . x) / ( sin . x)) / x) - (( ln . x) / (( sin . x) ^2 ))) by A1, FDIFF_8: 33

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

        hence thesis;

      end;

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

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

      hence thesis by A1, A2, FDIFF_8: 33, INTEGRA5: 13;

    end;

    theorem :: INTEGR13:17

    A c= Z & f = (( tan / ( id Z)) + ( ln / ( cos ^2 ))) & Z c= ( dom ( ln (#) tan )) & Z c= ( dom tan ) & Z = ( dom f) & (f | A) is continuous implies ( integral (f,A)) = ((( ln (#) tan ) . ( upper_bound A)) - (( ln (#) tan ) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & f = (( tan / ( id Z)) + ( ln / ( cos ^2 ))) & Z c= ( dom ( ln (#) tan )) & Z c= ( dom 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: ( ln (#) tan ) is_differentiable_on Z by A1, FDIFF_8: 32;

      Z = (( dom ( tan / ( id Z))) /\ ( dom ( ln / ( cos ^2 )))) by A1, VALUED_1:def 1;

      then

       A4: Z c= ( dom ( tan / ( id Z))) & Z c= ( dom ( ln / ( cos ^2 ))) by XBOOLE_1: 18;

      

       A5: for x st x in Z holds (f . x) = ((( tan . x) / x) + (( ln . x) / (( cos . x) ^2 )))

      proof

        let x;

        assume

         A6: x in Z;

        

        then ((( tan / ( id Z)) + ( ln / ( cos ^2 ))) . x) = ((( tan / ( id Z)) . x) + (( ln / ( cos ^2 )) . x)) by A1, VALUED_1:def 1

        .= ((( tan . x) / (( id Z) . x)) + (( ln / ( cos ^2 )) . x)) by A6, A4, RFUNCT_1:def 1

        .= ((( tan . x) / x) + (( ln / ( cos ^2 )) . x)) by A6, FUNCT_1: 18

        .= ((( tan . x) / x) + (( ln . x) / (( cos ^2 ) . x))) by A6, A4, RFUNCT_1:def 1

        .= ((( tan . x) / x) + (( ln . x) / (( cos . x) ^2 ))) by VALUED_1: 11;

        hence thesis by A1;

      end;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

        then ((( ln (#) tan ) `| Z) . x) = ((( tan x) / x) + (( ln . x) / (( cos . x) ^2 ))) by A1, FDIFF_8: 32

        .= ((( tan . x) / x) + (( ln . x) / (( cos . x) ^2 ))) by A1, A8, FDIFF_8: 1, SIN_COS9: 15

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

        hence thesis;

      end;

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

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

      hence thesis by A1, A2, FDIFF_8: 32, INTEGRA5: 13;

    end;

    theorem :: INTEGR13:18

    A c= Z & f = (( cot / ( id Z)) - ( ln / ( sin ^2 ))) & Z c= ( dom ( ln (#) cot )) & Z c= ( dom cot ) & Z = ( dom f) & (f | A) is continuous implies ( integral (f,A)) = ((( ln (#) cot ) . ( upper_bound A)) - (( ln (#) cot ) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & f = (( cot / ( id Z)) - ( ln / ( sin ^2 ))) & Z c= ( dom ( ln (#) cot )) & Z c= ( dom 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: ( ln (#) cot ) is_differentiable_on Z by A1, FDIFF_8: 33;

      Z = (( dom ( cot / ( id Z))) /\ ( dom ( ln / ( sin ^2 )))) by A1, VALUED_1: 12;

      then

       A4: Z c= ( dom ( cot / ( id Z))) & Z c= ( dom ( ln / ( sin ^2 ))) by XBOOLE_1: 18;

      

       A5: for x st x in Z holds (f . x) = ((( cot . x) / x) - (( ln . x) / (( sin . x) ^2 )))

      proof

        let x;

        assume

         A6: x in Z;

        

        then ((( cot / ( id Z)) - ( ln / ( sin ^2 ))) . x) = ((( cot / ( id Z)) . x) - (( ln / ( sin ^2 )) . x)) by A1, VALUED_1: 13

        .= ((( cot . x) / (( id Z) . x)) - (( ln / ( sin ^2 )) . x)) by A6, A4, RFUNCT_1:def 1

        .= ((( cot . x) / x) - (( ln / ( sin ^2 )) . x)) by A6, FUNCT_1: 18

        .= ((( cot . x) / x) - (( ln . x) / (( sin ^2 ) . x))) by A6, A4, RFUNCT_1:def 1

        .= ((( cot . x) / x) - (( ln . x) / (( sin . x) ^2 ))) by VALUED_1: 11;

        hence thesis by A1;

      end;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

        then ((( ln (#) cot ) `| Z) . x) = ((( cot x) / x) - (( ln . x) / (( sin . x) ^2 ))) by A1, FDIFF_8: 33

        .= ((( cot . x) / x) - (( ln . x) / (( sin . x) ^2 ))) by A1, A8, FDIFF_8: 2, SIN_COS9: 16

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

        hence thesis;

      end;

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

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

      hence thesis by A1, A2, FDIFF_8: 33, INTEGRA5: 13;

    end;

    theorem :: INTEGR13:19

    A c= Z & (for x st x in Z holds (f1 . x) = 1) & f = (( arctan / ( id Z)) + ( ln / (f1 + ( #Z 2)))) & Z c= ].( - 1), 1.[ & Z = ( dom f) & (f | A) is continuous implies ( integral (f,A)) = ((( ln (#) arctan ) . ( upper_bound A)) - (( ln (#) arctan ) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & (for x st x in Z holds (f1 . x) = 1) & f = (( arctan / ( id Z)) + ( ln / (f1 + ( #Z 2)))) & Z c= ].( - 1), 1.[ & 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 ( arctan / ( id Z))) /\ ( dom ( ln / (f1 + ( #Z 2))))) by A1, VALUED_1:def 1;

      then

       A3: Z c= ( dom ( arctan / ( id Z))) & Z c= ( dom ( ln / (f1 + ( #Z 2)))) by XBOOLE_1: 18;

      then Z c= (( dom arctan ) /\ (( dom ( id Z)) \ (( id Z) " { 0 }))) by RFUNCT_1:def 1;

      then

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

      Z c= (( dom ln ) /\ (( dom (f1 + ( #Z 2))) \ ((f1 + ( #Z 2)) " { 0 }))) by A3, RFUNCT_1:def 1;

      then

       A5: Z c= ( dom ln ) & Z c= (( dom (f1 + ( #Z 2))) \ ((f1 + ( #Z 2)) " { 0 })) by XBOOLE_1: 18;

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

      then

       A6: Z c= ( dom ( ln (#) arctan )) by VALUED_1:def 4;

      then

       A7: ( ln (#) arctan ) is_differentiable_on Z by A1, SIN_COS9: 127;

      

       A8: Z c= ( dom ((f1 + ( #Z 2)) ^ )) by A5, RFUNCT_1:def 2;

      ( dom ((f1 + ( #Z 2)) ^ )) c= ( dom (f1 + ( #Z 2))) by RFUNCT_1: 1;

      then

       A9: Z c= ( dom (f1 + ( #Z 2))) by A8;

      

       A10: for x st x in Z holds (f . x) = ((( arctan . x) / x) + (( ln . x) / (1 + (x ^2 ))))

      proof

        let x;

        assume

         A11: x in Z;

        

        then ((( arctan / ( id Z)) + ( ln / (f1 + ( #Z 2)))) . x) = ((( arctan / ( id Z)) . x) + (( ln / (f1 + ( #Z 2))) . x)) by A1, VALUED_1:def 1

        .= ((( arctan . x) * ((( id Z) . x) " )) + (( ln / (f1 + ( #Z 2))) . x)) by A3, A11, RFUNCT_1:def 1

        .= ((( arctan . x) * ((( id Z) . x) " )) + (( ln . x) * (((f1 + ( #Z 2)) . x) " ))) by A3, A11, RFUNCT_1:def 1

        .= ((( arctan . x) / x) + (( ln . x) / ((f1 + ( #Z 2)) . x))) by A11, FUNCT_1: 18

        .= ((( arctan . x) / x) + (( ln . x) / ((f1 . x) + (( #Z 2) . x)))) by A9, A11, VALUED_1:def 1

        .= ((( arctan . x) / x) + (( ln . x) / (1 + (( #Z 2) . x)))) by A1, A11

        .= ((( arctan . x) / x) + (( ln . x) / (1 + (x #Z 2)))) by TAYLOR_1:def 1

        .= ((( arctan . x) / x) + (( ln . x) / (1 + (x ^2 )))) by FDIFF_7: 1;

        hence thesis by A1;

      end;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

        then ((( ln (#) arctan ) `| Z) . x) = ((( arctan . x) / x) + (( ln . x) / (1 + (x ^2 )))) by A1, A6, SIN_COS9: 127

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

        hence thesis;

      end;

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

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

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

    end;

    theorem :: INTEGR13:20

    A c= Z & (for x st x in Z holds (f1 . x) = 1) & f = (( arccot / ( id Z)) - ( ln / (f1 + ( #Z 2)))) & Z c= ].( - 1), 1.[ & Z = ( dom f) & (f | A) is continuous implies ( integral (f,A)) = ((( ln (#) arccot ) . ( upper_bound A)) - (( ln (#) arccot ) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & (for x st x in Z holds (f1 . x) = 1) & f = (( arccot / ( id Z)) - ( ln / (f1 + ( #Z 2)))) & Z c= ].( - 1), 1.[ & 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 ( arccot / ( id Z))) /\ ( dom ( ln / (f1 + ( #Z 2))))) by A1, VALUED_1: 12;

      then

       A3: Z c= ( dom ( arccot / ( id Z))) & Z c= ( dom ( ln / (f1 + ( #Z 2)))) by XBOOLE_1: 18;

      then Z c= (( dom arccot ) /\ (( dom ( id Z)) \ (( id Z) " { 0 }))) by RFUNCT_1:def 1;

      then

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

      Z c= (( dom ln ) /\ (( dom (f1 + ( #Z 2))) \ ((f1 + ( #Z 2)) " { 0 }))) by A3, RFUNCT_1:def 1;

      then

       A5: Z c= ( dom ln ) & Z c= (( dom (f1 + ( #Z 2))) \ ((f1 + ( #Z 2)) " { 0 })) by XBOOLE_1: 18;

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

      then

       A6: Z c= ( dom ( ln (#) arccot )) by VALUED_1:def 4;

      then

       A7: ( ln (#) arccot ) is_differentiable_on Z by A1, SIN_COS9: 128;

      

       A8: Z c= ( dom ((f1 + ( #Z 2)) ^ )) by A5, RFUNCT_1:def 2;

      ( dom ((f1 + ( #Z 2)) ^ )) c= ( dom (f1 + ( #Z 2))) by RFUNCT_1: 1;

      then

       A9: Z c= ( dom (f1 + ( #Z 2))) by A8;

      

       A10: for x st x in Z holds (f . x) = ((( arccot . x) / x) - (( ln . x) / (1 + (x ^2 ))))

      proof

        let x;

        assume

         A11: x in Z;

        

        then ((( arccot / ( id Z)) - ( ln / (f1 + ( #Z 2)))) . x) = ((( arccot / ( id Z)) . x) - (( ln / (f1 + ( #Z 2))) . x)) by A1, VALUED_1: 13

        .= ((( arccot . x) * ((( id Z) . x) " )) - (( ln / (f1 + ( #Z 2))) . x)) by A3, A11, RFUNCT_1:def 1

        .= ((( arccot . x) * ((( id Z) . x) " )) - (( ln . x) * (((f1 + ( #Z 2)) . x) " ))) by A3, A11, RFUNCT_1:def 1

        .= ((( arccot . x) / x) - (( ln . x) / ((f1 + ( #Z 2)) . x))) by A11, FUNCT_1: 18

        .= ((( arccot . x) / x) - (( ln . x) / ((f1 . x) + (( #Z 2) . x)))) by A9, A11, VALUED_1:def 1

        .= ((( arccot . x) / x) - (( ln . x) / (1 + (( #Z 2) . x)))) by A1, A11

        .= ((( arccot . x) / x) - (( ln . x) / (1 + (x #Z 2)))) by TAYLOR_1:def 1

        .= ((( arccot . x) / x) - (( ln . x) / (1 + (x ^2 )))) by FDIFF_7: 1;

        hence thesis by A1;

      end;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

        then ((( ln (#) arccot ) `| Z) . x) = ((( arccot . x) / x) - (( ln . x) / (1 + (x ^2 )))) by A1, A6, SIN_COS9: 128

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

        hence thesis;

      end;

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

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

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

    end;

    theorem :: INTEGR13:21

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

    proof

      assume

       A1: A c= Z & f = (( exp_R * tan ) / ( 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 * tan )) /\ (( dom ( cos ^2 )) \ (( cos ^2 ) " { 0 }))) by A1, RFUNCT_1:def 1;

      then

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

      then

       A4: ( exp_R * tan ) is_differentiable_on Z by FDIFF_8: 16;

      

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

      proof

        let x;

        assume

         A6: x in Z;

        

        then ((( exp_R * tan ) / ( cos ^2 )) . x) = ((( exp_R * tan ) . x) / (( cos ^2 ) . x)) by A1, RFUNCT_1:def 1

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

        .= (( exp_R . ( tan . x)) / (( cos . x) ^2 )) by VALUED_1: 11;

        hence thesis by A1;

      end;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

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

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

        hence thesis;

      end;

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

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

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

    end;

    theorem :: INTEGR13:22

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

    proof

      assume

       A1: A c= Z & f = ( - (( exp_R * cot ) / ( 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;

      

       A3: Z = ( dom (( exp_R * cot ) / ( sin ^2 ))) by A1, VALUED_1: 8;

      then Z c= (( dom ( exp_R * cot )) /\ (( dom ( sin ^2 )) \ (( sin ^2 ) " { 0 }))) by RFUNCT_1:def 1;

      then

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

      then

       A5: ( exp_R * cot ) is_differentiable_on Z by FDIFF_8: 17;

      

       A6: for x st x in Z holds (f . x) = ( - (( exp_R . ( cot . x)) / (( sin . x) ^2 )))

      proof

        let x;

        assume

         A7: x in Z;

        (( - (( exp_R * cot ) / ( sin ^2 ))) . x) = ( - ((( exp_R * cot ) / ( sin ^2 )) . x)) by VALUED_1: 8

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

        .= ( - (( exp_R . ( cot . x)) / (( sin ^2 ) . x))) by A4, A7, FUNCT_1: 12

        .= ( - (( exp_R . ( cot . x)) / (( sin . x) ^2 ))) by VALUED_1: 11;

        hence thesis by A1;

      end;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

        then ((( exp_R * cot ) `| Z) . x) = ( - (( exp_R . ( cot . x)) / (( sin . x) ^2 ))) by A4, FDIFF_8: 17

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

        hence thesis;

      end;

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

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

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

    end;

    theorem :: INTEGR13:23

    

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

    proof

      assume

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

      then

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

      

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

      proof

        let x;

        assume x in Z;

        then x in ( dom ( cos / sin )) by A1, FUNCT_1: 11;

        hence thesis by FDIFF_8: 2;

      end;

      

       A4: ( exp_R * cot ) is_differentiable_on Z by A1, FDIFF_8: 17;

      then

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

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

      proof

        let x;

        assume

         A6: x in Z;

        then

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

        then

         A8: cot is_differentiable_in x by FDIFF_7: 47;

        

         A9: exp_R is_differentiable_in ( cot . x) by SIN_COS: 65;

        

         A10: ( exp_R * cot ) is_differentiable_in x by A4, A6, FDIFF_1: 9;

        ((( - ( exp_R * cot )) `| Z) . x) = ( diff (( - ( exp_R * cot )),x)) by A5, A6, FDIFF_1:def 7

        .= (( - 1) * ( diff (( exp_R * cot ),x))) by A10, FDIFF_1: 15

        .= (( - 1) * (( diff ( exp_R ,( cot . x))) * ( diff ( cot ,x)))) by A8, A9, FDIFF_2: 13

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

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

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

        hence thesis;

      end;

      hence thesis by A2, A4, FDIFF_1: 20;

    end;

    theorem :: INTEGR13:24

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

    proof

      assume

       A1: A c= Z & f = (( exp_R * cot ) / ( 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 * cot )) /\ (( dom ( sin ^2 )) \ (( sin ^2 ) " { 0 }))) by A1, RFUNCT_1:def 1;

      then

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

      then

       A4: ( - ( exp_R * cot )) is_differentiable_on Z by Th23;

      

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

      proof

        let x;

        assume

         A6: x in Z;

        

        then ((( exp_R * cot ) / ( sin ^2 )) . x) = ((( exp_R * cot ) . x) / (( sin ^2 ) . x)) by A1, RFUNCT_1:def 1

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

        .= (( exp_R . ( cot . x)) / (( sin . x) ^2 )) by VALUED_1: 11;

        hence thesis by A1;

      end;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

        then ((( - ( exp_R * cot )) `| Z) . x) = (( exp_R . ( cot . x)) / (( sin . x) ^2 )) by Th23, A3

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

        hence thesis;

      end;

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

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

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

    end;

    theorem :: INTEGR13:25

    A c= Z & f = ((( id Z) (#) (( cos * ln ) ^2 )) ^ ) & Z c= ( dom ( tan * ln )) & Z = ( dom f) & (f | A) is continuous implies ( integral (f,A)) = ((( tan * ln ) . ( upper_bound A)) - (( tan * ln ) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & f = ((( id Z) (#) (( cos * ln ) ^2 )) ^ ) & Z c= ( dom ( tan * 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: ( tan * ln ) is_differentiable_on Z by A1, FDIFF_8: 14;

      Z c= ( dom (( id Z) (#) (( cos * ln ) ^2 ))) by A1, RFUNCT_1: 1;

      then Z c= (( dom ( id Z)) /\ ( dom (( cos * ln ) ^2 ))) by VALUED_1:def 4;

      then Z c= ( dom (( cos * ln ) ^2 )) by XBOOLE_1: 18;

      then

       A4: Z c= ( dom ( cos * ln )) by VALUED_1: 11;

      

       A5: for x st x in Z holds (f . x) = (1 / (x * (( cos . ( ln . x)) ^2 )))

      proof

        let x;

        assume

         A6: x in Z;

        

        then (((( id Z) (#) (( cos * ln ) ^2 )) ^ ) . x) = (1 / ((( id Z) (#) (( cos * ln ) ^2 )) . x)) by A1, RFUNCT_1:def 2

        .= (1 / ((( id Z) . x) * ((( cos * ln ) ^2 ) . x))) by VALUED_1: 5

        .= (1 / (x * ((( cos * ln ) ^2 ) . x))) by A6, FUNCT_1: 18

        .= (1 / (x * ((( cos * ln ) . x) ^2 ))) by VALUED_1: 11

        .= (1 / (x * (( cos . ( ln . x)) ^2 ))) by A4, A6, FUNCT_1: 12;

        hence thesis by A1;

      end;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

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

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

        hence thesis;

      end;

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

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

      hence thesis by A1, A2, FDIFF_8: 14, INTEGRA5: 13;

    end;

    theorem :: INTEGR13:26

    A c= Z & f = ( - ((( id Z) (#) (( sin * ln ) ^2 )) ^ )) & Z c= ( dom ( cot * ln )) & Z = ( dom f) & (f | A) is continuous implies ( integral (f,A)) = ((( cot * ln ) . ( upper_bound A)) - (( cot * ln ) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & f = ( - ((( id Z) (#) (( sin * ln ) ^2 )) ^ )) & Z c= ( dom ( cot * 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: ( cot * ln ) is_differentiable_on Z by A1, FDIFF_8: 15;

      

       A4: Z = ( dom ((( id Z) (#) (( sin * ln ) ^2 )) ^ )) by A1, VALUED_1: 8;

      then Z c= ( dom (( id Z) (#) (( sin * ln ) ^2 ))) by RFUNCT_1: 1;

      then Z c= (( dom ( id Z)) /\ ( dom (( sin * ln ) ^2 ))) by VALUED_1:def 4;

      then Z c= ( dom (( sin * ln ) ^2 )) by XBOOLE_1: 18;

      then

       A5: Z c= ( dom ( sin * ln )) by VALUED_1: 11;

      

       A6: for x st x in Z holds (f . x) = ( - (1 / (x * (( sin . ( ln . x)) ^2 ))))

      proof

        let x;

        assume

         A7: x in Z;

        (( - ((( id Z) (#) (( sin * ln ) ^2 )) ^ )) . x) = ( - (((( id Z) (#) (( sin * ln ) ^2 )) ^ ) . x)) by VALUED_1: 8

        .= ( - (1 / ((( id Z) (#) (( sin * ln ) ^2 )) . x))) by A4, A7, RFUNCT_1:def 2

        .= ( - (1 / ((( id Z) . x) * ((( sin * ln ) ^2 ) . x)))) by VALUED_1: 5

        .= ( - (1 / (x * ((( sin * ln ) ^2 ) . x)))) by A7, FUNCT_1: 18

        .= ( - (1 / (x * ((( sin * ln ) . x) ^2 )))) by VALUED_1: 11

        .= ( - (1 / (x * (( sin . ( ln . x)) ^2 )))) by A5, A7, FUNCT_1: 12;

        hence thesis by A1;

      end;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

        then ((( cot * ln ) `| Z) . x) = ( - (1 / (x * (( sin . ( ln . x)) ^2 )))) by A1, FDIFF_8: 15

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

        hence thesis;

      end;

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

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

      hence thesis by A1, A2, FDIFF_8: 15, INTEGRA5: 13;

    end;

    theorem :: INTEGR13:27

    

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

    proof

      assume

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

      then

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

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

      then

       A3: Z c= ( dom ln ) by A1;

      

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

      proof

        let x;

        assume x in Z;

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

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

        hence thesis;

      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 ( cos / sin )) by A1, FUNCT_1: 11;

        hence thesis by FDIFF_8: 2;

      end;

      

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

      proof

        let x;

        assume x in Z;

        then x > 0 by A4;

        then x in ( right_open_halfline 0 ) by Lm2;

        hence thesis by TAYLOR_1: 18;

      end;

      

       A7: ( cot * ln ) is_differentiable_on Z by A1, FDIFF_8: 15;

      then

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

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

      proof

        let x;

        assume

         A9: x in Z;

        then

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

        

         A11: x > 0 & ( sin . ( ln . x)) <> 0 by A4, A5, A9;

        then

         A12: cot is_differentiable_in ( ln . x) by FDIFF_7: 47;

        

         A13: ( cot * ln ) is_differentiable_in x by A7, A9, FDIFF_1: 9;

        ((( - ( cot * ln )) `| Z) . x) = ( diff (( - ( cot * ln )),x)) by A8, A9, FDIFF_1:def 7

        .= (( - 1) * ( diff (( cot * ln ),x))) by A13, FDIFF_1: 15

        .= (( - 1) * (( diff ( cot ,( ln . x))) * ( diff ( ln ,x)))) by A10, A12, FDIFF_2: 13

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

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

        .= (( - 1) * ( - ((1 / x) / (( sin . ( ln . x)) ^2 )))) by A6, A9

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

        hence thesis;

      end;

      hence thesis by A2, A7, FDIFF_1: 20;

    end;

    theorem :: INTEGR13:28

    A c= Z & f = ((( id Z) (#) (( sin * ln ) ^2 )) ^ ) & Z c= ( dom ( cot * ln )) & Z = ( dom f) & (f | A) is continuous implies ( integral (f,A)) = ((( - ( cot * ln )) . ( upper_bound A)) - (( - ( cot * ln )) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & f = ((( id Z) (#) (( sin * ln ) ^2 )) ^ ) & Z c= ( dom ( cot * 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: ( - ( cot * ln )) is_differentiable_on Z by A1, Th27;

      Z c= ( dom (( id Z) (#) (( sin * ln ) ^2 ))) by A1, RFUNCT_1: 1;

      then Z c= (( dom ( id Z)) /\ ( dom (( sin * ln ) ^2 ))) by VALUED_1:def 4;

      then Z c= ( dom (( sin * ln ) ^2 )) by XBOOLE_1: 18;

      then

       A4: Z c= ( dom ( sin * ln )) by VALUED_1: 11;

      

       A5: for x st x in Z holds (f . x) = (1 / (x * (( sin . ( ln . x)) ^2 )))

      proof

        let x;

        assume

         A6: x in Z;

        

        then (((( id Z) (#) (( sin * ln ) ^2 )) ^ ) . x) = (1 / ((( id Z) (#) (( sin * ln ) ^2 )) . x)) by A1, RFUNCT_1:def 2

        .= (1 / ((( id Z) . x) * ((( sin * ln ) ^2 ) . x))) by VALUED_1: 5

        .= (1 / (x * ((( sin * ln ) ^2 ) . x))) by A6, FUNCT_1: 18

        .= (1 / (x * ((( sin * ln ) . x) ^2 ))) by VALUED_1: 11

        .= (1 / (x * (( sin . ( ln . x)) ^2 ))) by A4, A6, FUNCT_1: 12;

        hence thesis by A1;

      end;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

        then ((( - ( cot * ln )) `| Z) . x) = (1 / (x * (( sin . ( ln . x)) ^2 ))) by A1, Th27

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

        hence thesis;

      end;

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

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

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

    end;

    theorem :: INTEGR13:29

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

    proof

      assume

       A1: A c= Z & f = ( exp_R / (( cos * exp_R ) ^2 )) & Z c= ( dom ( tan * 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: ( tan * exp_R ) is_differentiable_on Z by A1, FDIFF_8: 12;

      Z = (( dom exp_R ) /\ (( dom (( cos * exp_R ) ^2 )) \ ((( cos * exp_R ) ^2 ) " { 0 }))) by A1, RFUNCT_1:def 1;

      then Z c= (( dom (( cos * exp_R ) ^2 )) \ ((( cos * exp_R ) ^2 ) " { 0 })) by XBOOLE_1: 18;

      then

       A4: Z c= ( dom ((( cos * exp_R ) ^2 ) ^ )) by RFUNCT_1:def 2;

      ( dom ((( cos * exp_R ) ^2 ) ^ )) c= ( dom (( cos * exp_R ) ^2 )) by RFUNCT_1: 1;

      then Z c= ( dom (( cos * exp_R ) ^2 )) by A4;

      then

       A5: Z c= ( dom ( cos * exp_R )) by VALUED_1: 11;

      

       A6: for x st x in Z holds (f . x) = (( exp_R . x) / (( cos . ( exp_R . x)) ^2 ))

      proof

        let x;

        assume

         A7: x in Z;

        

        then (( exp_R / (( cos * exp_R ) ^2 )) . x) = (( exp_R . x) / ((( cos * exp_R ) ^2 ) . x)) by A1, RFUNCT_1:def 1

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

        .= (( exp_R . x) / (( cos . ( exp_R . x)) ^2 )) by A5, A7, FUNCT_1: 12;

        hence thesis by A1;

      end;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

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

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

        hence thesis;

      end;

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

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

      hence thesis by A1, A2, FDIFF_8: 12, INTEGRA5: 13;

    end;

    theorem :: INTEGR13:30

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

    proof

      assume

       A1: A c= Z & f = ( - ( exp_R / (( sin * exp_R ) ^2 ))) & Z c= ( dom ( cot * 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: ( cot * exp_R ) is_differentiable_on Z by A1, FDIFF_8: 13;

      

       A4: Z = ( dom ( exp_R / (( sin * exp_R ) ^2 ))) by A1, VALUED_1: 8;

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

      then Z c= (( dom (( sin * exp_R ) ^2 )) \ ((( sin * exp_R ) ^2 ) " { 0 })) by XBOOLE_1: 18;

      then

       A5: Z c= ( dom ((( sin * exp_R ) ^2 ) ^ )) by RFUNCT_1:def 2;

      ( dom ((( sin * exp_R ) ^2 ) ^ )) c= ( dom (( sin * exp_R ) ^2 )) by RFUNCT_1: 1;

      then Z c= ( dom (( sin * exp_R ) ^2 )) by A5;

      then

       A6: Z c= ( dom ( sin * exp_R )) by VALUED_1: 11;

      

       A7: for x st x in Z holds (f . x) = ( - (( exp_R . x) / (( sin . ( exp_R . x)) ^2 )))

      proof

        let x;

        assume

         A8: x in Z;

        (( - ( exp_R / (( sin * exp_R ) ^2 ))) . x) = ( - (( exp_R / (( sin * exp_R ) ^2 )) . x)) by VALUED_1: 8

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

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

        .= ( - (( exp_R . x) / (( sin . ( exp_R . x)) ^2 ))) by A6, A8, FUNCT_1: 12;

        hence thesis by A1;

      end;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

        then ((( cot * exp_R ) `| Z) . x) = ( - (( exp_R . x) / (( sin . ( exp_R . x)) ^2 ))) by A1, FDIFF_8: 13

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

        hence thesis;

      end;

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

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

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

    end;

    theorem :: INTEGR13:31

    

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

    proof

      assume

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

      then

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

      

       A3: ( cot * exp_R ) is_differentiable_on Z by A1, FDIFF_8: 13;

      then

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

      

       A5: 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 ( cos / sin )) by A1, FUNCT_1: 11;

        hence thesis by FDIFF_8: 2;

      end;

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

      proof

        let x;

        assume

         A6: x in Z;

        

         A7: exp_R is_differentiable_in x by SIN_COS: 65;

        

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

        then

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

        

         A10: ( cot * exp_R ) is_differentiable_in x by A3, A6, FDIFF_1: 9;

        ((( - ( cot * exp_R )) `| Z) . x) = ( diff (( - ( cot * exp_R )),x)) by A4, A6, FDIFF_1:def 7

        .= (( - 1) * ( diff (( cot * exp_R ),x))) by A10, FDIFF_1: 15

        .= (( - 1) * (( diff ( cot ,( exp_R . x))) * ( diff ( exp_R ,x)))) by A7, A9, FDIFF_2: 13

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

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

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

        hence thesis;

      end;

      hence thesis by A4;

    end;

    theorem :: INTEGR13:32

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

    proof

      assume

       A1: A c= Z & f = ( exp_R / (( sin * exp_R ) ^2 )) & Z c= ( dom ( cot * 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: ( - ( cot * exp_R )) is_differentiable_on Z by A1, Th31;

      Z c= (( dom exp_R ) /\ (( dom (( sin * exp_R ) ^2 )) \ ((( sin * exp_R ) ^2 ) " { 0 }))) by A1, RFUNCT_1:def 1;

      then Z c= (( dom (( sin * exp_R ) ^2 )) \ ((( sin * exp_R ) ^2 ) " { 0 })) by XBOOLE_1: 18;

      then

       A4: Z c= ( dom ((( sin * exp_R ) ^2 ) ^ )) by RFUNCT_1:def 2;

      ( dom ((( sin * exp_R ) ^2 ) ^ )) c= ( dom (( sin * exp_R ) ^2 )) by RFUNCT_1: 1;

      then Z c= ( dom (( sin * exp_R ) ^2 )) by A4;

      then

       A5: Z c= ( dom ( sin * exp_R )) by VALUED_1: 11;

      

       A6: for x st x in Z holds (f . x) = (( exp_R . x) / (( sin . ( exp_R . x)) ^2 ))

      proof

        let x;

        assume

         A7: x in Z;

        

        then (( exp_R / (( sin * exp_R ) ^2 )) . x) = (( exp_R . x) / ((( sin * exp_R ) ^2 ) . x)) by A1, RFUNCT_1:def 1

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

        .= (( exp_R . x) / (( sin . ( exp_R . x)) ^2 )) by A5, A7, FUNCT_1: 12;

        hence thesis by A1;

      end;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

        then ((( - ( cot * exp_R )) `| Z) . x) = (( exp_R . x) / (( sin . ( exp_R . x)) ^2 )) by A1, Th31

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

        hence thesis;

      end;

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

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

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

    end;

    theorem :: INTEGR13:33

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

    proof

      assume

       A1: A c= Z & (for x st x in Z holds (f . x) = ( - (1 / ((x ^2 ) * (( cos . (1 / x)) ^2 ))))) & Z c= ( dom ( tan * (( 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: ( tan * (( id Z) ^ )) is_differentiable_on Z by A1, FDIFF_8: 8;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

        then ((( tan * (( id Z) ^ )) `| Z) . x) = ( - (1 / ((x ^2 ) * (( cos . (1 / x)) ^2 )))) by A1, A4, FDIFF_8: 8

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

        hence thesis;

      end;

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

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

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

    end;

    theorem :: INTEGR13:34

    

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

    proof

      set f = ( id Z);

      assume

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

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

      then

       A2: Z c= ( dom (f ^ )) by A1;

      

       A3: not 0 in Z

      proof

        assume

         A4: 0 in Z;

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

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

        then not 0 in { 0 } by A4, A2, XBOOLE_0:def 5;

        hence thesis by TARSKI:def 1;

      end;

      

       A5: Z c= ( dom ( - ( tan * (( id Z) ^ )))) by A1, VALUED_1: 8;

      

       A6: ( tan * (( id Z) ^ )) is_differentiable_on Z by A1, A3, FDIFF_8: 8;

      then

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

      

       A8: (f ^ ) is_differentiable_on Z & for x st x in Z holds (((f ^ ) `| Z) . x) = ( - (1 / (x ^2 ))) by A3, FDIFF_5: 4;

      

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

      proof

        let x;

        assume x in Z;

        then ((f ^ ) . x) in ( dom ( sin / cos )) by A1, FUNCT_1: 11;

        hence thesis by FDIFF_8: 1;

      end;

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

      proof

        let x;

        assume

         A10: x in Z;

        then

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

        

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

        then

         A13: tan is_differentiable_in ((f ^ ) . x) by FDIFF_7: 46;

        

         A14: ( tan * (f ^ )) is_differentiable_in x by A6, A10, FDIFF_1: 9;

        ((( - ( tan * (f ^ ))) `| Z) . x) = ( diff (( - ( tan * (f ^ ))),x)) by A7, A10, FDIFF_1:def 7

        .= (( - 1) * ( diff (( tan * (f ^ )),x))) by A14, FDIFF_1: 15

        .= (( - 1) * (( diff ( tan ,((f ^ ) . x))) * ( diff ((f ^ ),x)))) by A11, A13, FDIFF_2: 13

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

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

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

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

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

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

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

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

        hence thesis;

      end;

      hence thesis by A7;

    end;

    theorem :: INTEGR13:35

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

    proof

      assume

       A1: A c= Z & (for x st x in Z holds (f . x) = (1 / ((x ^2 ) * (( cos . (1 / x)) ^2 )))) & Z c= ( dom ( tan * (( 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: ( - ( tan * (( id Z) ^ ))) is_differentiable_on Z by A1, Th34;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

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

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

        hence thesis;

      end;

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

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

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

    end;

    theorem :: INTEGR13:36

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

    proof

      assume

       A1: A c= Z & (for x st x in Z holds (f . x) = (1 / ((x ^2 ) * (( sin . (1 / x)) ^2 )))) & Z c= ( dom ( cot * (( 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: ( cot * (( id Z) ^ )) is_differentiable_on Z by A1, FDIFF_8: 9;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

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

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

        hence thesis;

      end;

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

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

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

    end;

    theorem :: INTEGR13:37

    A c= Z & (for x st x in Z holds (f1 . x) = 1 & ( arctan . x) > 0 ) & f = (((f1 + ( #Z 2)) (#) arctan ) ^ ) & Z c= ].( - 1), 1.[ & Z c= ( dom ( ln * arctan )) & Z = ( dom f) & (f | A) is continuous implies ( integral (f,A)) = ((( ln * arctan ) . ( upper_bound A)) - (( ln * arctan ) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & (for x st x in Z holds (f1 . x) = 1 & ( arctan . x) > 0 ) & f = (((f1 + ( #Z 2)) (#) arctan ) ^ ) & Z c= ].( - 1), 1.[ & Z c= ( dom ( ln * arctan )) & Z = ( dom f) & (f | A) is continuous;

      then

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

      

       A3: for x st x in Z holds ( arctan . x) > 0 by A1;

      then

       A4: ( ln * arctan ) is_differentiable_on Z by A1, SIN_COS9: 89;

      Z c= ( dom ((f1 + ( #Z 2)) (#) arctan )) by A1, RFUNCT_1: 1;

      then Z c= (( dom (f1 + ( #Z 2))) /\ ( dom arctan )) by VALUED_1:def 4;

      then

       A5: Z c= ( dom (f1 + ( #Z 2))) by XBOOLE_1: 18;

      

       A6: for x st x in Z holds (f . x) = (1 / ((1 + (x ^2 )) * ( arctan . x)))

      proof

        let x;

        assume

         A7: x in Z;

        

        then ((((f1 + ( #Z 2)) (#) arctan ) ^ ) . x) = (1 / (((f1 + ( #Z 2)) (#) arctan ) . x)) by A1, RFUNCT_1:def 2

        .= (1 / (((f1 + ( #Z 2)) . x) * ( arctan . x))) by VALUED_1: 5

        .= (1 / (((f1 . x) + (( #Z 2) . x)) * ( arctan . x))) by A5, A7, VALUED_1:def 1

        .= (1 / (((f1 . x) + (x #Z 2)) * ( arctan . x))) by TAYLOR_1:def 1

        .= (1 / ((1 + (x #Z 2)) * ( arctan . x))) by A1, A7

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

        hence thesis by A1;

      end;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

        then ((( ln * arctan ) `| Z) . x) = (1 / ((1 + (x ^2 )) * ( arctan . x))) by A1, A3, SIN_COS9: 89

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

        hence thesis;

      end;

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

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

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

    end;

    theorem :: INTEGR13:38

    A c= Z & f = (n (#) ((( #Z (n - 1)) * arctan ) / (f1 + ( #Z 2)))) & (for x st x in Z holds (f1 . x) = 1) & Z c= ].( - 1), 1.[ & Z c= ( dom (( #Z n) * arctan )) & Z = ( dom f) & (f | A) is continuous implies ( integral (f,A)) = (((( #Z n) * arctan ) . ( upper_bound A)) - ((( #Z n) * arctan ) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & f = (n (#) ((( #Z (n - 1)) * arctan ) / (f1 + ( #Z 2)))) & (for x st x in Z holds (f1 . x) = 1) & Z c= ].( - 1), 1.[ & Z c= ( dom (( #Z n) * arctan )) & 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) * arctan ) is_differentiable_on Z by A1, SIN_COS9: 91;

      

       A4: Z = ( dom ((( #Z (n - 1)) * arctan ) / (f1 + ( #Z 2)))) by A1, VALUED_1:def 5;

      then Z c= (( dom (( #Z (n - 1)) * arctan )) /\ (( dom (f1 + ( #Z 2))) \ ((f1 + ( #Z 2)) " { 0 }))) by RFUNCT_1:def 1;

      then

       A5: Z c= ( dom (( #Z (n - 1)) * arctan )) & Z c= (( dom (f1 + ( #Z 2))) \ ((f1 + ( #Z 2)) " { 0 })) by XBOOLE_1: 18;

      then

       A6: Z c= ( dom ((f1 + ( #Z 2)) ^ )) by RFUNCT_1:def 2;

      ( dom ((f1 + ( #Z 2)) ^ )) c= ( dom (f1 + ( #Z 2))) by RFUNCT_1: 1;

      then

       A7: Z c= ( dom (f1 + ( #Z 2))) by A6;

      

       A8: for x st x in Z holds (f . x) = ((n * (( arctan . x) #Z (n - 1))) / (1 + (x ^2 )))

      proof

        let x;

        assume

         A9: x in Z;

        ((n (#) ((( #Z (n - 1)) * arctan ) / (f1 + ( #Z 2)))) . x) = (n * (((( #Z (n - 1)) * arctan ) / (f1 + ( #Z 2))) . x)) by VALUED_1: 6

        .= (n * (((( #Z (n - 1)) * arctan ) . x) * (((f1 + ( #Z 2)) . x) " ))) by A4, A9, RFUNCT_1:def 1

        .= ((n * ((( #Z (n - 1)) * arctan ) . x)) / ((f1 + ( #Z 2)) . x))

        .= ((n * (( #Z (n - 1)) . ( arctan . x))) / ((f1 + ( #Z 2)) . x)) by A5, A9, FUNCT_1: 12

        .= ((n * (( arctan . x) #Z (n - 1))) / ((f1 + ( #Z 2)) . x)) by TAYLOR_1:def 1

        .= ((n * (( arctan . x) #Z (n - 1))) / ((f1 . x) + (( #Z 2) . x))) by A7, A9, VALUED_1:def 1

        .= ((n * (( arctan . x) #Z (n - 1))) / (1 + (( #Z 2) . x))) by A1, A9

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

        .= ((n * (( arctan . x) #Z (n - 1))) / (1 + (x ^2 ))) by FDIFF_7: 1;

        hence thesis by A1;

      end;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

        then (((( #Z n) * arctan ) `| Z) . x) = ((n * (( arctan . x) #Z (n - 1))) / (1 + (x ^2 ))) by A1, SIN_COS9: 91

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

        hence thesis;

      end;

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

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

      hence thesis by A1, A2, INTEGRA5: 13, SIN_COS9: 91;

    end;

    theorem :: INTEGR13:39

    A c= Z & (for x st x in Z holds (f1 . x) = 1) & f = ( - (n (#) ((( #Z (n - 1)) * arccot ) / (f1 + ( #Z 2))))) & Z c= ].( - 1), 1.[ & Z c= ( dom (( #Z n) * arccot )) & Z = ( dom f) & (f | A) is continuous implies ( integral (f,A)) = (((( #Z n) * arccot ) . ( upper_bound A)) - ((( #Z n) * arccot ) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & (for x st x in Z holds (f1 . x) = 1) & f = ( - (n (#) ((( #Z (n - 1)) * arccot ) / (f1 + ( #Z 2))))) & Z c= ].( - 1), 1.[ & Z c= ( dom (( #Z n) * arccot )) & 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) * arccot ) is_differentiable_on Z by A1, SIN_COS9: 92;

      Z = ( dom (n (#) ((( #Z (n - 1)) * arccot ) / (f1 + ( #Z 2))))) by A1, VALUED_1: 8;

      then

       A4: Z = ( dom ((( #Z (n - 1)) * arccot ) / (f1 + ( #Z 2)))) by VALUED_1:def 5;

      then Z c= (( dom (( #Z (n - 1)) * arccot )) /\ (( dom (f1 + ( #Z 2))) \ ((f1 + ( #Z 2)) " { 0 }))) by RFUNCT_1:def 1;

      then

       A5: Z c= ( dom (( #Z (n - 1)) * arccot )) & Z c= (( dom (f1 + ( #Z 2))) \ ((f1 + ( #Z 2)) " { 0 })) by XBOOLE_1: 18;

      then

       A6: Z c= ( dom ((f1 + ( #Z 2)) ^ )) by RFUNCT_1:def 2;

      ( dom ((f1 + ( #Z 2)) ^ )) c= ( dom (f1 + ( #Z 2))) by RFUNCT_1: 1;

      then

       A7: Z c= ( dom (f1 + ( #Z 2))) by A6;

      

       A8: for x st x in Z holds (f . x) = ( - ((n * (( arccot . x) #Z (n - 1))) / (1 + (x ^2 ))))

      proof

        let x;

        assume

         A9: x in Z;

        (( - (n (#) ((( #Z (n - 1)) * arccot ) / (f1 + ( #Z 2))))) . x) = ( - ((n (#) ((( #Z (n - 1)) * arccot ) / (f1 + ( #Z 2)))) . x)) by VALUED_1: 8

        .= ( - (n * (((( #Z (n - 1)) * arccot ) / (f1 + ( #Z 2))) . x))) by VALUED_1: 6

        .= ( - (n * (((( #Z (n - 1)) * arccot ) . x) * (((f1 + ( #Z 2)) . x) " )))) by A4, A9, RFUNCT_1:def 1

        .= ( - ((n * ((( #Z (n - 1)) * arccot ) . x)) / ((f1 + ( #Z 2)) . x)))

        .= ( - ((n * (( #Z (n - 1)) . ( arccot . x))) / ((f1 + ( #Z 2)) . x))) by A5, A9, FUNCT_1: 12

        .= ( - ((n * (( arccot . x) #Z (n - 1))) / ((f1 + ( #Z 2)) . x))) by TAYLOR_1:def 1

        .= ( - ((n * (( arccot . x) #Z (n - 1))) / ((f1 . x) + (( #Z 2) . x)))) by A7, A9, VALUED_1:def 1

        .= ( - ((n * (( arccot . x) #Z (n - 1))) / (1 + (( #Z 2) . x)))) by A1, A9

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

        .= ( - ((n * (( arccot . x) #Z (n - 1))) / (1 + (x ^2 )))) by FDIFF_7: 1;

        hence thesis by A1;

      end;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

        then (((( #Z n) * arccot ) `| Z) . x) = ( - ((n * (( arccot . x) #Z (n - 1))) / (1 + (x ^2 )))) by A1, SIN_COS9: 92

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

        hence thesis;

      end;

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

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

      hence thesis by A1, A2, INTEGRA5: 13, SIN_COS9: 92;

    end;

    theorem :: INTEGR13:40

    

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

    proof

      assume

       A1: Z c= ( dom (( #Z n) * arccot )) & Z c= ].( - 1), 1.[;

      then

       A2: Z c= ( dom ( - (( #Z n) * arccot ))) by VALUED_1: 8;

      

       A3: (( #Z n) * arccot ) is_differentiable_on Z by A1, SIN_COS9: 92;

      then

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

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

      proof

        let x;

        assume

         A5: x in Z;

        then

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

         arccot is_differentiable_on Z by A1, SIN_COS9: 82;

        then

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

        

         A8: (( #Z n) * arccot ) is_differentiable_in x by A3, A5, FDIFF_1: 9;

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

        .= (( - 1) * ( diff ((( #Z n) * arccot ),x))) by A8, FDIFF_1: 15

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

        .= (( - 1) * ((n * (( arccot . x) #Z (n - 1))) * ( - (1 / (1 + (x ^2 )))))) by A6, SIN_COS9: 76

        .= ((n * (( arccot . x) #Z (n - 1))) / (1 + (x ^2 )));

        hence thesis;

      end;

      hence thesis by A2, A3, FDIFF_1: 20;

    end;

    theorem :: INTEGR13:41

    A c= Z & (for x st x in Z holds (f1 . x) = 1) & f = (n (#) ((( #Z (n - 1)) * arccot ) / (f1 + ( #Z 2)))) & Z c= ].( - 1), 1.[ & Z c= ( dom (( #Z n) * arccot )) & Z = ( dom f) & (f | A) is continuous implies ( integral (f,A)) = ((( - (( #Z n) * arccot )) . ( upper_bound A)) - (( - (( #Z n) * arccot )) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & (for x st x in Z holds (f1 . x) = 1) & f = (n (#) ((( #Z (n - 1)) * arccot ) / (f1 + ( #Z 2)))) & Z c= ].( - 1), 1.[ & Z c= ( dom (( #Z n) * arccot )) & 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) * arccot )) is_differentiable_on Z by A1, Th40;

      

       A4: Z = ( dom ((( #Z (n - 1)) * arccot ) / (f1 + ( #Z 2)))) by A1, VALUED_1:def 5;

      then Z c= (( dom (( #Z (n - 1)) * arccot )) /\ (( dom (f1 + ( #Z 2))) \ ((f1 + ( #Z 2)) " { 0 }))) by RFUNCT_1:def 1;

      then

       A5: Z c= ( dom (( #Z (n - 1)) * arccot )) & Z c= (( dom (f1 + ( #Z 2))) \ ((f1 + ( #Z 2)) " { 0 })) by XBOOLE_1: 18;

      then

       A6: Z c= ( dom ((f1 + ( #Z 2)) ^ )) by RFUNCT_1:def 2;

      ( dom ((f1 + ( #Z 2)) ^ )) c= ( dom (f1 + ( #Z 2))) by RFUNCT_1: 1;

      then

       A7: Z c= ( dom (f1 + ( #Z 2))) by A6;

      

       A8: for x st x in Z holds (f . x) = ((n * (( arccot . x) #Z (n - 1))) / (1 + (x ^2 )))

      proof

        let x;

        assume

         A9: x in Z;

        ((n (#) ((( #Z (n - 1)) * arccot ) / (f1 + ( #Z 2)))) . x) = (n * (((( #Z (n - 1)) * arccot ) / (f1 + ( #Z 2))) . x)) by VALUED_1: 6

        .= (n * (((( #Z (n - 1)) * arccot ) . x) * (((f1 + ( #Z 2)) . x) " ))) by A4, A9, RFUNCT_1:def 1

        .= ((n * ((( #Z (n - 1)) * arccot ) . x)) / ((f1 + ( #Z 2)) . x))

        .= ((n * (( #Z (n - 1)) . ( arccot . x))) / ((f1 + ( #Z 2)) . x)) by A5, A9, FUNCT_1: 12

        .= ((n * (( arccot . x) #Z (n - 1))) / ((f1 + ( #Z 2)) . x)) by TAYLOR_1:def 1

        .= ((n * (( arccot . x) #Z (n - 1))) / ((f1 . x) + (( #Z 2) . x))) by A7, A9, VALUED_1:def 1

        .= ((n * (( arccot . x) #Z (n - 1))) / (1 + (( #Z 2) . x))) by A1, A9

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

        .= ((n * (( arccot . x) #Z (n - 1))) / (1 + (x ^2 ))) by FDIFF_7: 1;

        hence thesis by A1;

      end;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

        then ((( - (( #Z n) * arccot )) `| Z) . x) = ((n * (( arccot . x) #Z (n - 1))) / (1 + (x ^2 ))) by A1, Th40

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

        hence thesis;

      end;

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

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

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

    end;

    theorem :: INTEGR13:42

    A c= Z & (for x st x in Z holds (f1 . x) = 1) & f = ( arctan / (f1 + ( #Z 2))) & Z c= ].( - 1), 1.[ & Z c= ( dom (( #Z 2) * arctan )) & Z = ( dom f) & (f | A) is continuous implies ( integral (f,A)) = ((((1 / 2) (#) (( #Z 2) * arctan )) . ( upper_bound A)) - (((1 / 2) (#) (( #Z 2) * arctan )) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & (for x st x in Z holds (f1 . x) = 1) & f = ( arctan / (f1 + ( #Z 2))) & Z c= ].( - 1), 1.[ & Z c= ( dom (( #Z 2) * arctan )) & Z = ( dom f) & (f | A) is continuous;

      then

       A2: Z c= ( dom ((1 / 2) (#) (( #Z 2) * arctan ))) by VALUED_1:def 5;

      

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

      

       A4: ((1 / 2) (#) (( #Z 2) * arctan )) is_differentiable_on Z by A1, A2, SIN_COS9: 93;

      Z c= (( dom arctan ) /\ (( dom (f1 + ( #Z 2))) \ ((f1 + ( #Z 2)) " { 0 }))) by A1, RFUNCT_1:def 1;

      then Z c= (( dom (f1 + ( #Z 2))) \ ((f1 + ( #Z 2)) " { 0 })) by XBOOLE_1: 18;

      then

       A5: Z c= ( dom ((f1 + ( #Z 2)) ^ )) by RFUNCT_1:def 2;

      ( dom ((f1 + ( #Z 2)) ^ )) c= ( dom (f1 + ( #Z 2))) by RFUNCT_1: 1;

      then

       A6: Z c= ( dom (f1 + ( #Z 2))) by A5;

      

       A7: for x st x in Z holds (f . x) = (( arctan . x) / (1 + (x ^2 )))

      proof

        let x;

        assume

         A8: x in Z;

        

        then (( arctan / (f1 + ( #Z 2))) . x) = (( arctan . x) / ((f1 + ( #Z 2)) . x)) by A1, RFUNCT_1:def 1

        .= (( arctan . x) / ((f1 . x) + (( #Z 2) . x))) by A6, A8, VALUED_1:def 1

        .= (( arctan . x) / ((f1 . x) + (x #Z 2))) by TAYLOR_1:def 1

        .= (( arctan . x) / (1 + (x #Z 2))) by A1, A8

        .= (( arctan . x) / (1 + (x ^2 ))) by FDIFF_7: 1;

        hence thesis by A1;

      end;

      

       A9: for x be Element of REAL st x in ( dom (((1 / 2) (#) (( #Z 2) * arctan )) `| Z)) holds ((((1 / 2) (#) (( #Z 2) * arctan )) `| Z) . x) = (f . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom (((1 / 2) (#) (( #Z 2) * arctan )) `| Z));

        then

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

        

        then ((((1 / 2) (#) (( #Z 2) * arctan )) `| Z) . x) = (( arctan . x) / (1 + (x ^2 ))) by A1, A2, SIN_COS9: 93

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

        hence thesis;

      end;

      ( dom (((1 / 2) (#) (( #Z 2) * arctan )) `| Z)) = ( dom f) by A1, A4, FDIFF_1:def 7;

      then (((1 / 2) (#) (( #Z 2) * arctan )) `| Z) = f by A9, PARTFUN1: 5;

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

    end;

    theorem :: INTEGR13:43

    A c= Z & (for x st x in Z holds (f1 . x) = 1) & f = ( - ( arccot / (f1 + ( #Z 2)))) & Z c= ].( - 1), 1.[ & Z c= ( dom (( #Z 2) * arccot )) & Z = ( dom f) & (f | A) is continuous implies ( integral (f,A)) = ((((1 / 2) (#) (( #Z 2) * arccot )) . ( upper_bound A)) - (((1 / 2) (#) (( #Z 2) * arccot )) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & (for x st x in Z holds (f1 . x) = 1) & f = ( - ( arccot / (f1 + ( #Z 2)))) & Z c= ].( - 1), 1.[ & Z c= ( dom (( #Z 2) * arccot )) & Z = ( dom f) & (f | A) is continuous;

      then

       A2: Z c= ( dom ((1 / 2) (#) (( #Z 2) * arccot ))) by VALUED_1:def 5;

      

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

      

       A4: ((1 / 2) (#) (( #Z 2) * arccot )) is_differentiable_on Z by A1, A2, SIN_COS9: 94;

      

       A5: Z = ( dom ( arccot / (f1 + ( #Z 2)))) by A1, VALUED_1: 8;

      then Z c= (( dom arccot ) /\ (( dom (f1 + ( #Z 2))) \ ((f1 + ( #Z 2)) " { 0 }))) by RFUNCT_1:def 1;

      then Z c= (( dom (f1 + ( #Z 2))) \ ((f1 + ( #Z 2)) " { 0 })) by XBOOLE_1: 18;

      then

       A6: Z c= ( dom ((f1 + ( #Z 2)) ^ )) by RFUNCT_1:def 2;

      ( dom ((f1 + ( #Z 2)) ^ )) c= ( dom (f1 + ( #Z 2))) by RFUNCT_1: 1;

      then

       A7: Z c= ( dom (f1 + ( #Z 2))) by A6;

      

       A8: for x st x in Z holds (f . x) = ( - (( arccot . x) / (1 + (x ^2 ))))

      proof

        let x;

        assume

         A9: x in Z;

        (( - ( arccot / (f1 + ( #Z 2)))) . x) = ( - (( arccot / (f1 + ( #Z 2))) . x)) by VALUED_1: 8

        .= ( - (( arccot . x) / ((f1 + ( #Z 2)) . x))) by A5, A9, RFUNCT_1:def 1

        .= ( - (( arccot . x) / ((f1 . x) + (( #Z 2) . x)))) by A7, A9, VALUED_1:def 1

        .= ( - (( arccot . x) / ((f1 . x) + (x #Z 2)))) by TAYLOR_1:def 1

        .= ( - (( arccot . x) / (1 + (x #Z 2)))) by A1, A9

        .= ( - (( arccot . x) / (1 + (x ^2 )))) by FDIFF_7: 1;

        hence thesis by A1;

      end;

      

       A10: for x be Element of REAL st x in ( dom (((1 / 2) (#) (( #Z 2) * arccot )) `| Z)) holds ((((1 / 2) (#) (( #Z 2) * arccot )) `| Z) . x) = (f . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom (((1 / 2) (#) (( #Z 2) * arccot )) `| Z));

        then

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

        

        then ((((1 / 2) (#) (( #Z 2) * arccot )) `| Z) . x) = ( - (( arccot . x) / (1 + (x ^2 )))) by A1, A2, SIN_COS9: 94

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

        hence thesis;

      end;

      ( dom (((1 / 2) (#) (( #Z 2) * arccot )) `| Z)) = ( dom f) by A1, A4, FDIFF_1:def 7;

      then (((1 / 2) (#) (( #Z 2) * arccot )) `| Z) = f by A10, PARTFUN1: 5;

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

    end;

    theorem :: INTEGR13:44

    

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

    proof

      assume

       A1: Z c= ( dom (( #Z 2) * arccot )) & Z c= ].( - 1), 1.[;

      then

       A2: Z c= ( dom ((1 / 2) (#) (( #Z 2) * arccot ))) by VALUED_1:def 5;

      then

       A3: Z c= ( dom ( - ((1 / 2) (#) (( #Z 2) * arccot )))) by VALUED_1: 8;

      

       A4: ((1 / 2) (#) (( #Z 2) * arccot )) is_differentiable_on Z by A2, A1, SIN_COS9: 94;

      then

       A5: (( - 1) (#) ((1 / 2) (#) (( #Z 2) * arccot ))) is_differentiable_on Z by A3, FDIFF_1: 20;

      

       A6: (( #Z 2) * arccot ) is_differentiable_on Z & for x st x in Z holds (((( #Z 2) * arccot ) `| Z) . x) = ( - ((2 * (( arccot . x) #Z (2 - 1))) / (1 + (x ^2 )))) by A1, SIN_COS9: 92;

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

      proof

        let x;

        assume

         A7: x in Z;

        then

         A8: ((1 / 2) (#) (( #Z 2) * arccot )) is_differentiable_in x by A4, FDIFF_1: 9;

        

         A9: (( #Z 2) * arccot ) is_differentiable_in x by A6, A7, FDIFF_1: 9;

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

        .= (( - 1) * ( diff (((1 / 2) (#) (( #Z 2) * arccot )),x))) by A8, FDIFF_1: 15

        .= (( - 1) * ((1 / 2) * ( diff ((( #Z 2) * arccot ),x)))) by A9, FDIFF_1: 15

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

        .= (( - 1) * ((1 / 2) * ( - ((2 * (( arccot . x) #Z (2 - 1))) / (1 + (x ^2 )))))) by A1, A7, SIN_COS9: 92

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

        .= (( - 1) * ( - ((1 / 2) * ((2 * ( arccot . x)) / (1 + (x ^2 )))))) by PREPOWER: 35

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

        hence thesis;

      end;

      hence thesis by A3, A4, FDIFF_1: 20;

    end;

    theorem :: INTEGR13:45

    A c= Z & (for x st x in Z holds (f1 . x) = 1) & f = ( arccot / (f1 + ( #Z 2))) & Z c= ].( - 1), 1.[ & Z c= ( dom (( #Z 2) * arccot )) & Z = ( dom f) & (f | A) is continuous implies ( integral (f,A)) = ((( - ((1 / 2) (#) (( #Z 2) * arccot ))) . ( upper_bound A)) - (( - ((1 / 2) (#) (( #Z 2) * arccot ))) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & (for x st x in Z holds (f1 . x) = 1) & f = ( arccot / (f1 + ( #Z 2))) & Z c= ].( - 1), 1.[ & Z c= ( dom (( #Z 2) * arccot )) & 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 / 2) (#) (( #Z 2) * arccot ))) is_differentiable_on Z by A1, Th44;

      Z c= (( dom arccot ) /\ (( dom (f1 + ( #Z 2))) \ ((f1 + ( #Z 2)) " { 0 }))) by A1, RFUNCT_1:def 1;

      then Z c= (( dom (f1 + ( #Z 2))) \ ((f1 + ( #Z 2)) " { 0 })) by XBOOLE_1: 18;

      then

       A4: Z c= ( dom ((f1 + ( #Z 2)) ^ )) by RFUNCT_1:def 2;

      ( dom ((f1 + ( #Z 2)) ^ )) c= ( dom (f1 + ( #Z 2))) by RFUNCT_1: 1;

      then

       A5: Z c= ( dom (f1 + ( #Z 2))) by A4;

      

       A6: for x st x in Z holds (f . x) = (( arccot . x) / (1 + (x ^2 )))

      proof

        let x;

        assume

         A7: x in Z;

        

        then (( arccot / (f1 + ( #Z 2))) . x) = (( arccot . x) / ((f1 + ( #Z 2)) . x)) by A1, RFUNCT_1:def 1

        .= (( arccot . x) / ((f1 . x) + (( #Z 2) . x))) by A5, A7, VALUED_1:def 1

        .= (( arccot . x) / ((f1 . x) + (x #Z 2))) by TAYLOR_1:def 1

        .= (( arccot . x) / (1 + (x #Z 2))) by A1, A7

        .= (( arccot . x) / (1 + (x ^2 ))) by FDIFF_7: 1;

        hence thesis by A1;

      end;

      

       A8: for x be Element of REAL st x in ( dom (( - ((1 / 2) (#) (( #Z 2) * arccot ))) `| Z)) holds ((( - ((1 / 2) (#) (( #Z 2) * arccot ))) `| Z) . x) = (f . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom (( - ((1 / 2) (#) (( #Z 2) * arccot ))) `| Z));

        then

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

        

        then ((( - ((1 / 2) (#) (( #Z 2) * arccot ))) `| Z) . x) = (( arccot . x) / (1 + (x ^2 ))) by A1, Th44

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

        hence thesis;

      end;

      ( dom (( - ((1 / 2) (#) (( #Z 2) * arccot ))) `| Z)) = ( dom f) by A1, A3, FDIFF_1:def 7;

      then (( - ((1 / 2) (#) (( #Z 2) * arccot ))) `| Z) = f by A8, PARTFUN1: 5;

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

    end;

    theorem :: INTEGR13:46

    A c= Z & (for x st x in Z holds (f1 . x) = 1) & f = ( arctan + (( id Z) / (f1 + ( #Z 2)))) & Z c= ].( - 1), 1.[ & Z = ( dom f) & (f | A) is continuous implies ( integral (f,A)) = (((( id Z) (#) arctan ) . ( upper_bound A)) - ((( id Z) (#) arctan ) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & (for x st x in Z holds (f1 . x) = 1) & f = ( arctan + (( id Z) / (f1 + ( #Z 2)))) & Z c= ].( - 1), 1.[ & 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 arctan ) /\ ( dom (( id Z) / (f1 + ( #Z 2))))) by A1, VALUED_1:def 1;

      then

       A3: Z c= ( dom arctan ) & Z c= ( dom (( id Z) / (f1 + ( #Z 2)))) by XBOOLE_1: 18;

      then Z c= (( dom ( id Z)) /\ (( dom (f1 + ( #Z 2))) \ ((f1 + ( #Z 2)) " { 0 }))) by RFUNCT_1:def 1;

      then

       A4: Z c= (( dom (f1 + ( #Z 2))) \ ((f1 + ( #Z 2)) " { 0 })) by XBOOLE_1: 18;

      

       A5: (( id Z) (#) arctan ) is_differentiable_on Z by A1, SIN_COS9: 95;

      

       A6: Z c= ( dom ((f1 + ( #Z 2)) ^ )) by A4, RFUNCT_1:def 2;

      ( dom ((f1 + ( #Z 2)) ^ )) c= ( dom (f1 + ( #Z 2))) by RFUNCT_1: 1;

      then

       A7: Z c= ( dom (f1 + ( #Z 2))) by A6;

      

       A8: for x st x in Z holds (f . x) = (( arctan . x) + (x / (1 + (x ^2 ))))

      proof

        let x;

        assume

         A9: x in Z;

        

        then (( arctan + (( id Z) / (f1 + ( #Z 2)))) . x) = (( arctan . x) + ((( id Z) / (f1 + ( #Z 2))) . x)) by A1, VALUED_1:def 1

        .= (( arctan . x) + ((( id Z) . x) / ((f1 + ( #Z 2)) . x))) by A3, A9, RFUNCT_1:def 1

        .= (( arctan . x) + (x / ((f1 + ( #Z 2)) . x))) by A9, FUNCT_1: 18

        .= (( arctan . x) + (x / ((f1 . x) + (( #Z 2) . x)))) by A7, A9, VALUED_1:def 1

        .= (( arctan . x) + (x / (1 + (( #Z 2) . x)))) by A1, A9

        .= (( arctan . x) + (x / (1 + (x #Z 2)))) by TAYLOR_1:def 1

        .= (( arctan . x) + (x / (1 + (x ^2 )))) by FDIFF_7: 1;

        hence thesis by A1;

      end;

      

       A10: for x be Element of REAL st x in ( dom ((( id Z) (#) arctan ) `| Z)) holds (((( id Z) (#) arctan ) `| Z) . x) = (f . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom ((( id Z) (#) arctan ) `| Z));

        then

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

        

        then (((( id Z) (#) arctan ) `| Z) . x) = (( arctan . x) + (x / (1 + (x ^2 )))) by A1, SIN_COS9: 95

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

        hence thesis;

      end;

      ( dom ((( id Z) (#) arctan ) `| Z)) = ( dom f) by A1, A5, FDIFF_1:def 7;

      then ((( id Z) (#) arctan ) `| Z) = f by A10, PARTFUN1: 5;

      hence thesis by A1, A2, INTEGRA5: 13, SIN_COS9: 95;

    end;

    theorem :: INTEGR13:47

    A c= Z & (for x st x in Z holds (f1 . x) = 1) & f = ( arccot - (( id Z) / (f1 + ( #Z 2)))) & Z c= ].( - 1), 1.[ & Z = ( dom f) & (f | A) is continuous implies ( integral (f,A)) = (((( id Z) (#) arccot ) . ( upper_bound A)) - ((( id Z) (#) arccot ) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & (for x st x in Z holds (f1 . x) = 1) & f = ( arccot - (( id Z) / (f1 + ( #Z 2)))) & Z c= ].( - 1), 1.[ & 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 arccot ) /\ ( dom (( id Z) / (f1 + ( #Z 2))))) by A1, VALUED_1: 12;

      then

       A3: Z c= ( dom arccot ) & Z c= ( dom (( id Z) / (f1 + ( #Z 2)))) by XBOOLE_1: 18;

      then Z c= (( dom ( id Z)) /\ (( dom (f1 + ( #Z 2))) \ ((f1 + ( #Z 2)) " { 0 }))) by RFUNCT_1:def 1;

      then

       A4: Z c= (( dom (f1 + ( #Z 2))) \ ((f1 + ( #Z 2)) " { 0 })) by XBOOLE_1: 18;

      

       A5: (( id Z) (#) arccot ) is_differentiable_on Z by A1, SIN_COS9: 96;

      

       A6: Z c= ( dom ((f1 + ( #Z 2)) ^ )) by A4, RFUNCT_1:def 2;

      ( dom ((f1 + ( #Z 2)) ^ )) c= ( dom (f1 + ( #Z 2))) by RFUNCT_1: 1;

      then

       A7: Z c= ( dom (f1 + ( #Z 2))) by A6;

      

       A8: for x st x in Z holds (f . x) = (( arccot . x) - (x / (1 + (x ^2 ))))

      proof

        let x;

        assume

         A9: x in Z;

        

        then (( arccot - (( id Z) / (f1 + ( #Z 2)))) . x) = (( arccot . x) - ((( id Z) / (f1 + ( #Z 2))) . x)) by A1, VALUED_1: 13

        .= (( arccot . x) - ((( id Z) . x) / ((f1 + ( #Z 2)) . x))) by A3, A9, RFUNCT_1:def 1

        .= (( arccot . x) - (x / ((f1 + ( #Z 2)) . x))) by A9, FUNCT_1: 18

        .= (( arccot . x) - (x / ((f1 . x) + (( #Z 2) . x)))) by A7, A9, VALUED_1:def 1

        .= (( arccot . x) - (x / (1 + (( #Z 2) . x)))) by A1, A9

        .= (( arccot . x) - (x / (1 + (x #Z 2)))) by TAYLOR_1:def 1

        .= (( arccot . x) - (x / (1 + (x ^2 )))) by FDIFF_7: 1;

        hence thesis by A1;

      end;

      

       A10: for x be Element of REAL st x in ( dom ((( id Z) (#) arccot ) `| Z)) holds (((( id Z) (#) arccot ) `| Z) . x) = (f . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom ((( id Z) (#) arccot ) `| Z));

        then

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

        

        then (((( id Z) (#) arccot ) `| Z) . x) = (( arccot . x) - (x / (1 + (x ^2 )))) by A1, SIN_COS9: 96

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

        hence thesis;

      end;

      ( dom ((( id Z) (#) arccot ) `| Z)) = ( dom f) by A1, A5, FDIFF_1:def 7;

      then ((( id Z) (#) arccot ) `| Z) = f by A10, PARTFUN1: 5;

      hence thesis by A1, A2, INTEGRA5: 13, SIN_COS9: 96;

    end;

    theorem :: INTEGR13:48

    A c= Z & Z c= ].( - 1), 1.[ & f = (( exp_R * arctan ) / (f1 + ( #Z 2))) & (for x st x in Z holds (f1 . x) = 1) & Z = ( dom f) & (f | A) is continuous implies ( integral (f,A)) = ((( exp_R * arctan ) . ( upper_bound A)) - (( exp_R * arctan ) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & Z c= ].( - 1), 1.[ & f = (( exp_R * arctan ) / (f1 + ( #Z 2))) & (for x st x in Z holds (f1 . x) = 1) & 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 * arctan )) /\ (( dom (f1 + ( #Z 2))) \ ((f1 + ( #Z 2)) " { 0 }))) by A1, RFUNCT_1:def 1;

      then

       A3: Z c= ( dom ( exp_R * arctan )) & Z c= (( dom (f1 + ( #Z 2))) \ ((f1 + ( #Z 2)) " { 0 })) by XBOOLE_1: 18;

      then

       A4: Z c= ( dom ((f1 + ( #Z 2)) ^ )) by RFUNCT_1:def 2;

      ( dom ((f1 + ( #Z 2)) ^ )) c= ( dom (f1 + ( #Z 2))) by RFUNCT_1: 1;

      then

       A5: Z c= ( dom (f1 + ( #Z 2))) by A4;

      

       A6: ( exp_R * arctan ) is_differentiable_on Z by A1, A3, SIN_COS9: 119;

      

       A7: for x st x in Z holds (f . x) = (( exp_R . ( arctan . x)) / (1 + (x ^2 )))

      proof

        let x;

        assume

         A8: x in Z;

        

        then ((( exp_R * arctan ) / (f1 + ( #Z 2))) . x) = ((( exp_R * arctan ) . x) / ((f1 + ( #Z 2)) . x)) by A1, RFUNCT_1:def 1

        .= (( exp_R . ( arctan . x)) / ((f1 + ( #Z 2)) . x)) by A3, A8, FUNCT_1: 12

        .= (( exp_R . ( arctan . x)) / ((f1 . x) + (( #Z 2) . x))) by A5, A8, VALUED_1:def 1

        .= (( exp_R . ( arctan . x)) / (1 + (( #Z 2) . x))) by A1, A8

        .= (( exp_R . ( arctan . x)) / (1 + (x #Z 2))) by TAYLOR_1:def 1

        .= (( exp_R . ( arctan . x)) / (1 + (x ^2 ))) by FDIFF_7: 1;

        hence thesis by A1;

      end;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

        then ((( exp_R * arctan ) `| Z) . x) = (( exp_R . ( arctan . x)) / (1 + (x ^2 ))) by A1, A3, SIN_COS9: 119

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

        hence thesis;

      end;

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

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

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

    end;

    theorem :: INTEGR13:49

    A c= Z & Z c= ].( - 1), 1.[ & f = ( - (( exp_R * arccot ) / (f1 + ( #Z 2)))) & (for x st x in Z holds (f1 . x) = 1) & Z = ( dom f) & (f | A) is continuous implies ( integral (f,A)) = ((( exp_R * arccot ) . ( upper_bound A)) - (( exp_R * arccot ) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & Z c= ].( - 1), 1.[ & f = ( - (( exp_R * arccot ) / (f1 + ( #Z 2)))) & (for x st x in Z holds (f1 . x) = 1) & 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 = ( dom (( exp_R * arccot ) / (f1 + ( #Z 2)))) by A1, VALUED_1: 8;

      then Z = (( dom ( exp_R * arccot )) /\ (( dom (f1 + ( #Z 2))) \ ((f1 + ( #Z 2)) " { 0 }))) by RFUNCT_1:def 1;

      then

       A4: Z c= ( dom ( exp_R * arccot )) & Z c= (( dom (f1 + ( #Z 2))) \ ((f1 + ( #Z 2)) " { 0 })) by XBOOLE_1: 18;

      then

       A5: Z c= ( dom ((f1 + ( #Z 2)) ^ )) by RFUNCT_1:def 2;

      ( dom ((f1 + ( #Z 2)) ^ )) c= ( dom (f1 + ( #Z 2))) by RFUNCT_1: 1;

      then

       A6: Z c= ( dom (f1 + ( #Z 2))) by A5;

      

       A7: ( exp_R * arccot ) is_differentiable_on Z by A1, A4, SIN_COS9: 120;

      

       A8: for x st x in Z holds (f . x) = ( - (( exp_R . ( arccot . x)) / (1 + (x ^2 ))))

      proof

        let x;

        assume

         A9: x in Z;

        (( - (( exp_R * arccot ) / (f1 + ( #Z 2)))) . x) = ( - ((( exp_R * arccot ) / (f1 + ( #Z 2))) . x)) by VALUED_1: 8

        .= ( - ((( exp_R * arccot ) . x) / ((f1 + ( #Z 2)) . x))) by A9, A3, RFUNCT_1:def 1

        .= ( - (( exp_R . ( arccot . x)) / ((f1 + ( #Z 2)) . x))) by A4, A9, FUNCT_1: 12

        .= ( - (( exp_R . ( arccot . x)) / ((f1 . x) + (( #Z 2) . x)))) by A6, A9, VALUED_1:def 1

        .= ( - (( exp_R . ( arccot . x)) / (1 + (( #Z 2) . x)))) by A1, A9

        .= ( - (( exp_R . ( arccot . x)) / (1 + (x #Z 2)))) by TAYLOR_1:def 1

        .= ( - (( exp_R . ( arccot . x)) / (1 + (x ^2 )))) by FDIFF_7: 1;

        hence thesis by A1;

      end;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

        then ((( exp_R * arccot ) `| Z) . x) = ( - (( exp_R . ( arccot . x)) / (1 + (x ^2 )))) by A1, A4, SIN_COS9: 120

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

        hence thesis;

      end;

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

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

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

    end;

    theorem :: INTEGR13:50

    

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

    proof

      assume

       A1: Z c= ( dom ( exp_R * arccot )) & Z c= ].( - 1), 1.[;

      then

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

      

       A3: ( exp_R * arccot ) is_differentiable_on Z by A1, SIN_COS9: 120;

      then

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

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

      proof

        let x;

        assume

         A5: x in Z;

        

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

        then

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

        

         A8: exp_R is_differentiable_in ( arccot . x) by SIN_COS: 65;

        

         A9: ( exp_R * arccot ) is_differentiable_in x by A3, A5, FDIFF_1: 9;

        ((( - ( exp_R * arccot )) `| Z) . x) = ( diff (( - ( exp_R * arccot )),x)) by A4, A5, FDIFF_1:def 7

        .= (( - 1) * ( diff (( exp_R * arccot ),x))) by A9, FDIFF_1: 15

        .= (( - 1) * (( diff ( exp_R ,( arccot . x))) * ( diff ( arccot ,x)))) by A7, A8, FDIFF_2: 13

        .= (( - 1) * (( diff ( exp_R ,( arccot . x))) * (( arccot `| Z) . x))) by A5, A6, FDIFF_1:def 7

        .= (( - 1) * (( diff ( exp_R ,( arccot . x))) * ( - (1 / (1 + (x ^2 )))))) by A5, A1, SIN_COS9: 82

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

        .= (( exp_R . ( arccot . x)) / (1 + (x ^2 ))) by SIN_COS: 65;

        hence thesis;

      end;

      hence thesis by A2, A3, FDIFF_1: 20;

    end;

    theorem :: INTEGR13:51

    A c= Z & Z c= ].( - 1), 1.[ & f = (( exp_R * arccot ) / (f1 + ( #Z 2))) & (for x st x in Z holds (f1 . x) = 1) & Z = ( dom f) & (f | A) is continuous implies ( integral (f,A)) = ((( - ( exp_R * arccot )) . ( upper_bound A)) - (( - ( exp_R * arccot )) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & Z c= ].( - 1), 1.[ & f = (( exp_R * arccot ) / (f1 + ( #Z 2))) & (for x st x in Z holds (f1 . x) = 1) & 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 * arccot )) /\ (( dom (f1 + ( #Z 2))) \ ((f1 + ( #Z 2)) " { 0 }))) by A1, RFUNCT_1:def 1;

      then

       A3: Z c= ( dom ( exp_R * arccot )) & Z c= (( dom (f1 + ( #Z 2))) \ ((f1 + ( #Z 2)) " { 0 })) by XBOOLE_1: 18;

      then

       A4: Z c= ( dom ((f1 + ( #Z 2)) ^ )) by RFUNCT_1:def 2;

      ( dom ((f1 + ( #Z 2)) ^ )) c= ( dom (f1 + ( #Z 2))) by RFUNCT_1: 1;

      then

       A5: Z c= ( dom (f1 + ( #Z 2))) by A4;

      

       A6: ( - ( exp_R * arccot )) is_differentiable_on Z by A1, A3, Th50;

      

       A7: for x st x in Z holds (f . x) = (( exp_R . ( arccot . x)) / (1 + (x ^2 )))

      proof

        let x;

        assume

         A8: x in Z;

        

        then ((( exp_R * arccot ) / (f1 + ( #Z 2))) . x) = ((( exp_R * arccot ) . x) / ((f1 + ( #Z 2)) . x)) by A1, RFUNCT_1:def 1

        .= (( exp_R . ( arccot . x)) / ((f1 + ( #Z 2)) . x)) by A3, A8, FUNCT_1: 12

        .= (( exp_R . ( arccot . x)) / ((f1 . x) + (( #Z 2) . x))) by A5, A8, VALUED_1:def 1

        .= (( exp_R . ( arccot . x)) / (1 + (( #Z 2) . x))) by A1, A8

        .= (( exp_R . ( arccot . x)) / (1 + (x #Z 2))) by TAYLOR_1:def 1

        .= (( exp_R . ( arccot . x)) / (1 + (x ^2 ))) by FDIFF_7: 1;

        hence thesis by A1;

      end;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

        then ((( - ( exp_R * arccot )) `| Z) . x) = (( exp_R . ( arccot . x)) / (1 + (x ^2 ))) by A1, A3, Th50

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

        hence thesis;

      end;

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

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

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

    end;

    theorem :: INTEGR13:52

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

    proof

      assume

       A1: A c= Z & Z c= ( dom ( ln * (f1 + f2))) & f = (( id Z) / (f1 + f2)) & f2 = ( #Z 2) & (for x st x in Z holds (f1 . x) = 1) & 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 ((1 / 2) (#) ( ln * (f1 + f2)))) by A1, VALUED_1:def 5;

      Z c= (( dom ( id Z)) /\ (( dom (f1 + f2)) \ ((f1 + f2) " { 0 }))) by A1, RFUNCT_1:def 1;

      then Z c= (( dom (f1 + f2)) \ ((f1 + f2) " { 0 })) by XBOOLE_1: 18;

      then

       A4: Z c= ( dom ((f1 + f2) ^ )) by RFUNCT_1:def 2;

      ( dom ((f1 + f2) ^ )) c= ( dom (f1 + f2)) by RFUNCT_1: 1;

      then

       A5: Z c= ( dom (f1 + f2)) by A4;

      

       A6: ((1 / 2) (#) ( ln * (f1 + f2))) is_differentiable_on Z by A1, A3, SIN_COS9: 102;

      

       A7: for x st x in Z holds (f . x) = (x / (1 + (x ^2 )))

      proof

        let x;

        assume

         A8: x in Z;

        

        then ((( id Z) / (f1 + f2)) . x) = ((( id Z) . x) / ((f1 + f2) . x)) by A1, RFUNCT_1:def 1

        .= (x / ((f1 + f2) . x)) by A8, FUNCT_1: 18

        .= (x / ((f1 . x) + (f2 . x))) by A5, A8, VALUED_1:def 1

        .= (x / (1 + (( #Z 2) . x))) by A1, A8

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

        .= (x / (1 + (x ^2 ))) by FDIFF_7: 1;

        hence thesis by A1;

      end;

      

       A9: for x be Element of REAL st x in ( dom (((1 / 2) (#) ( ln * (f1 + f2))) `| Z)) holds ((((1 / 2) (#) ( ln * (f1 + f2))) `| Z) . x) = (f . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom (((1 / 2) (#) ( ln * (f1 + f2))) `| Z));

        then

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

        

        then ((((1 / 2) (#) ( ln * (f1 + f2))) `| Z) . x) = (x / (1 + (x ^2 ))) by A1, A3, SIN_COS9: 102

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

        hence thesis;

      end;

      ( dom (((1 / 2) (#) ( ln * (f1 + f2))) `| Z)) = ( dom f) by A1, A6, FDIFF_1:def 7;

      then (((1 / 2) (#) ( ln * (f1 + f2))) `| Z) = f by A9, PARTFUN1: 5;

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

    end;

    theorem :: INTEGR13:53

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

    proof

      assume

       A1: A c= Z & Z c= ( dom ( ln * (f1 + f2))) & f = (( id Z) / (a (#) (f1 + f2))) & (for x st x in Z holds (h . x) = (x / a) & (f1 . x) = 1) & a <> 0 & f2 = (( #Z 2) * h) & 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 ((a / 2) (#) ( ln * (f1 + f2)))) by A1, VALUED_1:def 5;

      

       A4: for x st x in Z holds (f1 . x) = 1 by A1;

      

       A5: for x st x in Z holds (h . x) = (x / a) by A1;

      then

       A6: ((a / 2) (#) ( ln * (f1 + f2))) is_differentiable_on Z by A1, A3, A4, SIN_COS9: 108;

      

       A7: for x st x in Z holds (f . x) = (x / (a * (1 + ((x / a) ^2 ))))

      proof

        let x;

        assume

         A8: x in Z;

        then

         A9: x in ( dom (f1 + f2)) by A1, FUNCT_1: 11;

        ( dom (f1 + f2)) = (( dom f1) /\ ( dom f2)) by VALUED_1:def 1;

        then ( dom (f1 + f2)) c= ( dom f2) by XBOOLE_1: 18;

        then

         A10: x in ( dom f2) by A9;

        ((( id Z) / (a (#) (f1 + f2))) . x) = ((( id Z) . x) / ((a (#) (f1 + f2)) . x)) by A1, A8, RFUNCT_1:def 1

        .= (x / ((a (#) (f1 + f2)) . x)) by A8, FUNCT_1: 18

        .= (x / (a * ((f1 + f2) . x))) by VALUED_1: 6

        .= (x / (a * ((f1 . x) + (f2 . x)))) by A9, VALUED_1:def 1

        .= (x / (a * (1 + (f2 . x)))) by A4, A8

        .= (x / (a * (1 + (( #Z 2) . (h . x))))) by A1, A10, FUNCT_1: 12

        .= (x / (a * (1 + ((h . x) #Z 2)))) by TAYLOR_1:def 1

        .= (x / (a * (1 + ((h . x) ^2 )))) by FDIFF_7: 1

        .= (x / (a * (1 + ((x / a) ^2 )))) by A5, A8;

        hence thesis by A1;

      end;

      

       A11: for x be Element of REAL st x in ( dom (((a / 2) (#) ( ln * (f1 + f2))) `| Z)) holds ((((a / 2) (#) ( ln * (f1 + f2))) `| Z) . x) = (f . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom (((a / 2) (#) ( ln * (f1 + f2))) `| Z));

        then

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

        

        then ((((a / 2) (#) ( ln * (f1 + f2))) `| Z) . x) = (x / (a * (1 + ((x / a) ^2 )))) by A1, A3, A4, A5, SIN_COS9: 108

        .= (f . x) by A7, A12;

        hence thesis;

      end;

      ( dom (((a / 2) (#) ( ln * (f1 + f2))) `| Z)) = ( dom f) by A1, A6, FDIFF_1:def 7;

      then (((a / 2) (#) ( ln * (f1 + f2))) `| Z) = f by A11, PARTFUN1: 5;

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

    end;

    theorem :: INTEGR13:54

    

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

    proof

      set f = ( id Z);

      assume that

       A1: Z c= ( dom ((f ^ ) (#) arctan )) and

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

      

       A3: Z c= ( dom ( - ((f ^ ) (#) arctan ))) by A1, VALUED_1: 8;

      

       A4: for x st x in Z holds (f . x) = x by FUNCT_1: 18;

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

      then

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

      

       A6: not 0 in Z

      proof

        assume

         A7: 0 in Z;

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

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

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

        hence thesis by TARSKI:def 1;

      end;

      then

       A8: (f ^ ) is_differentiable_on Z & for x st x in Z holds (((f ^ ) `| Z) . x) = ( - (1 / (x ^2 ))) by FDIFF_5: 4;

      

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

      

       A10: ((f ^ ) (#) arctan ) is_differentiable_on Z by A1, A2, A6, SIN_COS9: 129;

      then

       A11: (( - 1) (#) ((f ^ ) (#) arctan )) is_differentiable_on Z by A3, FDIFF_1: 20;

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

      proof

        let x;

        assume

         A12: x in Z;

        then

         A13: ((f ^ ) (#) arctan ) is_differentiable_in x by A10, FDIFF_1: 9;

        

         A14: (f ^ ) is_differentiable_in x by A8, A12, FDIFF_1: 9;

        

         A15: arctan is_differentiable_in x by A9, A12, FDIFF_1: 9;

        ((( - ((f ^ ) (#) arctan )) `| Z) . x) = ( diff (( - ((f ^ ) (#) arctan )),x)) by A11, A12, FDIFF_1:def 7

        .= (( - 1) * ( diff (((f ^ ) (#) arctan ),x))) by A13, FDIFF_1: 15

        .= (( - 1) * ((( arctan . x) * ( diff ((f ^ ),x))) + (((f ^ ) . x) * ( diff ( arctan ,x))))) by A14, A15, FDIFF_1: 16

        .= (( - 1) * ((( arctan . x) * (((f ^ ) `| Z) . x)) + (((f ^ ) . x) * ( diff ( arctan ,x))))) by A8, A12, FDIFF_1:def 7

        .= (( - 1) * ((( arctan . x) * ( - (1 / (x ^2 )))) + (((f ^ ) . x) * ( diff ( arctan ,x))))) by A6, A12, FDIFF_5: 4

        .= (( - 1) * (( - (( arctan . x) * (1 / (x ^2 )))) + (((f ^ ) . x) * (( arctan `| Z) . x)))) by A9, A12, FDIFF_1:def 7

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

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

        .= (( - 1) * (( - (( arctan . x) / (x ^2 ))) + ((1 / x) * (1 / (1 + (x ^2 )))))) by A4, A12

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

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

        hence thesis;

      end;

      hence thesis by A3, A10, FDIFF_1: 20;

    end;

    theorem :: INTEGR13:55

    

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

    proof

      set f = ( id Z);

      assume that

       A1: Z c= ( dom ((f ^ ) (#) arccot )) and

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

      

       A3: Z c= ( dom ( - ((f ^ ) (#) arccot ))) by A1, VALUED_1: 8;

      

       A4: for x st x in Z holds (f . x) = x by FUNCT_1: 18;

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

      then

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

      

       A6: not 0 in Z

      proof

        assume

         A7: 0 in Z;

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

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

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

        hence thesis by TARSKI:def 1;

      end;

      then

       A8: (f ^ ) is_differentiable_on Z & for x st x in Z holds (((f ^ ) `| Z) . x) = ( - (1 / (x ^2 ))) by FDIFF_5: 4;

      

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

      

       A10: ((f ^ ) (#) arccot ) is_differentiable_on Z by A6, A1, A2, SIN_COS9: 130;

      then

       A11: (( - 1) (#) ((f ^ ) (#) arccot )) is_differentiable_on Z by A3, FDIFF_1: 20;

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

      proof

        let x;

        assume

         A12: x in Z;

        then

         A13: ((f ^ ) (#) arccot ) is_differentiable_in x by A10, FDIFF_1: 9;

        

         A14: (f ^ ) is_differentiable_in x by A8, A12, FDIFF_1: 9;

        

         A15: arccot is_differentiable_in x by A9, A12, FDIFF_1: 9;

        ((( - ((f ^ ) (#) arccot )) `| Z) . x) = ( diff (( - ((f ^ ) (#) arccot )),x)) by A11, A12, FDIFF_1:def 7

        .= (( - 1) * ( diff (((f ^ ) (#) arccot ),x))) by A13, FDIFF_1: 15

        .= (( - 1) * ((( arccot . x) * ( diff ((f ^ ),x))) + (((f ^ ) . x) * ( diff ( arccot ,x))))) by A14, A15, FDIFF_1: 16

        .= (( - 1) * ((( arccot . x) * (((f ^ ) `| Z) . x)) + (((f ^ ) . x) * ( diff ( arccot ,x))))) by A8, A12, FDIFF_1:def 7

        .= (( - 1) * ((( arccot . x) * ( - (1 / (x ^2 )))) + (((f ^ ) . x) * ( diff ( arccot ,x))))) by A12, A6, FDIFF_5: 4

        .= (( - 1) * (( - (( arccot . x) * (1 / (x ^2 )))) + (((f ^ ) . x) * (( arccot `| Z) . x)))) by A9, A12, FDIFF_1:def 7

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

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

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

        .= (( - 1) * (( - (( arccot . x) / (x ^2 ))) - ((1 / x) * (1 / (1 + (x ^2 )))))) by A4, A12

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

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

        hence thesis;

      end;

      hence thesis by A11;

    end;

    theorem :: INTEGR13:56

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

    proof

      assume

       A1: A c= Z & (for x st x in Z holds (f1 . x) = 1) & f = (( arctan / ( #Z 2)) - ((( id Z) (#) (f1 + ( #Z 2))) ^ )) & Z c= ( dom ((( id Z) ^ ) (#) arctan )) & Z c= ].( - 1), 1.[ & 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) ^ ) (#) arctan )) is_differentiable_on Z by A1, Th54;

      

       A4: Z = (( dom ( arctan / ( #Z 2))) /\ ( dom ((( id Z) (#) (f1 + ( #Z 2))) ^ ))) by A1, VALUED_1: 12;

      then

       A5: Z c= ( dom ( arctan / ( #Z 2))) by XBOOLE_1: 18;

      

       A6: Z c= ( dom ((( id Z) (#) (f1 + ( #Z 2))) ^ )) by A4, XBOOLE_1: 18;

      ( dom ((( id Z) (#) (f1 + ( #Z 2))) ^ )) c= ( dom (( id Z) (#) (f1 + ( #Z 2)))) by RFUNCT_1: 1;

      then Z c= ( dom (( id Z) (#) (f1 + ( #Z 2)))) by A6;

      then Z c= (( dom ( id Z)) /\ ( dom (f1 + ( #Z 2)))) by VALUED_1:def 4;

      then

       A7: Z c= ( dom (f1 + ( #Z 2))) by XBOOLE_1: 18;

      

       A8: for x st x in Z holds (f . x) = ((( arctan . x) / (x ^2 )) - (1 / (x * (1 + (x ^2 )))))

      proof

        let x;

        assume

         A9: x in Z;

        then

         A10: x in ( dom ((( id Z) (#) (f1 + ( #Z 2))) ^ )) by A6;

        ((( arctan / ( #Z 2)) - ((( id Z) (#) (f1 + ( #Z 2))) ^ )) . x) = ((( arctan / ( #Z 2)) . x) - (((( id Z) (#) (f1 + ( #Z 2))) ^ ) . x)) by A1, A9, VALUED_1: 13

        .= ((( arctan / ( #Z 2)) . x) - (1 / ((( id Z) (#) (f1 + ( #Z 2))) . x))) by A10, RFUNCT_1:def 2

        .= ((( arctan / ( #Z 2)) . x) - (1 / ((( id Z) . x) * ((f1 + ( #Z 2)) . x)))) by VALUED_1: 5

        .= ((( arctan / ( #Z 2)) . x) - (1 / ((( id Z) . x) * ((f1 . x) + (( #Z 2) . x))))) by A7, A9, VALUED_1:def 1

        .= ((( arctan / ( #Z 2)) . x) - (1 / (x * ((f1 . x) + (( #Z 2) . x))))) by A9, FUNCT_1: 18

        .= ((( arctan / ( #Z 2)) . x) - (1 / (x * (1 + (( #Z 2) . x))))) by A1, A9

        .= ((( arctan . x) / (( #Z 2) . x)) - (1 / (x * (1 + (( #Z 2) . x))))) by A9, A5, RFUNCT_1:def 1

        .= ((( arctan . x) / (x #Z 2)) - (1 / (x * (1 + (( #Z 2) . x))))) by TAYLOR_1:def 1

        .= ((( arctan . x) / (x #Z 2)) - (1 / (x * (1 + (x #Z 2))))) by TAYLOR_1:def 1

        .= ((( arctan . x) / (x ^2 )) - (1 / (x * (1 + (x #Z 2))))) by FDIFF_7: 1

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

        hence thesis by A1;

      end;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

        then ((( - ((( id Z) ^ ) (#) arctan )) `| Z) . x) = ((( arctan . x) / (x ^2 )) - (1 / (x * (1 + (x ^2 ))))) by A1, Th54

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

        hence thesis;

      end;

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

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

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

    end;

    theorem :: INTEGR13:57

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

    proof

      assume

       A1: A c= Z & (for x st x in Z holds (f1 . x) = 1) & f = (( arccot / ( #Z 2)) + ((( id Z) (#) (f1 + ( #Z 2))) ^ )) & Z c= ( dom ((( id Z) ^ ) (#) arccot )) & Z c= ].( - 1), 1.[ & 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) ^ ) (#) arccot )) is_differentiable_on Z by A1, Th55;

      

       A4: Z = (( dom ( arccot / ( #Z 2))) /\ ( dom ((( id Z) (#) (f1 + ( #Z 2))) ^ ))) by A1, VALUED_1:def 1;

      then

       A5: Z c= ( dom ( arccot / ( #Z 2))) by XBOOLE_1: 18;

      

       A6: Z c= ( dom ((( id Z) (#) (f1 + ( #Z 2))) ^ )) by A4, XBOOLE_1: 18;

      ( dom ((( id Z) (#) (f1 + ( #Z 2))) ^ )) c= ( dom (( id Z) (#) (f1 + ( #Z 2)))) by RFUNCT_1: 1;

      then Z c= ( dom (( id Z) (#) (f1 + ( #Z 2)))) by A6;

      then Z c= (( dom ( id Z)) /\ ( dom (f1 + ( #Z 2)))) by VALUED_1:def 4;

      then

       A7: Z c= ( dom (f1 + ( #Z 2))) by XBOOLE_1: 18;

      

       A8: for x st x in Z holds (f . x) = ((( arccot . x) / (x ^2 )) + (1 / (x * (1 + (x ^2 )))))

      proof

        let x;

        assume

         A9: x in Z;

        then

         A10: x in ( dom ((( id Z) (#) (f1 + ( #Z 2))) ^ )) by A6;

        ((( arccot / ( #Z 2)) + ((( id Z) (#) (f1 + ( #Z 2))) ^ )) . x) = ((( arccot / ( #Z 2)) . x) + (((( id Z) (#) (f1 + ( #Z 2))) ^ ) . x)) by A1, A9, VALUED_1:def 1

        .= ((( arccot / ( #Z 2)) . x) + (1 / ((( id Z) (#) (f1 + ( #Z 2))) . x))) by A10, RFUNCT_1:def 2

        .= ((( arccot / ( #Z 2)) . x) + (1 / ((( id Z) . x) * ((f1 + ( #Z 2)) . x)))) by VALUED_1: 5

        .= ((( arccot / ( #Z 2)) . x) + (1 / ((( id Z) . x) * ((f1 . x) + (( #Z 2) . x))))) by A7, A9, VALUED_1:def 1

        .= ((( arccot / ( #Z 2)) . x) + (1 / (x * ((f1 . x) + (( #Z 2) . x))))) by A9, FUNCT_1: 18

        .= ((( arccot / ( #Z 2)) . x) + (1 / (x * (1 + (( #Z 2) . x))))) by A1, A9

        .= ((( arccot . x) / (( #Z 2) . x)) + (1 / (x * (1 + (( #Z 2) . x))))) by A9, A5, RFUNCT_1:def 1

        .= ((( arccot . x) / (x #Z 2)) + (1 / (x * (1 + (( #Z 2) . x))))) by TAYLOR_1:def 1

        .= ((( arccot . x) / (x #Z 2)) + (1 / (x * (1 + (x #Z 2))))) by TAYLOR_1:def 1

        .= ((( arccot . x) / (x ^2 )) + (1 / (x * (1 + (x #Z 2))))) by FDIFF_7: 1

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

        hence thesis by A1;

      end;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

        then ((( - ((( id Z) ^ ) (#) arccot )) `| Z) . x) = ((( arccot . x) / (x ^2 )) + (1 / (x * (1 + (x ^2 ))))) by A1, Th55

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

        hence thesis;

      end;

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

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

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

    end;