integr11.miz



    begin

    reserve r,x,x0,a,b for Real;

    reserve n,m for Element of NAT ;

    reserve A for non empty closed_interval Subset of REAL ;

    reserve Z for open Subset of REAL ;

    

     Lm1: ( [#] REAL ) = ( dom ( AffineMap ((1 / 2), 0 ))) by FUNCT_2:def 1;

    

     Lm2: ( [#] REAL ) = ( dom ( sin * ( AffineMap (2, 0 )))) by FUNCT_2:def 1;

    

     Lm3: ( dom ((1 / 4) (#) ( sin * ( AffineMap (2, 0 ))))) = ( [#] REAL ) by FUNCT_2:def 1;

    theorem :: INTEGR11:1

    

     Th1: (( AffineMap ((1 / 2), 0 )) - ((1 / 4) (#) ( sin * ( AffineMap (2, 0 ))))) is_differentiable_on REAL & for x holds (((( AffineMap ((1 / 2), 0 )) - ((1 / 4) (#) ( sin * ( AffineMap (2, 0 ))))) `| REAL ) . x) = (( sin . x) ^2 )

    proof

      

       A1: for x st x in REAL holds (( AffineMap (2, 0 )) . x) = ((2 * x) + 0 ) by FCONT_1:def 4;

      then

       A2: ( sin * ( AffineMap (2, 0 ))) is_differentiable_on REAL by Lm2, FDIFF_4: 37;

      then

       A3: ((1 / 4) (#) ( sin * ( AffineMap (2, 0 )))) is_differentiable_on REAL by Lm3, FDIFF_1: 20;

      

       A4: ( dom (( AffineMap ((1 / 2), 0 )) - ((1 / 4) (#) ( sin * ( AffineMap (2, 0 )))))) = ( [#] REAL ) by FUNCT_2:def 1;

      

       A5: for x st x in REAL holds (( AffineMap ((1 / 2), 0 )) . x) = (((1 / 2) * x) + 0 ) by FCONT_1:def 4;

      then

       A6: ( AffineMap ((1 / 2), 0 )) is_differentiable_on REAL by Lm1, FDIFF_1: 23;

      hence (( AffineMap ((1 / 2), 0 )) - ((1 / 4) (#) ( sin * ( AffineMap (2, 0 ))))) is_differentiable_on REAL by A4, A3, FDIFF_1: 19;

      

       A7: for x st x in REAL holds ((((1 / 4) (#) ( sin * ( AffineMap (2, 0 )))) `| REAL ) . x) = ((1 / 2) * ( cos (2 * x)))

      proof

        let x;

        assume

         A8: x in REAL ;

        ((((1 / 4) (#) ( sin * ( AffineMap (2, 0 )))) `| REAL ) . x) = ((1 / 4) * ( diff (( sin * ( AffineMap (2, 0 ))),x))) by A2, Lm3, FDIFF_1: 20, A8

        .= ((1 / 4) * ((( sin * ( AffineMap (2, 0 ))) `| REAL ) . x)) by A2, FDIFF_1:def 7, A8

        .= ((1 / 4) * (2 * ( cos . ((2 * x) + 0 )))) by A1, Lm2, FDIFF_4: 37, A8

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

        hence thesis;

      end;

      

       A9: for x st x in REAL holds (((( AffineMap ((1 / 2), 0 )) - ((1 / 4) (#) ( sin * ( AffineMap (2, 0 ))))) `| REAL ) . x) = (( sin . x) ^2 )

      proof

        let x;

        assume

         A10: x in REAL ;

        (((( AffineMap ((1 / 2), 0 )) - ((1 / 4) (#) ( sin * ( AffineMap (2, 0 ))))) `| REAL ) . x) = (( diff (( AffineMap ((1 / 2), 0 )),x)) - ( diff (((1 / 4) (#) ( sin * ( AffineMap (2, 0 )))),x))) by A4, A6, A3, FDIFF_1: 19, A10

        .= (((( AffineMap ((1 / 2), 0 )) `| REAL ) . x) - ( diff (((1 / 4) (#) ( sin * ( AffineMap (2, 0 )))),x))) by A6, FDIFF_1:def 7, A10

        .= ((1 / 2) - ( diff (((1 / 4) (#) ( sin * ( AffineMap (2, 0 )))),x))) by A5, Lm1, FDIFF_1: 23, A10

        .= ((1 / 2) - ((((1 / 4) (#) ( sin * ( AffineMap (2, 0 )))) `| REAL ) . x)) by A3, FDIFF_1:def 7, A10

        .= ((1 / 2) - ((1 / 2) * ( cos (2 * x)))) by A7, A10

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

        .= (( sin x) ^2 ) by SIN_COS5: 20;

        hence thesis;

      end;

      let x;

      x in REAL by XREAL_0:def 1;

      hence thesis by A9;

    end;

    theorem :: INTEGR11:2

    

     Th2: (( AffineMap ((1 / 2), 0 )) + ((1 / 4) (#) ( sin * ( AffineMap (2, 0 ))))) is_differentiable_on REAL & for x holds (((( AffineMap ((1 / 2), 0 )) + ((1 / 4) (#) ( sin * ( AffineMap (2, 0 ))))) `| REAL ) . x) = (( cos . x) ^2 )

    proof

      

       A1: for x st x in REAL holds (( AffineMap (2, 0 )) . x) = ((2 * x) + 0 ) by FCONT_1:def 4;

      then

       A2: ( sin * ( AffineMap (2, 0 ))) is_differentiable_on REAL by Lm2, FDIFF_4: 37;

      then

       A3: ((1 / 4) (#) ( sin * ( AffineMap (2, 0 )))) is_differentiable_on REAL by Lm3, FDIFF_1: 20;

      

       A4: ( dom (( AffineMap ((1 / 2), 0 )) + ((1 / 4) (#) ( sin * ( AffineMap (2, 0 )))))) = ( [#] REAL ) by FUNCT_2:def 1;

      

       A5: for x st x in REAL holds (( AffineMap ((1 / 2), 0 )) . x) = (((1 / 2) * x) + 0 ) by FCONT_1:def 4;

      then

       A6: ( AffineMap ((1 / 2), 0 )) is_differentiable_on REAL by Lm1, FDIFF_1: 23;

      hence (( AffineMap ((1 / 2), 0 )) + ((1 / 4) (#) ( sin * ( AffineMap (2, 0 ))))) is_differentiable_on REAL by A4, A3, FDIFF_1: 18;

      

       A7: for x st x in REAL holds ((((1 / 4) (#) ( sin * ( AffineMap (2, 0 )))) `| REAL ) . x) = ((1 / 2) * ( cos (2 * x)))

      proof

        let x;

        assume

         A8: x in REAL ;

        ((((1 / 4) (#) ( sin * ( AffineMap (2, 0 )))) `| REAL ) . x) = ((1 / 4) * ( diff (( sin * ( AffineMap (2, 0 ))),x))) by A2, Lm3, FDIFF_1: 20, A8

        .= ((1 / 4) * ((( sin * ( AffineMap (2, 0 ))) `| REAL ) . x)) by A2, FDIFF_1:def 7, A8

        .= ((1 / 4) * (2 * ( cos . ((2 * x) + 0 )))) by A1, Lm2, FDIFF_4: 37, A8

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

        hence thesis;

      end;

      

       A9: for x st x in REAL holds (((( AffineMap ((1 / 2), 0 )) + ((1 / 4) (#) ( sin * ( AffineMap (2, 0 ))))) `| REAL ) . x) = (( cos . x) ^2 )

      proof

        let x;

        assume

         A10: x in REAL ;

        (((( AffineMap ((1 / 2), 0 )) + ((1 / 4) (#) ( sin * ( AffineMap (2, 0 ))))) `| REAL ) . x) = (( diff (( AffineMap ((1 / 2), 0 )),x)) + ( diff (((1 / 4) (#) ( sin * ( AffineMap (2, 0 )))),x))) by A4, A6, A3, FDIFF_1: 18, A10

        .= (((( AffineMap ((1 / 2), 0 )) `| REAL ) . x) + ( diff (((1 / 4) (#) ( sin * ( AffineMap (2, 0 )))),x))) by A6, FDIFF_1:def 7, A10

        .= ((1 / 2) + ( diff (((1 / 4) (#) ( sin * ( AffineMap (2, 0 )))),x))) by A5, Lm1, FDIFF_1: 23, A10

        .= ((1 / 2) + ((((1 / 4) (#) ( sin * ( AffineMap (2, 0 )))) `| REAL ) . x)) by A3, FDIFF_1:def 7, A10

        .= ((1 / 2) + ((1 / 2) * ( cos (2 * x)))) by A7, A10

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

        .= (( cos x) ^2 ) by SIN_COS5: 21;

        hence thesis;

      end;

      let x;

      x in REAL by XREAL_0:def 1;

      hence thesis by A9;

    end;

    theorem :: INTEGR11:3

    

     Th3: ((1 / (n + 1)) (#) (( #Z (n + 1)) * sin )) is_differentiable_on REAL & for x holds ((((1 / (n + 1)) (#) (( #Z (n + 1)) * sin )) `| REAL ) . x) = ((( sin . x) #Z n) * ( cos . x))

    proof

      

       A1: ( [#] REAL ) = ( dom ((1 / (n + 1)) (#) (( #Z (n + 1)) * sin ))) by FUNCT_2:def 1;

      (( #Z (n + 1)) * sin ) is_differentiable_in x0

      proof

         sin is_differentiable_in x0 by SIN_COS: 64;

        hence thesis by TAYLOR_1: 3;

      end;

      then ( [#] REAL ) = ( dom (( #Z (n + 1)) * sin )) & for x0 st x0 in REAL holds (( #Z (n + 1)) * sin ) is_differentiable_in x0 by FUNCT_2:def 1;

      then

       A2: (( #Z (n + 1)) * sin ) is_differentiable_on REAL by FDIFF_1: 9;

      hence ((1 / (n + 1)) (#) (( #Z (n + 1)) * sin )) is_differentiable_on REAL by A1, FDIFF_1: 20;

      

       A3: for x st x in REAL holds (((( #Z (n + 1)) * sin ) `| REAL ) . x) = (((n + 1) * (( sin . x) #Z n)) * ( cos . x))

      proof

        set m = (n + 1);

        let x;

        assume

         A4: x in REAL ;

         sin is_differentiable_in x by SIN_COS: 64;

        

        then ( diff ((( #Z m) * sin ),x)) = ((m * (( sin . x) #Z (m - 1))) * ( diff ( sin ,x))) by TAYLOR_1: 3

        .= ((m * (( sin . x) #Z (m - 1))) * ( cos . x)) by SIN_COS: 64;

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

      end;

      

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

      proof

        let x;

        assume

         A6: x in REAL ;

        ((((1 / (n + 1)) (#) (( #Z (n + 1)) * sin )) `| REAL ) . x) = ((1 / (n + 1)) * ( diff ((( #Z (n + 1)) * sin ),x))) by A1, A2, FDIFF_1: 20, A6

        .= ((1 / (n + 1)) * (((( #Z (n + 1)) * sin ) `| REAL ) . x)) by A2, FDIFF_1:def 7, A6

        .= ((1 / (n + 1)) * (((n + 1) * (( sin . x) #Z n)) * ( cos . x))) by A3, A6

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

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

        .= ((1 * (( sin . x) #Z n)) * ( cos . x)) by XCMPLX_1: 60;

        hence thesis;

      end;

      let x;

      x in REAL by XREAL_0:def 1;

      hence thesis by A5;

    end;

    theorem :: INTEGR11:4

    

     Th4: (( - (1 / (n + 1))) (#) (( #Z (n + 1)) * cos )) is_differentiable_on REAL & for x holds (((( - (1 / (n + 1))) (#) (( #Z (n + 1)) * cos )) `| REAL ) . x) = ((( cos . x) #Z n) * ( sin . x))

    proof

      

       A1: ( [#] REAL ) = ( dom (( - (1 / (n + 1))) (#) (( #Z (n + 1)) * cos ))) by FUNCT_2:def 1;

      (( #Z (n + 1)) * cos ) is_differentiable_in x0

      proof

         cos is_differentiable_in x0 by SIN_COS: 63;

        hence thesis by TAYLOR_1: 3;

      end;

      then

       A2: for x0 st x0 in REAL holds (( #Z (n + 1)) * cos ) is_differentiable_in x0;

      ( [#] REAL ) = ( dom ( #Z (n + 1))) & REAL = ( dom (( #Z (n + 1)) * cos )) by FUNCT_2:def 1;

      then

       A3: (( #Z (n + 1)) * cos ) is_differentiable_on REAL by A2, FDIFF_1: 9;

      hence (( - (1 / (n + 1))) (#) (( #Z (n + 1)) * cos )) is_differentiable_on REAL by A1, FDIFF_1: 20;

      

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

      proof

        set m = (n + 1);

        let x;

        assume

         A5: x in REAL ;

         cos is_differentiable_in x by SIN_COS: 63;

        

        then ( diff ((( #Z m) * cos ),x)) = ((m * (( cos . x) #Z (m - 1))) * ( diff ( cos ,x))) by TAYLOR_1: 3

        .= ((m * (( cos . x) #Z (m - 1))) * ( - ( sin . x))) by SIN_COS: 63

        .= ((( - m) * (( cos . x) #Z (m - 1))) * ( sin . x));

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

      end;

      

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

      proof

        let x;

        assume

         A7: x in REAL ;

        (((( - (1 / (n + 1))) (#) (( #Z (n + 1)) * cos )) `| REAL ) . x) = (( - (1 / (n + 1))) * ( diff ((( #Z (n + 1)) * cos ),x))) by A1, A3, FDIFF_1: 20, A7

        .= (( - (1 / (n + 1))) * (((( #Z (n + 1)) * cos ) `| REAL ) . x)) by A3, FDIFF_1:def 7, A7

        .= (( - (1 / (n + 1))) * ((( - (n + 1)) * (( cos . x) #Z n)) * ( sin . x))) by A4, A7

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

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

        .= ((1 * (( cos . x) #Z n)) * ( sin . x)) by XCMPLX_1: 60;

        hence thesis;

      end;

      let x;

      x in REAL by XREAL_0:def 1;

      hence thesis by A6;

    end;

    theorem :: INTEGR11:5

    

     Th5: (m + n) <> 0 & (m - n) <> 0 implies (((1 / (2 * (m + n))) (#) ( sin * ( AffineMap ((m + n), 0 )))) + ((1 / (2 * (m - n))) (#) ( sin * ( AffineMap ((m - n), 0 ))))) is_differentiable_on REAL & for x holds (((((1 / (2 * (m + n))) (#) ( sin * ( AffineMap ((m + n), 0 )))) + ((1 / (2 * (m - n))) (#) ( sin * ( AffineMap ((m - n), 0 ))))) `| REAL ) . x) = (( cos . (m * x)) * ( cos . (n * x)))

    proof

      assume that

       A1: (m + n) <> 0 and

       A2: (m - n) <> 0 ;

      

       A3: ( dom ( sin * ( AffineMap ((m - n), 0 )))) = ( [#] REAL ) & for x st x in REAL holds (( AffineMap ((m - n), 0 )) . x) = (((m - n) * x) + 0 ) by FCONT_1:def 4, FUNCT_2:def 1;

      then

       A4: ( sin * ( AffineMap ((m - n), 0 ))) is_differentiable_on REAL by FDIFF_4: 37;

      

       A5: ( dom ((1 / (2 * (m - n))) (#) ( sin * ( AffineMap ((m - n), 0 ))))) = ( [#] REAL ) by FUNCT_2:def 1;

      then

       A6: ((1 / (2 * (m - n))) (#) ( sin * ( AffineMap ((m - n), 0 )))) is_differentiable_on REAL by A4, FDIFF_1: 20;

      

       A7: for x st x in REAL holds ((((1 / (2 * (m - n))) (#) ( sin * ( AffineMap ((m - n), 0 )))) `| REAL ) . x) = ((1 / 2) * ( cos ((m - n) * x)))

      proof

        let x;

        assume

         A8: x in REAL ;

        ((((1 / (2 * (m - n))) (#) ( sin * ( AffineMap ((m - n), 0 )))) `| REAL ) . x) = ((1 / (2 * (m - n))) * ( diff (( sin * ( AffineMap ((m - n), 0 ))),x))) by A5, A4, FDIFF_1: 20, A8

        .= ((1 / (2 * (m - n))) * ((( sin * ( AffineMap ((m - n), 0 ))) `| REAL ) . x)) by A4, FDIFF_1:def 7, A8

        .= ((1 / (2 * (m - n))) * ((m - n) * ( cos . (((m - n) * x) + 0 )))) by A3, FDIFF_4: 37, A8

        .= (((m - n) * (1 / (2 * (m - n)))) * ( cos . (((m - n) * x) + 0 )))

        .= (((1 * (m - n)) / (2 * (m - n))) * ( cos . (((m - n) * x) + 0 ))) by XCMPLX_1: 74

        .= ((1 / 2) * ( cos ((m - n) * x))) by A2, XCMPLX_1: 91;

        hence thesis;

      end;

      

       A9: ( dom (((1 / (2 * (m + n))) (#) ( sin * ( AffineMap ((m + n), 0 )))) + ((1 / (2 * (m - n))) (#) ( sin * ( AffineMap ((m - n), 0 )))))) = ( [#] REAL ) by FUNCT_2:def 1;

      

       A10: ( dom ( sin * ( AffineMap ((m + n), 0 )))) = ( [#] REAL ) & for x st x in REAL holds (( AffineMap ((m + n), 0 )) . x) = (((m + n) * x) + 0 ) by FCONT_1:def 4, FUNCT_2:def 1;

      then

       A11: ( sin * ( AffineMap ((m + n), 0 ))) is_differentiable_on REAL by FDIFF_4: 37;

      

       A12: ( [#] REAL ) = ( dom ((1 / (2 * (m + n))) (#) ( sin * ( AffineMap ((m + n), 0 ))))) by FUNCT_2:def 1;

      then

       A13: ((1 / (2 * (m + n))) (#) ( sin * ( AffineMap ((m + n), 0 )))) is_differentiable_on REAL by A11, FDIFF_1: 20;

      hence (((1 / (2 * (m + n))) (#) ( sin * ( AffineMap ((m + n), 0 )))) + ((1 / (2 * (m - n))) (#) ( sin * ( AffineMap ((m - n), 0 ))))) is_differentiable_on REAL by A9, A6, FDIFF_1: 18;

      

       A14: for x st x in REAL holds ((((1 / (2 * (m + n))) (#) ( sin * ( AffineMap ((m + n), 0 )))) `| REAL ) . x) = ((1 / 2) * ( cos ((m + n) * x)))

      proof

        let x;

        assume

         A15: x in REAL ;

        ((((1 / (2 * (m + n))) (#) ( sin * ( AffineMap ((m + n), 0 )))) `| REAL ) . x) = ((1 / (2 * (m + n))) * ( diff (( sin * ( AffineMap ((m + n), 0 ))),x))) by A12, A11, FDIFF_1: 20, A15

        .= ((1 / (2 * (m + n))) * ((( sin * ( AffineMap ((m + n), 0 ))) `| REAL ) . x)) by A11, FDIFF_1:def 7, A15

        .= ((1 / (2 * (m + n))) * ((m + n) * ( cos . (((m + n) * x) + 0 )))) by A10, FDIFF_4: 37, A15

        .= (((m + n) * (1 / (2 * (m + n)))) * ( cos . (((m + n) * x) + 0 )))

        .= (((1 * (m + n)) / (2 * (m + n))) * ( cos . (((m + n) * x) + 0 ))) by XCMPLX_1: 74

        .= ((1 / 2) * ( cos ((m + n) * x))) by A1, XCMPLX_1: 91;

        hence thesis;

      end;

      

       A16: for x st x in REAL holds (((((1 / (2 * (m + n))) (#) ( sin * ( AffineMap ((m + n), 0 )))) + ((1 / (2 * (m - n))) (#) ( sin * ( AffineMap ((m - n), 0 ))))) `| REAL ) . x) = (( cos . (m * x)) * ( cos . (n * x)))

      proof

        let x;

        assume

         A17: x in REAL ;

        (((((1 / (2 * (m + n))) (#) ( sin * ( AffineMap ((m + n), 0 )))) + ((1 / (2 * (m - n))) (#) ( sin * ( AffineMap ((m - n), 0 ))))) `| REAL ) . x) = (( diff (((1 / (2 * (m + n))) (#) ( sin * ( AffineMap ((m + n), 0 )))),x)) + ( diff (((1 / (2 * (m - n))) (#) ( sin * ( AffineMap ((m - n), 0 )))),x))) by A9, A13, A6, FDIFF_1: 18, A17

        .= (((((1 / (2 * (m + n))) (#) ( sin * ( AffineMap ((m + n), 0 )))) `| REAL ) . x) + ( diff (((1 / (2 * (m - n))) (#) ( sin * ( AffineMap ((m - n), 0 )))),x))) by A13, FDIFF_1:def 7, A17

        .= (((((1 / (2 * (m + n))) (#) ( sin * ( AffineMap ((m + n), 0 )))) `| REAL ) . x) + ((((1 / (2 * (m - n))) (#) ( sin * ( AffineMap ((m - n), 0 )))) `| REAL ) . x)) by A6, FDIFF_1:def 7, A17

        .= (((1 / 2) * ( cos ((m + n) * x))) + ((((1 / (2 * (m - n))) (#) ( sin * ( AffineMap ((m - n), 0 )))) `| REAL ) . x)) by A14, A17

        .= (((1 / 2) * ( cos ((m + n) * x))) + ((1 / 2) * ( cos ((m - n) * x)))) by A7, A17

        .= ((1 / 2) * (( cos ((m + n) * x)) + ( cos ((m - n) * x))))

        .= ((1 / 2) * (2 * (( cos ((((m + n) * x) + ((m - n) * x)) / 2)) * ( cos ((((m + n) * x) - ((m - n) * x)) / 2))))) by SIN_COS4: 17

        .= (( cos . (m * x)) * ( cos . (n * x)));

        hence thesis;

      end;

      let x;

      x in REAL by XREAL_0:def 1;

      hence thesis by A16;

    end;

    theorem :: INTEGR11:6

    

     Th6: (m + n) <> 0 & (m - n) <> 0 implies (((1 / (2 * (m - n))) (#) ( sin * ( AffineMap ((m - n), 0 )))) - ((1 / (2 * (m + n))) (#) ( sin * ( AffineMap ((m + n), 0 ))))) is_differentiable_on REAL & for x holds (((((1 / (2 * (m - n))) (#) ( sin * ( AffineMap ((m - n), 0 )))) - ((1 / (2 * (m + n))) (#) ( sin * ( AffineMap ((m + n), 0 ))))) `| REAL ) . x) = (( sin . (m * x)) * ( sin . (n * x)))

    proof

      assume that

       A1: (m + n) <> 0 and

       A2: (m - n) <> 0 ;

      

       A3: ( dom ((1 / (2 * (m - n))) (#) ( sin * ( AffineMap ((m - n), 0 ))))) = ( [#] REAL ) by FUNCT_2:def 1;

      

       A4: ( dom ( sin * ( AffineMap ((m - n), 0 )))) = ( [#] REAL ) & for x st x in REAL holds (( AffineMap ((m - n), 0 )) . x) = (((m - n) * x) + 0 ) by FCONT_1:def 4, FUNCT_2:def 1;

      then

       A5: ( sin * ( AffineMap ((m - n), 0 ))) is_differentiable_on REAL by FDIFF_4: 37;

      then

       A6: ((1 / (2 * (m - n))) (#) ( sin * ( AffineMap ((m - n), 0 )))) is_differentiable_on REAL by A3, FDIFF_1: 20;

      

       A7: for x st x in REAL holds ((((1 / (2 * (m - n))) (#) ( sin * ( AffineMap ((m - n), 0 )))) `| REAL ) . x) = ((1 / 2) * ( cos ((m - n) * x)))

      proof

        let x;

        assume

         A8: x in REAL ;

        ((((1 / (2 * (m - n))) (#) ( sin * ( AffineMap ((m - n), 0 )))) `| REAL ) . x) = ((1 / (2 * (m - n))) * ( diff (( sin * ( AffineMap ((m - n), 0 ))),x))) by A3, A5, FDIFF_1: 20, A8

        .= ((1 / (2 * (m - n))) * ((( sin * ( AffineMap ((m - n), 0 ))) `| REAL ) . x)) by A5, FDIFF_1:def 7, A8

        .= ((1 / (2 * (m - n))) * ((m - n) * ( cos . (((m - n) * x) + 0 )))) by A4, FDIFF_4: 37, A8

        .= (((m - n) * (1 / (2 * (m - n)))) * ( cos . (((m - n) * x) + 0 )))

        .= (((1 * (m - n)) / (2 * (m - n))) * ( cos . (((m - n) * x) + 0 ))) by XCMPLX_1: 74

        .= ((1 / 2) * ( cos ((m - n) * x))) by A2, XCMPLX_1: 91;

        hence thesis;

      end;

      

       A9: ( dom (((1 / (2 * (m - n))) (#) ( sin * ( AffineMap ((m - n), 0 )))) - ((1 / (2 * (m + n))) (#) ( sin * ( AffineMap ((m + n), 0 )))))) = ( [#] REAL ) by FUNCT_2:def 1;

      

       A10: ( dom ( sin * ( AffineMap ((m + n), 0 )))) = ( [#] REAL ) & for x st x in REAL holds (( AffineMap ((m + n), 0 )) . x) = (((m + n) * x) + 0 ) by FCONT_1:def 4, FUNCT_2:def 1;

      then

       A11: ( sin * ( AffineMap ((m + n), 0 ))) is_differentiable_on REAL by FDIFF_4: 37;

      

       A12: REAL = ( dom ((1 / (2 * (m + n))) (#) ( sin * ( AffineMap ((m + n), 0 ))))) by FUNCT_2:def 1;

      then

       A13: ((1 / (2 * (m + n))) (#) ( sin * ( AffineMap ((m + n), 0 )))) is_differentiable_on REAL by A3, A11, FDIFF_1: 20;

      hence (((1 / (2 * (m - n))) (#) ( sin * ( AffineMap ((m - n), 0 )))) - ((1 / (2 * (m + n))) (#) ( sin * ( AffineMap ((m + n), 0 ))))) is_differentiable_on REAL by A9, A6, FDIFF_1: 19;

      

       A14: for x st x in REAL holds ((((1 / (2 * (m + n))) (#) ( sin * ( AffineMap ((m + n), 0 )))) `| REAL ) . x) = ((1 / 2) * ( cos ((m + n) * x)))

      proof

        let x;

        assume

         A15: x in REAL ;

        ((((1 / (2 * (m + n))) (#) ( sin * ( AffineMap ((m + n), 0 )))) `| REAL ) . x) = ((1 / (2 * (m + n))) * ( diff (( sin * ( AffineMap ((m + n), 0 ))),x))) by A12, A3, A11, FDIFF_1: 20, A15

        .= ((1 / (2 * (m + n))) * ((( sin * ( AffineMap ((m + n), 0 ))) `| REAL ) . x)) by A11, FDIFF_1:def 7, A15

        .= ((1 / (2 * (m + n))) * ((m + n) * ( cos . (((m + n) * x) + 0 )))) by A10, FDIFF_4: 37, A15

        .= (((m + n) * (1 / (2 * (m + n)))) * ( cos . (((m + n) * x) + 0 )))

        .= (((1 * (m + n)) / (2 * (m + n))) * ( cos . (((m + n) * x) + 0 ))) by XCMPLX_1: 74

        .= ((1 / 2) * ( cos ((m + n) * x))) by A1, XCMPLX_1: 91;

        hence thesis;

      end;

      

       A16: for x st x in REAL holds (((((1 / (2 * (m - n))) (#) ( sin * ( AffineMap ((m - n), 0 )))) - ((1 / (2 * (m + n))) (#) ( sin * ( AffineMap ((m + n), 0 ))))) `| REAL ) . x) = (( sin . (m * x)) * ( sin . (n * x)))

      proof

        let x;

        assume

         A17: x in REAL ;

        (((((1 / (2 * (m - n))) (#) ( sin * ( AffineMap ((m - n), 0 )))) - ((1 / (2 * (m + n))) (#) ( sin * ( AffineMap ((m + n), 0 ))))) `| REAL ) . x) = (( diff (((1 / (2 * (m - n))) (#) ( sin * ( AffineMap ((m - n), 0 )))),x)) - ( diff (((1 / (2 * (m + n))) (#) ( sin * ( AffineMap ((m + n), 0 )))),x))) by A9, A13, A6, FDIFF_1: 19, A17

        .= (((((1 / (2 * (m - n))) (#) ( sin * ( AffineMap ((m - n), 0 )))) `| REAL ) . x) - ( diff (((1 / (2 * (m + n))) (#) ( sin * ( AffineMap ((m + n), 0 )))),x))) by A6, FDIFF_1:def 7, A17

        .= (((((1 / (2 * (m - n))) (#) ( sin * ( AffineMap ((m - n), 0 )))) `| REAL ) . x) - ((((1 / (2 * (m + n))) (#) ( sin * ( AffineMap ((m + n), 0 )))) `| REAL ) . x)) by A13, FDIFF_1:def 7, A17

        .= (((1 / 2) * ( cos ((m - n) * x))) - ((((1 / (2 * (m + n))) (#) ( sin * ( AffineMap ((m + n), 0 )))) `| REAL ) . x)) by A7, A17

        .= (((1 / 2) * ( cos ((m - n) * x))) - ((1 / 2) * ( cos ((m + n) * x)))) by A14, A17

        .= ((1 / 2) * (( cos ((m - n) * x)) - ( cos ((m + n) * x))))

        .= ((1 / 2) * ( - (2 * (( sin ((((m - n) * x) + ((m + n) * x)) / 2)) * ( sin ((((m - n) * x) - ((m + n) * x)) / 2)))))) by SIN_COS4: 18

        .= ((1 / 2) * ( - (2 * (( sin (m * x)) * ( sin ( - (n * x)))))))

        .= ((1 / 2) * ( - (2 * (( sin (m * x)) * ( - ( sin (n * x))))))) by SIN_COS: 31

        .= (( sin . (m * x)) * ( sin . (n * x)));

        hence thesis;

      end;

      let x;

      x in REAL by XREAL_0:def 1;

      hence thesis by A16;

    end;

    theorem :: INTEGR11:7

    

     Th7: (m + n) <> 0 & (m - n) <> 0 implies (( - ((1 / (2 * (m + n))) (#) ( cos * ( AffineMap ((m + n), 0 ))))) - ((1 / (2 * (m - n))) (#) ( cos * ( AffineMap ((m - n), 0 ))))) is_differentiable_on REAL & for x holds (((( - ((1 / (2 * (m + n))) (#) ( cos * ( AffineMap ((m + n), 0 ))))) - ((1 / (2 * (m - n))) (#) ( cos * ( AffineMap ((m - n), 0 ))))) `| REAL ) . x) = (( sin . (m * x)) * ( cos . (n * x)))

    proof

      assume that

       A1: (m + n) <> 0 and

       A2: (m - n) <> 0 ;

      

       A3: ( dom ( cos * ( AffineMap ((m + n), 0 )))) = ( [#] REAL ) & for x st x in REAL holds (( AffineMap ((m + n), 0 )) . x) = (((m + n) * x) + 0 ) by FCONT_1:def 4, FUNCT_2:def 1;

      then

       A4: ( cos * ( AffineMap ((m + n), 0 ))) is_differentiable_on REAL by FDIFF_4: 38;

      

       A5: for x st x in REAL holds ((( - ((1 / (2 * (m + n))) (#) ( cos * ( AffineMap ((m + n), 0 ))))) `| REAL ) . x) = ((1 / 2) * ( sin ((m + n) * x)))

      proof

        let x;

        assume

         A6: x in REAL ;

        

         A7: ( dom ((( - 1) / (2 * (m + n))) (#) ( cos * ( AffineMap ((m + n), 0 ))))) = ( [#] REAL ) by FUNCT_2:def 1;

        ((( - ((1 / (2 * (m + n))) (#) ( cos * ( AffineMap ((m + n), 0 ))))) `| REAL ) . x) = ((((( - 1) * (1 / (2 * (m + n)))) (#) ( cos * ( AffineMap ((m + n), 0 )))) `| REAL ) . x) by RFUNCT_1: 17

        .= (((( - (1 / (2 * (m + n)))) (#) ( cos * ( AffineMap ((m + n), 0 )))) `| REAL ) . x)

        .= ((((( - 1) / (2 * (m + n))) (#) ( cos * ( AffineMap ((m + n), 0 )))) `| REAL ) . x) by XCMPLX_1: 187

        .= ((( - 1) / (2 * (m + n))) * ( diff (( cos * ( AffineMap ((m + n), 0 ))),x))) by A4, A7, FDIFF_1: 20, A6

        .= ((( - 1) / (2 * (m + n))) * ((( cos * ( AffineMap ((m + n), 0 ))) `| REAL ) . x)) by A4, FDIFF_1:def 7, A6

        .= ((( - 1) / (2 * (m + n))) * ( - ((m + n) * ( sin . (((m + n) * x) + 0 ))))) by A3, FDIFF_4: 38, A6

        .= ((( - (( - 1) / (2 * (m + n)))) * (m + n)) * ( sin . (((m + n) * x) + 0 )))

        .= (((1 / (2 * (m + n))) * (m + n)) * ( sin . (((m + n) * x) + 0 ))) by XCMPLX_1: 190

        .= (((1 * (m + n)) / (2 * (m + n))) * ( sin . (((m + n) * x) + 0 ))) by XCMPLX_1: 74

        .= ((1 / 2) * ( sin ((m + n) * x))) by A1, XCMPLX_1: 91;

        hence thesis;

      end;

      

       A8: ( dom ( - ((1 / (2 * (m + n))) (#) ( cos * ( AffineMap ((m + n), 0 )))))) = ( [#] REAL ) by FUNCT_2:def 1;

      ( dom ((1 / (2 * (m + n))) (#) ( cos * ( AffineMap ((m + n), 0 ))))) = ( [#] REAL ) by FUNCT_2:def 1;

      then ( - ((1 / (2 * (m + n))) (#) ( cos * ( AffineMap ((m + n), 0 ))))) = (( - 1) (#) ((1 / (2 * (m + n))) (#) ( cos * ( AffineMap ((m + n), 0 ))))) & ((1 / (2 * (m + n))) (#) ( cos * ( AffineMap ((m + n), 0 )))) is_differentiable_on REAL by A4, FDIFF_1: 20;

      then

       A9: ( - ((1 / (2 * (m + n))) (#) ( cos * ( AffineMap ((m + n), 0 ))))) is_differentiable_on REAL by A8, FDIFF_1: 20;

      

       A10: REAL = ( dom (( - ((1 / (2 * (m + n))) (#) ( cos * ( AffineMap ((m + n), 0 ))))) - ((1 / (2 * (m - n))) (#) ( cos * ( AffineMap ((m - n), 0 )))))) by FUNCT_2:def 1;

      

       A11: ( dom ( cos * ( AffineMap ((m - n), 0 )))) = ( [#] REAL ) & for x st x in REAL holds (( AffineMap ((m - n), 0 )) . x) = (((m - n) * x) + 0 ) by FCONT_1:def 4, FUNCT_2:def 1;

      then

       A12: ( cos * ( AffineMap ((m - n), 0 ))) is_differentiable_on REAL by FDIFF_4: 38;

      

       A13: ( dom ((1 / (2 * (m - n))) (#) ( cos * ( AffineMap ((m - n), 0 ))))) = ( [#] REAL ) by FUNCT_2:def 1;

      then

       A14: ((1 / (2 * (m - n))) (#) ( cos * ( AffineMap ((m - n), 0 )))) is_differentiable_on REAL by A12, FDIFF_1: 20;

      hence (( - ((1 / (2 * (m + n))) (#) ( cos * ( AffineMap ((m + n), 0 ))))) - ((1 / (2 * (m - n))) (#) ( cos * ( AffineMap ((m - n), 0 ))))) is_differentiable_on REAL by A8, A10, A9, FDIFF_1: 19;

      

       A15: for x st x in REAL holds ((((1 / (2 * (m - n))) (#) ( cos * ( AffineMap ((m - n), 0 )))) `| REAL ) . x) = ( - ((1 / 2) * ( sin ((m - n) * x))))

      proof

        let x;

        assume

         A16: x in REAL ;

        ((((1 / (2 * (m - n))) (#) ( cos * ( AffineMap ((m - n), 0 )))) `| REAL ) . x) = ((1 / (2 * (m - n))) * ( diff (( cos * ( AffineMap ((m - n), 0 ))),x))) by A13, A12, FDIFF_1: 20, A16

        .= ((1 / (2 * (m - n))) * ((( cos * ( AffineMap ((m - n), 0 ))) `| REAL ) . x)) by A12, FDIFF_1:def 7, A16

        .= ((1 / (2 * (m - n))) * ( - ((m - n) * ( sin . (((m - n) * x) + 0 ))))) by A11, FDIFF_4: 38, A16

        .= ((( - (1 / (2 * (m - n)))) * (m - n)) * ( sin . (((m - n) * x) + 0 )))

        .= (((( - 1) / (2 * (m - n))) * (m - n)) * ( sin . (((m - n) * x) + 0 ))) by XCMPLX_1: 187

        .= (((( - 1) * (m - n)) / (2 * (m - n))) * ( sin . (((m - n) * x) + 0 ))) by XCMPLX_1: 74

        .= ((( - 1) / 2) * ( sin ((m - n) * x))) by A2, XCMPLX_1: 91;

        hence thesis;

      end;

      

       A17: for x st x in REAL holds (((( - ((1 / (2 * (m + n))) (#) ( cos * ( AffineMap ((m + n), 0 ))))) - ((1 / (2 * (m - n))) (#) ( cos * ( AffineMap ((m - n), 0 ))))) `| REAL ) . x) = (( sin . (m * x)) * ( cos . (n * x)))

      proof

        let x;

        assume

         A18: x in REAL ;

        (((( - ((1 / (2 * (m + n))) (#) ( cos * ( AffineMap ((m + n), 0 ))))) - ((1 / (2 * (m - n))) (#) ( cos * ( AffineMap ((m - n), 0 ))))) `| REAL ) . x) = (( diff (( - ((1 / (2 * (m + n))) (#) ( cos * ( AffineMap ((m + n), 0 ))))),x)) - ( diff (((1 / (2 * (m - n))) (#) ( cos * ( AffineMap ((m - n), 0 )))),x))) by A8, A10, A9, A14, FDIFF_1: 19, A18

        .= (((( - ((1 / (2 * (m + n))) (#) ( cos * ( AffineMap ((m + n), 0 ))))) `| REAL ) . x) - ( diff (((1 / (2 * (m - n))) (#) ( cos * ( AffineMap ((m - n), 0 )))),x))) by A9, FDIFF_1:def 7, A18

        .= (((( - ((1 / (2 * (m + n))) (#) ( cos * ( AffineMap ((m + n), 0 ))))) `| REAL ) . x) - ((((1 / (2 * (m - n))) (#) ( cos * ( AffineMap ((m - n), 0 )))) `| REAL ) . x)) by A14, FDIFF_1:def 7, A18

        .= (((1 / 2) * ( sin ((m + n) * x))) - ((((1 / (2 * (m - n))) (#) ( cos * ( AffineMap ((m - n), 0 )))) `| REAL ) . x)) by A5, A18

        .= (((1 / 2) * ( sin ((m + n) * x))) - ( - ((1 / 2) * ( sin ((m - n) * x))))) by A15, A18

        .= ((1 / 2) * (( sin ((m + n) * x)) + ( sin ((m - n) * x))))

        .= ((1 / 2) * (2 * (( cos ((((m + n) * x) - ((m - n) * x)) / 2)) * ( sin ((((m + n) * x) + ((m - n) * x)) / 2))))) by SIN_COS4: 15

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

        hence thesis;

      end;

      let x;

      x in REAL by XREAL_0:def 1;

      hence thesis by A17;

    end;

    theorem :: INTEGR11:8

    

     Th8: n <> 0 implies (((1 / (n ^2 )) (#) ( sin * ( AffineMap (n, 0 )))) - (( AffineMap ((1 / n), 0 )) (#) ( cos * ( AffineMap (n, 0 ))))) is_differentiable_on REAL & for x holds (((((1 / (n ^2 )) (#) ( sin * ( AffineMap (n, 0 )))) - (( AffineMap ((1 / n), 0 )) (#) ( cos * ( AffineMap (n, 0 ))))) `| REAL ) . x) = (x * ( sin . (n * x)))

    proof

      

       A1: ( dom (((1 / (n ^2 )) (#) ( sin * ( AffineMap (n, 0 )))) - (( AffineMap ((1 / n), 0 )) (#) ( cos * ( AffineMap (n, 0 )))))) = ( [#] REAL ) by FUNCT_2:def 1;

      

       A2: ( dom ( AffineMap ((1 / n), 0 ))) = REAL & for x st x in REAL holds (( AffineMap ((1 / n), 0 )) . x) = (((1 / n) * x) + 0 ) by FCONT_1:def 4, FUNCT_2:def 1;

      then

       A3: ( AffineMap ((1 / n), 0 )) is_differentiable_on REAL by A1, FDIFF_1: 23;

      

       A4: for x st x in REAL holds (( AffineMap (n, 0 )) . x) = ((n * x) + 0 ) by FCONT_1:def 4;

      

       A5: ( dom ( sin * ( AffineMap (n, 0 )))) = ( [#] REAL ) by FUNCT_2:def 1;

      then

       A6: ( sin * ( AffineMap (n, 0 ))) is_differentiable_on REAL by A4, FDIFF_4: 37;

      

       A7: ( dom ((1 / (n ^2 )) (#) ( sin * ( AffineMap (n, 0 ))))) = REAL by FUNCT_2:def 1;

      then

       A8: ((1 / (n ^2 )) (#) ( sin * ( AffineMap (n, 0 )))) is_differentiable_on REAL by A1, A6, FDIFF_1: 20;

      assume

       A9: n <> 0 ;

      

       A10: for x st x in REAL holds ((((1 / (n ^2 )) (#) ( sin * ( AffineMap (n, 0 )))) `| REAL ) . x) = ((1 / n) * ( cos (n * x)))

      proof

        let x;

        assume

         A11: x in REAL ;

        ((((1 / (n ^2 )) (#) ( sin * ( AffineMap (n, 0 )))) `| REAL ) . x) = ((1 / (n ^2 )) * ( diff (( sin * ( AffineMap (n, 0 ))),x))) by A7, A1, A6, FDIFF_1: 20, A11

        .= ((1 / (n ^2 )) * ((( sin * ( AffineMap (n, 0 ))) `| REAL ) . x)) by A6, FDIFF_1:def 7, A11

        .= ((1 / (n ^2 )) * (n * ( cos . ((n * x) + 0 )))) by A5, A4, FDIFF_4: 37, A11

        .= ((n * (1 / (n * n))) * ( cos . ((n * x) + 0 )))

        .= (((n * 1) / (n * n)) * ( cos . ((n * x) + 0 ))) by XCMPLX_1: 74

        .= ((1 / n) * ( cos . ((n * x) + 0 ))) by A9, XCMPLX_1: 91;

        hence thesis;

      end;

      

       A12: ( dom ( cos * ( AffineMap (n, 0 )))) = ( [#] REAL ) by FUNCT_2:def 1;

      then

       A13: ( cos * ( AffineMap (n, 0 ))) is_differentiable_on REAL by A4, FDIFF_4: 38;

      

       A14: ( dom (( AffineMap ((1 / n), 0 )) (#) ( cos * ( AffineMap (n, 0 ))))) = REAL by FUNCT_2:def 1;

      then

       A15: (( AffineMap ((1 / n), 0 )) (#) ( cos * ( AffineMap (n, 0 )))) is_differentiable_on REAL by A1, A3, A13, FDIFF_1: 21;

      hence (((1 / (n ^2 )) (#) ( sin * ( AffineMap (n, 0 )))) - (( AffineMap ((1 / n), 0 )) (#) ( cos * ( AffineMap (n, 0 ))))) is_differentiable_on REAL by A1, A8, FDIFF_1: 19;

      

       A16: for x st x in REAL holds (((( AffineMap ((1 / n), 0 )) (#) ( cos * ( AffineMap (n, 0 )))) `| REAL ) . x) = (((1 / n) * ( cos . (n * x))) - (x * ( sin . (n * x))))

      proof

        let x;

        assume

         A17: x in REAL ;

        (((( AffineMap ((1 / n), 0 )) (#) ( cos * ( AffineMap (n, 0 )))) `| REAL ) . x) = (((( cos * ( AffineMap (n, 0 ))) . x) * ( diff (( AffineMap ((1 / n), 0 )),x))) + ((( AffineMap ((1 / n), 0 )) . x) * ( diff (( cos * ( AffineMap (n, 0 ))),x)))) by A14, A1, A3, A13, FDIFF_1: 21, A17

        .= (((( cos * ( AffineMap (n, 0 ))) . x) * ((( AffineMap ((1 / n), 0 )) `| REAL ) . x)) + ((( AffineMap ((1 / n), 0 )) . x) * ( diff (( cos * ( AffineMap (n, 0 ))),x)))) by A3, FDIFF_1:def 7, A17

        .= (((( cos * ( AffineMap (n, 0 ))) . x) * (1 / n)) + ((( AffineMap ((1 / n), 0 )) . x) * ( diff (( cos * ( AffineMap (n, 0 ))),x)))) by A1, A2, FDIFF_1: 23, A17

        .= (((( cos * ( AffineMap (n, 0 ))) . x) * (1 / n)) + ((( AffineMap ((1 / n), 0 )) . x) * ((( cos * ( AffineMap (n, 0 ))) `| REAL ) . x))) by A13, FDIFF_1:def 7, A17

        .= (((( cos * ( AffineMap (n, 0 ))) . x) * (1 / n)) + ((( AffineMap ((1 / n), 0 )) . x) * ( - (n * ( sin . ((n * x) + 0 )))))) by A12, A4, FDIFF_4: 38, A17

        .= (((( cos * ( AffineMap (n, 0 ))) . x) * (1 / n)) + ((((1 / n) * x) + 0 ) * ( - (n * ( sin . ((n * x) + 0 )))))) by FCONT_1:def 4

        .= ((( cos . (( AffineMap (n, 0 )) . x)) * (1 / n)) + (((1 / n) * x) * ( - (n * ( sin . ((n * x) + 0 )))))) by A12, FUNCT_1: 12, A17

        .= (((1 / n) * ( cos . (n * x))) + ( - ((((1 / n) * n) * x) * ( sin . (n * x))))) by FCONT_1:def 4

        .= (((1 / n) * ( cos . (n * x))) + ( - ((1 * x) * ( sin . (n * x))))) by A9, XCMPLX_1: 87

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

        hence thesis;

      end;

      

       A18: for x st x in REAL holds (((((1 / (n ^2 )) (#) ( sin * ( AffineMap (n, 0 )))) - (( AffineMap ((1 / n), 0 )) (#) ( cos * ( AffineMap (n, 0 ))))) `| REAL ) . x) = (x * ( sin . (n * x)))

      proof

        let x;

        assume

         A19: x in REAL ;

        (((((1 / (n ^2 )) (#) ( sin * ( AffineMap (n, 0 )))) - (( AffineMap ((1 / n), 0 )) (#) ( cos * ( AffineMap (n, 0 ))))) `| REAL ) . x) = (( diff (((1 / (n ^2 )) (#) ( sin * ( AffineMap (n, 0 )))),x)) - ( diff ((( AffineMap ((1 / n), 0 )) (#) ( cos * ( AffineMap (n, 0 )))),x))) by A1, A8, A15, FDIFF_1: 19, A19

        .= (((((1 / (n ^2 )) (#) ( sin * ( AffineMap (n, 0 )))) `| REAL ) . x) - ( diff ((( AffineMap ((1 / n), 0 )) (#) ( cos * ( AffineMap (n, 0 )))),x))) by A8, FDIFF_1:def 7, A19

        .= (((1 / n) * ( cos (n * x))) - ( diff ((( AffineMap ((1 / n), 0 )) (#) ( cos * ( AffineMap (n, 0 )))),x))) by A10, A19

        .= (((1 / n) * ( cos (n * x))) - (((( AffineMap ((1 / n), 0 )) (#) ( cos * ( AffineMap (n, 0 )))) `| REAL ) . x)) by A15, FDIFF_1:def 7, A19

        .= (((1 / n) * ( cos (n * x))) - (((1 / n) * ( cos . (n * x))) - (x * ( sin . (n * x))))) by A16, A19

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

        hence thesis;

      end;

      let x;

      x in REAL by XREAL_0:def 1;

      hence thesis by A18;

    end;

    theorem :: INTEGR11:9

    

     Th9: n <> 0 implies (((1 / (n ^2 )) (#) ( cos * ( AffineMap (n, 0 )))) + (( AffineMap ((1 / n), 0 )) (#) ( sin * ( AffineMap (n, 0 ))))) is_differentiable_on REAL & for x holds (((((1 / (n ^2 )) (#) ( cos * ( AffineMap (n, 0 )))) + (( AffineMap ((1 / n), 0 )) (#) ( sin * ( AffineMap (n, 0 ))))) `| REAL ) . x) = (x * ( cos . (n * x)))

    proof

      

       A1: ( dom (((1 / (n ^2 )) (#) ( cos * ( AffineMap (n, 0 )))) + (( AffineMap ((1 / n), 0 )) (#) ( sin * ( AffineMap (n, 0 )))))) = ( [#] REAL ) by FUNCT_2:def 1;

      

       A2: ( dom ( AffineMap ((1 / n), 0 ))) = REAL & for x st x in REAL holds (( AffineMap ((1 / n), 0 )) . x) = (((1 / n) * x) + 0 ) by FCONT_1:def 4, FUNCT_2:def 1;

      then

       A3: ( AffineMap ((1 / n), 0 )) is_differentiable_on REAL by A1, FDIFF_1: 23;

      

       A4: for x st x in REAL holds (( AffineMap (n, 0 )) . x) = ((n * x) + 0 ) by FCONT_1:def 4;

      

       A5: ( dom ( cos * ( AffineMap (n, 0 )))) = ( [#] REAL ) by FUNCT_2:def 1;

      then

       A6: ( cos * ( AffineMap (n, 0 ))) is_differentiable_on REAL by A4, FDIFF_4: 38;

      

       A7: ( dom ((1 / (n ^2 )) (#) ( cos * ( AffineMap (n, 0 ))))) = REAL by FUNCT_2:def 1;

      then

       A8: ((1 / (n ^2 )) (#) ( cos * ( AffineMap (n, 0 )))) is_differentiable_on REAL by A1, A6, FDIFF_1: 20;

      assume

       A9: n <> 0 ;

      

       A10: for x st x in REAL holds ((((1 / (n ^2 )) (#) ( cos * ( AffineMap (n, 0 )))) `| REAL ) . x) = ( - ((1 / n) * ( sin (n * x))))

      proof

        let x;

        assume

         A11: x in REAL ;

        ((((1 / (n ^2 )) (#) ( cos * ( AffineMap (n, 0 )))) `| REAL ) . x) = ((1 / (n ^2 )) * ( diff (( cos * ( AffineMap (n, 0 ))),x))) by A7, A1, A6, FDIFF_1: 20, A11

        .= ((1 / (n ^2 )) * ((( cos * ( AffineMap (n, 0 ))) `| REAL ) . x)) by A6, FDIFF_1:def 7, A11

        .= ((1 / (n ^2 )) * ( - (n * ( sin . ((n * x) + 0 ))))) by A5, A4, FDIFF_4: 38, A11

        .= ((( - 1) * (n * (1 / (n * n)))) * ( sin . ((n * x) + 0 )))

        .= ((( - 1) * (n / ((n * n) / 1))) * ( sin . ((n * x) + 0 ))) by XCMPLX_1: 79

        .= ((( - 1) * ((n * 1) / (n * n))) * ( sin . ((n * x) + 0 )))

        .= ((( - 1) * (1 / n)) * ( sin . ((n * x) + 0 ))) by A9, XCMPLX_1: 91;

        hence thesis;

      end;

      

       A12: ( dom ( sin * ( AffineMap (n, 0 )))) = ( [#] REAL ) by FUNCT_2:def 1;

      then

       A13: ( sin * ( AffineMap (n, 0 ))) is_differentiable_on REAL by A4, FDIFF_4: 37;

      

       A14: ( dom (( AffineMap ((1 / n), 0 )) (#) ( sin * ( AffineMap (n, 0 ))))) = REAL by FUNCT_2:def 1;

      then

       A15: (( AffineMap ((1 / n), 0 )) (#) ( sin * ( AffineMap (n, 0 )))) is_differentiable_on REAL by A1, A3, A13, FDIFF_1: 21;

      hence (((1 / (n ^2 )) (#) ( cos * ( AffineMap (n, 0 )))) + (( AffineMap ((1 / n), 0 )) (#) ( sin * ( AffineMap (n, 0 ))))) is_differentiable_on REAL by A1, A8, FDIFF_1: 18;

      

       A16: for x st x in REAL holds (((( AffineMap ((1 / n), 0 )) (#) ( sin * ( AffineMap (n, 0 )))) `| REAL ) . x) = (((1 / n) * ( sin . (n * x))) + (x * ( cos . (n * x))))

      proof

        let x;

        assume

         A17: x in REAL ;

        (((( AffineMap ((1 / n), 0 )) (#) ( sin * ( AffineMap (n, 0 )))) `| REAL ) . x) = (((( sin * ( AffineMap (n, 0 ))) . x) * ( diff (( AffineMap ((1 / n), 0 )),x))) + ((( AffineMap ((1 / n), 0 )) . x) * ( diff (( sin * ( AffineMap (n, 0 ))),x)))) by A14, A1, A3, A13, FDIFF_1: 21, A17

        .= (((( sin * ( AffineMap (n, 0 ))) . x) * ((( AffineMap ((1 / n), 0 )) `| REAL ) . x)) + ((( AffineMap ((1 / n), 0 )) . x) * ( diff (( sin * ( AffineMap (n, 0 ))),x)))) by A3, FDIFF_1:def 7, A17

        .= (((( sin * ( AffineMap (n, 0 ))) . x) * (1 / n)) + ((( AffineMap ((1 / n), 0 )) . x) * ( diff (( sin * ( AffineMap (n, 0 ))),x)))) by A1, A2, FDIFF_1: 23, A17

        .= (((( sin * ( AffineMap (n, 0 ))) . x) * (1 / n)) + ((( AffineMap ((1 / n), 0 )) . x) * ((( sin * ( AffineMap (n, 0 ))) `| REAL ) . x))) by A13, FDIFF_1:def 7, A17

        .= (((( sin * ( AffineMap (n, 0 ))) . x) * (1 / n)) + ((( AffineMap ((1 / n), 0 )) . x) * (n * ( cos . ((n * x) + 0 ))))) by A12, A4, FDIFF_4: 37, A17

        .= (((( sin * ( AffineMap (n, 0 ))) . x) * (1 / n)) + ((((1 / n) * x) + 0 ) * (n * ( cos . ((n * x) + 0 ))))) by FCONT_1:def 4

        .= ((( sin . (( AffineMap (n, 0 )) . x)) * (1 / n)) + (((1 / n) * x) * (n * ( cos . ((n * x) + 0 ))))) by A12, FUNCT_1: 12, A17

        .= (((1 / n) * ( sin . (n * x))) + ((((1 / n) * n) * x) * ( cos . (n * x)))) by FCONT_1:def 4

        .= (((1 / n) * ( sin . (n * x))) + ((1 * x) * ( cos . (n * x)))) by A9, XCMPLX_1: 87

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

        hence thesis;

      end;

      

       A18: for x st x in REAL holds (((((1 / (n ^2 )) (#) ( cos * ( AffineMap (n, 0 )))) + (( AffineMap ((1 / n), 0 )) (#) ( sin * ( AffineMap (n, 0 ))))) `| REAL ) . x) = (x * ( cos . (n * x)))

      proof

        let x;

        assume

         A19: x in REAL ;

        (((((1 / (n ^2 )) (#) ( cos * ( AffineMap (n, 0 )))) + (( AffineMap ((1 / n), 0 )) (#) ( sin * ( AffineMap (n, 0 ))))) `| REAL ) . x) = (( diff (((1 / (n ^2 )) (#) ( cos * ( AffineMap (n, 0 )))),x)) + ( diff ((( AffineMap ((1 / n), 0 )) (#) ( sin * ( AffineMap (n, 0 )))),x))) by A1, A8, A15, FDIFF_1: 18, A19

        .= (((((1 / (n ^2 )) (#) ( cos * ( AffineMap (n, 0 )))) `| REAL ) . x) + ( diff ((( AffineMap ((1 / n), 0 )) (#) ( sin * ( AffineMap (n, 0 )))),x))) by A8, FDIFF_1:def 7, A19

        .= (( - ((1 / n) * ( sin (n * x)))) + ( diff ((( AffineMap ((1 / n), 0 )) (#) ( sin * ( AffineMap (n, 0 )))),x))) by A10, A19

        .= (( - ((1 / n) * ( sin (n * x)))) + (((( AffineMap ((1 / n), 0 )) (#) ( sin * ( AffineMap (n, 0 )))) `| REAL ) . x)) by A15, FDIFF_1:def 7, A19

        .= (( - ((1 / n) * ( sin (n * x)))) + (((1 / n) * ( sin . (n * x))) + (x * ( cos . (n * x))))) by A16, A19

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

        hence thesis;

      end;

      let x;

      x in REAL by XREAL_0:def 1;

      hence thesis by A18;

    end;

    theorem :: INTEGR11:10

    

     Th10: ((( AffineMap (1, 0 )) (#) cosh ) - sinh ) is_differentiable_on REAL & for x holds ((((( AffineMap (1, 0 )) (#) cosh ) - sinh ) `| REAL ) . x) = (x * ( sinh . x))

    proof

      

       A1: ( dom ((( AffineMap (1, 0 )) (#) cosh ) - sinh )) = ( [#] REAL ) by FUNCT_2:def 1;

      

       A2: ( dom ( AffineMap (1, 0 ))) = ( [#] REAL ) & for x st x in REAL holds (( AffineMap (1, 0 )) . x) = ((1 * x) + 0 ) by FCONT_1:def 4, FUNCT_2:def 1;

      then

       A3: ( AffineMap (1, 0 )) is_differentiable_on REAL by FDIFF_1: 23;

      

       A4: ( dom (( AffineMap (1, 0 )) (#) cosh )) = ( [#] REAL ) by FUNCT_2:def 1;

      then

       A5: (( AffineMap (1, 0 )) (#) cosh ) is_differentiable_on REAL by A3, FDIFF_1: 21, SIN_COS2: 35;

      hence ((( AffineMap (1, 0 )) (#) cosh ) - sinh ) is_differentiable_on REAL by A1, FDIFF_1: 19, SIN_COS2: 34;

      

       A6: for x st x in REAL holds (((( AffineMap (1, 0 )) (#) cosh ) `| REAL ) . x) = (( cosh . x) + (x * ( sinh . x)))

      proof

        let x;

        assume

         A7: x in REAL ;

        (((( AffineMap (1, 0 )) (#) cosh ) `| REAL ) . x) = ((( cosh . x) * ( diff (( AffineMap (1, 0 )),x))) + ((( AffineMap (1, 0 )) . x) * ( diff ( cosh ,x)))) by A4, A3, FDIFF_1: 21, SIN_COS2: 35, A7

        .= ((( cosh . x) * ((( AffineMap (1, 0 )) `| REAL ) . x)) + ((( AffineMap (1, 0 )) . x) * ( diff ( cosh ,x)))) by A3, FDIFF_1:def 7, A7

        .= ((( cosh . x) * 1) + ((( AffineMap (1, 0 )) . x) * ( diff ( cosh ,x)))) by A2, FDIFF_1: 23, A7

        .= (( cosh . x) + ((( AffineMap (1, 0 )) . x) * ( sinh . x))) by SIN_COS2: 35

        .= (( cosh . x) + (((1 * x) + 0 ) * ( sinh . x))) by FCONT_1:def 4

        .= (( cosh . x) + (x * ( sinh . x)));

        hence thesis;

      end;

      

       A8: for x st x in REAL holds ((((( AffineMap (1, 0 )) (#) cosh ) - sinh ) `| REAL ) . x) = (x * ( sinh . x))

      proof

        let x;

        assume

         A9: x in REAL ;

        ((((( AffineMap (1, 0 )) (#) cosh ) - sinh ) `| REAL ) . x) = (( diff ((( AffineMap (1, 0 )) (#) cosh ),x)) - ( diff ( sinh ,x))) by A1, A5, FDIFF_1: 19, SIN_COS2: 34, A9

        .= ((((( AffineMap (1, 0 )) (#) cosh ) `| REAL ) . x) - ( diff ( sinh ,x))) by A5, FDIFF_1:def 7, A9

        .= ((( cosh . x) + (x * ( sinh . x))) - ( diff ( sinh ,x))) by A6, A9

        .= ((( cosh . x) + (x * ( sinh . x))) - ( cosh . x)) by SIN_COS2: 34

        .= (x * ( sinh . x));

        hence thesis;

      end;

      let x;

      x in REAL by XREAL_0:def 1;

      hence thesis by A8;

    end;

    theorem :: INTEGR11:11

    

     Th11: ((( AffineMap (1, 0 )) (#) sinh ) - cosh ) is_differentiable_on REAL & for x holds ((((( AffineMap (1, 0 )) (#) sinh ) - cosh ) `| REAL ) . x) = (x * ( cosh . x))

    proof

      

       A1: ( dom ((( AffineMap (1, 0 )) (#) sinh ) - cosh )) = ( [#] REAL ) by FUNCT_2:def 1;

      

       A2: ( dom ( AffineMap (1, 0 ))) = ( [#] REAL ) & for x st x in REAL holds (( AffineMap (1, 0 )) . x) = ((1 * x) + 0 ) by FCONT_1:def 4, FUNCT_2:def 1;

      then

       A3: ( AffineMap (1, 0 )) is_differentiable_on REAL by FDIFF_1: 23;

      

       A4: ( dom (( AffineMap (1, 0 )) (#) sinh )) = ( [#] REAL ) by FUNCT_2:def 1;

      then

       A5: (( AffineMap (1, 0 )) (#) sinh ) is_differentiable_on REAL by A3, FDIFF_1: 21, SIN_COS2: 34;

      hence ((( AffineMap (1, 0 )) (#) sinh ) - cosh ) is_differentiable_on REAL by A1, FDIFF_1: 19, SIN_COS2: 35;

      

       A6: for x st x in REAL holds (((( AffineMap (1, 0 )) (#) sinh ) `| REAL ) . x) = (( sinh . x) + (x * ( cosh . x)))

      proof

        let x;

        assume

         A7: x in REAL ;

        (((( AffineMap (1, 0 )) (#) sinh ) `| REAL ) . x) = ((( sinh . x) * ( diff (( AffineMap (1, 0 )),x))) + ((( AffineMap (1, 0 )) . x) * ( diff ( sinh ,x)))) by A4, A3, FDIFF_1: 21, SIN_COS2: 34, A7

        .= ((( sinh . x) * ((( AffineMap (1, 0 )) `| REAL ) . x)) + ((( AffineMap (1, 0 )) . x) * ( diff ( sinh ,x)))) by A3, FDIFF_1:def 7, A7

        .= ((( sinh . x) * 1) + ((( AffineMap (1, 0 )) . x) * ( diff ( sinh ,x)))) by A2, FDIFF_1: 23, A7

        .= (( sinh . x) + ((( AffineMap (1, 0 )) . x) * ( cosh . x))) by SIN_COS2: 34

        .= (( sinh . x) + (((1 * x) + 0 ) * ( cosh . x))) by FCONT_1:def 4

        .= (( sinh . x) + (x * ( cosh . x)));

        hence thesis;

      end;

      

       A8: for x st x in REAL holds ((((( AffineMap (1, 0 )) (#) sinh ) - cosh ) `| REAL ) . x) = (x * ( cosh . x))

      proof

        let x;

        assume

         A9: x in REAL ;

        ((((( AffineMap (1, 0 )) (#) sinh ) - cosh ) `| REAL ) . x) = (( diff ((( AffineMap (1, 0 )) (#) sinh ),x)) - ( diff ( cosh ,x))) by A1, A5, FDIFF_1: 19, SIN_COS2: 35, A9

        .= ((((( AffineMap (1, 0 )) (#) sinh ) `| REAL ) . x) - ( diff ( cosh ,x))) by A5, FDIFF_1:def 7, A9

        .= ((( sinh . x) + (x * ( cosh . x))) - ( diff ( cosh ,x))) by A6, A9

        .= ((( sinh . x) + (x * ( cosh . x))) - ( sinh . x)) by SIN_COS2: 35

        .= (x * ( cosh . x));

        hence thesis;

      end;

      let x;

      x in REAL by XREAL_0:def 1;

      hence thesis by A8;

    end;

    theorem :: INTEGR11:12

    

     Th12: (a * (n + 1)) <> 0 implies ((1 / (a * (n + 1))) (#) (( #Z (n + 1)) * ( AffineMap (a,b)))) is_differentiable_on REAL & for x holds ((((1 / (a * (n + 1))) (#) (( #Z (n + 1)) * ( AffineMap (a,b)))) `| REAL ) . x) = (((a * x) + b) #Z n)

    proof

      assume

       A1: (a * (n + 1)) <> 0 ;

      

       A2: ( [#] REAL ) = ( dom ((1 / (a * (n + 1))) (#) (( #Z (n + 1)) * ( AffineMap (a,b))))) by FUNCT_2:def 1;

      

       A3: ( [#] REAL ) = ( dom ( AffineMap (a,b))) by FUNCT_2:def 1;

      

       A4: for x st x in REAL holds (( AffineMap (a,b)) . x) = ((a * x) + b) by FCONT_1:def 4;

      then

       A5: ( AffineMap (a,b)) is_differentiable_on REAL by A3, FDIFF_1: 23;

      (( #Z (n + 1)) * ( AffineMap (a,b))) is_differentiable_in x

      proof

        x in REAL by XREAL_0:def 1;

        then ( AffineMap (a,b)) is_differentiable_in x by A3, A5, FDIFF_1: 9;

        hence thesis by TAYLOR_1: 3;

      end;

      then ( [#] REAL ) = ( dom (( #Z (n + 1)) * ( AffineMap (a,b)))) & for x st x in REAL holds (( #Z (n + 1)) * ( AffineMap (a,b))) is_differentiable_in x by FUNCT_2:def 1;

      then

       A6: (( #Z (n + 1)) * ( AffineMap (a,b))) is_differentiable_on REAL by FDIFF_1: 9;

      hence ((1 / (a * (n + 1))) (#) (( #Z (n + 1)) * ( AffineMap (a,b)))) is_differentiable_on REAL by A2, FDIFF_1: 20;

      

       A7: for x st x in REAL holds (((( #Z (n + 1)) * ( AffineMap (a,b))) `| REAL ) . x) = ((a * (n + 1)) * ((( AffineMap (a,b)) . x) #Z n))

      proof

        set m = (n + 1);

        let x;

        assume

         A8: x in REAL ;

        ( AffineMap (a,b)) is_differentiable_in x by A3, A5, FDIFF_1: 9, A8;

        

        then ( diff ((( #Z m) * ( AffineMap (a,b))),x)) = ((m * ((( AffineMap (a,b)) . x) #Z (m - 1))) * ( diff (( AffineMap (a,b)),x))) by TAYLOR_1: 3

        .= ((m * ((( AffineMap (a,b)) . x) #Z (m - 1))) * ((( AffineMap (a,b)) `| REAL ) . x)) by A5, FDIFF_1:def 7, A8

        .= ((m * ((( AffineMap (a,b)) . x) #Z (m - 1))) * a) by A3, A4, FDIFF_1: 23, A8;

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

      end;

      

       A9: for x st x in REAL holds ((((1 / (a * (n + 1))) (#) (( #Z (n + 1)) * ( AffineMap (a,b)))) `| REAL ) . x) = (((a * x) + b) #Z n)

      proof

        let x;

        assume

         A10: x in REAL ;

        ((((1 / (a * (n + 1))) (#) (( #Z (n + 1)) * ( AffineMap (a,b)))) `| REAL ) . x) = ((1 / (a * (n + 1))) * ( diff ((( #Z (n + 1)) * ( AffineMap (a,b))),x))) by A2, A6, FDIFF_1: 20, A10

        .= ((1 / (a * (n + 1))) * (((( #Z (n + 1)) * ( AffineMap (a,b))) `| REAL ) . x)) by A6, FDIFF_1:def 7, A10

        .= ((1 / (a * (n + 1))) * ((a * (n + 1)) * ((( AffineMap (a,b)) . x) #Z n))) by A7, A10

        .= (((1 / (a * (n + 1))) * (a * (n + 1))) * ((( AffineMap (a,b)) . x) #Z n))

        .= (((a * (n + 1)) / (a * (n + 1))) * ((( AffineMap (a,b)) . x) #Z n)) by XCMPLX_1: 99

        .= (1 * ((( AffineMap (a,b)) . x) #Z n)) by A1, XCMPLX_1: 60

        .= (((a * x) + b) #Z n) by FCONT_1:def 4;

        hence thesis;

      end;

      let x;

      x in REAL by XREAL_0:def 1;

      hence thesis by A9;

    end;

    begin

    theorem :: INTEGR11:13

    

     Th13: ( integral (( sin ^2 ),A)) = (((( AffineMap ((1 / 2), 0 )) - ((1 / 4) (#) ( sin * ( AffineMap (2, 0 ))))) . ( upper_bound A)) - ((( AffineMap ((1 / 2), 0 )) - ((1 / 4) (#) ( sin * ( AffineMap (2, 0 ))))) . ( lower_bound A)))

    proof

      

       A1: for x be Element of REAL st x in ( dom ((( AffineMap ((1 / 2), 0 )) - ((1 / 4) (#) ( sin * ( AffineMap (2, 0 ))))) `| REAL )) holds (((( AffineMap ((1 / 2), 0 )) - ((1 / 4) (#) ( sin * ( AffineMap (2, 0 ))))) `| REAL ) . x) = (( sin ^2 ) . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom ((( AffineMap ((1 / 2), 0 )) - ((1 / 4) (#) ( sin * ( AffineMap (2, 0 ))))) `| REAL ));

        (((( AffineMap ((1 / 2), 0 )) - ((1 / 4) (#) ( sin * ( AffineMap (2, 0 ))))) `| REAL ) . x) = (( sin . x) ^2 ) by Th1

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

        hence thesis;

      end;

      

       A2: ( dom ( sin ^2 )) = REAL by SIN_COS: 24, VALUED_1: 11;

      then ( dom ((( AffineMap ((1 / 2), 0 )) - ((1 / 4) (#) ( sin * ( AffineMap (2, 0 ))))) `| REAL )) = ( dom ( sin ^2 )) by Th1, FDIFF_1:def 7;

      then

       A3: ((( AffineMap ((1 / 2), 0 )) - ((1 / 4) (#) ( sin * ( AffineMap (2, 0 ))))) `| REAL ) = ( sin ^2 ) by A1, PARTFUN1: 5;

      (( sin ^2 ) | A) is bounded by A2, INTEGRA5: 10;

      hence thesis by A2, A3, Th1, INTEGRA5: 11, INTEGRA5: 13;

    end;

    

     Lm4: ( dom ( AffineMap (2, 0 ))) = ( [#] REAL ) by FUNCT_2:def 1;

    

     Lm5: ( dom (( AffineMap ((1 / 2), 0 )) - ((1 / 4) (#) ( sin * ( AffineMap (2, 0 )))))) = REAL by FUNCT_2:def 1;

    reconsider pp = PI as Element of REAL by XREAL_0:def 1;

    

     Lm6: 0 in REAL by XREAL_0:def 1;

    theorem :: INTEGR11:14

    A = [. 0 , PI .] implies ( integral (( sin ^2 ),A)) = ( PI / 2)

    proof

      assume A = [. 0 , PI .];

      then ( upper_bound A) = PI & ( lower_bound A) = 0 by INTEGRA8: 37;

      

      then ( integral (( sin ^2 ),A)) = (((( AffineMap ((1 / 2), 0 )) - ((1 / 4) (#) ( sin * ( AffineMap (2, 0 ))))) . pp) - ((( AffineMap ((1 / 2), 0 )) - ((1 / 4) (#) ( sin * ( AffineMap (2, 0 ))))) . 0 )) by Th13

      .= (((( AffineMap ((1 / 2), 0 )) . PI ) - (((1 / 4) (#) ( sin * ( AffineMap (2, 0 )))) . PI )) - ((( AffineMap ((1 / 2), 0 )) - ((1 / 4) (#) ( sin * ( AffineMap (2, 0 ))))) . 0 )) by Lm5, VALUED_1: 13

      .= (((( AffineMap ((1 / 2), 0 )) . PI ) - (((1 / 4) (#) ( sin * ( AffineMap (2, 0 )))) . PI )) - ((( AffineMap ((1 / 2), 0 )) . 0 ) - (((1 / 4) (#) ( sin * ( AffineMap (2, 0 )))) . 0 ))) by Lm5, VALUED_1: 13, Lm6

      .= (((((1 / 2) * PI ) + 0 ) - (((1 / 4) (#) ( sin * ( AffineMap (2, 0 )))) . PI )) - ((( AffineMap ((1 / 2), 0 )) . 0 ) - (((1 / 4) (#) ( sin * ( AffineMap (2, 0 )))) . 0 ))) by FCONT_1:def 4

      .= ((((1 / 2) * PI ) - ((1 / 4) * (( sin * ( AffineMap (2, 0 ))) . pp))) - ((( AffineMap ((1 / 2), 0 )) . 0 ) - (((1 / 4) (#) ( sin * ( AffineMap (2, 0 )))) . 0 ))) by VALUED_1: 6

      .= ((((1 / 2) * PI ) - ((1 / 4) * ( sin . (( AffineMap (2, 0 )) . PI )))) - ((( AffineMap ((1 / 2), 0 )) . 0 ) - (((1 / 4) (#) ( sin * ( AffineMap (2, 0 )))) . 0 ))) by Lm4, FUNCT_1: 13

      .= ((((1 / 2) * PI ) - ((1 / 4) * ( sin . ((2 * PI ) + 0 )))) - ((( AffineMap ((1 / 2), 0 )) . 0 ) - (((1 / 4) (#) ( sin * ( AffineMap (2, 0 )))) . 0 ))) by FCONT_1:def 4

      .= ((((1 / 2) * PI ) - ((1 / 4) * ( sin . ((2 * PI ) + 0 )))) - ( 0 - (((1 / 4) (#) ( sin * ( AffineMap (2, 0 )))) . 0 ))) by FCONT_1: 48

      .= (((((1 / 2) * PI ) - ((1 / 4) * ( sin . ((2 * PI ) + 0 )))) - 0 ) + (((1 / 4) (#) ( sin * ( AffineMap (2, 0 )))) . 0 ))

      .= ((((1 / 2) * PI ) - ((1 / 4) * ( sin . ((2 * PI ) + 0 )))) + ((1 / 4) * (( sin * ( AffineMap (2, 0 ))) . 0 ))) by VALUED_1: 6

      .= ((((1 / 2) * PI ) - ((1 / 4) * ( sin . ((2 * PI ) + 0 )))) + ((1 / 4) * ( sin . (( AffineMap (2, 0 )) . 0 )))) by Lm4, FUNCT_1: 13, Lm6

      .= ((((1 / 2) * PI ) - ((1 / 4) * ( sin . ( 0 + ((2 * PI ) * 1))))) + ((1 / 4) * ( sin . 0 ))) by FCONT_1: 48

      .= ((((1 / 2) * PI ) - ((1 / 4) * ( sin . 0 ))) + ((1 / 4) * ( sin . 0 ))) by SIN_COS6: 8

      .= ( PI / 2);

      hence thesis;

    end;

    reconsider dp = (2 * PI ), ddp = ((2 * (2 * PI )) + 0 ) as Element of REAL by XREAL_0:def 1;

    theorem :: INTEGR11:15

    A = [. 0 , (2 * PI ).] implies ( integral (( sin ^2 ),A)) = PI

    proof

      assume A = [. 0 , (2 * PI ).];

      then ( upper_bound A) = (2 * PI ) & ( lower_bound A) = 0 by INTEGRA8: 37;

      

      then ( integral (( sin ^2 ),A)) = (((( AffineMap ((1 / 2), 0 )) - ((1 / 4) (#) ( sin * ( AffineMap (2, 0 ))))) . dp) - ((( AffineMap ((1 / 2), 0 )) - ((1 / 4) (#) ( sin * ( AffineMap (2, 0 ))))) . 0 )) by Th13

      .= (((( AffineMap ((1 / 2), 0 )) . (2 * PI )) - (((1 / 4) (#) ( sin * ( AffineMap (2, 0 )))) . (2 * PI ))) - ((( AffineMap ((1 / 2), 0 )) - ((1 / 4) (#) ( sin * ( AffineMap (2, 0 ))))) . 0 )) by Lm5, VALUED_1: 13

      .= (((( AffineMap ((1 / 2), 0 )) . (2 * PI )) - (((1 / 4) (#) ( sin * ( AffineMap (2, 0 )))) . (2 * PI ))) - ((( AffineMap ((1 / 2), 0 )) . 0 ) - (((1 / 4) (#) ( sin * ( AffineMap (2, 0 )))) . 0 ))) by Lm5, VALUED_1: 13, Lm6

      .= (((((1 / 2) * (2 * PI )) + 0 ) - (((1 / 4) (#) ( sin * ( AffineMap (2, 0 )))) . (2 * PI ))) - ((( AffineMap ((1 / 2), 0 )) . 0 ) - (((1 / 4) (#) ( sin * ( AffineMap (2, 0 )))) . 0 ))) by FCONT_1:def 4

      .= ((((1 / 2) * (2 * PI )) - ((1 / 4) * (( sin * ( AffineMap (2, 0 ))) . (2 * PI )))) - ((( AffineMap ((1 / 2), 0 )) . 0 ) - (((1 / 4) (#) ( sin * ( AffineMap (2, 0 )))) . 0 ))) by VALUED_1: 6

      .= ((((1 / 2) * (2 * PI )) - ((1 / 4) * ( sin . (( AffineMap (2, 0 )) . dp)))) - ((( AffineMap ((1 / 2), 0 )) . 0 ) - (((1 / 4) (#) ( sin * ( AffineMap (2, 0 )))) . 0 ))) by Lm4, FUNCT_1: 13

      .= ((((1 / 2) * (2 * PI )) - ((1 / 4) * ( sin . ddp))) - ((( AffineMap ((1 / 2), 0 )) . 0 ) - (((1 / 4) (#) ( sin * ( AffineMap (2, 0 )))) . 0 ))) by FCONT_1:def 4

      .= ((((1 / 2) * (2 * PI )) - ((1 / 4) * ( sin . (((2 * 2) * PI ) + 0 )))) - ( 0 - (((1 / 4) (#) ( sin * ( AffineMap (2, 0 )))) . 0 ))) by FCONT_1: 48

      .= (((((1 / 2) * (2 * PI )) - ((1 / 4) * ( sin . (((2 * 2) * PI ) + 0 )))) - 0 ) + (((1 / 4) (#) ( sin * ( AffineMap (2, 0 )))) . 0 ))

      .= ((((1 / 2) * (2 * PI )) - ((1 / 4) * ( sin . (((2 * 2) * PI ) + 0 )))) + ((1 / 4) * (( sin * ( AffineMap (2, 0 ))) . 0 ))) by VALUED_1: 6

      .= ((((1 / 2) * (2 * PI )) - ((1 / 4) * ( sin . (((2 * 2) * PI ) + 0 )))) + ((1 / 4) * ( sin . (( AffineMap (2, 0 )) . 0 )))) by Lm4, Lm6, FUNCT_1: 13

      .= ((((1 / 2) * (2 * PI )) - ((1 / 4) * ( sin . ( 0 + ((2 * PI ) * 2))))) + ((1 / 4) * ( sin . 0 ))) by FCONT_1: 48

      .= ((((1 / 2) * (2 * PI )) - ((1 / 4) * ( sin . 0 ))) + ((1 / 4) * ( sin . 0 ))) by SIN_COS6: 8

      .= PI ;

      hence thesis;

    end;

    theorem :: INTEGR11:16

    

     Th16: ( integral (( cos ^2 ),A)) = (((( AffineMap ((1 / 2), 0 )) + ((1 / 4) (#) ( sin * ( AffineMap (2, 0 ))))) . ( upper_bound A)) - ((( AffineMap ((1 / 2), 0 )) + ((1 / 4) (#) ( sin * ( AffineMap (2, 0 ))))) . ( lower_bound A)))

    proof

      

       A1: for x be Element of REAL st x in ( dom ((( AffineMap ((1 / 2), 0 )) + ((1 / 4) (#) ( sin * ( AffineMap (2, 0 ))))) `| REAL )) holds (((( AffineMap ((1 / 2), 0 )) + ((1 / 4) (#) ( sin * ( AffineMap (2, 0 ))))) `| REAL ) . x) = (( cos ^2 ) . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom ((( AffineMap ((1 / 2), 0 )) + ((1 / 4) (#) ( sin * ( AffineMap (2, 0 ))))) `| REAL ));

        (((( AffineMap ((1 / 2), 0 )) + ((1 / 4) (#) ( sin * ( AffineMap (2, 0 ))))) `| REAL ) . x) = (( cos . x) ^2 ) by Th2

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

        hence thesis;

      end;

      

       A2: ( dom ( cos ^2 )) = REAL by SIN_COS: 24, VALUED_1: 11;

      then ( dom ((( AffineMap ((1 / 2), 0 )) + ((1 / 4) (#) ( sin * ( AffineMap (2, 0 ))))) `| REAL )) = ( dom ( cos ^2 )) by Th2, FDIFF_1:def 7;

      then

       A3: ((( AffineMap ((1 / 2), 0 )) + ((1 / 4) (#) ( sin * ( AffineMap (2, 0 ))))) `| REAL ) = ( cos ^2 ) by A1, PARTFUN1: 5;

      (( cos ^2 ) | A) is bounded by A2, INTEGRA5: 10;

      hence thesis by A2, A3, Th2, INTEGRA5: 11, INTEGRA5: 13;

    end;

    theorem :: INTEGR11:17

    A = [. 0 , PI .] implies ( integral (( cos ^2 ),A)) = ( PI / 2)

    proof

      assume A = [. 0 , PI .];

      then ( upper_bound A) = PI & ( lower_bound A) = 0 by INTEGRA8: 37;

      

      then ( integral (( cos ^2 ),A)) = (((( AffineMap ((1 / 2), 0 )) + ((1 / 4) (#) ( sin * ( AffineMap (2, 0 ))))) . PI ) - ((( AffineMap ((1 / 2), 0 )) + ((1 / 4) (#) ( sin * ( AffineMap (2, 0 ))))) . 0 )) by Th16

      .= (((( AffineMap ((1 / 2), 0 )) . PI ) + (((1 / 4) (#) ( sin * ( AffineMap (2, 0 )))) . pp)) - ((( AffineMap ((1 / 2), 0 )) + ((1 / 4) (#) ( sin * ( AffineMap (2, 0 ))))) . 0 )) by VALUED_1: 1

      .= (((( AffineMap ((1 / 2), 0 )) . PI ) + (((1 / 4) (#) ( sin * ( AffineMap (2, 0 )))) . PI )) - ((( AffineMap ((1 / 2), 0 )) . 0 ) + (((1 / 4) (#) ( sin * ( AffineMap (2, 0 )))) . 0 ))) by VALUED_1: 1, Lm6

      .= (((((1 / 2) * PI ) + 0 ) + (((1 / 4) (#) ( sin * ( AffineMap (2, 0 )))) . PI )) - ((( AffineMap ((1 / 2), 0 )) . 0 ) + (((1 / 4) (#) ( sin * ( AffineMap (2, 0 )))) . 0 ))) by FCONT_1:def 4

      .= ((((1 / 2) * PI ) + ((1 / 4) * (( sin * ( AffineMap (2, 0 ))) . PI ))) - ((( AffineMap ((1 / 2), 0 )) . 0 ) + (((1 / 4) (#) ( sin * ( AffineMap (2, 0 )))) . 0 ))) by VALUED_1: 6

      .= ((((1 / 2) * PI ) + ((1 / 4) * ( sin . (( AffineMap (2, 0 )) . pp)))) - ((( AffineMap ((1 / 2), 0 )) . 0 ) + (((1 / 4) (#) ( sin * ( AffineMap (2, 0 )))) . 0 ))) by Lm4, FUNCT_1: 13

      .= ((((1 / 2) * PI ) + ((1 / 4) * ( sin . ((2 * PI ) + 0 )))) - ((( AffineMap ((1 / 2), 0 )) . 0 ) + (((1 / 4) (#) ( sin * ( AffineMap (2, 0 )))) . 0 ))) by FCONT_1:def 4

      .= ((((1 / 2) * PI ) + ((1 / 4) * ( sin . ((2 * PI ) + 0 )))) - ( 0 + (((1 / 4) (#) ( sin * ( AffineMap (2, 0 )))) . 0 ))) by FCONT_1: 48

      .= ((((1 / 2) * PI ) + ((1 / 4) * ( sin . ((2 * PI ) + 0 )))) - ((1 / 4) * (( sin * ( AffineMap (2, 0 ))) . 0 ))) by VALUED_1: 6

      .= ((((1 / 2) * PI ) + ((1 / 4) * ( sin . ((2 * PI ) + 0 )))) - ((1 / 4) * ( sin . (( AffineMap (2, 0 )) . 0 )))) by Lm4, FUNCT_1: 13, Lm6

      .= ((((1 / 2) * PI ) + ((1 / 4) * ( sin . ( 0 + ((2 * PI ) * 1))))) - ((1 / 4) * ( sin . 0 ))) by FCONT_1: 48

      .= ((((1 / 2) * PI ) + ((1 / 4) * ( sin . 0 ))) - ((1 / 4) * ( sin . 0 ))) by SIN_COS6: 8

      .= ( PI / 2);

      hence thesis;

    end;

    theorem :: INTEGR11:18

    A = [. 0 , (2 * PI ).] implies ( integral (( cos ^2 ),A)) = PI

    proof

      assume A = [. 0 , (2 * PI ).];

      then ( upper_bound A) = (2 * PI ) & ( lower_bound A) = 0 by INTEGRA8: 37;

      

      then ( integral (( cos ^2 ),A)) = (((( AffineMap ((1 / 2), 0 )) + ((1 / 4) (#) ( sin * ( AffineMap (2, 0 ))))) . (2 * PI )) - ((( AffineMap ((1 / 2), 0 )) + ((1 / 4) (#) ( sin * ( AffineMap (2, 0 ))))) . 0 )) by Th16

      .= (((( AffineMap ((1 / 2), 0 )) . (2 * PI )) + (((1 / 4) (#) ( sin * ( AffineMap (2, 0 )))) . dp)) - ((( AffineMap ((1 / 2), 0 )) + ((1 / 4) (#) ( sin * ( AffineMap (2, 0 ))))) . 0 )) by VALUED_1: 1

      .= (((( AffineMap ((1 / 2), 0 )) . (2 * PI )) + (((1 / 4) (#) ( sin * ( AffineMap (2, 0 )))) . (2 * PI ))) - ((( AffineMap ((1 / 2), 0 )) . 0 ) + (((1 / 4) (#) ( sin * ( AffineMap (2, 0 )))) . 0 ))) by VALUED_1: 1, Lm6

      .= (((((1 / 2) * (2 * PI )) + 0 ) + (((1 / 4) (#) ( sin * ( AffineMap (2, 0 )))) . dp)) - ((( AffineMap ((1 / 2), 0 )) . 0 ) + (((1 / 4) (#) ( sin * ( AffineMap (2, 0 )))) . 0 ))) by FCONT_1:def 4

      .= ((((1 / 2) * (2 * PI )) + ((1 / 4) * (( sin * ( AffineMap (2, 0 ))) . (2 * PI )))) - ((( AffineMap ((1 / 2), 0 )) . 0 ) + (((1 / 4) (#) ( sin * ( AffineMap (2, 0 )))) . 0 ))) by VALUED_1: 6

      .= ((((1 / 2) * (2 * PI )) + ((1 / 4) * ( sin . (( AffineMap (2, 0 )) . dp)))) - ((( AffineMap ((1 / 2), 0 )) . 0 ) + (((1 / 4) (#) ( sin * ( AffineMap (2, 0 )))) . 0 ))) by Lm4, FUNCT_1: 13

      .= ((((1 / 2) * (2 * PI )) + ((1 / 4) * ( sin . ddp))) - ((( AffineMap ((1 / 2), 0 )) . 0 ) + (((1 / 4) (#) ( sin * ( AffineMap (2, 0 )))) . 0 ))) by FCONT_1:def 4

      .= ((((1 / 2) * (2 * PI )) + ((1 / 4) * ( sin . (((2 * 2) * PI ) + 0 )))) - ( 0 + (((1 / 4) (#) ( sin * ( AffineMap (2, 0 )))) . 0 ))) by FCONT_1: 48

      .= ((((1 / 2) * (2 * PI )) + ((1 / 4) * ( sin . (((2 * 2) * PI ) + 0 )))) - ((1 / 4) * (( sin * ( AffineMap (2, 0 ))) . 0 ))) by VALUED_1: 6

      .= ((((1 / 2) * (2 * PI )) + ((1 / 4) * ( sin . (((2 * 2) * PI ) + 0 )))) - ((1 / 4) * ( sin . (( AffineMap (2, 0 )) . 0 )))) by Lm4, FUNCT_1: 13, Lm6

      .= ((((1 / 2) * (2 * PI )) + ((1 / 4) * ( sin . ( 0 + ((2 * PI ) * 2))))) - ((1 / 4) * ( sin . 0 ))) by FCONT_1: 48

      .= ((((1 / 2) * (2 * PI )) + ((1 / 4) * ( sin . 0 ))) - ((1 / 4) * ( sin . 0 ))) by SIN_COS6: 8

      .= PI ;

      hence thesis;

    end;

    theorem :: INTEGR11:19

    

     Th19: ( integral (((( #Z n) * sin ) (#) cos ),A)) = ((((1 / (n + 1)) (#) (( #Z (n + 1)) * sin )) . ( upper_bound A)) - (((1 / (n + 1)) (#) (( #Z (n + 1)) * sin )) . ( lower_bound A)))

    proof

      

       A1: ( [#] REAL ) = ( dom ((( #Z n) * sin ) (#) cos )) by FUNCT_2:def 1;

      

       A2: for x be Element of REAL st x in ( dom (((1 / (n + 1)) (#) (( #Z (n + 1)) * sin )) `| REAL )) holds ((((1 / (n + 1)) (#) (( #Z (n + 1)) * sin )) `| REAL ) . x) = (((( #Z n) * sin ) (#) cos ) . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom (((1 / (n + 1)) (#) (( #Z (n + 1)) * sin )) `| REAL ));

        ((((1 / (n + 1)) (#) (( #Z (n + 1)) * sin )) `| REAL ) . x) = ((( sin . x) #Z n) * ( cos . x)) by Th3

        .= ((( #Z n) . ( sin . x)) * ( cos . x)) by TAYLOR_1:def 1

        .= (((( #Z n) * sin ) . x) * ( cos . x)) by FUNCT_1: 13, SIN_COS: 24

        .= (((( #Z n) * sin ) (#) cos ) . x) by A1, VALUED_1:def 4;

        hence thesis;

      end;

      (( #Z n) * sin ) is_differentiable_in x0

      proof

         sin is_differentiable_in x0 by SIN_COS: 64;

        hence thesis by TAYLOR_1: 3;

      end;

      then ( dom (( #Z n) * sin )) = REAL & for x0 st x0 in REAL holds (( #Z n) * sin ) is_differentiable_in x0 by FUNCT_2:def 1;

      then (( #Z n) * sin ) is_differentiable_on REAL by A1, FDIFF_1: 9;

      then

       A3: (((( #Z n) * sin ) (#) cos ) | REAL ) is continuous by A1, FDIFF_1: 21, FDIFF_1: 25, SIN_COS: 67;

      then (((( #Z n) * sin ) (#) cos ) | A) is continuous by FCONT_1: 16;

      then

       A4: ((( #Z n) * sin ) (#) cos ) is_integrable_on A by A1, INTEGRA5: 11;

      ((1 / (n + 1)) (#) (( #Z (n + 1)) * sin )) is_differentiable_on REAL by Th3;

      then ( dom (((1 / (n + 1)) (#) (( #Z (n + 1)) * sin )) `| REAL )) = ( dom ((( #Z n) * sin ) (#) cos )) by A1, FDIFF_1:def 7;

      then

       A5: (((1 / (n + 1)) (#) (( #Z (n + 1)) * sin )) `| REAL ) = ((( #Z n) * sin ) (#) cos ) by A2, PARTFUN1: 5;

      (((( #Z n) * sin ) (#) cos ) | A) is bounded by A1, A3, INTEGRA5: 10;

      hence thesis by A4, A5, Th3, INTEGRA5: 13;

    end;

    theorem :: INTEGR11:20

    A = [. 0 , PI .] implies ( integral (((( #Z n) * sin ) (#) cos ),A)) = 0

    proof

      assume A = [. 0 , PI .];

      then ( upper_bound A) = PI & ( lower_bound A) = 0 by INTEGRA8: 37;

      

      then ( integral (((( #Z n) * sin ) (#) cos ),A)) = ((((1 / (n + 1)) (#) (( #Z (n + 1)) * sin )) . PI ) - (((1 / (n + 1)) (#) (( #Z (n + 1)) * sin )) . 0 )) by Th19

      .= (((1 / (n + 1)) * ((( #Z (n + 1)) * sin ) . PI )) - (((1 / (n + 1)) (#) (( #Z (n + 1)) * sin )) . 0 )) by VALUED_1: 6

      .= (((1 / (n + 1)) * ((( #Z (n + 1)) * sin ) . PI )) - ((1 / (n + 1)) * ((( #Z (n + 1)) * sin ) . 0 ))) by VALUED_1: 6

      .= (((1 / (n + 1)) * (( #Z (n + 1)) . ( sin . pp))) - ((1 / (n + 1)) * ((( #Z (n + 1)) * sin ) . 0 ))) by FUNCT_1: 13, SIN_COS: 24

      .= (((1 / (n + 1)) * (( #Z (n + 1)) . ( sin . PI ))) - ((1 / (n + 1)) * (( #Z (n + 1)) . ( sin . 0 )))) by FUNCT_1: 13, SIN_COS: 24, Lm6

      .= 0 by SIN_COS: 30, SIN_COS: 76;

      hence thesis;

    end;

    theorem :: INTEGR11:21

    A = [. 0 , (2 * PI ).] implies ( integral (((( #Z n) * sin ) (#) cos ),A)) = 0

    proof

      assume A = [. 0 , (2 * PI ).];

      then ( upper_bound A) = (2 * PI ) & ( lower_bound A) = 0 by INTEGRA8: 37;

      

      then ( integral (((( #Z n) * sin ) (#) cos ),A)) = ((((1 / (n + 1)) (#) (( #Z (n + 1)) * sin )) . (2 * PI )) - (((1 / (n + 1)) (#) (( #Z (n + 1)) * sin )) . 0 )) by Th19

      .= (((1 / (n + 1)) * ((( #Z (n + 1)) * sin ) . (2 * PI ))) - (((1 / (n + 1)) (#) (( #Z (n + 1)) * sin )) . 0 )) by VALUED_1: 6

      .= (((1 / (n + 1)) * ((( #Z (n + 1)) * sin ) . dp)) - ((1 / (n + 1)) * ((( #Z (n + 1)) * sin ) . 0 ))) by VALUED_1: 6

      .= (((1 / (n + 1)) * (( #Z (n + 1)) . ( sin . (2 * PI )))) - ((1 / (n + 1)) * ((( #Z (n + 1)) * sin ) . 0 ))) by FUNCT_1: 13, SIN_COS: 24

      .= (((1 / (n + 1)) * (( #Z (n + 1)) . ( sin . (2 * PI )))) - ((1 / (n + 1)) * (( #Z (n + 1)) . ( sin . 0 )))) by FUNCT_1: 13, SIN_COS: 24, Lm6

      .= 0 by SIN_COS: 30, SIN_COS: 76;

      hence thesis;

    end;

    theorem :: INTEGR11:22

    

     Th22: ( integral (((( #Z n) * cos ) (#) sin ),A)) = (((( - (1 / (n + 1))) (#) (( #Z (n + 1)) * cos )) . ( upper_bound A)) - ((( - (1 / (n + 1))) (#) (( #Z (n + 1)) * cos )) . ( lower_bound A)))

    proof

      

       A1: ( [#] REAL ) = ( dom ((( #Z n) * cos ) (#) sin )) by FUNCT_2:def 1;

      

       A2: for x be Element of REAL st x in ( dom ((( - (1 / (n + 1))) (#) (( #Z (n + 1)) * cos )) `| REAL )) holds (((( - (1 / (n + 1))) (#) (( #Z (n + 1)) * cos )) `| REAL ) . x) = (((( #Z n) * cos ) (#) sin ) . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom ((( - (1 / (n + 1))) (#) (( #Z (n + 1)) * cos )) `| REAL ));

        (((( - (1 / (n + 1))) (#) (( #Z (n + 1)) * cos )) `| REAL ) . x) = ((( cos . x) #Z n) * ( sin . x)) by Th4

        .= ((( #Z n) . ( cos . x)) * ( sin . x)) by TAYLOR_1:def 1

        .= (((( #Z n) * cos ) . x) * ( sin . x)) by FUNCT_1: 13, SIN_COS: 24

        .= (((( #Z n) * cos ) (#) sin ) . x) by A1, VALUED_1:def 4;

        hence thesis;

      end;

      (( #Z n) * cos ) is_differentiable_in x0

      proof

         cos is_differentiable_in x0 by SIN_COS: 63;

        hence thesis by TAYLOR_1: 3;

      end;

      then ( dom (( #Z n) * cos )) = REAL & for x0 st x0 in REAL holds (( #Z n) * cos ) is_differentiable_in x0 by FUNCT_2:def 1;

      then (( #Z n) * cos ) is_differentiable_on REAL by A1, FDIFF_1: 9;

      then

       A3: (((( #Z n) * cos ) (#) sin ) | REAL ) is continuous by A1, FDIFF_1: 21, FDIFF_1: 25, SIN_COS: 68;

      then (((( #Z n) * cos ) (#) sin ) | A) is continuous by FCONT_1: 16;

      then

       A4: ((( #Z n) * cos ) (#) sin ) is_integrable_on A by A1, INTEGRA5: 11;

      (( - (1 / (n + 1))) (#) (( #Z (n + 1)) * cos )) is_differentiable_on REAL by Th4;

      then ( dom ((( - (1 / (n + 1))) (#) (( #Z (n + 1)) * cos )) `| REAL )) = ( dom ((( #Z n) * cos ) (#) sin )) by A1, FDIFF_1:def 7;

      then

       A5: ((( - (1 / (n + 1))) (#) (( #Z (n + 1)) * cos )) `| REAL ) = ((( #Z n) * cos ) (#) sin ) by A2, PARTFUN1: 5;

      (((( #Z n) * cos ) (#) sin ) | A) is bounded by A1, A3, INTEGRA5: 10;

      hence thesis by A4, A5, Th4, INTEGRA5: 13;

    end;

    theorem :: INTEGR11:23

    A = [. 0 , (2 * PI ).] implies ( integral (((( #Z n) * cos ) (#) sin ),A)) = 0

    proof

      assume A = [. 0 , (2 * PI ).];

      then ( upper_bound A) = (2 * PI ) & ( lower_bound A) = 0 by INTEGRA8: 37;

      

      then ( integral (((( #Z n) * cos ) (#) sin ),A)) = (((( - (1 / (n + 1))) (#) (( #Z (n + 1)) * cos )) . (2 * PI )) - ((( - (1 / (n + 1))) (#) (( #Z (n + 1)) * cos )) . 0 )) by Th22

      .= ((( - (1 / (n + 1))) * ((( #Z (n + 1)) * cos ) . (2 * PI ))) - ((( - (1 / (n + 1))) (#) (( #Z (n + 1)) * cos )) . 0 )) by VALUED_1: 6

      .= ((( - (1 / (n + 1))) * ((( #Z (n + 1)) * cos ) . (2 * PI ))) - (( - (1 / (n + 1))) * ((( #Z (n + 1)) * cos ) . 0 ))) by VALUED_1: 6

      .= ((( - (1 / (n + 1))) * (( #Z (n + 1)) . ( cos . dp))) - (( - (1 / (n + 1))) * ((( #Z (n + 1)) * cos ) . 0 ))) by FUNCT_1: 13, SIN_COS: 24

      .= ((( - (1 / (n + 1))) * (( #Z (n + 1)) . ( cos . (2 * PI )))) - (( - (1 / (n + 1))) * (( #Z (n + 1)) . ( cos . 0 )))) by FUNCT_1: 13, SIN_COS: 24, Lm6

      .= 0 by SIN_COS: 30, SIN_COS: 76;

      hence thesis;

    end;

    reconsider pd = ( PI / 2), mpd = ( - ( PI / 2)) as Element of REAL by XREAL_0:def 1;

    theorem :: INTEGR11:24

    A = [.( - ( PI / 2)), ( PI / 2).] implies ( integral (((( #Z n) * cos ) (#) sin ),A)) = 0

    proof

      assume A = [.( - ( PI / 2)), ( PI / 2).];

      then ( upper_bound A) = ( PI / 2) & ( lower_bound A) = ( - ( PI / 2)) by INTEGRA8: 37;

      

      then ( integral (((( #Z n) * cos ) (#) sin ),A)) = (((( - (1 / (n + 1))) (#) (( #Z (n + 1)) * cos )) . ( PI / 2)) - ((( - (1 / (n + 1))) (#) (( #Z (n + 1)) * cos )) . ( - ( PI / 2)))) by Th22

      .= ((( - (1 / (n + 1))) * ((( #Z (n + 1)) * cos ) . ( PI / 2))) - ((( - (1 / (n + 1))) (#) (( #Z (n + 1)) * cos )) . ( - ( PI / 2)))) by VALUED_1: 6

      .= ((( - (1 / (n + 1))) * ((( #Z (n + 1)) * cos ) . ( PI / 2))) - (( - (1 / (n + 1))) * ((( #Z (n + 1)) * cos ) . ( - ( PI / 2))))) by VALUED_1: 6

      .= ((( - (1 / (n + 1))) * (( #Z (n + 1)) . ( cos . pd))) - (( - (1 / (n + 1))) * ((( #Z (n + 1)) * cos ) . mpd))) by FUNCT_1: 13, SIN_COS: 24

      .= ((( - (1 / (n + 1))) * (( #Z (n + 1)) . ( cos . pd))) - (( - (1 / (n + 1))) * (( #Z (n + 1)) . ( cos . ( - ( PI / 2)))))) by FUNCT_1: 13, SIN_COS: 24

      .= ((( - (1 / (n + 1))) * (( #Z (n + 1)) . ( cos . ( PI / 2)))) - (( - (1 / (n + 1))) * (( #Z (n + 1)) . ( cos . ( PI / 2))))) by SIN_COS: 30

      .= 0 ;

      hence thesis;

    end;

    theorem :: INTEGR11:25

    (m + n) <> 0 & (m - n) <> 0 implies ( integral ((( cos * ( AffineMap (m, 0 ))) (#) ( cos * ( AffineMap (n, 0 )))),A)) = (((((1 / (2 * (m + n))) (#) ( sin * ( AffineMap ((m + n), 0 )))) + ((1 / (2 * (m - n))) (#) ( sin * ( AffineMap ((m - n), 0 ))))) . ( upper_bound A)) - ((((1 / (2 * (m + n))) (#) ( sin * ( AffineMap ((m + n), 0 )))) + ((1 / (2 * (m - n))) (#) ( sin * ( AffineMap ((m - n), 0 ))))) . ( lower_bound A)))

    proof

      assume

       A1: (m + n) <> 0 & (m - n) <> 0 ;

      

       A2: for x st x in REAL holds (( AffineMap (n, 0 )) . x) = (n * x)

      proof

        let x;

        assume x in REAL ;

        (( AffineMap (n, 0 )) . x) = ((n * x) + 0 ) by FCONT_1:def 4

        .= (n * x);

        hence thesis;

      end;

      

       A3: ( dom ( cos * ( AffineMap (n, 0 )))) = ( [#] REAL ) by FUNCT_2:def 1;

      

       A4: ( dom ( cos * ( AffineMap (m, 0 )))) = ( [#] REAL ) by FUNCT_2:def 1;

      

       A5: for x st x in REAL holds (( AffineMap (m, 0 )) . x) = (m * x)

      proof

        let x;

        assume x in REAL ;

        (( AffineMap (m, 0 )) . x) = ((m * x) + 0 ) by FCONT_1:def 4

        .= (m * x);

        hence thesis;

      end;

      

       A6: for x be Element of REAL st x in ( dom ((((1 / (2 * (m + n))) (#) ( sin * ( AffineMap ((m + n), 0 )))) + ((1 / (2 * (m - n))) (#) ( sin * ( AffineMap ((m - n), 0 ))))) `| REAL )) holds (((((1 / (2 * (m + n))) (#) ( sin * ( AffineMap ((m + n), 0 )))) + ((1 / (2 * (m - n))) (#) ( sin * ( AffineMap ((m - n), 0 ))))) `| REAL ) . x) = ((( cos * ( AffineMap (m, 0 ))) (#) ( cos * ( AffineMap (n, 0 )))) . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom ((((1 / (2 * (m + n))) (#) ( sin * ( AffineMap ((m + n), 0 )))) + ((1 / (2 * (m - n))) (#) ( sin * ( AffineMap ((m - n), 0 ))))) `| REAL ));

        (((((1 / (2 * (m + n))) (#) ( sin * ( AffineMap ((m + n), 0 )))) + ((1 / (2 * (m - n))) (#) ( sin * ( AffineMap ((m - n), 0 ))))) `| REAL ) . x) = (( cos . (m * x)) * ( cos . (n * x))) by A1, Th5

        .= (( cos . (( AffineMap (m, 0 )) . x)) * ( cos . (n * x))) by A5

        .= (( cos . (( AffineMap (m, 0 )) . x)) * ( cos . (( AffineMap (n, 0 )) . x))) by A2

        .= ((( cos * ( AffineMap (m, 0 ))) . x) * ( cos . (( AffineMap (n, 0 )) . x))) by A4, FUNCT_1: 12

        .= ((( cos * ( AffineMap (m, 0 ))) . x) * (( cos * ( AffineMap (n, 0 ))) . x)) by A3, FUNCT_1: 12

        .= ((( cos * ( AffineMap (m, 0 ))) (#) ( cos * ( AffineMap (n, 0 )))) . x) by VALUED_1: 5;

        hence thesis;

      end;

      

       A7: ( [#] REAL ) = ( dom (( cos * ( AffineMap (m, 0 ))) (#) ( cos * ( AffineMap (n, 0 ))))) by FUNCT_2:def 1;

      (((1 / (2 * (m + n))) (#) ( sin * ( AffineMap ((m + n), 0 )))) + ((1 / (2 * (m - n))) (#) ( sin * ( AffineMap ((m - n), 0 ))))) is_differentiable_on REAL by A1, Th5;

      then ( dom ((((1 / (2 * (m + n))) (#) ( sin * ( AffineMap ((m + n), 0 )))) + ((1 / (2 * (m - n))) (#) ( sin * ( AffineMap ((m - n), 0 ))))) `| REAL )) = ( dom (( cos * ( AffineMap (m, 0 ))) (#) ( cos * ( AffineMap (n, 0 ))))) by A7, FDIFF_1:def 7;

      then

       A8: ((((1 / (2 * (m + n))) (#) ( sin * ( AffineMap ((m + n), 0 )))) + ((1 / (2 * (m - n))) (#) ( sin * ( AffineMap ((m - n), 0 ))))) `| REAL ) = (( cos * ( AffineMap (m, 0 ))) (#) ( cos * ( AffineMap (n, 0 )))) by A6, PARTFUN1: 5;

      ((( cos * ( AffineMap (m, 0 ))) (#) ( cos * ( AffineMap (n, 0 )))) | A) is continuous;

      then

       A9: (( cos * ( AffineMap (m, 0 ))) (#) ( cos * ( AffineMap (n, 0 )))) is_integrable_on A by A7, INTEGRA5: 11;

      ((( cos * ( AffineMap (m, 0 ))) (#) ( cos * ( AffineMap (n, 0 )))) | A) is bounded by A7, INTEGRA5: 10;

      hence thesis by A1, A9, A8, Th5, INTEGRA5: 13;

    end;

    theorem :: INTEGR11:26

    (m + n) <> 0 & (m - n) <> 0 implies ( integral ((( sin * ( AffineMap (m, 0 ))) (#) ( sin * ( AffineMap (n, 0 )))),A)) = (((((1 / (2 * (m - n))) (#) ( sin * ( AffineMap ((m - n), 0 )))) - ((1 / (2 * (m + n))) (#) ( sin * ( AffineMap ((m + n), 0 ))))) . ( upper_bound A)) - ((((1 / (2 * (m - n))) (#) ( sin * ( AffineMap ((m - n), 0 )))) - ((1 / (2 * (m + n))) (#) ( sin * ( AffineMap ((m + n), 0 ))))) . ( lower_bound A)))

    proof

      assume

       A1: (m + n) <> 0 & (m - n) <> 0 ;

      

       A2: for x st x in REAL holds (( AffineMap (n, 0 )) . x) = (n * x)

      proof

        let x;

        assume x in REAL ;

        (( AffineMap (n, 0 )) . x) = ((n * x) + 0 ) by FCONT_1:def 4

        .= (n * x);

        hence thesis;

      end;

      

       A3: ( dom ( sin * ( AffineMap (n, 0 )))) = ( [#] REAL ) by FUNCT_2:def 1;

      

       A4: ( dom ( sin * ( AffineMap (m, 0 )))) = ( [#] REAL ) by FUNCT_2:def 1;

      

       A5: for x st x in REAL holds (( AffineMap (m, 0 )) . x) = (m * x)

      proof

        let x;

        assume x in REAL ;

        (( AffineMap (m, 0 )) . x) = ((m * x) + 0 ) by FCONT_1:def 4

        .= (m * x);

        hence thesis;

      end;

      

       A6: for x be Element of REAL st x in ( dom ((((1 / (2 * (m - n))) (#) ( sin * ( AffineMap ((m - n), 0 )))) - ((1 / (2 * (m + n))) (#) ( sin * ( AffineMap ((m + n), 0 ))))) `| REAL )) holds (((((1 / (2 * (m - n))) (#) ( sin * ( AffineMap ((m - n), 0 )))) - ((1 / (2 * (m + n))) (#) ( sin * ( AffineMap ((m + n), 0 ))))) `| REAL ) . x) = ((( sin * ( AffineMap (m, 0 ))) (#) ( sin * ( AffineMap (n, 0 )))) . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom ((((1 / (2 * (m - n))) (#) ( sin * ( AffineMap ((m - n), 0 )))) - ((1 / (2 * (m + n))) (#) ( sin * ( AffineMap ((m + n), 0 ))))) `| REAL ));

        (((((1 / (2 * (m - n))) (#) ( sin * ( AffineMap ((m - n), 0 )))) - ((1 / (2 * (m + n))) (#) ( sin * ( AffineMap ((m + n), 0 ))))) `| REAL ) . x) = (( sin . (m * x)) * ( sin . (n * x))) by A1, Th6

        .= (( sin . (( AffineMap (m, 0 )) . x)) * ( sin . (n * x))) by A5

        .= (( sin . (( AffineMap (m, 0 )) . x)) * ( sin . (( AffineMap (n, 0 )) . x))) by A2

        .= ((( sin * ( AffineMap (m, 0 ))) . x) * ( sin . (( AffineMap (n, 0 )) . x))) by A4, FUNCT_1: 12

        .= ((( sin * ( AffineMap (m, 0 ))) . x) * (( sin * ( AffineMap (n, 0 ))) . x)) by A3, FUNCT_1: 12

        .= ((( sin * ( AffineMap (m, 0 ))) (#) ( sin * ( AffineMap (n, 0 )))) . x) by VALUED_1: 5;

        hence thesis;

      end;

      

       A7: REAL = ( dom (( sin * ( AffineMap (m, 0 ))) (#) ( sin * ( AffineMap (n, 0 ))))) by FUNCT_2:def 1;

      ((( sin * ( AffineMap (m, 0 ))) (#) ( sin * ( AffineMap (n, 0 )))) | A) is continuous;

      then

       A8: (( sin * ( AffineMap (m, 0 ))) (#) ( sin * ( AffineMap (n, 0 )))) is_integrable_on A by A7, INTEGRA5: 11;

      (((1 / (2 * (m - n))) (#) ( sin * ( AffineMap ((m - n), 0 )))) - ((1 / (2 * (m + n))) (#) ( sin * ( AffineMap ((m + n), 0 ))))) is_differentiable_on REAL by A1, Th6;

      then ( dom ((((1 / (2 * (m - n))) (#) ( sin * ( AffineMap ((m - n), 0 )))) - ((1 / (2 * (m + n))) (#) ( sin * ( AffineMap ((m + n), 0 ))))) `| REAL )) = ( dom (( sin * ( AffineMap (m, 0 ))) (#) ( sin * ( AffineMap (n, 0 ))))) by A7, FDIFF_1:def 7;

      then

       A9: ((((1 / (2 * (m - n))) (#) ( sin * ( AffineMap ((m - n), 0 )))) - ((1 / (2 * (m + n))) (#) ( sin * ( AffineMap ((m + n), 0 ))))) `| REAL ) = (( sin * ( AffineMap (m, 0 ))) (#) ( sin * ( AffineMap (n, 0 )))) by A6, PARTFUN1: 5;

      ((( sin * ( AffineMap (m, 0 ))) (#) ( sin * ( AffineMap (n, 0 )))) | A) is bounded by A7, INTEGRA5: 10;

      hence thesis by A1, A8, A9, Th6, INTEGRA5: 13;

    end;

    theorem :: INTEGR11:27

    (m + n) <> 0 & (m - n) <> 0 implies ( integral ((( sin * ( AffineMap (m, 0 ))) (#) ( cos * ( AffineMap (n, 0 )))),A)) = (((( - ((1 / (2 * (m + n))) (#) ( cos * ( AffineMap ((m + n), 0 ))))) - ((1 / (2 * (m - n))) (#) ( cos * ( AffineMap ((m - n), 0 ))))) . ( upper_bound A)) - ((( - ((1 / (2 * (m + n))) (#) ( cos * ( AffineMap ((m + n), 0 ))))) - ((1 / (2 * (m - n))) (#) ( cos * ( AffineMap ((m - n), 0 ))))) . ( lower_bound A)))

    proof

      assume

       A1: (m + n) <> 0 & (m - n) <> 0 ;

      

       A2: for x st x in REAL holds (( AffineMap (n, 0 )) . x) = (n * x)

      proof

        let x;

        assume x in REAL ;

        (( AffineMap (n, 0 )) . x) = ((n * x) + 0 ) by FCONT_1:def 4

        .= (n * x);

        hence thesis;

      end;

      

       A3: ( dom ( cos * ( AffineMap (n, 0 )))) = ( [#] REAL ) by FUNCT_2:def 1;

      

       A4: ( dom ( sin * ( AffineMap (m, 0 )))) = ( [#] REAL ) by FUNCT_2:def 1;

      

       A5: for x st x in REAL holds (( AffineMap (m, 0 )) . x) = (m * x)

      proof

        let x;

        assume x in REAL ;

        (( AffineMap (m, 0 )) . x) = ((m * x) + 0 ) by FCONT_1:def 4

        .= (m * x);

        hence thesis;

      end;

      

       A6: for x be Element of REAL st x in ( dom ((( - ((1 / (2 * (m + n))) (#) ( cos * ( AffineMap ((m + n), 0 ))))) - ((1 / (2 * (m - n))) (#) ( cos * ( AffineMap ((m - n), 0 ))))) `| REAL )) holds (((( - ((1 / (2 * (m + n))) (#) ( cos * ( AffineMap ((m + n), 0 ))))) - ((1 / (2 * (m - n))) (#) ( cos * ( AffineMap ((m - n), 0 ))))) `| REAL ) . x) = ((( sin * ( AffineMap (m, 0 ))) (#) ( cos * ( AffineMap (n, 0 )))) . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom ((( - ((1 / (2 * (m + n))) (#) ( cos * ( AffineMap ((m + n), 0 ))))) - ((1 / (2 * (m - n))) (#) ( cos * ( AffineMap ((m - n), 0 ))))) `| REAL ));

        (((( - ((1 / (2 * (m + n))) (#) ( cos * ( AffineMap ((m + n), 0 ))))) - ((1 / (2 * (m - n))) (#) ( cos * ( AffineMap ((m - n), 0 ))))) `| REAL ) . x) = (( sin . (m * x)) * ( cos . (n * x))) by A1, Th7

        .= (( sin . (( AffineMap (m, 0 )) . x)) * ( cos . (n * x))) by A5

        .= (( sin . (( AffineMap (m, 0 )) . x)) * ( cos . (( AffineMap (n, 0 )) . x))) by A2

        .= ((( sin * ( AffineMap (m, 0 ))) . x) * ( cos . (( AffineMap (n, 0 )) . x))) by A4, FUNCT_1: 12

        .= ((( sin * ( AffineMap (m, 0 ))) . x) * (( cos * ( AffineMap (n, 0 ))) . x)) by A3, FUNCT_1: 12

        .= ((( sin * ( AffineMap (m, 0 ))) (#) ( cos * ( AffineMap (n, 0 )))) . x) by VALUED_1: 5;

        hence thesis;

      end;

      

       A7: ( [#] REAL ) = ( dom (( sin * ( AffineMap (m, 0 ))) (#) ( cos * ( AffineMap (n, 0 ))))) by FUNCT_2:def 1;

      ((( sin * ( AffineMap (m, 0 ))) (#) ( cos * ( AffineMap (n, 0 )))) | A) is continuous;

      then

       A8: (( sin * ( AffineMap (m, 0 ))) (#) ( cos * ( AffineMap (n, 0 )))) is_integrable_on A by A7, INTEGRA5: 11;

      (( - ((1 / (2 * (m + n))) (#) ( cos * ( AffineMap ((m + n), 0 ))))) - ((1 / (2 * (m - n))) (#) ( cos * ( AffineMap ((m - n), 0 ))))) is_differentiable_on REAL by A1, Th7;

      then ( dom ((( - ((1 / (2 * (m + n))) (#) ( cos * ( AffineMap ((m + n), 0 ))))) - ((1 / (2 * (m - n))) (#) ( cos * ( AffineMap ((m - n), 0 ))))) `| REAL )) = ( dom (( sin * ( AffineMap (m, 0 ))) (#) ( cos * ( AffineMap (n, 0 ))))) by A7, FDIFF_1:def 7;

      then

       A9: ((( - ((1 / (2 * (m + n))) (#) ( cos * ( AffineMap ((m + n), 0 ))))) - ((1 / (2 * (m - n))) (#) ( cos * ( AffineMap ((m - n), 0 ))))) `| REAL ) = (( sin * ( AffineMap (m, 0 ))) (#) ( cos * ( AffineMap (n, 0 )))) by A6, PARTFUN1: 5;

      ((( sin * ( AffineMap (m, 0 ))) (#) ( cos * ( AffineMap (n, 0 )))) | A) is bounded by A7, INTEGRA5: 10;

      hence thesis by A1, A8, A9, Th7, INTEGRA5: 13;

    end;

    theorem :: INTEGR11:28

    n <> 0 implies ( integral ((( AffineMap (1, 0 )) (#) ( sin * ( AffineMap (n, 0 )))),A)) = (((((1 / (n ^2 )) (#) ( sin * ( AffineMap (n, 0 )))) - (( AffineMap ((1 / n), 0 )) (#) ( cos * ( AffineMap (n, 0 ))))) . ( upper_bound A)) - ((((1 / (n ^2 )) (#) ( sin * ( AffineMap (n, 0 )))) - (( AffineMap ((1 / n), 0 )) (#) ( cos * ( AffineMap (n, 0 ))))) . ( lower_bound A)))

    proof

      assume

       A1: n <> 0 ;

      

       A2: for x st x in REAL holds (( AffineMap (n, 0 )) . x) = (n * x)

      proof

        let x;

        assume x in REAL ;

        (( AffineMap (n, 0 )) . x) = ((n * x) + 0 ) by FCONT_1:def 4

        .= (n * x);

        hence thesis;

      end;

      

       A3: ( dom ( sin * ( AffineMap (n, 0 )))) = ( [#] REAL ) by FUNCT_2:def 1;

      

       A4: for x st x in REAL holds (( AffineMap (1, 0 )) . x) = x

      proof

        let x;

        assume x in REAL ;

        (( AffineMap (1, 0 )) . x) = ((1 * x) + 0 ) by FCONT_1:def 4

        .= x;

        hence thesis;

      end;

      

       A5: for x be Element of REAL st x in ( dom ((((1 / (n ^2 )) (#) ( sin * ( AffineMap (n, 0 )))) - (( AffineMap ((1 / n), 0 )) (#) ( cos * ( AffineMap (n, 0 ))))) `| REAL )) holds (((((1 / (n ^2 )) (#) ( sin * ( AffineMap (n, 0 )))) - (( AffineMap ((1 / n), 0 )) (#) ( cos * ( AffineMap (n, 0 ))))) `| REAL ) . x) = ((( AffineMap (1, 0 )) (#) ( sin * ( AffineMap (n, 0 )))) . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom ((((1 / (n ^2 )) (#) ( sin * ( AffineMap (n, 0 )))) - (( AffineMap ((1 / n), 0 )) (#) ( cos * ( AffineMap (n, 0 ))))) `| REAL ));

        (((((1 / (n ^2 )) (#) ( sin * ( AffineMap (n, 0 )))) - (( AffineMap ((1 / n), 0 )) (#) ( cos * ( AffineMap (n, 0 ))))) `| REAL ) . x) = (x * ( sin . (n * x))) by A1, Th8

        .= (x * ( sin . (( AffineMap (n, 0 )) . x))) by A2

        .= (x * (( sin * ( AffineMap (n, 0 ))) . x)) by A3, FUNCT_1: 12

        .= ((( AffineMap (1, 0 )) . x) * (( sin * ( AffineMap (n, 0 ))) . x)) by A4

        .= ((( AffineMap (1, 0 )) (#) ( sin * ( AffineMap (n, 0 )))) . x) by VALUED_1: 5;

        hence thesis;

      end;

      

       A6: ( dom (( AffineMap (1, 0 )) (#) ( sin * ( AffineMap (n, 0 ))))) = ( [#] REAL ) by FUNCT_2:def 1;

      (((1 / (n ^2 )) (#) ( sin * ( AffineMap (n, 0 )))) - (( AffineMap ((1 / n), 0 )) (#) ( cos * ( AffineMap (n, 0 ))))) is_differentiable_on REAL by A1, Th8;

      then ( dom ((((1 / (n ^2 )) (#) ( sin * ( AffineMap (n, 0 )))) - (( AffineMap ((1 / n), 0 )) (#) ( cos * ( AffineMap (n, 0 ))))) `| REAL )) = ( dom (( AffineMap (1, 0 )) (#) ( sin * ( AffineMap (n, 0 ))))) by A6, FDIFF_1:def 7;

      then

       A7: ((((1 / (n ^2 )) (#) ( sin * ( AffineMap (n, 0 )))) - (( AffineMap ((1 / n), 0 )) (#) ( cos * ( AffineMap (n, 0 ))))) `| REAL ) = (( AffineMap (1, 0 )) (#) ( sin * ( AffineMap (n, 0 )))) by A5, PARTFUN1: 5;

      ((( AffineMap (1, 0 )) (#) ( sin * ( AffineMap (n, 0 )))) | A) is continuous;

      then

       A8: (( AffineMap (1, 0 )) (#) ( sin * ( AffineMap (n, 0 )))) is_integrable_on A by A6, INTEGRA5: 11;

      ((( AffineMap (1, 0 )) (#) ( sin * ( AffineMap (n, 0 )))) | A) is bounded by A6, INTEGRA5: 10;

      hence thesis by A1, A8, A7, Th8, INTEGRA5: 13;

    end;

    theorem :: INTEGR11:29

    n <> 0 implies ( integral ((( AffineMap (1, 0 )) (#) ( cos * ( AffineMap (n, 0 )))),A)) = (((((1 / (n ^2 )) (#) ( cos * ( AffineMap (n, 0 )))) + (( AffineMap ((1 / n), 0 )) (#) ( sin * ( AffineMap (n, 0 ))))) . ( upper_bound A)) - ((((1 / (n ^2 )) (#) ( cos * ( AffineMap (n, 0 )))) + (( AffineMap ((1 / n), 0 )) (#) ( sin * ( AffineMap (n, 0 ))))) . ( lower_bound A)))

    proof

      assume

       A1: n <> 0 ;

      

       A2: for x st x in REAL holds (( AffineMap (n, 0 )) . x) = (n * x)

      proof

        let x;

        assume x in REAL ;

        (( AffineMap (n, 0 )) . x) = ((n * x) + 0 ) by FCONT_1:def 4

        .= (n * x);

        hence thesis;

      end;

      

       A3: ( dom ( cos * ( AffineMap (n, 0 )))) = ( [#] REAL ) by FUNCT_2:def 1;

      

       A4: for x st x in REAL holds (( AffineMap (1, 0 )) . x) = x

      proof

        let x;

        assume x in REAL ;

        (( AffineMap (1, 0 )) . x) = ((1 * x) + 0 ) by FCONT_1:def 4

        .= x;

        hence thesis;

      end;

      

       A5: for x be Element of REAL st x in ( dom ((((1 / (n ^2 )) (#) ( cos * ( AffineMap (n, 0 )))) + (( AffineMap ((1 / n), 0 )) (#) ( sin * ( AffineMap (n, 0 ))))) `| REAL )) holds (((((1 / (n ^2 )) (#) ( cos * ( AffineMap (n, 0 )))) + (( AffineMap ((1 / n), 0 )) (#) ( sin * ( AffineMap (n, 0 ))))) `| REAL ) . x) = ((( AffineMap (1, 0 )) (#) ( cos * ( AffineMap (n, 0 )))) . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom ((((1 / (n ^2 )) (#) ( cos * ( AffineMap (n, 0 )))) + (( AffineMap ((1 / n), 0 )) (#) ( sin * ( AffineMap (n, 0 ))))) `| REAL ));

        (((((1 / (n ^2 )) (#) ( cos * ( AffineMap (n, 0 )))) + (( AffineMap ((1 / n), 0 )) (#) ( sin * ( AffineMap (n, 0 ))))) `| REAL ) . x) = (x * ( cos . (n * x))) by A1, Th9

        .= (x * ( cos . (( AffineMap (n, 0 )) . x))) by A2

        .= (x * (( cos * ( AffineMap (n, 0 ))) . x)) by A3, FUNCT_1: 12

        .= ((( AffineMap (1, 0 )) . x) * (( cos * ( AffineMap (n, 0 ))) . x)) by A4

        .= ((( AffineMap (1, 0 )) (#) ( cos * ( AffineMap (n, 0 )))) . x) by VALUED_1: 5;

        hence thesis;

      end;

      

       A6: ( dom (( AffineMap (1, 0 )) (#) ( cos * ( AffineMap (n, 0 ))))) = ( [#] REAL ) by FUNCT_2:def 1;

      (((1 / (n ^2 )) (#) ( cos * ( AffineMap (n, 0 )))) + (( AffineMap ((1 / n), 0 )) (#) ( sin * ( AffineMap (n, 0 ))))) is_differentiable_on REAL by A1, Th9;

      then ( dom ((((1 / (n ^2 )) (#) ( cos * ( AffineMap (n, 0 )))) + (( AffineMap ((1 / n), 0 )) (#) ( sin * ( AffineMap (n, 0 ))))) `| REAL )) = ( dom (( AffineMap (1, 0 )) (#) ( cos * ( AffineMap (n, 0 ))))) by A6, FDIFF_1:def 7;

      then

       A7: ((((1 / (n ^2 )) (#) ( cos * ( AffineMap (n, 0 )))) + (( AffineMap ((1 / n), 0 )) (#) ( sin * ( AffineMap (n, 0 ))))) `| REAL ) = (( AffineMap (1, 0 )) (#) ( cos * ( AffineMap (n, 0 )))) by A5, PARTFUN1: 5;

      ((( AffineMap (1, 0 )) (#) ( cos * ( AffineMap (n, 0 )))) | A) is continuous;

      then

       A8: (( AffineMap (1, 0 )) (#) ( cos * ( AffineMap (n, 0 )))) is_integrable_on A by A6, INTEGRA5: 11;

      ((( AffineMap (1, 0 )) (#) ( cos * ( AffineMap (n, 0 )))) | A) is bounded by A6, INTEGRA5: 10;

      hence thesis by A1, A8, A7, Th9, INTEGRA5: 13;

    end;

    theorem :: INTEGR11:30

    ( integral ((( AffineMap (1, 0 )) (#) sinh ),A)) = ((((( AffineMap (1, 0 )) (#) cosh ) - sinh ) . ( upper_bound A)) - (((( AffineMap (1, 0 )) (#) cosh ) - sinh ) . ( lower_bound A)))

    proof

      

       A1: for x be Element of REAL st x in ( dom (((( AffineMap (1, 0 )) (#) cosh ) - sinh ) `| REAL )) holds ((((( AffineMap (1, 0 )) (#) cosh ) - sinh ) `| REAL ) . x) = ((( AffineMap (1, 0 )) (#) sinh ) . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom (((( AffineMap (1, 0 )) (#) cosh ) - sinh ) `| REAL ));

        ((((( AffineMap (1, 0 )) (#) cosh ) - sinh ) `| REAL ) . x) = (((1 * x) + 0 ) * ( sinh . x)) by Th10

        .= ((( AffineMap (1, 0 )) . x) * ( sinh . x)) by FCONT_1:def 4

        .= ((( AffineMap (1, 0 )) (#) sinh ) . x) by VALUED_1: 5;

        hence thesis;

      end;

      

       A2: ( dom (( AffineMap (1, 0 )) (#) sinh )) = ( [#] REAL ) by FUNCT_2:def 1;

      then ( dom (((( AffineMap (1, 0 )) (#) cosh ) - sinh ) `| REAL )) = ( dom (( AffineMap (1, 0 )) (#) sinh )) by Th10, FDIFF_1:def 7;

      then

       A3: (((( AffineMap (1, 0 )) (#) cosh ) - sinh ) `| REAL ) = (( AffineMap (1, 0 )) (#) sinh ) by A1, PARTFUN1: 5;

      ( dom ( AffineMap (1, 0 ))) = ( [#] REAL ) & for x st x in REAL holds (( AffineMap (1, 0 )) . x) = ((1 * x) + 0 ) by FCONT_1:def 4, FUNCT_2:def 1;

      then ( AffineMap (1, 0 )) is_differentiable_on REAL by FDIFF_1: 23;

      then

       A4: ((( AffineMap (1, 0 )) (#) sinh ) | REAL ) is continuous by A2, FDIFF_1: 21, FDIFF_1: 25, SIN_COS2: 34;

      then

       A5: ((( AffineMap (1, 0 )) (#) sinh ) | A) is continuous by FCONT_1: 16;

      ((( AffineMap (1, 0 )) (#) sinh ) | A) is bounded by A2, A4, INTEGRA5: 10;

      hence thesis by A2, A5, A3, Th10, INTEGRA5: 11, INTEGRA5: 13;

    end;

    theorem :: INTEGR11:31

    ( integral ((( AffineMap (1, 0 )) (#) cosh ),A)) = ((((( AffineMap (1, 0 )) (#) sinh ) - cosh ) . ( upper_bound A)) - (((( AffineMap (1, 0 )) (#) sinh ) - cosh ) . ( lower_bound A)))

    proof

      

       A1: for x be Element of REAL st x in ( dom (((( AffineMap (1, 0 )) (#) sinh ) - cosh ) `| REAL )) holds ((((( AffineMap (1, 0 )) (#) sinh ) - cosh ) `| REAL ) . x) = ((( AffineMap (1, 0 )) (#) cosh ) . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom (((( AffineMap (1, 0 )) (#) sinh ) - cosh ) `| REAL ));

        ((((( AffineMap (1, 0 )) (#) sinh ) - cosh ) `| REAL ) . x) = (((1 * x) + 0 ) * ( cosh . x)) by Th11

        .= ((( AffineMap (1, 0 )) . x) * ( cosh . x)) by FCONT_1:def 4

        .= ((( AffineMap (1, 0 )) (#) cosh ) . x) by VALUED_1: 5;

        hence thesis;

      end;

      

       A2: ( dom (( AffineMap (1, 0 )) (#) cosh )) = ( [#] REAL ) by FUNCT_2:def 1;

      then ( dom (((( AffineMap (1, 0 )) (#) sinh ) - cosh ) `| REAL )) = ( dom (( AffineMap (1, 0 )) (#) cosh )) by Th11, FDIFF_1:def 7;

      then

       A3: (((( AffineMap (1, 0 )) (#) sinh ) - cosh ) `| REAL ) = (( AffineMap (1, 0 )) (#) cosh ) by A1, PARTFUN1: 5;

      ( dom ( AffineMap (1, 0 ))) = ( [#] REAL ) & for x st x in REAL holds (( AffineMap (1, 0 )) . x) = ((1 * x) + 0 ) by FCONT_1:def 4, FUNCT_2:def 1;

      then ( AffineMap (1, 0 )) is_differentiable_on REAL by FDIFF_1: 23;

      then

       A4: ((( AffineMap (1, 0 )) (#) cosh ) | REAL ) is continuous by A2, FDIFF_1: 21, FDIFF_1: 25, SIN_COS2: 35;

      then

       A5: ((( AffineMap (1, 0 )) (#) cosh ) | A) is continuous by FCONT_1: 16;

      ((( AffineMap (1, 0 )) (#) cosh ) | A) is bounded by A2, A4, INTEGRA5: 10;

      hence thesis by A2, A5, A3, Th11, INTEGRA5: 11, INTEGRA5: 13;

    end;

    theorem :: INTEGR11:32

    (a * (n + 1)) <> 0 implies ( integral ((( #Z n) * ( AffineMap (a,b))),A)) = ((((1 / (a * (n + 1))) (#) (( #Z (n + 1)) * ( AffineMap (a,b)))) . ( upper_bound A)) - (((1 / (a * (n + 1))) (#) (( #Z (n + 1)) * ( AffineMap (a,b)))) . ( lower_bound A)))

    proof

      assume

       A1: (a * (n + 1)) <> 0 ;

      

       A2: ( [#] REAL ) = ( dom ( AffineMap (a,b))) by FUNCT_2:def 1;

      

       A3: for x be Element of REAL st x in ( dom (((1 / (a * (n + 1))) (#) (( #Z (n + 1)) * ( AffineMap (a,b)))) `| REAL )) holds ((((1 / (a * (n + 1))) (#) (( #Z (n + 1)) * ( AffineMap (a,b)))) `| REAL ) . x) = ((( #Z n) * ( AffineMap (a,b))) . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom (((1 / (a * (n + 1))) (#) (( #Z (n + 1)) * ( AffineMap (a,b)))) `| REAL ));

        ((((1 / (a * (n + 1))) (#) (( #Z (n + 1)) * ( AffineMap (a,b)))) `| REAL ) . x) = (((a * x) + b) #Z n) by A1, Th12

        .= ((( AffineMap (a,b)) . x) #Z n) by FCONT_1:def 4

        .= (( #Z n) . (( AffineMap (a,b)) . x)) by TAYLOR_1:def 1

        .= ((( #Z n) * ( AffineMap (a,b))) . x) by A2, FUNCT_1: 13;

        hence thesis;

      end;

      

       A4: ( [#] REAL ) = ( dom (( #Z n) * ( AffineMap (a,b)))) by FUNCT_2:def 1;

      for x st x in REAL holds (( AffineMap (a,b)) . x) = ((a * x) + b) by FCONT_1:def 4;

      then

       A5: ( AffineMap (a,b)) is_differentiable_on REAL by A2, FDIFF_1: 23;

      (( #Z n) * ( AffineMap (a,b))) is_differentiable_in x

      proof

        x in REAL by XREAL_0:def 1;

        then ( AffineMap (a,b)) is_differentiable_in x by A2, A5, FDIFF_1: 9;

        hence thesis by TAYLOR_1: 3;

      end;

      then for x st x in REAL holds (( #Z n) * ( AffineMap (a,b))) is_differentiable_in x;

      then (( #Z n) * ( AffineMap (a,b))) is_differentiable_on REAL by A4, FDIFF_1: 9;

      then

       A6: ((( #Z n) * ( AffineMap (a,b))) | REAL ) is continuous by FDIFF_1: 25;

      then ((( #Z n) * ( AffineMap (a,b))) | A) is continuous by FCONT_1: 16;

      then

       A7: (( #Z n) * ( AffineMap (a,b))) is_integrable_on A by A4, INTEGRA5: 11;

      ((1 / (a * (n + 1))) (#) (( #Z (n + 1)) * ( AffineMap (a,b)))) is_differentiable_on REAL by A1, Th12;

      then ( dom (((1 / (a * (n + 1))) (#) (( #Z (n + 1)) * ( AffineMap (a,b)))) `| REAL )) = ( dom (( #Z n) * ( AffineMap (a,b)))) by A4, FDIFF_1:def 7;

      then

       A8: (((1 / (a * (n + 1))) (#) (( #Z (n + 1)) * ( AffineMap (a,b)))) `| REAL ) = (( #Z n) * ( AffineMap (a,b))) by A3, PARTFUN1: 5;

      ((( #Z n) * ( AffineMap (a,b))) | A) is bounded by A4, A6, INTEGRA5: 10;

      hence thesis by A1, A7, A8, Th12, INTEGRA5: 13;

    end;

    begin

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

    theorem :: INTEGR11:33

    

     Th33: Z c= ( dom ((1 / 2) (#) f)) & f = ( #Z 2) implies ((1 / 2) (#) f) is_differentiable_on Z & for x st x in Z holds ((((1 / 2) (#) f) `| Z) . x) = x

    proof

      assume that

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

       A2: f = ( #Z 2);

      Z c= ( dom f) & for x st x in Z holds f is_differentiable_in x by A1, A2, TAYLOR_1: 2, VALUED_1:def 5;

      then

       A3: f is_differentiable_on Z by FDIFF_1: 9;

      

       A4: for x st x in Z holds ((f `| Z) . x) = (2 * x)

      proof

        let x;

        (2 * (x #Z (2 - 1))) = (2 * x) by PREPOWER: 35;

        then

         A5: ( diff (f,x)) = (2 * x) by A2, TAYLOR_1: 2;

        assume x in Z;

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

      end;

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

      proof

        let x;

        assume

         A6: x in Z;

        

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

        .= ((1 / 2) * ((f `| Z) . x)) by A3, A6, FDIFF_1:def 7

        .= ((1 / 2) * (2 * x)) by A4, A6

        .= x;

        hence thesis;

      end;

      hence thesis by A1, A3, FDIFF_1: 20;

    end;

    theorem :: INTEGR11:34

    A c= Z & f = ( #Z 2) & Z = ( dom ((1 / 2) (#) f)) implies ( integral (( id Z),A)) = ((((1 / 2) (#) f) . ( upper_bound A)) - (((1 / 2) (#) f) . ( lower_bound A)))

    proof

      assume that

       A1: A c= Z and

       A2: f = ( #Z 2) & Z = ( dom ((1 / 2) (#) f));

      

       A3: A c= ( dom ( id Z)) by A1;

      then

       A4: (( id Z) | A) is bounded by INTEGRA5: 10;

      

       A5: ((1 / 2) (#) f) is_differentiable_on Z by A2, Th33;

      

       A6: for x be Element of REAL st x in ( dom (((1 / 2) (#) f) `| Z)) holds ((((1 / 2) (#) f) `| Z) . x) = (( id Z) . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom (((1 / 2) (#) f) `| Z));

        then

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

        

        then ((((1 / 2) (#) f) `| Z) . x) = x by A2, Th33

        .= (( id Z) . x) by A7, FUNCT_1: 18;

        hence thesis;

      end;

      ( dom (((1 / 2) (#) f) `| Z)) = ( dom ( id Z)) by A5, FDIFF_1:def 7;

      then

       A8: (((1 / 2) (#) f) `| Z) = ( id Z) by A6, PARTFUN1: 5;

      (( id Z) | A) is continuous;

      then ( id Z) is_integrable_on A by A3, INTEGRA5: 11;

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

    end;

    theorem :: INTEGR11:35

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

    proof

      set g = ( id Z);

      assume that

       A1: not 0 in Z and

       A2: A c= Z and

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

       A4: ( dom f) = Z and

       A5: (f | A) is continuous;

      

       A6: f is_integrable_on A by A2, A4, A5, INTEGRA5: 11;

      

       A7: (g ^ ) is_differentiable_on Z by A1, FDIFF_5: 4;

      

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

      proof

        let x be Element of REAL ;

        assume x in ( dom ((g ^ ) `| Z));

        then

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

        

        then (((g ^ ) `| Z) . x) = ( - (1 / (x ^2 ))) by A1, FDIFF_5: 4

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

        hence thesis;

      end;

      ( dom ((g ^ ) `| Z)) = ( dom f) by A4, A7, FDIFF_1:def 7;

      then ((g ^ ) `| Z) = f by A8, PARTFUN1: 5;

      hence thesis by A2, A4, A5, A6, A7, INTEGRA5: 10, INTEGRA5: 13;

    end;

    theorem :: INTEGR11:36

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

    proof

      assume that

       A1: A c= Z and

       A2: f1 = ( #Z 2) and

       A3: for x st x in Z holds (f2 . x) = 1 & x <> 0 & (f . x) = ((2 * x) / ((1 + (x ^2 )) ^2 )) and

       A4: ( dom (f1 / (f2 + f1))) = Z and

       A5: Z = ( dom f) and

       A6: (f | A) is continuous;

      

       A7: f is_integrable_on A by A1, A5, A6, INTEGRA5: 11;

      

       A8: for x st x in Z holds (f2 . x) = 1 & x <> 0 by A3;

      then

       A9: (f1 / (f2 + f1)) is_differentiable_on Z by A2, A4, FDIFF_6: 7;

      

       A10: for x be Element of REAL st x in ( dom ((f1 / (f2 + f1)) `| Z)) holds (((f1 / (f2 + f1)) `| Z) . x) = (f . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom ((f1 / (f2 + f1)) `| Z));

        then

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

        

        then (((f1 / (f2 + f1)) `| Z) . x) = ((2 * x) / ((1 + (x ^2 )) ^2 )) by A2, A4, A8, FDIFF_6: 7

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

        hence thesis;

      end;

      ( dom ((f1 / (f2 + f1)) `| Z)) = ( dom f) by A5, A9, FDIFF_1:def 7;

      then ((f1 / (f2 + f1)) `| Z) = f by A10, PARTFUN1: 5;

      hence thesis by A1, A5, A6, A7, A9, INTEGRA5: 10, INTEGRA5: 13;

    end;

    theorem :: INTEGR11:37

    

     Th37: (Z c= ( dom ( tan + sec )) & for x st x in Z holds (1 + ( sin . x)) <> 0 & (1 - ( sin . x)) <> 0 ) implies ( tan + sec ) is_differentiable_on Z & for x st x in Z holds ((( tan + sec ) `| Z) . x) = (1 / (1 - ( sin . x)))

    proof

      assume that

       A1: Z c= ( dom ( tan + sec )) and

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

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

      then

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

      then

       A4: for x st x in Z holds ( cos . x) <> 0 by FDIFF_8: 1;

      then

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

      for x st x in Z holds tan is_differentiable_in x

      proof

        let x;

        assume x in Z;

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

        hence thesis by FDIFF_7: 46;

      end;

      then

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

      for x st x in Z holds ((( tan + sec ) `| Z) . x) = (1 / (1 - ( sin . x)))

      proof

        let x;

        assume

         A7: x in Z;

        then

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

        

         A9: (1 + ( sin . x)) <> 0 by A2, A7;

        ((( tan + sec ) `| Z) . x) = (( diff ( tan ,x)) + ( diff (( cos ^ ),x))) by A1, A5, A6, A7, FDIFF_1: 18

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

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

        .= ((1 / (( cos . x) ^2 )) + (( sin . x) / (( cos . x) ^2 ))) by A4, A7, FDIFF_4: 39

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

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

        .= ((1 + ( sin . x)) / ((1 + ( sin . x)) * (1 - ( sin . x))))

        .= (((1 + ( sin . x)) / (1 + ( sin . x))) / (1 - ( sin . x))) by XCMPLX_1: 78

        .= (1 / (1 - ( sin . x))) by A9, XCMPLX_1: 60;

        hence thesis;

      end;

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

    end;

    theorem :: INTEGR11:38

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

    proof

      assume that

       A1: A c= Z and

       A2: for x st x in Z holds (1 + ( sin . x)) <> 0 & (1 - ( sin . x)) <> 0 & (f . x) = (1 / (1 - ( sin . x))) and

       A3: ( dom ( tan + sec )) = Z and

       A4: Z = ( dom f) and

       A5: (f | A) is continuous;

      

       A6: f is_integrable_on A by A1, A4, A5, INTEGRA5: 11;

      

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

      then

       A8: ( tan + sec ) is_differentiable_on Z by A3, Th37;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

        then ((( tan + sec ) `| Z) . x) = (1 / (1 - ( sin . x))) by A3, A7, Th37

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

        hence thesis;

      end;

      ( dom (( tan + sec ) `| Z)) = ( dom f) by A4, A8, FDIFF_1:def 7;

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

      hence thesis by A1, A4, A5, A6, A8, INTEGRA5: 10, INTEGRA5: 13;

    end;

    theorem :: INTEGR11:39

    

     Th39: (Z c= ( dom ( tan - sec )) & for x st x in Z holds (1 + ( sin . x)) <> 0 & (1 - ( sin . x)) <> 0 ) implies ( tan - sec ) is_differentiable_on Z & for x st x in Z holds ((( tan - sec ) `| Z) . x) = (1 / (1 + ( sin . x)))

    proof

      assume that

       A1: Z c= ( dom ( tan - sec )) and

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

      Z c= (( dom tan ) /\ ( dom ( cos ^ ))) by A1, VALUED_1: 12;

      then

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

      then

       A4: for x st x in Z holds ( cos . x) <> 0 by FDIFF_8: 1;

      then

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

      for x st x in Z holds tan is_differentiable_in x

      proof

        let x;

        assume x in Z;

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

        hence thesis by FDIFF_7: 46;

      end;

      then

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

      for x st x in Z holds ((( tan - sec ) `| Z) . x) = (1 / (1 + ( sin . x)))

      proof

        let x;

        assume

         A7: x in Z;

        then

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

        

         A9: (1 - ( sin . x)) <> 0 by A2, A7;

        ((( tan - sec ) `| Z) . x) = (( diff ( tan ,x)) - ( diff (( cos ^ ),x))) by A1, A5, A6, A7, FDIFF_1: 19

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

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

        .= ((1 / (( cos . x) ^2 )) - (( sin . x) / (( cos . x) ^2 ))) by A4, A7, FDIFF_4: 39

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

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

        .= ((1 - ( sin . x)) / ((1 + ( sin . x)) * (1 - ( sin . x))))

        .= (((1 - ( sin . x)) / (1 - ( sin . x))) / (1 + ( sin . x))) by XCMPLX_1: 78

        .= (1 / (1 + ( sin . x))) by A9, XCMPLX_1: 60;

        hence thesis;

      end;

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

    end;

    theorem :: INTEGR11:40

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

    proof

      assume that

       A1: A c= Z and

       A2: for x st x in Z holds (1 + ( sin . x)) <> 0 & (1 - ( sin . x)) <> 0 & (f . x) = (1 / (1 + ( sin . x))) and

       A3: ( dom ( tan - sec )) = Z and

       A4: Z = ( dom f) and

       A5: (f | A) is continuous;

      

       A6: f is_integrable_on A by A1, A4, A5, INTEGRA5: 11;

      

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

      then

       A8: ( tan - sec ) is_differentiable_on Z by A3, Th39;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

        then ((( tan - sec ) `| Z) . x) = (1 / (1 + ( sin . x))) by A3, A7, Th39

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

        hence thesis;

      end;

      ( dom (( tan - sec ) `| Z)) = ( dom f) by A4, A8, FDIFF_1:def 7;

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

      hence thesis by A1, A4, A5, A6, A8, INTEGRA5: 10, INTEGRA5: 13;

    end;

    theorem :: INTEGR11:41

    

     Th41: (Z c= ( dom (( - cot ) + cosec )) & for x st x in Z holds (1 + ( cos . x)) <> 0 & (1 - ( cos . x)) <> 0 ) implies (( - cot ) + cosec ) is_differentiable_on Z & for x st x in Z holds (((( - cot ) + cosec ) `| Z) . x) = (1 / (1 + ( cos . x)))

    proof

      assume that

       A1: Z c= ( dom (( - cot ) + cosec )) and

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

      Z c= (( dom ( - cot )) /\ ( dom ( sin ^ ))) by A1, VALUED_1:def 1;

      then

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

      then

       A4: Z c= ( dom cot ) by VALUED_1: 8;

      for x st x in Z holds cot is_differentiable_in x

      proof

        let x;

        assume x in Z;

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

        hence thesis by FDIFF_7: 47;

      end;

      then

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

      then

       A6: (( - 1) (#) cot ) is_differentiable_on Z by A3, FDIFF_1: 20;

      

       A7: for x st x in Z holds ( sin . x) <> 0 by A4, FDIFF_8: 2;

      then

       A8: ( sin ^ ) is_differentiable_on Z by FDIFF_4: 40;

      for x st x in Z holds (((( - cot ) + cosec ) `| Z) . x) = (1 / (1 + ( cos . x)))

      proof

        let x;

        assume

         A9: x in Z;

        then

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

        

         A11: (1 - ( cos . x)) <> 0 by A2, A9;

        (((( - cot ) + cosec ) `| Z) . x) = (( diff (( - cot ),x)) + ( diff (( sin ^ ),x))) by A1, A8, A6, A9, FDIFF_1: 18

        .= ((((( - 1) (#) cot ) `| Z) . x) + ( diff (( sin ^ ),x))) by A6, A9, FDIFF_1:def 7

        .= ((( - 1) * ( diff ( cot ,x))) + ( diff (( sin ^ ),x))) by A3, A5, A9, FDIFF_1: 20

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

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

        .= ((1 / (( sin . x) ^2 )) + ( - (( cos . x) / (( sin . x) ^2 )))) by A7, A9, FDIFF_4: 40

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

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

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

        .= ((1 - ( cos . x)) / ((1 - ( cos . x)) * (1 + ( cos . x))))

        .= (((1 - ( cos . x)) / (1 - ( cos . x))) / (1 + ( cos . x))) by XCMPLX_1: 78

        .= (1 / (1 + ( cos . x))) by A11, XCMPLX_1: 60;

        hence thesis;

      end;

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

    end;

    theorem :: INTEGR11:42

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

    proof

      assume that

       A1: A c= Z and

       A2: for x st x in Z holds (1 + ( cos . x)) <> 0 & (1 - ( cos . x)) <> 0 & (f . x) = (1 / (1 + ( cos . x))) and

       A3: ( dom (( - cot ) + cosec )) = Z and

       A4: Z = ( dom f) and

       A5: (f | A) is continuous;

      

       A6: f is_integrable_on A by A1, A4, A5, INTEGRA5: 11;

      

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

      then

       A8: (( - cot ) + cosec ) is_differentiable_on Z by A3, Th41;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

        then (((( - cot ) + cosec ) `| Z) . x) = (1 / (1 + ( cos . x))) by A3, A7, Th41

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

        hence thesis;

      end;

      ( dom ((( - cot ) + cosec ) `| Z)) = ( dom f) by A4, A8, FDIFF_1:def 7;

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

      hence thesis by A1, A4, A5, A6, A8, INTEGRA5: 10, INTEGRA5: 13;

    end;

    theorem :: INTEGR11:43

    

     Th43: (Z c= ( dom (( - cot ) - cosec )) & for x st x in Z holds (1 + ( cos . x)) <> 0 & (1 - ( cos . x)) <> 0 ) implies (( - cot ) - cosec ) is_differentiable_on Z & for x st x in Z holds (((( - cot ) - cosec ) `| Z) . x) = (1 / (1 - ( cos . x)))

    proof

      assume that

       A1: Z c= ( dom (( - cot ) - cosec )) and

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

      Z c= (( dom ( - cot )) /\ ( dom ( sin ^ ))) by A1, VALUED_1: 12;

      then

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

      then

       A4: Z c= ( dom cot ) by VALUED_1: 8;

      for x st x in Z holds cot is_differentiable_in x

      proof

        let x;

        assume x in Z;

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

        hence thesis by FDIFF_7: 47;

      end;

      then

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

      then

       A6: (( - 1) (#) cot ) is_differentiable_on Z by A3, FDIFF_1: 20;

      

       A7: for x st x in Z holds ( sin . x) <> 0 by A4, FDIFF_8: 2;

      then

       A8: ( sin ^ ) is_differentiable_on Z by FDIFF_4: 40;

      for x st x in Z holds (((( - cot ) - cosec ) `| Z) . x) = (1 / (1 - ( cos . x)))

      proof

        let x;

        assume

         A9: x in Z;

        then

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

        

         A11: (1 + ( cos . x)) <> 0 by A2, A9;

        (((( - cot ) - cosec ) `| Z) . x) = (( diff (( - cot ),x)) - ( diff (( sin ^ ),x))) by A1, A8, A6, A9, FDIFF_1: 19

        .= ((((( - 1) (#) cot ) `| Z) . x) - ( diff (( sin ^ ),x))) by A6, A9, FDIFF_1:def 7

        .= ((( - 1) * ( diff ( cot ,x))) - ( diff (( sin ^ ),x))) by A3, A5, A9, FDIFF_1: 20

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

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

        .= ((1 / (( sin . x) ^2 )) - ( - (( cos . x) / (( sin . x) ^2 )))) by A7, A9, FDIFF_4: 40

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

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

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

        .= ((1 + ( cos . x)) / ((1 + ( cos . x)) * (1 - ( cos . x))))

        .= (((1 + ( cos . x)) / (1 + ( cos . x))) / (1 - ( cos . x))) by XCMPLX_1: 78

        .= (1 / (1 - ( cos . x))) by A11, XCMPLX_1: 60;

        hence thesis;

      end;

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

    end;

    theorem :: INTEGR11:44

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

    proof

      assume that

       A1: A c= Z and

       A2: for x st x in Z holds (1 + ( cos . x)) <> 0 & (1 - ( cos . x)) <> 0 & (f . x) = (1 / (1 - ( cos . x))) and

       A3: ( dom (( - cot ) - cosec )) = Z and

       A4: Z = ( dom f) and

       A5: (f | A) is continuous;

      

       A6: f is_integrable_on A by A1, A4, A5, INTEGRA5: 11;

      

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

      then

       A8: (( - cot ) - cosec ) is_differentiable_on Z by A3, Th43;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

        then (((( - cot ) - cosec ) `| Z) . x) = (1 / (1 - ( cos . x))) by A3, A7, Th43

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

        hence thesis;

      end;

      ( dom ((( - cot ) - cosec ) `| Z)) = ( dom f) by A4, A8, FDIFF_1:def 7;

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

      hence thesis by A1, A4, A5, A6, A8, INTEGRA5: 10, INTEGRA5: 13;

    end;

    theorem :: INTEGR11:45

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

    proof

      assume that

       A1: A c= Z and

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

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

       A4: Z = ( dom f) and

       A5: (f | A) is continuous;

      

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

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

        then (( arctan `| Z) . x) = (1 / (1 + (x ^2 ))) by A2, SIN_COS9: 81

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

        hence thesis;

      end;

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

      then

       A9: ( arctan `| Z) = f by A7, PARTFUN1: 5;

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

      hence thesis by A1, A2, A9, INTEGRA5: 13, SIN_COS9: 81;

    end;

    theorem :: INTEGR11:46

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

    proof

      assume that

       A1: A c= Z and

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

       A3: for x st x in Z holds (f . x) = (r / (1 + (x ^2 ))) and

       A4: Z = ( dom f) and

       A5: (f | A) is continuous;

      

       A6: (r (#) arctan ) is_differentiable_on Z by A2, SIN_COS9: 83;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

        then (((r (#) arctan ) `| Z) . x) = (r / (1 + (x ^2 ))) by A2, SIN_COS9: 83

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

        hence thesis;

      end;

      ( dom ((r (#) arctan ) `| Z)) = ( dom f) by A4, A6, FDIFF_1:def 7;

      then

       A9: ((r (#) arctan ) `| Z) = f by A7, PARTFUN1: 5;

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

      hence thesis by A1, A2, A9, INTEGRA5: 13, SIN_COS9: 83;

    end;

    theorem :: INTEGR11:47

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

    proof

      assume that

       A1: A c= Z and

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

       A3: for x st x in Z holds (f . x) = ( - (1 / (1 + (x ^2 )))) and

       A4: Z = ( dom f) and

       A5: (f | A) is continuous;

      

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

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

        then (( arccot `| Z) . x) = ( - (1 / (1 + (x ^2 )))) by A2, SIN_COS9: 82

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

        hence thesis;

      end;

      ( dom ( arccot `| Z)) = ( dom f) by A4, A6, FDIFF_1:def 7;

      then

       A9: ( arccot `| Z) = f by A7, PARTFUN1: 5;

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

      hence thesis by A1, A2, A9, INTEGRA5: 13, SIN_COS9: 82;

    end;

    theorem :: INTEGR11:48

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

    proof

      assume that

       A1: A c= Z and

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

       A3: for x st x in Z holds (f . x) = ( - (r / (1 + (x ^2 )))) and

       A4: Z = ( dom f) and

       A5: (f | A) is continuous;

      

       A6: (r (#) arccot ) is_differentiable_on Z by A2, SIN_COS9: 84;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

        then (((r (#) arccot ) `| Z) . x) = ( - (r / (1 + (x ^2 )))) by A2, SIN_COS9: 84

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

        hence thesis;

      end;

      ( dom ((r (#) arccot ) `| Z)) = ( dom f) by A4, A6, FDIFF_1:def 7;

      then

       A9: ((r (#) arccot ) `| Z) = f by A7, PARTFUN1: 5;

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

      hence thesis by A1, A2, A9, INTEGRA5: 13, SIN_COS9: 84;

    end;

    theorem :: INTEGR11:49

    

     Th49: (Z c= ( dom ((( id Z) + cot ) - cosec )) & for x st x in Z holds (1 + ( cos . x)) <> 0 & (1 - ( cos . x)) <> 0 ) implies ((( id Z) + cot ) - cosec ) is_differentiable_on Z & for x st x in Z holds ((((( id Z) + cot ) - cosec ) `| Z) . x) = (( cos . x) / (1 + ( cos . x)))

    proof

      assume that

       A1: Z c= ( dom ((( id Z) + cot ) - cosec )) and

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

      

       A3: Z c= (( dom (( id Z) + cot )) /\ ( dom cosec )) by A1, VALUED_1: 12;

      then

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

      then Z c= (( dom ( id Z)) /\ ( dom cot )) by VALUED_1:def 1;

      then

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

      

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

      

       A7: Z c= ( dom ( id Z));

      then

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

      for x st x in Z holds cot is_differentiable_in x

      proof

        let x;

        assume x in Z;

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

        hence thesis by FDIFF_7: 47;

      end;

      then

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

      then

       A10: (( id Z) + cot ) is_differentiable_on Z by A4, A8, FDIFF_1: 18;

      

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

      then

       A12: cosec is_differentiable_on Z by FDIFF_9: 5;

      

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

      proof

        let x;

        assume

         A14: x in Z;

        then

         A15: ( sin . x) <> 0 by A5, FDIFF_8: 2;

        then

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

        (((( id Z) + cot ) `| Z) . x) = (( diff (( id Z),x)) + ( diff ( cot ,x))) by A4, A9, A8, A14, FDIFF_1: 18

        .= (((( id Z) `| Z) . x) + ( diff ( cot ,x))) by A8, A14, FDIFF_1:def 7

        .= (1 + ( diff ( cot ,x))) by A7, A6, A14, FDIFF_1: 23

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

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

        .= (((( sin . x) ^2 ) / (( sin . x) ^2 )) - (1 / (( sin . x) ^2 ))) by A16, XCMPLX_1: 60

        .= (((( sin . x) ^2 ) - 1) / (( sin . x) ^2 )) by XCMPLX_1: 120

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

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

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

        hence thesis;

      end;

      for x st x in Z holds ((((( id Z) + cot ) - cosec ) `| Z) . x) = (( cos . x) / (1 + ( cos . x)))

      proof

        let x;

        assume

         A17: x in Z;

        then

         A18: (1 - ( cos . x)) <> 0 by A2;

        ((((( id Z) + cot ) - cosec ) `| Z) . x) = (( diff ((( id Z) + cot ),x)) - ( diff ( cosec ,x))) by A1, A12, A10, A17, FDIFF_1: 19

        .= ((((( id Z) + cot ) `| Z) . x) - ( diff ( cosec ,x))) by A10, A17, FDIFF_1:def 7

        .= (( - ((( cos . x) ^2 ) / (( sin . x) ^2 ))) - ( diff ( cosec ,x))) by A13, A17

        .= (( - ((( cos . x) ^2 ) / (( sin . x) ^2 ))) - (( cosec `| Z) . x)) by A12, A17, FDIFF_1:def 7

        .= (( - ((( cos . x) ^2 ) / (( sin . x) ^2 ))) - ( - (( cos . x) / (( sin . x) ^2 )))) by A11, A17, FDIFF_9: 5

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

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

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

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

        .= ((( cos . x) * (1 - ( cos . x))) / ((1 - ( cos . x)) * (1 + ( cos . x))))

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

        .= ((( cos . x) * ((1 - ( cos . x)) / (1 - ( cos . x)))) / (1 + ( cos . x))) by XCMPLX_1: 74

        .= ((( cos . x) * 1) / (1 + ( cos . x))) by A18, XCMPLX_1: 60

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

        hence thesis;

      end;

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

    end;

    theorem :: INTEGR11:50

    A c= Z & (for x st x in Z holds (1 + ( cos . x)) <> 0 & (1 - ( cos . x)) <> 0 & (f . x) = (( cos . x) / (1 + ( cos . x)))) & ( dom ((( id Z) + cot ) - cosec )) = Z & Z = ( dom f) & (f | A) is continuous implies ( integral (f,A)) = ((((( id Z) + cot ) - cosec ) . ( upper_bound A)) - (((( id Z) + cot ) - cosec ) . ( lower_bound A)))

    proof

      assume that

       A1: A c= Z and

       A2: for x st x in Z holds (1 + ( cos . x)) <> 0 & (1 - ( cos . x)) <> 0 & (f . x) = (( cos . x) / (1 + ( cos . x))) and

       A3: ( dom ((( id Z) + cot ) - cosec )) = Z and

       A4: Z = ( dom f) and

       A5: (f | A) is continuous;

      

       A6: f is_integrable_on A by A1, A4, A5, INTEGRA5: 11;

      

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

      then

       A8: ((( id Z) + cot ) - cosec ) is_differentiable_on Z by A3, Th49;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

        then ((((( id Z) + cot ) - cosec ) `| Z) . x) = (( cos . x) / (1 + ( cos . x))) by A3, A7, Th49

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

        hence thesis;

      end;

      ( dom (((( id Z) + cot ) - cosec ) `| Z)) = ( dom f) by A4, A8, FDIFF_1:def 7;

      then (((( id Z) + cot ) - cosec ) `| Z) = f by A9, PARTFUN1: 5;

      hence thesis by A1, A4, A5, A6, A8, INTEGRA5: 10, INTEGRA5: 13;

    end;

    theorem :: INTEGR11:51

    

     Th51: (Z c= ( dom ((( id Z) + cot ) + cosec )) & for x st x in Z holds (1 + ( cos . x)) <> 0 & (1 - ( cos . x)) <> 0 ) implies ((( id Z) + cot ) + cosec ) is_differentiable_on Z & for x st x in Z holds ((((( id Z) + cot ) + cosec ) `| Z) . x) = (( cos . x) / (( cos . x) - 1))

    proof

      assume that

       A1: Z c= ( dom ((( id Z) + cot ) + cosec )) and

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

      

       A3: Z c= (( dom (( id Z) + cot )) /\ ( dom cosec )) by A1, VALUED_1:def 1;

      then

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

      then Z c= (( dom ( id Z)) /\ ( dom cot )) by VALUED_1:def 1;

      then

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

      

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

      

       A7: Z c= ( dom ( id Z));

      then

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

      for x st x in Z holds cot is_differentiable_in x

      proof

        let x;

        assume x in Z;

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

        hence thesis by FDIFF_7: 47;

      end;

      then

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

      then

       A10: (( id Z) + cot ) is_differentiable_on Z by A4, A8, FDIFF_1: 18;

      

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

      then

       A12: cosec is_differentiable_on Z by FDIFF_9: 5;

      

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

      proof

        let x;

        assume

         A14: x in Z;

        then

         A15: ( sin . x) <> 0 by A5, FDIFF_8: 2;

        then

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

        (((( id Z) + cot ) `| Z) . x) = (( diff (( id Z),x)) + ( diff ( cot ,x))) by A4, A9, A8, A14, FDIFF_1: 18

        .= (((( id Z) `| Z) . x) + ( diff ( cot ,x))) by A8, A14, FDIFF_1:def 7

        .= (1 + ( diff ( cot ,x))) by A7, A6, A14, FDIFF_1: 23

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

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

        .= (((( sin . x) ^2 ) / (( sin . x) ^2 )) - (1 / (( sin . x) ^2 ))) by A16, XCMPLX_1: 60

        .= (((( sin . x) ^2 ) - 1) / (( sin . x) ^2 )) by XCMPLX_1: 120

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

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

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

        hence thesis;

      end;

      for x st x in Z holds ((((( id Z) + cot ) + cosec ) `| Z) . x) = (( cos . x) / (( cos . x) - 1))

      proof

        let x;

        assume

         A17: x in Z;

        then

         A18: (1 + ( cos . x)) <> 0 by A2;

        ((((( id Z) + cot ) + cosec ) `| Z) . x) = (( diff ((( id Z) + cot ),x)) + ( diff ( cosec ,x))) by A1, A12, A10, A17, FDIFF_1: 18

        .= ((((( id Z) + cot ) `| Z) . x) + ( diff ( cosec ,x))) by A10, A17, FDIFF_1:def 7

        .= (( - ((( cos . x) ^2 ) / (( sin . x) ^2 ))) + ( diff ( cosec ,x))) by A13, A17

        .= (( - ((( cos . x) ^2 ) / (( sin . x) ^2 ))) + (( cosec `| Z) . x)) by A12, A17, FDIFF_1:def 7

        .= (( - ((( cos . x) ^2 ) / (( sin . x) ^2 ))) + ( - (( cos . x) / (( sin . x) ^2 )))) by A11, A17, FDIFF_9: 5

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

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

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

        .= ( - ((( cos . x) * (( cos . x) + 1)) / (1 - (( cos . x) ^2 )))) by SIN_COS: 28

        .= ( - ((( cos . x) * (( cos . x) + 1)) / ((1 + ( cos . x)) * (1 - ( cos . x)))))

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

        .= ( - ((( cos . x) * ((1 + ( cos . x)) / (1 + ( cos . x)))) / (1 - ( cos . x)))) by XCMPLX_1: 74

        .= ( - ((( cos . x) * 1) / (1 - ( cos . x)))) by A18, XCMPLX_1: 60

        .= (( cos . x) / ( - (1 - ( cos . x)))) by XCMPLX_1: 188

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

        hence thesis;

      end;

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

    end;

    theorem :: INTEGR11:52

    A c= Z & (for x st x in Z holds (1 + ( cos . x)) <> 0 & (1 - ( cos . x)) <> 0 & (f . x) = (( cos . x) / (( cos . x) - 1))) & ( dom ((( id Z) + cot ) + cosec )) = Z & Z = ( dom f) & (f | A) is continuous implies ( integral (f,A)) = ((((( id Z) + cot ) + cosec ) . ( upper_bound A)) - (((( id Z) + cot ) + cosec ) . ( lower_bound A)))

    proof

      assume that

       A1: A c= Z and

       A2: for x st x in Z holds (1 + ( cos . x)) <> 0 & (1 - ( cos . x)) <> 0 & (f . x) = (( cos . x) / (( cos . x) - 1)) and

       A3: ( dom ((( id Z) + cot ) + cosec )) = Z and

       A4: Z = ( dom f) and

       A5: (f | A) is continuous;

      

       A6: f is_integrable_on A by A1, A4, A5, INTEGRA5: 11;

      

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

      then

       A8: ((( id Z) + cot ) + cosec ) is_differentiable_on Z by A3, Th51;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

        then ((((( id Z) + cot ) + cosec ) `| Z) . x) = (( cos . x) / (( cos . x) - 1)) by A3, A7, Th51

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

        hence thesis;

      end;

      ( dom (((( id Z) + cot ) + cosec ) `| Z)) = ( dom f) by A4, A8, FDIFF_1:def 7;

      then (((( id Z) + cot ) + cosec ) `| Z) = f by A9, PARTFUN1: 5;

      hence thesis by A1, A4, A5, A6, A8, INTEGRA5: 10, INTEGRA5: 13;

    end;

    theorem :: INTEGR11:53

    

     Th53: (Z c= ( dom ((( id Z) - tan ) + sec )) & for x st x in Z holds (1 + ( sin . x)) <> 0 & (1 - ( sin . x)) <> 0 ) implies ((( id Z) - tan ) + sec ) is_differentiable_on Z & for x st x in Z holds ((((( id Z) - tan ) + sec ) `| Z) . x) = (( sin . x) / (( sin . x) + 1))

    proof

      assume that

       A1: Z c= ( dom ((( id Z) - tan ) + sec )) and

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

      

       A3: Z c= (( dom (( id Z) - tan )) /\ ( dom sec )) by A1, VALUED_1:def 1;

      then

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

      then

       A5: Z c= (( dom ( id Z)) /\ ( dom tan )) by VALUED_1: 12;

      

       A6: Z c= ( dom ( id Z));

      

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

      then

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

      

       A9: Z c= ( dom tan ) by A5, XBOOLE_1: 18;

      for x st x in Z holds tan is_differentiable_in x

      proof

        let x;

        assume x in Z;

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

        hence thesis by FDIFF_7: 46;

      end;

      then

       A10: tan is_differentiable_on Z by A9, FDIFF_1: 9;

      then

       A11: (( id Z) - tan ) is_differentiable_on Z by A4, A8, FDIFF_1: 19;

      

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

      then

       A13: sec is_differentiable_on Z by FDIFF_9: 4;

      

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

      proof

        let x;

        assume

         A15: x in Z;

        then

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

        then

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

        (((( id Z) - tan ) `| Z) . x) = (( diff (( id Z),x)) - ( diff ( tan ,x))) by A4, A10, A8, A15, FDIFF_1: 19

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

        .= (1 - ( diff ( tan ,x))) by A6, A7, A15, FDIFF_1: 23

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

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

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

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

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

        hence thesis;

      end;

      for x st x in Z holds ((((( id Z) - tan ) + sec ) `| Z) . x) = (( sin . x) / (( sin . x) + 1))

      proof

        let x;

        assume

         A18: x in Z;

        then

         A19: (1 - ( sin . x)) <> 0 by A2;

        ((((( id Z) - tan ) + sec ) `| Z) . x) = (( diff ((( id Z) - tan ),x)) + ( diff ( sec ,x))) by A1, A13, A11, A18, FDIFF_1: 18

        .= ((((( id Z) - tan ) `| Z) . x) + ( diff ( sec ,x))) by A11, A18, FDIFF_1:def 7

        .= (( - ((( sin . x) ^2 ) / (( cos . x) ^2 ))) + ( diff ( sec ,x))) by A14, A18

        .= (( - ((( sin . x) ^2 ) / (( cos . x) ^2 ))) + (( sec `| Z) . x)) by A13, A18, FDIFF_1:def 7

        .= (( - ((( sin . x) ^2 ) / (( cos . x) ^2 ))) + (( sin . x) / (( cos . x) ^2 ))) by A12, A18, FDIFF_9: 4

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

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

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

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

        .= ((( sin . x) * (1 - ( sin . x))) / ((1 - ( sin . x)) * (1 + ( sin . x))))

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

        .= ((( sin . x) * ((1 - ( sin . x)) / (1 - ( sin . x)))) / (1 + ( sin . x))) by XCMPLX_1: 74

        .= ((( sin . x) * 1) / (1 + ( sin . x))) by A19, XCMPLX_1: 60

        .= (( sin . x) / (1 + ( sin . x)));

        hence thesis;

      end;

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

    end;

    theorem :: INTEGR11:54

    A c= Z & (for x st x in Z holds (1 + ( sin . x)) <> 0 & (1 - ( sin . x)) <> 0 & (f . x) = (( sin . x) / (1 + ( sin . x)))) & Z c= ( dom ((( id Z) - tan ) + sec )) & Z = ( dom f) & (f | A) is continuous implies ( integral (f,A)) = ((((( id Z) - tan ) + sec ) . ( upper_bound A)) - (((( id Z) - tan ) + sec ) . ( lower_bound A)))

    proof

      assume that

       A1: A c= Z and

       A2: for x st x in Z holds (1 + ( sin . x)) <> 0 & (1 - ( sin . x)) <> 0 & (f . x) = (( sin . x) / (1 + ( sin . x))) and

       A3: Z c= ( dom ((( id Z) - tan ) + sec )) and

       A4: Z = ( dom f) and

       A5: (f | A) is continuous;

      

       A6: f is_integrable_on A by A1, A4, A5, INTEGRA5: 11;

      

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

      then

       A8: ((( id Z) - tan ) + sec ) is_differentiable_on Z by A3, Th53;

      

       A9: for x be Element of REAL st x in ( dom (((( id Z) - tan ) + sec ) `| Z)) holds ((((( id Z) - tan ) + sec ) `| Z) . x) = (f . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom (((( id Z) - tan ) + sec ) `| Z));

        then

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

        

        then ((((( id Z) - tan ) + sec ) `| Z) . x) = (( sin . x) / (1 + ( sin . x))) by A3, A7, Th53

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

        hence thesis;

      end;

      ( dom (((( id Z) - tan ) + sec ) `| Z)) = ( dom f) by A4, A8, FDIFF_1:def 7;

      then (((( id Z) - tan ) + sec ) `| Z) = f by A9, PARTFUN1: 5;

      hence thesis by A1, A4, A5, A6, A8, INTEGRA5: 10, INTEGRA5: 13;

    end;

    theorem :: INTEGR11:55

    

     Th55: (Z c= ( dom ((( id Z) - tan ) - sec )) & for x st x in Z holds (1 + ( sin . x)) <> 0 & (1 - ( sin . x)) <> 0 ) implies ((( id Z) - tan ) - sec ) is_differentiable_on Z & for x st x in Z holds ((((( id Z) - tan ) - sec ) `| Z) . x) = (( sin . x) / (( sin . x) - 1))

    proof

      assume that

       A1: Z c= ( dom ((( id Z) - tan ) - sec )) and

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

      

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

      then

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

      then Z c= (( dom ( id Z)) /\ ( dom tan )) by VALUED_1: 12;

      then

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

      

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

      

       A7: Z c= ( dom ( id Z));

      then

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

      for x st x in Z holds tan is_differentiable_in x

      proof

        let x;

        assume x in Z;

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

        hence thesis by FDIFF_7: 46;

      end;

      then

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

      then

       A10: (( id Z) - tan ) is_differentiable_on Z by A4, A8, FDIFF_1: 19;

      

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

      then

       A12: sec is_differentiable_on Z by FDIFF_9: 4;

      

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

      proof

        let x;

        assume

         A14: x in Z;

        then

         A15: ( cos . x) <> 0 by A5, FDIFF_8: 1;

        then

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

        (((( id Z) - tan ) `| Z) . x) = (( diff (( id Z),x)) - ( diff ( tan ,x))) by A4, A9, A8, A14, FDIFF_1: 19

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

        .= (1 - ( diff ( tan ,x))) by A7, A6, A14, FDIFF_1: 23

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

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

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

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

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

        hence thesis;

      end;

      for x st x in Z holds ((((( id Z) - tan ) - sec ) `| Z) . x) = (( sin . x) / (( sin . x) - 1))

      proof

        let x;

        assume

         A17: x in Z;

        then

         A18: (1 + ( sin . x)) <> 0 by A2;

        ((((( id Z) - tan ) - sec ) `| Z) . x) = (( diff ((( id Z) - tan ),x)) - ( diff ( sec ,x))) by A1, A12, A10, A17, FDIFF_1: 19

        .= ((((( id Z) - tan ) `| Z) . x) - ( diff ( sec ,x))) by A10, A17, FDIFF_1:def 7

        .= (( - ((( sin . x) ^2 ) / (( cos . x) ^2 ))) - ( diff ( sec ,x))) by A13, A17

        .= (( - ((( sin . x) ^2 ) / (( cos . x) ^2 ))) - (( sec `| Z) . x)) by A12, A17, FDIFF_1:def 7

        .= (( - ((( sin . x) ^2 ) / (( cos . x) ^2 ))) - (( sin . x) / (( cos . x) ^2 ))) by A11, A17, FDIFF_9: 4

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

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

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

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

        .= ( - ((( sin . x) * (1 + ( sin . x))) / ((1 + ( sin . x)) * (1 - ( sin . x)))))

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

        .= ( - ((( sin . x) * ((1 + ( sin . x)) / (1 + ( sin . x)))) / (1 - ( sin . x)))) by XCMPLX_1: 74

        .= ( - ((( sin . x) * 1) / (1 - ( sin . x)))) by A18, XCMPLX_1: 60

        .= (( sin . x) / ( - (1 - ( sin . x)))) by XCMPLX_1: 188

        .= (( sin . x) / (( sin . x) - 1));

        hence thesis;

      end;

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

    end;

    theorem :: INTEGR11:56

    A c= Z & (for x st x in Z holds (1 + ( sin . x)) <> 0 & (1 - ( sin . x)) <> 0 & (f . x) = (( sin . x) / (( sin . x) - 1))) & Z c= ( dom ((( id Z) - tan ) - sec )) & Z = ( dom f) & (f | A) is continuous implies ( integral (f,A)) = ((((( id Z) - tan ) - sec ) . ( upper_bound A)) - (((( id Z) - tan ) - sec ) . ( lower_bound A)))

    proof

      assume that

       A1: A c= Z and

       A2: for x st x in Z holds (1 + ( sin . x)) <> 0 & (1 - ( sin . x)) <> 0 & (f . x) = (( sin . x) / (( sin . x) - 1)) and

       A3: Z c= ( dom ((( id Z) - tan ) - sec )) and

       A4: Z = ( dom f) and

       A5: (f | A) is continuous;

      

       A6: f is_integrable_on A by A1, A4, A5, INTEGRA5: 11;

      

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

      then

       A8: ((( id Z) - tan ) - sec ) is_differentiable_on Z by A3, Th55;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

        then ((((( id Z) - tan ) - sec ) `| Z) . x) = (( sin . x) / (( sin . x) - 1)) by A3, A7, Th55

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

        hence thesis;

      end;

      ( dom (((( id Z) - tan ) - sec ) `| Z)) = ( dom f) by A4, A8, FDIFF_1:def 7;

      then (((( id Z) - tan ) - sec ) `| Z) = f by A9, PARTFUN1: 5;

      hence thesis by A1, A4, A5, A6, A8, INTEGRA5: 10, INTEGRA5: 13;

    end;

    theorem :: INTEGR11:57

    

     Th57: 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) = (( tan . x) ^2 )

    proof

      

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

      assume

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

      then Z c= (( dom tan ) /\ ( dom ( id Z))) by VALUED_1: 12;

      then

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

      

       A4: Z c= ( dom ( id Z));

      then

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

      for x st x in Z holds tan is_differentiable_in x

      proof

        let x;

        assume x in Z;

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

        hence thesis by FDIFF_7: 46;

      end;

      then

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

      for x st x in Z holds ((( tan - ( id Z)) `| Z) . x) = (( tan . x) ^2 )

      proof

        let x;

        assume

         A7: x in Z;

        then

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

        then

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

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

        .= ((1 / (( cos . x) ^2 )) - ( diff (( id Z),x))) by A8, FDIFF_7: 46

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

        .= ((1 / (( cos . x) ^2 )) - 1) by A4, A1, A7, FDIFF_1: 23

        .= ((1 / (( cos . x) ^2 )) - ((( cos . x) ^2 ) / (( cos . x) ^2 ))) by A9, XCMPLX_1: 60

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

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

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

        .= (( tan . x) * ( tan x)) by A3, A7, FDIFF_8: 1, SIN_COS9: 15

        .= (( tan . x) ^2 ) by A3, A7, FDIFF_8: 1, SIN_COS9: 15;

        hence thesis;

      end;

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

    end;

    theorem :: INTEGR11:58

    A c= Z & (for x st x in Z holds ( cos . x) > 0 & (f . x) = (( tan . 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 that

       A1: A c= Z and

       A2: for x st x in Z holds ( cos . x) > 0 & (f . x) = (( tan . x) ^2 ) and

       A3: Z c= ( dom ( tan - ( id Z))) and

       A4: Z = ( dom f) and

       A5: (f | A) is continuous;

      

       A6: f is_integrable_on A by A1, A4, A5, INTEGRA5: 11;

      

       A7: ( tan - ( id Z)) is_differentiable_on Z by A3, Th57;

      

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

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

        

        then ((( tan - ( id Z)) `| Z) . x) = (( tan . x) ^2 ) by A3, Th57

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

        hence thesis;

      end;

      ( dom (( tan - ( id Z)) `| Z)) = ( dom f) by A4, A7, FDIFF_1:def 7;

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

      hence thesis by A1, A4, A5, A6, A7, INTEGRA5: 10, INTEGRA5: 13;

    end;

    theorem :: INTEGR11:59

    

     Th59: Z c= ( dom (( - cot ) - ( id Z))) implies (( - cot ) - ( id Z)) is_differentiable_on Z & for x st x in Z holds (((( - cot ) - ( id Z)) `| Z) . x) = (( cot . x) ^2 )

    proof

      set f = ( - cot );

      

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

      assume

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

      then Z c= (( dom ( - cot )) /\ ( dom ( id Z))) by VALUED_1: 12;

      then

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

      then

       A4: Z c= ( dom cot ) by VALUED_1: 8;

      for x st x in Z holds cot is_differentiable_in x

      proof

        let x;

        assume x in Z;

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

        hence thesis by FDIFF_7: 47;

      end;

      then

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

      then

       A6: (( - 1) (#) cot ) is_differentiable_on Z by A3, FDIFF_1: 20;

      

       A7: Z c= ( dom ( id Z));

      then

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

      for x st x in Z holds (((( - cot ) - ( id Z)) `| Z) . x) = (( cot . x) ^2 )

      proof

        let x;

        assume

         A9: x in Z;

        then

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

        then

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

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

        .= ((((( - 1) (#) cot ) `| Z) . x) - ( diff (( id Z),x))) by A6, A9, FDIFF_1:def 7

        .= ((( - 1) * ( diff ( cot ,x))) - ( diff (( id Z),x))) by A3, A5, A9, FDIFF_1: 20

        .= ((( - 1) * ( - (1 / (( sin . x) ^2 )))) - ( diff (( id Z),x))) by A10, FDIFF_7: 47

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

        .= ((1 / (( sin . x) ^2 )) - 1) by A7, A1, A9, FDIFF_1: 23

        .= ((1 / (( sin . x) ^2 )) - ((( sin . x) ^2 ) / (( sin . x) ^2 ))) by A11, XCMPLX_1: 60

        .= ((1 - (( sin . x) ^2 )) / (( sin . x) ^2 )) by XCMPLX_1: 120

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

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

        .= (( cot . x) * ( cot x)) by A4, A9, FDIFF_8: 2, SIN_COS9: 16

        .= (( cot . x) ^2 ) by A4, A9, FDIFF_8: 2, SIN_COS9: 16;

        hence thesis;

      end;

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

    end;

    theorem :: INTEGR11:60

    A c= Z & (for x st x in Z holds ( sin . x) > 0 & (f . x) = (( cot . 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 that

       A1: A c= Z and

       A2: for x st x in Z holds ( sin . x) > 0 & (f . x) = (( cot . x) ^2 ) and

       A3: Z c= ( dom (( - cot ) - ( id Z))) and

       A4: Z = ( dom f) and

       A5: (f | A) is continuous;

      

       A6: f is_integrable_on A by A1, A4, A5, INTEGRA5: 11;

      

       A7: (( - cot ) - ( id Z)) is_differentiable_on Z by A3, Th59;

      

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

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

        

        then (((( - cot ) - ( id Z)) `| Z) . x) = (( cot . x) ^2 ) by A3, Th59

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

        hence thesis;

      end;

      ( dom ((( - cot ) - ( id Z)) `| Z)) = ( dom f) by A4, A7, FDIFF_1:def 7;

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

      hence thesis by A1, A4, A5, A6, A7, INTEGRA5: 10, INTEGRA5: 13;

    end;

    theorem :: INTEGR11:61

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

    proof

      assume that

       A1: A c= Z and

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

       A3: ( dom tan ) = Z and

       A4: Z = ( dom f) and

       A5: (f | A) is continuous;

      

       A6: f is_integrable_on A by A1, A4, A5, INTEGRA5: 11;

      

       A7: tan is_differentiable_on Z by A3, INTEGRA8: 33;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

        then (( tan `| Z) . x) = (1 / (( cos . x) ^2 )) by A3, INTEGRA8: 33

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

        hence thesis;

      end;

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

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

      hence thesis by A1, A4, A5, A6, A7, INTEGRA5: 10, INTEGRA5: 13;

    end;

    theorem :: INTEGR11:62

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

    proof

      assume that

       A1: A c= Z and

       A2: for x st x in Z holds (f . x) = ( - (1 / (( sin . x) ^2 ))) & ( sin . x) <> 0 and

       A3: ( dom cot ) = Z and

       A4: Z = ( dom f) and

       A5: (f | A) is continuous;

      

       A6: f is_integrable_on A by A1, A4, A5, INTEGRA5: 11;

      

       A7: cot is_differentiable_on Z by A3, INTEGRA8: 34;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

        then (( cot `| Z) . x) = ( - (1 / (( sin . x) ^2 ))) by A3, INTEGRA8: 34

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

        hence thesis;

      end;

      ( dom ( cot `| Z)) = ( dom f) by A4, A7, FDIFF_1:def 7;

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

      hence thesis by A1, A4, A5, A6, A7, INTEGRA5: 10, INTEGRA5: 13;

    end;

    theorem :: INTEGR11:63

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

    proof

      assume that

       A1: A c= Z and

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

       A3: Z c= ( dom ( sec - ( id Z))) and

       A4: Z = ( dom f) and

       A5: (f | A) is continuous;

      

       A6: ( sec - ( id Z)) is_differentiable_on Z by A3, FDIFF_9: 22;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

        then ((( sec - ( id Z)) `| Z) . x) = ((( sin . x) - (( cos . x) ^2 )) / (( cos . x) ^2 )) by A3, FDIFF_9: 22

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

        hence thesis;

      end;

      ( dom (( sec - ( id Z)) `| Z)) = ( dom f) by A4, A6, FDIFF_1:def 7;

      then

       A9: (( sec - ( id Z)) `| Z) = f by A7, PARTFUN1: 5;

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

      hence thesis by A1, A3, A9, FDIFF_9: 22, INTEGRA5: 13;

    end;

    theorem :: INTEGR11:64

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

    proof

      assume that

       A1: A c= Z and

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

       A3: Z c= ( dom (( - cosec ) - ( id Z))) and

       A4: Z = ( dom f) and

       A5: (f | A) is continuous;

      

       A6: (( - cosec ) - ( id Z)) is_differentiable_on Z by A3, FDIFF_9: 23;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

        then (((( - cosec ) - ( id Z)) `| Z) . x) = ((( cos . x) - (( sin . x) ^2 )) / (( sin . x) ^2 )) by A3, FDIFF_9: 23

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

        hence thesis;

      end;

      ( dom ((( - cosec ) - ( id Z)) `| Z)) = ( dom f) by A4, A6, FDIFF_1:def 7;

      then

       A9: ((( - cosec ) - ( id Z)) `| Z) = f by A7, PARTFUN1: 5;

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

      hence thesis by A1, A3, A9, FDIFF_9: 23, INTEGRA5: 13;

    end;

    theorem :: INTEGR11:65

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

    proof

      set f = cot ;

      assume that

       A1: A c= Z and

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

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

       A4: Z = ( dom cot ) and

       A5: (f | A) is continuous;

      

       A6: ( ln * sin ) is_differentiable_on Z by A2, A3, FDIFF_4: 43;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        then

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

        ((( ln * sin ) `| Z) . x) = ( cot x) by A2, A3, A8, FDIFF_4: 43

        .= (f . x) by A9, SIN_COS9: 16;

        hence thesis;

      end;

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

      then

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

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

      hence thesis by A1, A2, A3, A10, FDIFF_4: 43, INTEGRA5: 13;

    end;

    theorem :: INTEGR11:66

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

    proof

      assume that

       A1: A c= Z and

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

       A3: for x st x in Z holds (f . x) = (( arcsin . x) / ( sqrt (1 - (x ^2 )))) and

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

       A5: Z = ( dom f) and

       A6: (f | A) is continuous;

      

       A7: ((1 / 2) (#) (( #Z 2) * arcsin )) is_differentiable_on Z by A2, A4, FDIFF_7: 12;

      

       A8: for x be Element of REAL st x in ( dom (((1 / 2) (#) (( #Z 2) * arcsin )) `| Z)) holds ((((1 / 2) (#) (( #Z 2) * arcsin )) `| Z) . x) = (f . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom (((1 / 2) (#) (( #Z 2) * arcsin )) `| Z));

        then

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

        

        then ((((1 / 2) (#) (( #Z 2) * arcsin )) `| Z) . x) = (( arcsin . x) / ( sqrt (1 - (x ^2 )))) by A2, A4, FDIFF_7: 12

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

        hence thesis;

      end;

      ( dom (((1 / 2) (#) (( #Z 2) * arcsin )) `| Z)) = ( dom f) by A5, A7, FDIFF_1:def 7;

      then

       A10: (((1 / 2) (#) (( #Z 2) * arcsin )) `| Z) = f by A8, PARTFUN1: 5;

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

      hence thesis by A1, A2, A4, A10, FDIFF_7: 12, INTEGRA5: 13;

    end;

    theorem :: INTEGR11:67

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

    proof

      assume that

       A1: A c= Z and

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

       A3: for x st x in Z holds (f . x) = ( - (( arccos . x) / ( sqrt (1 - (x ^2 ))))) and

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

       A5: Z = ( dom f) and

       A6: (f | A) is continuous;

      

       A7: ((1 / 2) (#) (( #Z 2) * arccos )) is_differentiable_on Z by A2, A4, FDIFF_7: 13;

      

       A8: for x be Element of REAL st x in ( dom (((1 / 2) (#) (( #Z 2) * arccos )) `| Z)) holds ((((1 / 2) (#) (( #Z 2) * arccos )) `| Z) . x) = (f . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom (((1 / 2) (#) (( #Z 2) * arccos )) `| Z));

        then

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

        

        then ((((1 / 2) (#) (( #Z 2) * arccos )) `| Z) . x) = ( - (( arccos . x) / ( sqrt (1 - (x ^2 ))))) by A2, A4, FDIFF_7: 13

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

        hence thesis;

      end;

      ( dom (((1 / 2) (#) (( #Z 2) * arccos )) `| Z)) = ( dom f) by A5, A7, FDIFF_1:def 7;

      then

       A10: (((1 / 2) (#) (( #Z 2) * arccos )) `| Z) = f by A8, PARTFUN1: 5;

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

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

    end;

    theorem :: INTEGR11:68

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

    proof

      assume that

       A1: A c= Z and

       A2: Z c= ].( - 1), 1.[ & f = (f1 - f2) & (f2 = ( #Z 2) & for x st x in Z holds (f1 . x) = 1 & (f . x) > 0 & x <> 0 ) and

       A3: ( dom arcsin ) = Z and

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

      

       A5: ( arcsin | A) is bounded by A1, A3, INTEGRA5: 10;

      

       A6: ((( id Z) (#) arcsin ) + (( #R (1 / 2)) * f)) is_differentiable_on Z by A2, A4, FDIFF_7: 23;

      

       A7: for x be Element of REAL st x in ( dom (((( id Z) (#) arcsin ) + (( #R (1 / 2)) * f)) `| Z)) holds ((((( id Z) (#) arcsin ) + (( #R (1 / 2)) * f)) `| Z) . x) = ( arcsin . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom (((( id Z) (#) arcsin ) + (( #R (1 / 2)) * f)) `| Z));

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

        hence thesis by A2, A4, FDIFF_7: 23;

      end;

      ( dom (((( id Z) (#) arcsin ) + (( #R (1 / 2)) * f)) `| Z)) = ( dom arcsin ) by A3, A6, FDIFF_1:def 7;

      then (((( id Z) (#) arcsin ) + (( #R (1 / 2)) * f)) `| Z) = arcsin by A7, PARTFUN1: 5;

      hence thesis by A1, A3, A5, A6, INTEGRA5: 11, INTEGRA5: 13;

    end;

    theorem :: INTEGR11:69

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

    proof

      assume that

       A1: A c= Z and

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

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

       A4: ( dom ( arcsin * f3)) = Z and

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

       A6: (( arcsin * f3) | A) is continuous;

      

       A7: ( arcsin * f3) is_integrable_on A by A1, A4, A6, INTEGRA5: 11;

      

       A8: ((( id Z) (#) ( arcsin * f3)) + (( #R (1 / 2)) * f)) is_differentiable_on Z by A2, A3, A5, FDIFF_7: 28;

      

       A9: for x be Element of REAL st x in ( dom (((( id Z) (#) ( arcsin * f3)) + (( #R (1 / 2)) * f)) `| Z)) holds ((((( id Z) (#) ( arcsin * f3)) + (( #R (1 / 2)) * f)) `| Z) . x) = (( arcsin * f3) . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom (((( id Z) (#) ( arcsin * f3)) + (( #R (1 / 2)) * f)) `| Z));

        then

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

        

        then ((((( id Z) (#) ( arcsin * f3)) + (( #R (1 / 2)) * f)) `| Z) . x) = ( arcsin . (x / a)) by A2, A3, A5, FDIFF_7: 28

        .= ( arcsin . (f3 . x)) by A3, A10

        .= (( arcsin * f3) . x) by A4, A10, FUNCT_1: 12;

        hence thesis;

      end;

      ( dom (((( id Z) (#) ( arcsin * f3)) + (( #R (1 / 2)) * f)) `| Z)) = ( dom ( arcsin * f3)) by A4, A8, FDIFF_1:def 7;

      then (((( id Z) (#) ( arcsin * f3)) + (( #R (1 / 2)) * f)) `| Z) = ( arcsin * f3) by A9, PARTFUN1: 5;

      hence thesis by A1, A4, A6, A7, A8, INTEGRA5: 10, INTEGRA5: 13;

    end;

    theorem :: INTEGR11:70

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

    proof

      assume that

       A1: A c= Z and

       A2: Z c= ].( - 1), 1.[ & f = (f1 - f2) & (f2 = ( #Z 2) & for x st x in Z holds (f1 . x) = 1 & (f . x) > 0 & x <> 0 ) and

       A3: ( dom arccos ) = Z and

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

      

       A5: ( arccos | A) is bounded by A1, A3, INTEGRA5: 10;

      

       A6: ((( id Z) (#) arccos ) - (( #R (1 / 2)) * f)) is_differentiable_on Z by A2, A4, FDIFF_7: 24;

      

       A7: for x be Element of REAL st x in ( dom (((( id Z) (#) arccos ) - (( #R (1 / 2)) * f)) `| Z)) holds ((((( id Z) (#) arccos ) - (( #R (1 / 2)) * f)) `| Z) . x) = ( arccos . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom (((( id Z) (#) arccos ) - (( #R (1 / 2)) * f)) `| Z));

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

        hence thesis by A2, A4, FDIFF_7: 24;

      end;

      ( dom (((( id Z) (#) arccos ) - (( #R (1 / 2)) * f)) `| Z)) = ( dom arccos ) by A3, A6, FDIFF_1:def 7;

      then (((( id Z) (#) arccos ) - (( #R (1 / 2)) * f)) `| Z) = arccos by A7, PARTFUN1: 5;

      hence thesis by A1, A3, A5, A6, INTEGRA5: 11, INTEGRA5: 13;

    end;

    theorem :: INTEGR11:71

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

    proof

      assume that

       A1: A c= Z and

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

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

       A4: ( dom ( arccos * f3)) = Z and

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

       A6: (( arccos * f3) | A) is continuous;

      

       A7: ( arccos * f3) is_integrable_on A by A1, A4, A6, INTEGRA5: 11;

      

       A8: ((( id Z) (#) ( arccos * f3)) - (( #R (1 / 2)) * f)) is_differentiable_on Z by A2, A3, A5, FDIFF_7: 29;

      

       A9: for x be Element of REAL st x in ( dom (((( id Z) (#) ( arccos * f3)) - (( #R (1 / 2)) * f)) `| Z)) holds ((((( id Z) (#) ( arccos * f3)) - (( #R (1 / 2)) * f)) `| Z) . x) = (( arccos * f3) . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom (((( id Z) (#) ( arccos * f3)) - (( #R (1 / 2)) * f)) `| Z));

        then

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

        

        then ((((( id Z) (#) ( arccos * f3)) - (( #R (1 / 2)) * f)) `| Z) . x) = ( arccos . (x / a)) by A2, A3, A5, FDIFF_7: 29

        .= ( arccos . (f3 . x)) by A3, A10

        .= (( arccos * f3) . x) by A4, A10, FUNCT_1: 12;

        hence thesis;

      end;

      ( dom (((( id Z) (#) ( arccos * f3)) - (( #R (1 / 2)) * f)) `| Z)) = ( dom ( arccos * f3)) by A4, A8, FDIFF_1:def 7;

      then (((( id Z) (#) ( arccos * f3)) - (( #R (1 / 2)) * f)) `| Z) = ( arccos * f3) by A9, PARTFUN1: 5;

      hence thesis by A1, A4, A6, A7, A8, INTEGRA5: 10, INTEGRA5: 13;

    end;

    theorem :: INTEGR11:72

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

    proof

      assume that

       A1: A c= Z and

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

       A3: f2 = ( #Z 2) & for x st x in Z holds (f1 . x) = 1 and

       A4: Z = ( dom arctan ) and

       A5: Z = ( dom ((( id Z) (#) arctan ) - ((1 / 2) (#) ( ln * (f1 + f2)))));

       ].( - 1), 1.[ c= [.( - 1), 1.] & A c= ].( - 1), 1.[ by A1, A2, XBOOLE_1: 1, XXREAL_1: 25;

      then ( arctan | A) is continuous by FCONT_1: 16, SIN_COS9: 53, XBOOLE_1: 1;

      then

       A6: arctan is_integrable_on A & ( arctan | A) is bounded by A1, A4, INTEGRA5: 10, INTEGRA5: 11;

      

       A7: ((( id Z) (#) arctan ) - ((1 / 2) (#) ( ln * (f1 + f2)))) is_differentiable_on Z by A2, A3, A5, SIN_COS9: 103;

      

       A8: for x be Element of REAL st x in ( dom (((( id Z) (#) arctan ) - ((1 / 2) (#) ( ln * (f1 + f2)))) `| Z)) holds ((((( id Z) (#) arctan ) - ((1 / 2) (#) ( ln * (f1 + f2)))) `| Z) . x) = ( arctan . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom (((( id Z) (#) arctan ) - ((1 / 2) (#) ( ln * (f1 + f2)))) `| Z));

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

        hence thesis by A2, A3, A5, SIN_COS9: 103;

      end;

      ( dom (((( id Z) (#) arctan ) - ((1 / 2) (#) ( ln * (f1 + f2)))) `| Z)) = ( dom arctan ) by A4, A7, FDIFF_1:def 7;

      then (((( id Z) (#) arctan ) - ((1 / 2) (#) ( ln * (f1 + f2)))) `| Z) = arctan by A8, PARTFUN1: 5;

      hence thesis by A1, A2, A3, A5, A6, INTEGRA5: 13, SIN_COS9: 103;

    end;

    theorem :: INTEGR11:73

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

    proof

      assume that

       A1: A c= Z and

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

       A3: f2 = ( #Z 2) & for x st x in Z holds (f1 . x) = 1 and

       A4: ( dom arccot ) = Z and

       A5: Z = ( dom ((( id Z) (#) arccot ) + ((1 / 2) (#) ( ln * (f1 + f2)))));

       ].( - 1), 1.[ c= [.( - 1), 1.] & A c= ].( - 1), 1.[ by A1, A2, XBOOLE_1: 1, XXREAL_1: 25;

      then ( arccot | A) is continuous by FCONT_1: 16, SIN_COS9: 54, XBOOLE_1: 1;

      then

       A6: arccot is_integrable_on A & ( arccot | A) is bounded by A1, A4, INTEGRA5: 10, INTEGRA5: 11;

      

       A7: ((( id Z) (#) arccot ) + ((1 / 2) (#) ( ln * (f1 + f2)))) is_differentiable_on Z by A2, A3, A5, SIN_COS9: 104;

      

       A8: for x be Element of REAL st x in ( dom (((( id Z) (#) arccot ) + ((1 / 2) (#) ( ln * (f1 + f2)))) `| Z)) holds ((((( id Z) (#) arccot ) + ((1 / 2) (#) ( ln * (f1 + f2)))) `| Z) . x) = ( arccot . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom (((( id Z) (#) arccot ) + ((1 / 2) (#) ( ln * (f1 + f2)))) `| Z));

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

        hence thesis by A2, A3, A5, SIN_COS9: 104;

      end;

      ( dom (((( id Z) (#) arccot ) + ((1 / 2) (#) ( ln * (f1 + f2)))) `| Z)) = ( dom arccot ) by A4, A7, FDIFF_1:def 7;

      then (((( id Z) (#) arccot ) + ((1 / 2) (#) ( ln * (f1 + f2)))) `| Z) = arccot by A8, PARTFUN1: 5;

      hence thesis by A1, A2, A3, A5, A6, INTEGRA5: 13, SIN_COS9: 104;

    end;