integra8.miz



    begin

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

    reserve A for non empty closed_interval Subset of REAL ;

    reserve p,r,x,x0 for Real;

    reserve n for Element of NAT ;

    reserve Z for open Subset of REAL ;

    

     Lm1: ( sin ( PI / 4)) > 0

    proof

      ( PI / 4) < ( PI / 1) by XREAL_1: 76;

      then

       A1: ( PI / 4) < ( PI + ((2 * PI ) * 0 ));

      ( 0 / 4) < ( PI / 4) by XREAL_1: 74;

      hence thesis by A1, SIN_COS6: 11;

    end;

    

     Lm2: ( sin ( - ( PI / 4))) < 0

    proof

      ( 0 / 4) < ( PI / 4) by XREAL_1: 74;

      then

       A1: (( PI / 4) * ( - 1)) < ( 0 * ( - 1)) by XREAL_1: 69;

      ( PI / 4) < ( PI / 1) by XREAL_1: 76;

      then

       A2: ( PI * ( - 1)) < (( PI / 4) * ( - 1)) by XREAL_1: 69;

      ( PI + ((2 * PI ) * ( - 1))) < r & r < ((2 * PI ) + ((2 * PI ) * ( - 1))) implies ( sin r) < 0 by SIN_COS6: 12;

      hence thesis by A1, A2;

    end;

    theorem :: INTEGRA8:1

    

     Th1: ( sin (x + ((2 * n) * PI ))) = ( sin x)

    proof

      ( sin . x) = ( sin . (((2 * PI ) * n) + x)) by SIN_COS2: 10;

      hence thesis;

    end;

    theorem :: INTEGRA8:2

    

     Th2: ( sin (x + (((2 * n) + 1) * PI ))) = ( - ( sin x))

    proof

      defpred X[ Nat] means ( sin (x + (((2 * $1) + 1) * PI ))) = ( - ( sin x));

      

       A1: for n be Nat st X[n] holds X[(n + 1)]

      proof

        let n be Nat;

        assume

         A2: ( sin (x + (((2 * n) + 1) * PI ))) = ( - ( sin x));

        ( sin (x + (((2 * (n + 1)) + 1) * PI ))) = ( sin ((x + (((2 * n) + 1) * PI )) + (2 * PI )))

        .= ((( sin (x + (((2 * n) + 1) * PI ))) * ( cos (2 * PI ))) + (( cos (x + (((2 * n) + 1) * PI ))) * ( sin (2 * PI )))) by SIN_COS: 75

        .= ( - ( sin x)) by A2, SIN_COS: 77;

        hence thesis;

      end;

      

       A3: X[ 0 ] by SIN_COS: 79;

      for n be Nat holds X[n] from NAT_1:sch 2( A3, A1);

      hence thesis;

    end;

    theorem :: INTEGRA8:3

    

     Th3: ( cos (x + ((2 * n) * PI ))) = ( cos x)

    proof

      ( cos . x) = ( cos . (x + ((2 * PI ) * n))) by SIN_COS6: 10;

      hence thesis;

    end;

    theorem :: INTEGRA8:4

    

     Th4: ( cos (x + (((2 * n) + 1) * PI ))) = ( - ( cos x))

    proof

      defpred X[ Nat] means ( cos (x + (((2 * $1) + 1) * PI ))) = ( - ( cos x));

      

       A1: for n be Nat st X[n] holds X[(n + 1)]

      proof

        let n be Nat;

        assume

         A2: ( cos (x + (((2 * n) + 1) * PI ))) = ( - ( cos x));

        ( cos (x + (((2 * (n + 1)) + 1) * PI ))) = ( cos ((x + (((2 * n) + 1) * PI )) + (2 * PI )))

        .= ((( cos (x + (((2 * n) + 1) * PI ))) * ( cos (2 * PI ))) - (( sin (x + (((2 * n) + 1) * PI ))) * ( sin (2 * PI )))) by SIN_COS: 75

        .= ( - ( cos x)) by A2, SIN_COS: 77;

        hence thesis;

      end;

      

       A3: X[ 0 ] by SIN_COS: 79;

      for n be Nat holds X[n] from NAT_1:sch 2( A3, A1);

      hence thesis;

    end;

    theorem :: INTEGRA8:5

    

     Th5: ( sin (x / 2)) >= 0 implies ( sin (x / 2)) = ( sqrt ((1 - ( cos x)) / 2))

    proof

      assume

       A1: ( sin (x / 2)) >= 0 ;

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

      .= ( sqrt ((1 - (1 - (2 * (( sin (x / 2)) ^2 )))) / 2)) by SIN_COS5: 7

      .= |.( sin (x / 2)).| by COMPLEX1: 72

      .= ( sin (x / 2)) by A1, ABSVALUE:def 1;

      hence thesis;

    end;

    theorem :: INTEGRA8:6

    

     Th6: ( sin (x / 2)) < 0 implies ( sin (x / 2)) = ( - ( sqrt ((1 - ( cos x)) / 2)))

    proof

      assume

       A1: ( sin (x / 2)) < 0 ;

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

      .= ( sqrt ((1 - (1 - (2 * (( sin (x / 2)) ^2 )))) / 2)) by SIN_COS5: 7

      .= |.( sin (x / 2)).| by COMPLEX1: 72

      .= ( - ( sin (x / 2))) by A1, ABSVALUE:def 1;

      hence thesis;

    end;

    theorem :: INTEGRA8:7

    

     Th7: ( sin ( PI / 4)) = (( sqrt 2) / 2)

    proof

      

       A1: ( sqrt 2) > 0 by SQUARE_1: 25;

      ( sin (( PI / 2) / 2)) = ( sqrt ((1 - ( cos ( PI / 2))) / 2)) by Lm1, Th5;

      

      then ( sin ( PI / 4)) = (1 / ( sqrt 2)) by SIN_COS: 77, SQUARE_1: 18, SQUARE_1: 30

      .= ((( sqrt 2) * 1) / (( sqrt 2) * ( sqrt 2))) by A1, XCMPLX_1: 91

      .= ((( sqrt 2) * 1) / (( sqrt 2) ^2 ));

      hence thesis by SQUARE_1:def 2;

    end;

    theorem :: INTEGRA8:8

    

     Th8: ( sin ( - ( PI / 4))) = ( - (( sqrt 2) / 2))

    proof

      

       A1: ( cos ( - ( PI / 2))) = ( sin (( PI / 2) - ( - ( PI / 2)))) by SIN_COS: 79

      .= 0 by SIN_COS: 77;

      

       A2: ( sqrt 2) > 0 by SQUARE_1: 25;

      ( sin (( - ( PI / 2)) / 2)) = ( - ( sqrt ((1 - ( cos ( - ( PI / 2)))) / 2))) by Lm2, Th6;

      

      then ( sin ( - ( PI / 4))) = ( - (1 / ( sqrt 2))) by A1, SQUARE_1: 18, SQUARE_1: 30

      .= ( - ((( sqrt 2) * 1) / (( sqrt 2) * ( sqrt 2)))) by A2, XCMPLX_1: 91

      .= ( - ((( sqrt 2) * 1) / (( sqrt 2) ^2 )));

      hence thesis by SQUARE_1:def 2;

    end;

    theorem :: INTEGRA8:9

    

     Th9: [.( - (( sqrt 2) / 2)), (( sqrt 2) / 2).] c= ].( - 1), 1.[

    proof

      

       A1: ( sqrt 2) > 0 by SQUARE_1: 25;

      ( sqrt 2) < ( sqrt 4) by SQUARE_1: 27;

      then

       A2: (( sqrt 2) / 2) < (2 / 2) by SQUARE_1: 20, XREAL_1: 74;

      then ((( sqrt 2) / 2) * ( - 1)) > (1 * ( - 1)) by XREAL_1: 69;

      then

       A3: ( - (( sqrt 2) / 2)) in ].( - 1), 1.[ by A1, XXREAL_1: 4;

      (( sqrt 2) / 2) > 0 by A1, XREAL_1: 139;

      then (( sqrt 2) / 2) in ].( - 1), 1.[ by A2, XXREAL_1: 4;

      hence thesis by A3, XXREAL_2:def 12;

    end;

    theorem :: INTEGRA8:10

    

     Th10: ( arcsin (( sqrt 2) / 2)) = ( PI / 4)

    proof

      ( PI / 4) < ( PI / 2) by XREAL_1: 76;

      hence thesis by Th7, SIN_COS6: 69;

    end;

    theorem :: INTEGRA8:11

    

     Th11: ( arcsin ( - (( sqrt 2) / 2))) = ( - ( PI / 4))

    proof

      ( PI / 4) < ( PI / 2) by XREAL_1: 76;

      then (( PI / 4) * ( - 1)) > (( PI / 2) * ( - 1)) by XREAL_1: 69;

      hence thesis by Th8, SIN_COS6: 69;

    end;

    theorem :: INTEGRA8:12

    

     Th12: ( cos (x / 2)) >= 0 implies ( cos (x / 2)) = ( sqrt ((1 + ( cos x)) / 2))

    proof

      assume

       A1: ( cos (x / 2)) >= 0 ;

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

      .= ( sqrt ((1 + ((2 * (( cos (x / 2)) ^2 )) - 1)) / 2)) by SIN_COS5: 7

      .= |.( cos (x / 2)).| by COMPLEX1: 72

      .= ( cos (x / 2)) by A1, ABSVALUE:def 1;

      hence thesis;

    end;

    

     Lm3: ( cos ( PI / 4)) > 0

    proof

      ( 0 / 2) < ( PI / 2) by XREAL_1: 74;

      then (( PI / 2) * ( - 1)) < ( 0 * ( - 1)) by XREAL_1: 69;

      then

       A1: (( - ( PI / 2)) + ((2 * PI ) * 0 )) < ( PI / 4);

      ( PI / 4) < (( PI / 2) + ((2 * PI ) * 0 )) by XREAL_1: 76;

      hence thesis by A1, SIN_COS6: 13;

    end;

    theorem :: INTEGRA8:13

    

     Th13: ( cos ( PI / 4)) = (( sqrt 2) / 2)

    proof

      

       A1: ( sqrt 2) > 0 by SQUARE_1: 25;

      ( cos (( PI / 2) / 2)) = ( sqrt ((1 + ( cos ( PI / 2))) / 2)) by Lm3, Th12

      .= (1 / ( sqrt 2)) by SIN_COS: 77, SQUARE_1: 18, SQUARE_1: 30

      .= ((( sqrt 2) * 1) / (( sqrt 2) * ( sqrt 2))) by A1, XCMPLX_1: 91

      .= ((( sqrt 2) * 1) / (( sqrt 2) ^2 ));

      hence thesis by SQUARE_1:def 2;

    end;

    theorem :: INTEGRA8:14

    

     Th14: ( cos ((3 * PI ) / 4)) = ( - (( sqrt 2) / 2))

    proof

      ( cos ((3 * PI ) / 4)) = ( cos (( PI / 2) + ( PI / 4)))

      .= ( - (( sqrt 2) / 2)) by Th7, SIN_COS: 79;

      hence thesis;

    end;

    theorem :: INTEGRA8:15

    

     Th15: ( arccos (( sqrt 2) / 2)) = ( PI / 4)

    proof

      ( PI / 4) < ( PI / 1) by XREAL_1: 76;

      hence thesis by Th13, SIN_COS6: 92;

    end;

    theorem :: INTEGRA8:16

    

     Th16: ( arccos ( - (( sqrt 2) / 2))) = ((3 * PI ) / 4)

    proof

      ((3 / 4) * PI ) < (1 * PI ) by XREAL_1: 68;

      hence thesis by Th14, SIN_COS6: 92;

    end;

    theorem :: INTEGRA8:17

    

     Th17: ( sinh . 1) = ((( number_e ^2 ) - 1) / (2 * number_e ))

    proof

      ( sinh . 1) = (( number_e - ( exp_R ( - 1))) / 2) by IRRAT_1:def 7, SIN_COS2:def 1

      .= ((( number_e / 1) - (1 / number_e )) / 2) by IRRAT_1:def 7, TAYLOR_1: 4

      .= (((( number_e * number_e ) / (1 * number_e )) - (1 / number_e )) / 2) by TAYLOR_1: 11, XCMPLX_1: 91

      .= (((( number_e ^2 ) / number_e ) - (1 / number_e )) / 2)

      .= (((( number_e ^2 ) - 1) / number_e ) / 2) by XCMPLX_1: 120

      .= ((( number_e ^2 ) - 1) / (2 * number_e )) by XCMPLX_1: 78;

      hence thesis;

    end;

    theorem :: INTEGRA8:18

    

     Th18: ( cosh . 0 ) = 1

    proof

      ( cosh . 0 ) = ((( exp_R . 0 ) + ( exp_R . ( - 0 ))) / 2) by SIN_COS2:def 3

      .= 1 by SIN_COS: 51;

      hence thesis;

    end;

    theorem :: INTEGRA8:19

    

     Th19: ( cosh . 1) = ((( number_e ^2 ) + 1) / (2 * number_e ))

    proof

      ( cosh . 1) = (( number_e + ( exp_R ( - 1))) / 2) by IRRAT_1:def 7, SIN_COS2:def 3

      .= ((( number_e / 1) + (1 / number_e )) / 2) by IRRAT_1:def 7, TAYLOR_1: 4

      .= (((( number_e * number_e ) / (1 * number_e )) + (1 / number_e )) / 2) by TAYLOR_1: 11, XCMPLX_1: 91

      .= (((( number_e ^2 ) / number_e ) + (1 / number_e )) / 2)

      .= (((( number_e ^2 ) + 1) / number_e ) / 2) by XCMPLX_1: 62

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

      hence thesis;

    end;

    

     Lm4: (( - f1) (#) ( - f2)) = (f1 (#) f2)

    proof

      (( - f1) (#) ( - f2)) = (( - 1) (#) (f1 (#) ( - f2))) by RFUNCT_1: 12

      .= (f1 (#) ( - ( - f2))) by RFUNCT_1: 13;

      hence thesis;

    end;

    theorem :: INTEGRA8:20

    

     Th20: for L1 be LinearFunc holds ( - L1) is LinearFunc

    proof

      let L1 be LinearFunc;

      consider g1 be Real such that

       A1: for p holds (L1 . p) = (g1 * p) by FDIFF_1:def 3;

      

       A2: L1 is total by FDIFF_1:def 3;

      now

        let p;

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

        

        thus (( - L1) . p) = ( - (L1 . pp)) by A2, RFUNCT_1: 58

        .= ( - (g1 * p)) by A1

        .= (( - g1) * p);

      end;

      hence thesis by A2, FDIFF_1:def 3;

    end;

    theorem :: INTEGRA8:21

    

     Th21: for R1 be RestFunc holds ( - R1) is RestFunc

    proof

      let R1 be RestFunc;

      

       A1: R1 is total by FDIFF_1:def 2;

      then

       A2: ( dom R1) = REAL by PARTFUN1:def 2;

      

       A3: for h be 0 -convergent non-zero Real_Sequence holds ( - (R1 /* h)) = (( - R1) /* h)

      proof

        let h be 0 -convergent non-zero Real_Sequence;

        ( rng h) c= ( dom R1) by A2, VALUED_0:def 3;

        hence thesis by RFUNCT_2: 10;

      end;

      now

        let h be 0 -convergent non-zero Real_Sequence;

        

         A4: ((h " ) (#) (R1 /* h)) is convergent by FDIFF_1:def 2;

        

         A5: ((h " ) (#) (( - R1) /* h)) = ((h " ) (#) ( - (R1 /* h))) by A3

        .= ( - ((h " ) (#) (R1 /* h))) by SEQ_1: 19;

        hence ((h " ) (#) (( - R1) /* h)) is convergent by A4, SEQ_2: 9;

        

         A6: ( lim ((h " ) (#) (R1 /* h))) = 0 by FDIFF_1:def 2;

        

        thus ( lim ((h " ) (#) (( - R1) /* h))) = ( - ( lim ((h " ) (#) (R1 /* h)))) by A4, A5, SEQ_2: 10

        .= 0 by A6;

      end;

      hence thesis by A1, FDIFF_1:def 2;

    end;

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

    theorem :: INTEGRA8:22

    

     Th22: for f1, x0 st f1 is_differentiable_in x0 holds ( - f1) is_differentiable_in x0 & ( diff (( - f1),x0)) = ( - ( diff (f1,x0)))

    proof

      let f1, x0;

      assume

       A1: f1 is_differentiable_in x0;

      then

      consider N1 be Neighbourhood of x0 such that

       A2: N1 c= ( dom f1) and

       A3: ex L be LinearFunc, R be RestFunc st for x st x in N1 holds ((f1 . x) - (f1 . x0)) = ((L . (x - x0)) + (R . (x - x0))) by FDIFF_1:def 4;

      consider L1 be LinearFunc, R1 be RestFunc such that

       A4: for x st x in N1 holds ((f1 . x) - (f1 . x0)) = ((L1 . (x - x0)) + (R1 . (x - x0))) by A3;

      reconsider R = ( - R1) as RestFunc by Th21;

      reconsider L = ( - L1) as LinearFunc by Th20;

      

       A5: L1 is total by FDIFF_1:def 3;

      consider N be Neighbourhood of x0 such that

       A6: N c= N1;

      

       A7: R1 is total by FDIFF_1:def 2;

       A8:

      now

        let x;

        assume

         A9: x in N;

        reconsider xx = x, xx0 = x0 as Element of REAL by XREAL_0:def 1;

        

        thus ((( - f1) . x) - (( - f1) . x0)) = (( - (f1 . x)) - (( - f1) . x0)) by VALUED_1: 8

        .= (( - (f1 . x)) - ( - (f1 . x0))) by VALUED_1: 8

        .= ( - ((f1 . x) - (f1 . x0)))

        .= ( - ((L1 . (x - x0)) + (R1 . (x - x0)))) by A4, A6, A9

        .= (( - (L1 . (x - x0))) + ( - (R1 . (x - x0))))

        .= ((L . (xx - xx0)) + ( - (R1 . (x - x0)))) by A5, RFUNCT_1: 58

        .= ((L . (x - x0)) + (R . (x - x0))) by A7, RFUNCT_1: 58;

      end;

      N c= ( dom f1) by A2, A6, XBOOLE_1: 1;

      then

       A10: N c= ( dom ( - f1)) by VALUED_1: 8;

      hence ( - f1) is_differentiable_in x0 by A8, FDIFF_1:def 4;

      

      hence ( diff (( - f1),x0)) = (L . 1) by A10, A8, FDIFF_1:def 5

      .= ( - (L1 . jj)) by A5, RFUNCT_1: 58

      .= ( - ( diff (f1,x0))) by A1, A2, A4, FDIFF_1:def 5;

    end;

    theorem :: INTEGRA8:23

    

     Th23: for f1, Z st Z c= ( dom ( - f1)) & f1 is_differentiable_on Z holds ( - f1) is_differentiable_on Z & for x st x in Z holds ((( - f1) `| Z) . x) = ( - ( diff (f1,x)))

    proof

      let f1, Z;

      assume that

       A1: Z c= ( dom ( - f1)) and

       A2: f1 is_differentiable_on Z;

      now

        let x0;

        assume x0 in Z;

        then f1 is_differentiable_in x0 by A2, FDIFF_1: 9;

        hence ( - f1) is_differentiable_in x0 by Th22;

      end;

      hence

       A3: ( - f1) is_differentiable_on Z by A1, FDIFF_1: 9;

      now

        let x;

        assume

         A4: x in Z;

        then

         A5: f1 is_differentiable_in x by A2, FDIFF_1: 9;

        

        thus ((( - f1) `| Z) . x) = ( diff (( - f1),x)) by A3, A4, FDIFF_1:def 7

        .= ( - ( diff (f1,x))) by A5, Th22;

      end;

      hence thesis;

    end;

    theorem :: INTEGRA8:24

    ( - sin ) is_differentiable_on REAL

    proof

      ( dom ( - sin )) = ( [#] REAL ) by FUNCT_2:def 1;

      hence thesis by Th23, SIN_COS: 68;

    end;

    theorem :: INTEGRA8:25

    

     Th25: ( - cos ) is_differentiable_in x & ( diff (( - cos ),x)) = ( sin . x)

    proof

      

       A1: cos is_differentiable_in x by SIN_COS: 63;

      

      then ( diff (( - cos ),x)) = ( - ( diff ( cos ,x))) by Th22

      .= ( - ( - ( sin . x))) by SIN_COS: 63;

      hence thesis by A1, Th22;

    end;

    theorem :: INTEGRA8:26

    

     Th26: ( - cos ) is_differentiable_on REAL & for x st x in REAL holds ( diff (( - cos ),x)) = ( sin . x)

    proof

      ( dom ( - cos )) = ( [#] REAL ) by FUNCT_2:def 1;

      hence thesis by Th23, Th25, SIN_COS: 67;

    end;

    theorem :: INTEGRA8:27

    

     Th27: ( sin `| REAL ) = cos

    proof

      for x st x in REAL holds ( diff ( sin ,x)) = ( cos . x) by SIN_COS: 68;

      hence thesis by FDIFF_1:def 7, SIN_COS: 24, SIN_COS: 68;

    end;

    theorem :: INTEGRA8:28

    

     Th28: ( cos `| REAL ) = ( - sin )

    proof

      

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

      proof

        let x be Element of REAL ;

        assume x in ( dom ( cos `| REAL ));

        (( cos `| REAL ) . x) = ( diff ( cos ,x)) by FDIFF_1:def 7, SIN_COS: 67

        .= ( - ( sin . x)) by SIN_COS: 63;

        hence thesis by VALUED_1: 8;

      end;

      ( dom ( - sin )) = REAL by FUNCT_2:def 1;

      then ( dom ( cos `| REAL )) = ( dom ( - sin )) by FDIFF_1:def 7, SIN_COS: 67;

      hence thesis by A1, PARTFUN1: 5;

    end;

    theorem :: INTEGRA8:29

    

     Th29: (( - cos ) `| REAL ) = sin by Th26, FDIFF_1:def 7, SIN_COS: 24;

    theorem :: INTEGRA8:30

    

     Th30: ( sinh `| REAL ) = cosh

    proof

      for x st x in REAL holds ( diff ( sinh ,x)) = ( cosh . x) by SIN_COS2: 34;

      hence thesis by FDIFF_1:def 7, SIN_COS2: 30, SIN_COS2: 34;

    end;

    theorem :: INTEGRA8:31

    

     Th31: ( cosh `| REAL ) = sinh

    proof

      for x st x in REAL holds ( diff ( cosh ,x)) = ( sinh . x) by SIN_COS2: 35;

      hence thesis by FDIFF_1:def 7, SIN_COS2: 30, SIN_COS2: 35;

    end;

    theorem :: INTEGRA8:32

    

     Th32: ( exp_R `| REAL ) = exp_R

    proof

      for x st x in REAL holds ( diff ( exp_R ,x)) = ( exp_R . x) by SIN_COS: 66;

      hence thesis by FDIFF_1:def 7, SIN_COS: 47, SIN_COS: 66;

    end;

    theorem :: INTEGRA8:33

    

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

    proof

      assume that

       A1: Z c= ( dom tan );

      

       A2: for x st x in Z holds tan is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then x in ( dom tan ) by A1;

        then

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

         sin is_differentiable_in x & cos is_differentiable_in x by SIN_COS: 63, SIN_COS: 64;

        hence thesis by A3, FDIFF_2: 14;

      end;

      then

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

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

      proof

        let x;

        

         A5: sin is_differentiable_in x & cos is_differentiable_in x by SIN_COS: 63, SIN_COS: 64;

        assume

         A6: x in Z;

        then x in ( dom tan ) by A1;

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

        

        then ( diff ( tan ,x)) = (((( diff ( sin ,x)) * ( cos . x)) - (( diff ( cos ,x)) * ( sin . x))) / (( cos . x) ^2 )) by A5, FDIFF_2: 14

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

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

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

        .= (1 / (( cos . x) ^2 )) by SIN_COS: 28;

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

      end;

      hence thesis by A1, A2, FDIFF_1: 9;

    end;

    theorem :: INTEGRA8:34

    

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

    proof

      assume that

       A1: Z c= ( dom cot );

      

       A2: for x st x in Z holds cot is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then x in ( dom cot ) by A1;

        then

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

         sin is_differentiable_in x & cos is_differentiable_in x by SIN_COS: 63, SIN_COS: 64;

        hence thesis by A3, FDIFF_2: 14;

      end;

      then

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

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

      proof

        let x;

        

         A5: sin is_differentiable_in x & cos is_differentiable_in x by SIN_COS: 63, SIN_COS: 64;

        assume

         A6: x in Z;

        then x in ( dom cot ) by A1;

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

        

        then ( diff ( cot ,x)) = (((( diff ( cos ,x)) * ( sin . x)) - (( diff ( sin ,x)) * ( cos . x))) / (( sin . x) ^2 )) by A5, FDIFF_2: 14

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

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

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

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

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

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

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

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

      end;

      hence thesis by A1, A2, FDIFF_1: 9;

    end;

    theorem :: INTEGRA8:35

    for r be Real holds ( rng ( REAL --> r)) c= REAL

    proof

      let r be Real;

      ( rng ( REAL --> r)) c= {r} by FUNCOP_1: 13;

      hence thesis by XBOOLE_1: 1;

    end;

    definition

      let r be Real;

      :: INTEGRA8:def1

      func Cst (r) -> Function of REAL , REAL equals ( REAL --> r);

      coherence

      proof

        reconsider r as Element of REAL by XREAL_0:def 1;

        ( REAL --> r) is Function of REAL , REAL ;

        hence thesis;

      end;

    end

    theorem :: INTEGRA8:36

    

     Th36: for a,b be Real, A be non empty closed_interval Subset of REAL holds ( chi (A,A)) = (( Cst 1) | A)

    proof

      let a,b be Real, A be non empty closed_interval Subset of REAL ;

      ( dom (( Cst 1) | A)) = A & for x be object st x in A holds (x in A implies ((( Cst 1) | A) . x) = 1) & ( not x in A implies ((( Cst 1) | A) . x) = 0 )

      proof

        

         A1: ( dom ( Cst 1)) = REAL & ( dom (( Cst 1) | A)) = (( dom ( Cst 1)) /\ A) by FUNCOP_1: 13, RELAT_1: 61;

        hence ( dom (( Cst 1) | A)) = A by XBOOLE_1: 28;

        let x be object;

        assume

         A2: x in A;

        then x in ( dom (( Cst 1) | A)) by A1, XBOOLE_0:def 4;

        

        then ((( Cst 1) | A) . x) = (( REAL --> 1) . x) by FUNCT_1: 47

        .= 1 by A2, FUNCOP_1: 7;

        hence thesis by A2;

      end;

      hence thesis by FUNCT_3:def 3;

    end;

    theorem :: INTEGRA8:37

    

     Th37: for a,b be Real, A be non empty closed_interval Subset of REAL st A = [.a, b.] holds ( upper_bound A) = b & ( lower_bound A) = a

    proof

      let a,b be Real, A be non empty closed_interval Subset of REAL ;

      

       A1: A = [.( lower_bound A), ( upper_bound A).] by INTEGRA1: 4;

      assume A = [.a, b.];

      hence thesis by A1, INTEGRA1: 5;

    end;

    begin

    theorem :: INTEGRA8:38

    for a,b be Real st a <= b holds ( integral (( Cst 1),a,b)) = (b - a)

    proof

      let a,b be Real;

      assume a <= b;

      then [.a, b.] = ['a, b'] by INTEGRA5:def 3;

      then

      reconsider A = [.a, b.] as non empty closed_interval Subset of REAL ;

      ( upper_bound A) = b & ( lower_bound A) = a by Th37;

      then

       A1: ( vol A) = (b - a) by INTEGRA1:def 5;

      ( integral (( Cst 1),a,b)) = ( integral (( Cst 1),A)) & (( Cst 1) || A) = ( chi (A,A)) by Th36, INTEGRA5: 19;

      hence thesis by A1, INTEGRA4: 2;

    end;

    

     Lm5: ( dom sin ) = REAL by FUNCT_2:def 1;

    

     Lm6: ( dom cos ) = REAL by FUNCT_2:def 1;

    

     Lm7: ( dom ( - sin )) = REAL by FUNCT_2:def 1;

    

     Lm8: ( dom exp_R ) = REAL by FUNCT_2:def 1;

    

     Lm9: ( dom sinh ) = REAL by FUNCT_2:def 1;

    

     Lm10: ( dom cosh ) = REAL by FUNCT_2:def 1;

    

     Lm11: cos is_integrable_on A & ( cos | A) is bounded

    proof

      ( cos | A) is continuous;

      hence thesis by Lm6, INTEGRA5: 10, INTEGRA5: 11;

    end;

    theorem :: INTEGRA8:39

    

     Th39: ( integral ( cos ,A)) = (( sin . ( upper_bound A)) - ( sin . ( lower_bound A)))

    proof

      

       A1: for x be Element of REAL st x in ( dom ( sin `| REAL )) holds (( sin `| REAL ) . x) = ( cos . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom ( sin `| REAL ));

        (( sin `| REAL ) . x) = ( diff ( sin ,x)) by FDIFF_1:def 7, SIN_COS: 68;

        hence thesis by SIN_COS: 64;

      end;

      

       A2: cos is_integrable_on A & ( cos | A) is bounded by Lm11;

      ( dom ( sin `| REAL )) = ( dom cos ) by FDIFF_1:def 7, SIN_COS: 24, SIN_COS: 68;

      then ( sin `| REAL ) = cos by A1, PARTFUN1: 5;

      hence thesis by A2, INTEGRA5: 13, SIN_COS: 68;

    end;

    theorem :: INTEGRA8:40

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

    proof

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

      then ( upper_bound A) = ( PI / 2) & ( lower_bound A) = 0 by Th37;

      

      then ( integral ( cos ,A)) = (1 - ( sin . 0 )) by Th39, SIN_COS: 77

      .= (1 - ( cos . (( PI / 2) - 0 ))) by SIN_COS: 78

      .= (1 - 0 ) by SIN_COS: 77;

      hence thesis;

    end;

    theorem :: INTEGRA8:41

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

    proof

      assume A = [. 0 , PI .];

      then ( upper_bound A) = PI & ( lower_bound A) = 0 by Th37;

      

      then ( integral ( cos ,A)) = ( 0 - ( sin . 0 )) by Th39, SIN_COS: 76

      .= ( 0 - ( sin . ( 0 + (2 * PI )))) by SIN_COS: 78

      .= ( 0 - 0 ) by SIN_COS: 76;

      hence thesis;

    end;

    theorem :: INTEGRA8:42

    A = [. 0 , (( PI * 3) / 2).] implies ( integral ( cos ,A)) = ( - 1)

    proof

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

      then ( upper_bound A) = (( PI * 3) / 2) & ( lower_bound A) = 0 by Th37;

      

      then ( integral ( cos ,A)) = (( - 1) - ( sin . 0 )) by Th39, SIN_COS: 76

      .= (( - 1) - ( sin . ( 0 + (2 * PI )))) by SIN_COS: 78

      .= (( - 1) - 0 ) by SIN_COS: 76;

      hence thesis;

    end;

    theorem :: INTEGRA8:43

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

    proof

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

      then ( upper_bound A) = ( PI * 2) & ( lower_bound A) = 0 by Th37;

      

      then ( integral ( cos ,A)) = ( 0 - ( sin . 0 )) by Th39, SIN_COS: 76

      .= ( 0 - ( sin . ( 0 + (2 * PI )))) by SIN_COS: 78

      .= ( 0 - 0 ) by SIN_COS: 76;

      hence thesis;

    end;

    theorem :: INTEGRA8:44

    A = [.((2 * n) * PI ), (((2 * n) + 1) * PI ).] implies ( integral ( cos ,A)) = 0

    proof

      assume A = [.((2 * n) * PI ), (((2 * n) + 1) * PI ).];

      then ( upper_bound A) = (((2 * n) + 1) * PI ) & ( lower_bound A) = ((2 * n) * PI ) by Th37;

      

      then ( integral ( cos ,A)) = (( sin ( 0 + (((2 * n) + 1) * PI ))) - ( sin ( 0 + ((2 * n) * PI )))) by Th39

      .= (( - ( sin 0 )) - ( sin ( 0 + ((2 * n) * PI )))) by Th2

      .= (( - ( sin 0 )) - ( sin 0 )) by Th1

      .= (( - ( sin ( 0 + (2 * PI )))) - ( sin 0 )) by SIN_COS: 79

      .= ( 0 - 0 ) by SIN_COS: 77, SIN_COS: 79;

      hence thesis;

    end;

    theorem :: INTEGRA8:45

    A = [.(x + ((2 * n) * PI )), (x + (((2 * n) + 1) * PI )).] implies ( integral ( cos ,A)) = ( - (2 * ( sin x)))

    proof

      assume A = [.(x + ((2 * n) * PI )), (x + (((2 * n) + 1) * PI )).];

      then ( upper_bound A) = (x + (((2 * n) + 1) * PI )) & ( lower_bound A) = (x + ((2 * n) * PI )) by Th37;

      

      then ( integral ( cos ,A)) = (( sin (x + (((2 * n) + 1) * PI ))) - ( sin (x + ((2 * n) * PI )))) by Th39

      .= (( - ( sin x)) - ( sin (x + ((2 * n) * PI )))) by Th2

      .= (( - ( sin x)) - ( sin x)) by Th1

      .= ( - (2 * ( sin x)));

      hence thesis;

    end;

    

     Lm12: ( - sin ) is_integrable_on A & (( - sin ) | A) is bounded

    proof

      (( - sin ) | A) is continuous;

      hence thesis by Lm7, INTEGRA5: 10, INTEGRA5: 11;

    end;

    theorem :: INTEGRA8:46

    

     Th46: ( integral (( - sin ),A)) = (( cos . ( upper_bound A)) - ( cos . ( lower_bound A)))

    proof

      

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

      proof

        let x be Element of REAL ;

        assume x in ( dom ( cos `| REAL ));

        (( cos `| REAL ) . x) = ( diff ( cos ,x)) by FDIFF_1:def 7, SIN_COS: 67

        .= ( - ( sin . x)) by SIN_COS: 63;

        hence thesis by VALUED_1: 8;

      end;

      

       A2: ( - sin ) is_integrable_on A & (( - sin ) | A) is bounded by Lm12;

      ( dom ( - sin )) = REAL by FUNCT_2:def 1;

      then ( dom ( cos `| REAL )) = ( dom ( - sin )) by FDIFF_1:def 7, SIN_COS: 67;

      then ( cos `| REAL ) = ( - sin ) by A1, PARTFUN1: 5;

      hence thesis by A2, INTEGRA5: 13, SIN_COS: 67;

    end;

    theorem :: INTEGRA8:47

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

    proof

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

      then ( upper_bound A) = ( PI / 2) & ( lower_bound A) = 0 by Th37;

      

      then ( integral (( - sin ),A)) = ( 0 - ( cos . 0 )) by Th46, SIN_COS: 76

      .= ( 0 - ( sin . (( PI / 2) - 0 ))) by SIN_COS: 78

      .= ( 0 - 1) by SIN_COS: 76;

      hence thesis;

    end;

    theorem :: INTEGRA8:48

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

    proof

      assume A = [. 0 , PI .];

      then ( upper_bound A) = PI & ( lower_bound A) = 0 by Th37;

      

      then ( integral (( - sin ),A)) = (( - 1) - ( cos . 0 )) by Th46, SIN_COS: 76

      .= (( - 1) - ( sin . (( PI / 2) - 0 ))) by SIN_COS: 78

      .= (( - 1) - 1) by SIN_COS: 76;

      hence thesis;

    end;

    theorem :: INTEGRA8:49

    A = [. 0 , (( PI * 3) / 2).] implies ( integral (( - sin ),A)) = ( - 1)

    proof

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

      then ( upper_bound A) = (( PI * 3) / 2) & ( lower_bound A) = 0 by Th37;

      

      then ( integral (( - sin ),A)) = ( 0 - ( cos . 0 )) by Th46, SIN_COS: 76

      .= ( 0 - ( sin . (( PI / 2) - 0 ))) by SIN_COS: 78

      .= ( 0 - 1) by SIN_COS: 76;

      hence thesis;

    end;

    theorem :: INTEGRA8:50

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

    proof

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

      then ( upper_bound A) = ( PI * 2) & ( lower_bound A) = 0 by Th37;

      

      then ( integral (( - sin ),A)) = (1 - ( cos . 0 )) by Th46, SIN_COS: 76

      .= (1 - ( sin . (( PI / 2) - 0 ))) by SIN_COS: 78

      .= (1 - 1) by SIN_COS: 76;

      hence thesis;

    end;

    theorem :: INTEGRA8:51

    A = [.((2 * n) * PI ), (((2 * n) + 1) * PI ).] implies ( integral (( - sin ),A)) = ( - 2)

    proof

      assume A = [.((2 * n) * PI ), (((2 * n) + 1) * PI ).];

      then ( upper_bound A) = (((2 * n) + 1) * PI ) & ( lower_bound A) = ((2 * n) * PI ) by Th37;

      

      then ( integral (( - sin ),A)) = (( cos ( 0 + (((2 * n) + 1) * PI ))) - ( cos ( 0 + ((2 * n) * PI )))) by Th46

      .= (( - ( cos 0 )) - ( cos ( 0 + ((2 * n) * PI )))) by Th4

      .= (( - ( cos 0 )) - ( cos 0 )) by Th3

      .= (( - ( cos ( 0 + (2 * PI )))) - ( cos 0 )) by SIN_COS: 79

      .= (( - 1) - 1) by SIN_COS: 77, SIN_COS: 79;

      hence thesis;

    end;

    theorem :: INTEGRA8:52

    A = [.(x + ((2 * n) * PI )), (x + (((2 * n) + 1) * PI )).] implies ( integral (( - sin ),A)) = ( - (2 * ( cos x)))

    proof

      assume A = [.(x + ((2 * n) * PI )), (x + (((2 * n) + 1) * PI )).];

      then ( upper_bound A) = (x + (((2 * n) + 1) * PI )) & ( lower_bound A) = (x + ((2 * n) * PI )) by Th37;

      

      then ( integral (( - sin ),A)) = (( cos (x + (((2 * n) + 1) * PI ))) - ( cos (x + ((2 * n) * PI )))) by Th46

      .= (( - ( cos x)) - ( cos (x + ((2 * n) * PI )))) by Th4

      .= (( - ( cos x)) - ( cos x)) by Th3

      .= ( - (2 * ( cos x)));

      hence thesis;

    end;

    

     Lm13: exp_R is_integrable_on A & ( exp_R | A) is bounded

    proof

      ( exp_R | A) is continuous;

      hence thesis by Lm8, INTEGRA5: 10, INTEGRA5: 11;

    end;

    theorem :: INTEGRA8:53

    

     Th53: ( integral ( exp_R ,A)) = (( exp_R . ( upper_bound A)) - ( exp_R . ( lower_bound A)))

    proof

      

       A1: for x be Element of REAL st x in ( dom ( exp_R `| REAL )) holds (( exp_R `| REAL ) . x) = ( exp_R . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom ( exp_R `| REAL ));

        (( exp_R `| REAL ) . x) = ( diff ( exp_R ,x)) by FDIFF_1:def 7, SIN_COS: 66;

        hence thesis by SIN_COS: 65;

      end;

      

       A2: exp_R is_integrable_on A & ( exp_R | A) is bounded by Lm13;

      ( dom ( exp_R `| REAL )) = ( dom exp_R ) by FDIFF_1:def 7, SIN_COS: 47, SIN_COS: 66;

      then ( exp_R `| REAL ) = exp_R by A1, PARTFUN1: 5;

      hence thesis by A2, INTEGRA5: 13, SIN_COS: 66;

    end;

    reconsider jj = 1 as Real;

    theorem :: INTEGRA8:54

    A = [. 0 , 1.] implies ( integral ( exp_R ,A)) = ( number_e - 1)

    proof

      assume A = [. 0 , 1.];

      then A = [. 0 , jj.];

      then ( upper_bound A) = 1 & ( lower_bound A) = 0 by Th37;

      hence thesis by Th53, IRRAT_1:def 7, SIN_COS: 51;

    end;

    

     Lm14: ( sinh | A) is continuous

    proof

      ( sinh | REAL ) is continuous by FDIFF_1: 25, SIN_COS2: 34;

      hence thesis by FCONT_1: 16;

    end;

    

     Lm15: sinh is_integrable_on A & ( sinh | A) is bounded by Lm14, Lm9, INTEGRA5: 10, INTEGRA5: 11;

    theorem :: INTEGRA8:55

    

     Th55: ( integral ( sinh ,A)) = (( cosh . ( upper_bound A)) - ( cosh . ( lower_bound A)))

    proof

      

       A1: for x be Element of REAL st x in ( dom ( cosh `| REAL )) holds (( cosh `| REAL ) . x) = ( sinh . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom ( cosh `| REAL ));

        (( cosh `| REAL ) . x) = ( diff ( cosh ,x)) by FDIFF_1:def 7, SIN_COS2: 35;

        hence thesis by SIN_COS2: 35;

      end;

      

       A2: sinh is_integrable_on A & ( sinh | A) is bounded by Lm15;

      ( dom ( cosh `| REAL )) = ( dom sinh ) by FDIFF_1:def 7, SIN_COS2: 30, SIN_COS2: 35;

      then ( cosh `| REAL ) = sinh by A1, PARTFUN1: 5;

      hence thesis by A2, INTEGRA5: 13, SIN_COS2: 35;

    end;

    theorem :: INTEGRA8:56

    A = [. 0 , 1.] implies ( integral ( sinh ,A)) = ((( number_e - 1) ^2 ) / (2 * number_e ))

    proof

      ( exp_R 1) > 0 by SIN_COS: 55;

      then

       A1: (2 * number_e ) > 0 by IRRAT_1:def 7, XREAL_1: 129;

      assume A = [. 0 , 1.];

      then A = [. 0 , jj.];

      then ( upper_bound A) = 1 & ( lower_bound A) = 0 by Th37;

      

      then ( integral ( sinh ,A)) = (((( number_e ^2 ) + 1) / (2 * number_e )) - 1) by Th18, Th19, Th55

      .= (((( number_e ^2 ) + 1) / (2 * number_e )) - ((2 * number_e ) / (2 * number_e ))) by A1, XCMPLX_1: 60

      .= (((( number_e ^2 ) + 1) - (2 * number_e )) / (2 * number_e )) by XCMPLX_1: 120

      .= (((( number_e ^2 ) - ((2 * number_e ) * 1)) + (1 ^2 )) / (2 * number_e ))

      .= ((( number_e - 1) ^2 ) / (2 * number_e ));

      hence thesis;

    end;

    

     Lm16: ( cosh | A) is continuous

    proof

      ( cosh | REAL ) is continuous by FDIFF_1: 25, SIN_COS2: 35;

      hence thesis by FCONT_1: 16;

    end;

    

     Lm17: cosh is_integrable_on A & ( cosh | A) is bounded by Lm16, Lm10, INTEGRA5: 10, INTEGRA5: 11;

    theorem :: INTEGRA8:57

    

     Th57: ( integral ( cosh ,A)) = (( sinh . ( upper_bound A)) - ( sinh . ( lower_bound A)))

    proof

      

       A1: for x be Element of REAL st x in ( dom ( sinh `| REAL )) holds (( sinh `| REAL ) . x) = ( cosh . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom ( sinh `| REAL ));

        (( sinh `| REAL ) . x) = ( diff ( sinh ,x)) by FDIFF_1:def 7, SIN_COS2: 34;

        hence thesis by SIN_COS2: 34;

      end;

      

       A2: cosh is_integrable_on A & ( cosh | A) is bounded by Lm17;

      ( dom ( sinh `| REAL )) = ( dom cosh ) by FDIFF_1:def 7, SIN_COS2: 30, SIN_COS2: 34;

      then ( sinh `| REAL ) = cosh by A1, PARTFUN1: 5;

      hence thesis by A2, INTEGRA5: 13, SIN_COS2: 34;

    end;

    theorem :: INTEGRA8:58

    A = [. 0 , 1.] implies ( integral ( cosh ,A)) = ((( number_e ^2 ) - 1) / (2 * number_e ))

    proof

      assume A = [. 0 , 1.];

      then A = [. 0 , jj.];

      then ( upper_bound A) = 1 & ( lower_bound A) = 0 by Th37;

      

      then ( integral ( cosh ,A)) = (( sinh . 1) - 0 ) by Th57, SIN_COS2: 16

      .= ((( number_e ^2 ) - 1) / (2 * number_e )) by Th17;

      hence thesis;

    end;

    theorem :: INTEGRA8:59

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

    proof

      assume that

       A1: A c= Z and

       A2: ( dom tan ) = Z and

       A3: ( dom tan ) = ( dom f2) and

       A4: for x st x in Z holds (f2 . x) = (1 / (( cos . x) ^2 )) & ( cos . x) <> 0 and

       A5: (f2 | A) is continuous;

      

       A6: f2 is_integrable_on A by A1, A2, A3, A5, INTEGRA5: 11;

      

       A7: tan is_differentiable_on Z by A2, Th33;

      

       A8: for x be Element of REAL st x in ( dom ( tan `| Z)) holds (( tan `| Z) . x) = (f2 . 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 A2, Th33

        .= (f2 . x) by A4, A9;

        hence thesis;

      end;

      ( dom ( tan `| Z)) = ( dom f2) by A2, A3, A7, FDIFF_1:def 7;

      then ( tan `| Z) = f2 by A8, PARTFUN1: 5;

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

    end;

    theorem :: INTEGRA8:60

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

    proof

      assume that

       A1: A c= Z and

       A2: ( dom cot ) = Z and

       A3: ( dom cot ) = ( dom f2) and

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

       A5: (f2 | A) is continuous;

      

       A6: f2 is_integrable_on A by A1, A2, A3, A5, INTEGRA5: 11;

      

       A7: cot is_differentiable_on Z by A2, Th34;

      

       A8: for x be Element of REAL st x in ( dom ( cot `| Z)) holds (( cot `| Z) . x) = (f2 . 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 A2, Th34

        .= (f2 . x) by A4, A9;

        hence thesis;

      end;

      ( dom ( cot `| Z)) = ( dom f2) by A2, A3, A7, FDIFF_1:def 7;

      then ( cot `| Z) = f2 by A8, PARTFUN1: 5;

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

    end;

    theorem :: INTEGRA8:61

    ( dom tanh ) = ( dom f2) & (for x st x in REAL holds (f2 . x) = (1 / (( cosh . x) ^2 ))) & (f2 | A) is continuous implies ( integral (f2,A)) = (( tanh . ( upper_bound A)) - ( tanh . ( lower_bound A)))

    proof

      assume that

       A1: ( dom tanh ) = ( dom f2) and

       A2: for x st x in REAL holds (f2 . x) = (1 / (( cosh . x) ^2 )) and

       A3: (f2 | A) is continuous;

      

       A4: for x be Element of REAL st x in ( dom ( tanh `| REAL )) holds (( tanh `| REAL ) . x) = (f2 . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom ( tanh `| REAL ));

        (( tanh `| REAL ) . x) = ( diff ( tanh ,x)) by FDIFF_1:def 7, SIN_COS2: 36

        .= (1 / (( cosh . x) ^2 )) by SIN_COS2: 33

        .= (f2 . x) by A2;

        hence thesis;

      end;

      ( dom ( tanh `| REAL )) = ( dom f2) by A1, FDIFF_1:def 7, SIN_COS2: 30, SIN_COS2: 36;

      then

       A5: ( tanh `| REAL ) = f2 by A4, PARTFUN1: 5;

      

       A6: ( dom tanh ) = REAL by FUNCT_2:def 1;

      then f2 is_integrable_on A by A1, A3, INTEGRA5: 11;

      hence thesis by A1, A3, A6, A5, INTEGRA5: 10, INTEGRA5: 13, SIN_COS2: 36;

    end;

    

     Lm18: ( dom ( arcsin `| ].( - 1), 1.[)) = ].( - 1), 1.[ by FDIFF_1:def 7, SIN_COS6: 83;

    theorem :: INTEGRA8:62

    

     Th62: A c= ].( - 1), 1.[ & ( dom ( arcsin `| ].( - 1), 1.[)) = ( dom f2) & (for x holds x in ].( - 1), 1.[ & (f2 . x) = (1 / ( sqrt (1 - (x ^2 ))))) & (f2 | A) is continuous implies ( integral (f2,A)) = (( arcsin . ( upper_bound A)) - ( arcsin . ( lower_bound A)))

    proof

      assume that

       A1: A c= ].( - 1), 1.[ and

       A2: ( dom ( arcsin `| ].( - 1), 1.[)) = ( dom f2) and

       A3: for x holds x in ].( - 1), 1.[ & (f2 . x) = (1 / ( sqrt (1 - (x ^2 )))) and

       A4: (f2 | A) is continuous;

      for x be Element of REAL st x in ( dom ( arcsin `| ].( - 1), 1.[)) holds (( arcsin `| ].( - 1), 1.[) . x) = (f2 . x)

      proof

        let x be Element of REAL ;

        assume

         A5: x in ( dom ( arcsin `| ].( - 1), 1.[));

        then

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

        (( arcsin `| ].( - 1), 1.[) . x) = ( diff ( arcsin ,x)) by A5, Lm18, FDIFF_1:def 7, SIN_COS6: 83

        .= (1 / ( sqrt (1 - (x ^2 )))) by A6, SIN_COS6: 83

        .= (f2 . x) by A3;

        hence thesis;

      end;

      then

       A7: ( arcsin `| ].( - 1), 1.[) = f2 by A2, PARTFUN1: 5;

      A c= ( dom f2) & f2 is_integrable_on A by A1, A2, A4, Lm18, INTEGRA5: 11;

      hence thesis by A1, A4, A7, INTEGRA5: 10, INTEGRA5: 13, SIN_COS6: 83;

    end;

    theorem :: INTEGRA8:63

    

     Th63: A c= ].( - 1), 1.[ & ( dom ( arccos `| ].( - 1), 1.[)) = ( dom f2) & (for x holds x in ].( - 1), 1.[ & (f2 . x) = ( - (1 / ( sqrt (1 - (x ^2 )))))) & (f2 | A) is continuous implies ( integral (f2,A)) = (( arccos . ( upper_bound A)) - ( arccos . ( lower_bound A)))

    proof

      assume that

       A1: A c= ].( - 1), 1.[ and

       A2: ( dom ( arccos `| ].( - 1), 1.[)) = ( dom f2) and

       A3: for x holds x in ].( - 1), 1.[ & (f2 . x) = ( - (1 / ( sqrt (1 - (x ^2 ))))) and

       A4: (f2 | A) is continuous;

      

       A5: A c= ( dom f2) by A1, A2, FDIFF_1:def 7, SIN_COS6: 106;

      

       A6: ( dom ( arccos `| ].( - 1), 1.[)) = ].( - 1), 1.[ by FDIFF_1:def 7, SIN_COS6: 106;

      for x be Element of REAL st x in ( dom ( arccos `| ].( - 1), 1.[)) holds (( arccos `| ].( - 1), 1.[) . x) = (f2 . x)

      proof

        let x be Element of REAL ;

        assume

         A7: x in ( dom ( arccos `| ].( - 1), 1.[));

        then

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

        (( arccos `| ].( - 1), 1.[) . x) = ( diff ( arccos ,x)) by A6, A7, FDIFF_1:def 7, SIN_COS6: 106

        .= ( - (1 / ( sqrt (1 - (x ^2 ))))) by A8, SIN_COS6: 106

        .= (f2 . x) by A3;

        hence thesis;

      end;

      then

       A9: ( arccos `| ].( - 1), 1.[) = f2 by A2, PARTFUN1: 5;

      f2 is_integrable_on A by A6, A1, A2, A4, INTEGRA5: 11;

      hence thesis by A1, A4, A5, A9, INTEGRA5: 10, INTEGRA5: 13, SIN_COS6: 106;

    end;

    theorem :: INTEGRA8:64

    A = [.( - (( sqrt 2) / 2)), (( sqrt 2) / 2).] & ( dom ( arcsin `| ].( - 1), 1.[)) = ( dom f2) & (for x holds x in ].( - 1), 1.[ & (f2 . x) = (1 / ( sqrt (1 - (x ^2 ))))) & (f2 | A) is continuous implies ( integral (f2,A)) = ( PI / 2)

    proof

      assume that

       A1: A = [.( - (( sqrt 2) / 2)), (( sqrt 2) / 2).] and

       A2: (( dom ( arcsin `| ].( - 1), 1.[)) = ( dom f2) & for x holds x in ].( - 1), 1.[ & (f2 . x) = (1 / ( sqrt (1 - (x ^2 ))))) & (f2 | A) is continuous;

      ( upper_bound A) = (( sqrt 2) / 2) & ( lower_bound A) = ( - (( sqrt 2) / 2)) by A1, Th37;

      

      then ( integral (f2,A)) = (( arcsin . (( sqrt 2) / 2)) - ( arcsin . ( - (( sqrt 2) / 2)))) by A1, A2, Th9, Th62

      .= (( arcsin (( sqrt 2) / 2)) - ( arcsin . ( - (( sqrt 2) / 2)))) by SIN_COS6:def 2

      .= (( arcsin (( sqrt 2) / 2)) - ( arcsin ( - (( sqrt 2) / 2)))) by SIN_COS6:def 2

      .= ((2 * PI ) / 4) by Th10, Th11;

      hence thesis;

    end;

    theorem :: INTEGRA8:65

    A = [.( - (( sqrt 2) / 2)), (( sqrt 2) / 2).] & ( dom ( arccos `| ].( - 1), 1.[)) = ( dom f2) & (for x holds x in ].( - 1), 1.[ & (f2 . x) = ( - (1 / ( sqrt (1 - (x ^2 )))))) & (f2 | A) is continuous implies ( integral (f2,A)) = ( - ( PI / 2))

    proof

      assume that

       A1: A = [.( - (( sqrt 2) / 2)), (( sqrt 2) / 2).] and

       A2: (( dom ( arccos `| ].( - 1), 1.[)) = ( dom f2) & for x holds x in ].( - 1), 1.[ & (f2 . x) = ( - (1 / ( sqrt (1 - (x ^2 )))))) & (f2 | A) is continuous;

      ( upper_bound A) = (( sqrt 2) / 2) & ( lower_bound A) = ( - (( sqrt 2) / 2)) by A1, Th37;

      

      then ( integral (f2,A)) = (( arccos . (( sqrt 2) / 2)) - ( arccos . ( - (( sqrt 2) / 2)))) by A1, A2, Th9, Th63

      .= (( arccos (( sqrt 2) / 2)) - ( arccos . ( - (( sqrt 2) / 2)))) by SIN_COS6:def 4

      .= (( arccos (( sqrt 2) / 2)) - ( arccos ( - (( sqrt 2) / 2)))) by SIN_COS6:def 4

      .= (( - (2 * PI )) / 4) by Th15, Th16;

      hence thesis;

    end;

    theorem :: INTEGRA8:66

    

     Th66: f is_differentiable_on Z & g is_differentiable_on Z & A c= Z & (f `| Z) is_integrable_on A & ((f `| Z) | A) is bounded & (g `| Z) is_integrable_on A & ((g `| Z) | A) is bounded implies ( integral (((f `| Z) + (g `| Z)),A)) = ((((f . ( upper_bound A)) - (f . ( lower_bound A))) + (g . ( upper_bound A))) - (g . ( lower_bound A)))

    proof

      assume that

       A1: f is_differentiable_on Z and

       A2: g is_differentiable_on Z and

       A3: A c= Z and

       A4: (f `| Z) is_integrable_on A and

       A5: ((f `| Z) | A) is bounded and

       A6: (g `| Z) is_integrable_on A and

       A7: ((g `| Z) | A) is bounded;

      

       A8: ((f `| Z) || A) is integrable & ((g `| Z) || A) is integrable by A4, A6;

      A c= ( dom (g `| Z)) by A2, A3, FDIFF_1:def 7;

      then

       A9: ((g `| Z) || A) is Function of A, REAL by FUNCT_2: 68, INTEGRA5: 6;

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

      then

       A10: ((f `| Z) || A) is Function of A, REAL by FUNCT_2: 68, INTEGRA5: 6;

      

       A11: (((f `| Z) || A) | A) is bounded & (((g `| Z) || A) | A) is bounded by A5, A7, INTEGRA5: 9;

      ( integral (((f `| Z) + (g `| Z)),A)) = ( integral (((f `| Z) || A) + ((g `| Z) || A))) by INTEGRA5: 5

      .= (( integral ((f `| Z),A)) + ( integral ((g `| Z),A))) by A8, A10, A9, A11, INTEGRA1: 57

      .= (((f . ( upper_bound A)) - (f . ( lower_bound A))) + ( integral ((g `| Z),A))) by A1, A3, A4, A5, INTEGRA5: 13

      .= (((f . ( upper_bound A)) - (f . ( lower_bound A))) + ((g . ( upper_bound A)) - (g . ( lower_bound A)))) by A2, A3, A6, A7, INTEGRA5: 13;

      hence thesis;

    end;

    theorem :: INTEGRA8:67

    

     Th67: f is_differentiable_on Z & g is_differentiable_on Z & A c= Z & (f `| Z) is_integrable_on A & ((f `| Z) | A) is bounded & (g `| Z) is_integrable_on A & ((g `| Z) | A) is bounded implies ( integral (((f `| Z) - (g `| Z)),A)) = (((f . ( upper_bound A)) - (f . ( lower_bound A))) - ((g . ( upper_bound A)) - (g . ( lower_bound A))))

    proof

      assume that

       A1: f is_differentiable_on Z and

       A2: g is_differentiable_on Z and

       A3: A c= Z and

       A4: (f `| Z) is_integrable_on A and

       A5: ((f `| Z) | A) is bounded and

       A6: (g `| Z) is_integrable_on A and

       A7: ((g `| Z) | A) is bounded;

      

       A8: ((f `| Z) || A) is integrable & ((g `| Z) || A) is integrable by A4, A6;

      A c= ( dom (g `| Z)) by A2, A3, FDIFF_1:def 7;

      then

       A9: ((g `| Z) || A) is Function of A, REAL by FUNCT_2: 68, INTEGRA5: 6;

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

      then

       A10: ((f `| Z) || A) is Function of A, REAL by FUNCT_2: 68, INTEGRA5: 6;

      

       A11: (((f `| Z) || A) | A) is bounded & (((g `| Z) || A) | A) is bounded by A5, A7, INTEGRA5: 9;

      ( integral (((f `| Z) - (g `| Z)),A)) = ( integral (((f `| Z) || A) - ((g `| Z) || A))) by RFUNCT_1: 47

      .= (( integral ((f `| Z),A)) - ( integral ((g `| Z) || A))) by A8, A10, A9, A11, INTEGRA2: 33

      .= (((f . ( upper_bound A)) - (f . ( lower_bound A))) - ( integral ((g `| Z),A))) by A1, A3, A4, A5, INTEGRA5: 13

      .= (((f . ( upper_bound A)) - (f . ( lower_bound A))) - ((g . ( upper_bound A)) - (g . ( lower_bound A)))) by A2, A3, A6, A7, INTEGRA5: 13;

      hence thesis;

    end;

    theorem :: INTEGRA8:68

    

     Th68: f is_differentiable_on Z & A c= Z & (f `| Z) is_integrable_on A & ((f `| Z) | A) is bounded implies ( integral ((r (#) (f `| Z)),A)) = ((r * (f . ( upper_bound A))) - (r * (f . ( lower_bound A))))

    proof

      assume that

       A1: f is_differentiable_on Z & A c= Z and

       A2: (f `| Z) is_integrable_on A & ((f `| Z) | A) is bounded;

      

       A3: ((f `| Z) || A) is integrable & (((f `| Z) || A) | A) is bounded by A2, INTEGRA5: 9;

      A c= ( dom (f `| Z)) by A1, FDIFF_1:def 7;

      then

       A4: ((f `| Z) || A) is Function of A, REAL by FUNCT_2: 68, INTEGRA5: 6;

      ( integral ((r (#) (f `| Z)),A)) = ( integral (r (#) ((f `| Z) || A))) by RFUNCT_1: 49

      .= (r * ( integral ((f `| Z),A))) by A4, A3, INTEGRA2: 31

      .= (r * ((f . ( upper_bound A)) - (f . ( lower_bound A)))) by A1, A2, INTEGRA5: 13;

      hence thesis;

    end;

    

     Lm19: sin is_integrable_on A & ( sin | A) is bounded

    proof

      ( sin | A) is continuous;

      hence thesis by Lm5, INTEGRA5: 10, INTEGRA5: 11;

    end;

    theorem :: INTEGRA8:69

    

     Th69: ( integral (( sin + cos ),A)) = ((((( - cos ) . ( upper_bound A)) - (( - cos ) . ( lower_bound A))) + ( sin . ( upper_bound A))) - ( sin . ( lower_bound A)))

    proof

      

       A1: ( [#] REAL ) is open Subset of REAL ;

      

       A2: sin is_integrable_on A & ( sin | A) is bounded by Lm19;

       cos is_integrable_on A & ( cos | A) is bounded by Lm11;

      hence thesis by A2, A1, Th26, Th27, Th29, Th66, SIN_COS: 68;

    end;

    theorem :: INTEGRA8:70

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

    proof

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

      then ( upper_bound A) = ( PI / 2) & ( lower_bound A) = 0 by Th37;

      

      then ( integral (( sin + cos ),A)) = ((((( - cos ) . ( PI / 2)) - (( - cos ) . 0 )) + ( sin . ( PI / 2))) - ( sin . 0 )) by Th69

      .= (((( - ( cos . ( PI / 2))) - (( - cos ) . 0 )) + ( sin . ( PI / 2))) - ( sin . 0 )) by VALUED_1: 8

      .= (((( - 0 ) - ( - ( cos . 0 ))) + 1) - ( sin . 0 )) by SIN_COS: 76, VALUED_1: 8

      .= ((( - ( - ( cos . 0 ))) + 1) - ( sin . ( 0 + (2 * PI )))) by SIN_COS: 78

      .= ((( - ( - ( cos . ( 0 + (2 * PI ))))) + 1) - 0 ) by SIN_COS: 76, SIN_COS: 78

      .= 2 by SIN_COS: 76;

      hence thesis;

    end;

    theorem :: INTEGRA8:71

    A = [. 0 , PI .] implies ( integral (( sin + cos ),A)) = 2

    proof

      assume A = [. 0 , PI .];

      then ( upper_bound A) = PI & ( lower_bound A) = 0 by Th37;

      

      then ( integral (( sin + cos ),A)) = ((((( - cos ) . PI ) - (( - cos ) . 0 )) + ( sin . PI )) - ( sin . 0 )) by Th69

      .= (((( - ( cos . PI )) - (( - cos ) . 0 )) + ( sin . PI )) - ( sin . 0 )) by VALUED_1: 8

      .= (((( - ( cos . PI )) - ( - ( cos . 0 ))) + ( sin . PI )) - ( sin . 0 )) by VALUED_1: 8

      .= ((( - ( - ( cos . 0 ))) + 1) - ( sin . ( 0 + (2 * PI )))) by SIN_COS: 76, SIN_COS: 78

      .= ((( - ( - ( cos . ( 0 + (2 * PI ))))) + 1) - 0 ) by SIN_COS: 76, SIN_COS: 78

      .= 2 by SIN_COS: 76;

      hence thesis;

    end;

    theorem :: INTEGRA8:72

    A = [. 0 , (( PI * 3) / 2).] implies ( integral (( sin + cos ),A)) = 0

    proof

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

      then ( upper_bound A) = (( PI * 3) / 2) & ( lower_bound A) = 0 by Th37;

      

      then ( integral (( sin + cos ),A)) = ((((( - cos ) . (( PI * 3) / 2)) - (( - cos ) . 0 )) + ( sin . (( PI * 3) / 2))) - ( sin . 0 )) by Th69

      .= (((( - ( cos . (( PI * 3) / 2))) - (( - cos ) . 0 )) + ( sin . (( PI * 3) / 2))) - ( sin . 0 )) by VALUED_1: 8

      .= (((( - ( cos . (( PI * 3) / 2))) - ( - ( cos . 0 ))) + ( sin . (( PI * 3) / 2))) - ( sin . 0 )) by VALUED_1: 8

      .= (((( - ( cos . (( PI * 3) / 2))) - ( - ( cos . ( 0 + (2 * PI ))))) + ( sin . (( PI * 3) / 2))) - ( sin . 0 )) by SIN_COS: 78

      .= (((( - 0 ) + 1) + ( - 1)) - 0 ) by SIN_COS: 76, SIN_COS: 78;

      hence thesis;

    end;

    theorem :: INTEGRA8:73

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

    proof

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

      then ( upper_bound A) = ( PI * 2) & ( lower_bound A) = 0 by Th37;

      

      then ( integral (( sin + cos ),A)) = ((((( - cos ) . ( PI * 2)) - (( - cos ) . 0 )) + ( sin . ( PI * 2))) - ( sin . 0 )) by Th69

      .= (((( - ( cos . ( PI * 2))) - (( - cos ) . 0 )) + ( sin . ( PI * 2))) - ( sin . 0 )) by VALUED_1: 8

      .= (((( - ( cos . ( PI * 2))) - ( - ( cos . 0 ))) + ( sin . ( PI * 2))) - ( sin . 0 )) by VALUED_1: 8

      .= (((( - ( cos . ( PI * 2))) - ( - ( cos . ( 0 + (2 * PI ))))) + ( sin . ( PI * 2))) - ( sin . 0 )) by SIN_COS: 78

      .= (((( - 1) + 1) + 0 ) - 0 ) by SIN_COS: 76, SIN_COS: 78;

      hence thesis;

    end;

    theorem :: INTEGRA8:74

    A = [.((2 * n) * PI ), (((2 * n) + 1) * PI ).] implies ( integral (( sin + cos ),A)) = 2

    proof

      assume A = [.((2 * n) * PI ), (((2 * n) + 1) * PI ).];

      then ( upper_bound A) = (((2 * n) + 1) * PI ) & ( lower_bound A) = ((2 * n) * PI ) by Th37;

      

      then ( integral (( sin + cos ),A)) = ((((( - cos ) . (((2 * n) + 1) * PI )) - (( - cos ) . ((2 * n) * PI ))) + ( sin . (((2 * n) + 1) * PI ))) - ( sin . ((2 * n) * PI ))) by Th69

      .= (((( - ( cos . (((2 * n) + 1) * PI ))) - (( - cos ) . ((2 * n) * PI ))) + ( sin . (((2 * n) + 1) * PI ))) - ( sin . ((2 * n) * PI ))) by VALUED_1: 8

      .= (((( - ( cos . (((2 * n) + 1) * PI ))) - ( - ( cos ( 0 + ((2 * n) * PI ))))) + ( sin . (((2 * n) + 1) * PI ))) - ( sin . ( 0 + ((2 * n) * PI )))) by VALUED_1: 8

      .= (((( - ( cos . (((2 * n) + 1) * PI ))) - ( - ( cos 0 ))) + ( sin . (((2 * n) + 1) * PI ))) - ( sin . ( 0 + ((2 * n) * PI )))) by Th3

      .= (((( - ( cos . (((2 * n) + 1) * PI ))) + ( cos 0 )) + ( sin . (((2 * n) + 1) * PI ))) - ( sin . ( 0 + ((2 * n) * PI ))))

      .= (((( - ( cos . (((2 * n) + 1) * PI ))) + ( cos ( 0 + (2 * PI )))) + ( sin . (((2 * n) + 1) * PI ))) - ( sin . ( 0 + ((2 * n) * PI )))) by SIN_COS: 79

      .= (((( - ( cos . (((2 * n) + 1) * PI ))) + 1) + ( sin . (((2 * n) + 1) * PI ))) - ( sin ( 0 + ((2 * n) * PI )))) by SIN_COS: 77

      .= (((( - ( cos . (((2 * n) + 1) * PI ))) + 1) + ( sin . (((2 * n) + 1) * PI ))) - ( sin 0 )) by Th1

      .= (((( - ( cos . (((2 * n) + 1) * PI ))) + 1) + ( sin . (((2 * n) + 1) * PI ))) - ( sin ( 0 + (2 * PI )))) by SIN_COS: 79

      .= ((( - ( cos ( 0 + (((2 * n) + 1) * PI )))) + 1) + ( sin ( 0 + (((2 * n) + 1) * PI )))) by SIN_COS: 77

      .= ((( - ( cos ( 0 + (((2 * n) + 1) * PI )))) + 1) + ( - ( sin 0 ))) by Th2

      .= ((( - ( - ( cos 0 ))) + 1) + ( - ( sin 0 ))) by Th4

      .= ((( cos 0 ) + 1) - ( sin 0 ))

      .= ((( cos ( 0 + (2 * PI ))) + 1) - ( sin 0 )) by SIN_COS: 79

      .= ((( cos ( 0 + (2 * PI ))) + 1) - ( sin ( 0 + (2 * PI )))) by SIN_COS: 79

      .= 2 by SIN_COS: 77;

      hence thesis;

    end;

    theorem :: INTEGRA8:75

    A = [.(x + ((2 * n) * PI )), (x + (((2 * n) + 1) * PI )).] implies ( integral (( sin + cos ),A)) = ((2 * ( cos x)) - (2 * ( sin x)))

    proof

      assume A = [.(x + ((2 * n) * PI )), (x + (((2 * n) + 1) * PI )).];

      then ( upper_bound A) = (x + (((2 * n) + 1) * PI )) & ( lower_bound A) = (x + ((2 * n) * PI )) by Th37;

      

      then ( integral (( sin + cos ),A)) = ((((( - cos ) . (x + (((2 * n) + 1) * PI ))) - (( - cos ) . (x + ((2 * n) * PI )))) + ( sin . (x + (((2 * n) + 1) * PI )))) - ( sin . (x + ((2 * n) * PI )))) by Th69

      .= (((( - ( cos . (x + (((2 * n) + 1) * PI )))) - (( - cos ) . (x + ((2 * n) * PI )))) + ( sin . (x + (((2 * n) + 1) * PI )))) - ( sin . (x + ((2 * n) * PI )))) by VALUED_1: 8

      .= (((( - ( cos (x + (((2 * n) + 1) * PI )))) - ( - ( cos (x + ((2 * n) * PI ))))) + ( sin (x + (((2 * n) + 1) * PI )))) - ( sin (x + ((2 * n) * PI )))) by VALUED_1: 8

      .= (((( - ( - ( cos x))) - ( - ( cos (x + ((2 * n) * PI ))))) + ( sin (x + (((2 * n) + 1) * PI )))) - ( sin (x + ((2 * n) * PI )))) by Th4

      .= (((( - ( - ( cos x))) - ( - ( cos x))) + ( sin (x + (((2 * n) + 1) * PI )))) - ( sin (x + ((2 * n) * PI )))) by Th3

      .= (((( - ( - ( cos x))) - ( - ( cos x))) + ( - ( sin x))) - ( sin (x + ((2 * n) * PI )))) by Th2

      .= (((( cos x) + ( cos x)) - ( sin x)) - ( sin x)) by Th1

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

      hence thesis;

    end;

    theorem :: INTEGRA8:76

    

     Th76: ( integral (( sinh + cosh ),A)) = (((( cosh . ( upper_bound A)) - ( cosh . ( lower_bound A))) + ( sinh . ( upper_bound A))) - ( sinh . ( lower_bound A)))

    proof

      

       A1: ( [#] REAL ) is open Subset of REAL ;

      ( cosh | A) is continuous by Lm16;

      then

       A2: cosh is_integrable_on A by Lm10, INTEGRA5: 11;

      ( sinh | A) is continuous by Lm14;

      then

       A3: sinh is_integrable_on A by Lm9, INTEGRA5: 11;

      ( cosh | A) is bounded & ( sinh | A) is bounded by Lm9, Lm10, Lm14, Lm16, INTEGRA5: 10;

      hence thesis by A2, A3, A1, Th30, Th31, Th66, SIN_COS2: 34, SIN_COS2: 35;

    end;

    theorem :: INTEGRA8:77

    A = [. 0 , 1.] implies ( integral (( sinh + cosh ),A)) = ( number_e - 1)

    proof

      

       A1: number_e > 0 by IRRAT_1:def 7, SIN_COS: 55;

      assume A = [. 0 , 1.];

      then ( upper_bound A) = 1 & ( lower_bound A) = 0 by Th37;

      

      then ( integral (( sinh + cosh ),A)) = (((( cosh . 1) - ( cosh . 0 )) + ( sinh . 1)) - ( sinh . 0 )) by Th76

      .= ((((( number_e ^2 ) + 1) / (2 * number_e )) + ((( number_e ^2 ) - 1) / (2 * number_e ))) - 1) by Th17, Th18, Th19, SIN_COS2: 16

      .= ((((( number_e ^2 ) + 1) + (( number_e ^2 ) - 1)) / (2 * number_e )) - 1) by XCMPLX_1: 62

      .= (((2 * ( number_e ^2 )) / (2 * number_e )) - 1)

      .= ((( number_e ^2 ) / number_e ) - 1) by XCMPLX_1: 91

      .= ((( number_e * number_e ) / number_e ) - 1)

      .= ( number_e - 1) by A1, XCMPLX_1: 89;

      hence thesis;

    end;

    theorem :: INTEGRA8:78

    

     Th78: ( integral (( sin - cos ),A)) = (((( - cos ) . ( upper_bound A)) - (( - cos ) . ( lower_bound A))) - (( sin . ( upper_bound A)) - ( sin . ( lower_bound A))))

    proof

      

       A1: ( [#] REAL ) is open Subset of REAL ;

      

       A2: sin is_integrable_on A & ( sin | A) is bounded by Lm19;

       cos is_integrable_on A & ( cos | A) is bounded by Lm11;

      hence thesis by A2, A1, Th26, Th27, Th29, Th67, SIN_COS: 68;

    end;

    theorem :: INTEGRA8:79

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

    proof

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

      then ( upper_bound A) = ( PI / 2) & ( lower_bound A) = 0 by Th37;

      

      then ( integral (( sin - cos ),A)) = (((( - cos ) . ( PI / 2)) - (( - cos ) . 0 )) - (( sin . ( PI / 2)) - ( sin . 0 ))) by Th78

      .= ((( - ( cos . ( PI / 2))) - (( - cos ) . 0 )) - (( sin . ( PI / 2)) - ( sin . 0 ))) by VALUED_1: 8

      .= ((( - 0 ) - ( - ( cos . 0 ))) - (1 - ( sin . 0 ))) by SIN_COS: 76, VALUED_1: 8

      .= (( - ( - ( cos . 0 ))) - (1 - ( sin . ( 0 + (2 * PI ))))) by SIN_COS: 78

      .= (( - ( - ( cos . ( 0 + (2 * PI ))))) - (1 - 0 )) by SIN_COS: 76, SIN_COS: 78

      .= 0 by SIN_COS: 76;

      hence thesis;

    end;

    theorem :: INTEGRA8:80

    A = [. 0 , PI .] implies ( integral (( sin - cos ),A)) = 2

    proof

      assume A = [. 0 , PI .];

      then ( upper_bound A) = PI & ( lower_bound A) = 0 by Th37;

      

      then ( integral (( sin - cos ),A)) = (((( - cos ) . PI ) - (( - cos ) . 0 )) - (( sin . PI ) - ( sin . 0 ))) by Th78

      .= ((( - ( cos . PI )) - (( - cos ) . 0 )) - (( sin . PI ) - ( sin . 0 ))) by VALUED_1: 8

      .= ((( - ( cos . PI )) - ( - ( cos . 0 ))) - (( sin . PI ) - ( sin . 0 ))) by VALUED_1: 8

      .= ((( - ( - ( cos . 0 ))) + 1) - (( sin . ( 0 + (2 * PI ))) - 0 )) by SIN_COS: 76, SIN_COS: 78

      .= ((( - ( - ( cos . ( 0 + (2 * PI ))))) + 1) - 0 ) by SIN_COS: 76, SIN_COS: 78

      .= 2 by SIN_COS: 76;

      hence thesis;

    end;

    theorem :: INTEGRA8:81

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

    proof

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

      then ( upper_bound A) = (( PI * 3) / 2) & ( lower_bound A) = 0 by Th37;

      

      then ( integral (( sin - cos ),A)) = (((( - cos ) . (( PI * 3) / 2)) - (( - cos ) . 0 )) - (( sin . (( PI * 3) / 2)) - ( sin . 0 ))) by Th78

      .= ((( - ( cos . (( PI * 3) / 2))) - (( - cos ) . 0 )) - (( sin . (( PI * 3) / 2)) - ( sin . 0 ))) by VALUED_1: 8

      .= ((( - ( cos . (( PI * 3) / 2))) - ( - ( cos . 0 ))) - (( sin . (( PI * 3) / 2)) - ( sin . 0 ))) by VALUED_1: 8

      .= ((( - ( cos . (( PI * 3) / 2))) - ( - ( cos . ( 0 + (2 * PI ))))) - (( sin . (( PI * 3) / 2)) - ( sin . 0 ))) by SIN_COS: 78

      .= ((( - 0 ) + 1) - (( - 1) - 0 )) by SIN_COS: 76, SIN_COS: 78;

      hence thesis;

    end;

    theorem :: INTEGRA8:82

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

    proof

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

      then ( upper_bound A) = ( PI * 2) & ( lower_bound A) = 0 by Th37;

      

      then ( integral (( sin - cos ),A)) = (((( - cos ) . ( PI * 2)) - (( - cos ) . 0 )) - (( sin . ( PI * 2)) - ( sin . 0 ))) by Th78

      .= ((( - ( cos . ( PI * 2))) - (( - cos ) . 0 )) - (( sin . ( PI * 2)) - ( sin . 0 ))) by VALUED_1: 8

      .= ((( - ( cos . ( PI * 2))) - ( - ( cos . 0 ))) - (( sin . ( PI * 2)) - ( sin . 0 ))) by VALUED_1: 8

      .= ((( - ( cos . ( PI * 2))) - ( - ( cos . ( 0 + (2 * PI ))))) - (( sin . ( PI * 2)) - ( sin . 0 ))) by SIN_COS: 78

      .= ((( - 1) + 1) - ( 0 - 0 )) by SIN_COS: 76, SIN_COS: 78;

      hence thesis;

    end;

    theorem :: INTEGRA8:83

    A = [.((2 * n) * PI ), (((2 * n) + 1) * PI ).] implies ( integral (( sin - cos ),A)) = 2

    proof

      assume A = [.((2 * n) * PI ), (((2 * n) + 1) * PI ).];

      then ( upper_bound A) = (((2 * n) + 1) * PI ) & ( lower_bound A) = ((2 * n) * PI ) by Th37;

      

      then ( integral (( sin - cos ),A)) = (((( - cos ) . (((2 * n) + 1) * PI )) - (( - cos ) . ((2 * n) * PI ))) - (( sin . (((2 * n) + 1) * PI )) - ( sin . ((2 * n) * PI )))) by Th78

      .= ((( - ( cos . (((2 * n) + 1) * PI ))) - (( - cos ) . ((2 * n) * PI ))) - (( sin . (((2 * n) + 1) * PI )) - ( sin . ((2 * n) * PI )))) by VALUED_1: 8

      .= ((( - ( cos . (((2 * n) + 1) * PI ))) - ( - ( cos ( 0 + ((2 * n) * PI ))))) - (( sin . (((2 * n) + 1) * PI )) - ( sin . ( 0 + ((2 * n) * PI ))))) by VALUED_1: 8

      .= ((( - ( cos . (((2 * n) + 1) * PI ))) - ( - ( cos 0 ))) - (( sin . (((2 * n) + 1) * PI )) - ( sin . ( 0 + ((2 * n) * PI ))))) by Th3

      .= ((( - ( cos . (((2 * n) + 1) * PI ))) + ( cos 0 )) - (( sin . (((2 * n) + 1) * PI )) - ( sin . ( 0 + ((2 * n) * PI )))))

      .= ((( - ( cos . (((2 * n) + 1) * PI ))) + ( cos ( 0 + (2 * PI )))) - (( sin . (((2 * n) + 1) * PI )) - ( sin . ( 0 + ((2 * n) * PI ))))) by SIN_COS: 79

      .= ((( - ( cos . (((2 * n) + 1) * PI ))) + 1) - (( sin . (((2 * n) + 1) * PI )) - ( sin ( 0 + ((2 * n) * PI ))))) by SIN_COS: 77

      .= ((( - ( cos . (((2 * n) + 1) * PI ))) + 1) - (( sin . (((2 * n) + 1) * PI )) - ( sin 0 ))) by Th1

      .= ((( - ( cos . (((2 * n) + 1) * PI ))) + 1) - (( sin . (((2 * n) + 1) * PI )) - ( sin ( 0 + (2 * PI ))))) by SIN_COS: 79

      .= ((( - ( cos ( 0 + (((2 * n) + 1) * PI )))) + 1) - ( sin ( 0 + (((2 * n) + 1) * PI )))) by SIN_COS: 77

      .= ((( - ( cos ( 0 + (((2 * n) + 1) * PI )))) + 1) - ( - ( sin 0 ))) by Th2

      .= ((( - ( - ( cos 0 ))) + 1) - ( - ( sin 0 ))) by Th4

      .= ((( cos 0 ) + 1) + ( sin 0 ))

      .= ((( cos ( 0 + (2 * PI ))) + 1) + ( sin 0 )) by SIN_COS: 79

      .= ((( cos ( 0 + (2 * PI ))) + 1) + ( sin ( 0 + (2 * PI )))) by SIN_COS: 79

      .= 2 by SIN_COS: 77;

      hence thesis;

    end;

    theorem :: INTEGRA8:84

    A = [.(x + ((2 * n) * PI )), (x + (((2 * n) + 1) * PI )).] implies ( integral (( sin - cos ),A)) = ((2 * ( cos x)) + (2 * ( sin x)))

    proof

      assume A = [.(x + ((2 * n) * PI )), (x + (((2 * n) + 1) * PI )).];

      then ( upper_bound A) = (x + (((2 * n) + 1) * PI )) & ( lower_bound A) = (x + ((2 * n) * PI )) by Th37;

      

      then ( integral (( sin - cos ),A)) = (((( - cos ) . (x + (((2 * n) + 1) * PI ))) - (( - cos ) . (x + ((2 * n) * PI )))) - (( sin . (x + (((2 * n) + 1) * PI ))) - ( sin . (x + ((2 * n) * PI ))))) by Th78

      .= ((( - ( cos . (x + (((2 * n) + 1) * PI )))) - (( - cos ) . (x + ((2 * n) * PI )))) - (( sin . (x + (((2 * n) + 1) * PI ))) - ( sin . (x + ((2 * n) * PI ))))) by VALUED_1: 8

      .= ((( - ( cos (x + (((2 * n) + 1) * PI )))) - ( - ( cos (x + ((2 * n) * PI ))))) - (( sin (x + (((2 * n) + 1) * PI ))) - ( sin (x + ((2 * n) * PI ))))) by VALUED_1: 8

      .= ((( - ( - ( cos x))) - ( - ( cos (x + ((2 * n) * PI ))))) - (( sin (x + (((2 * n) + 1) * PI ))) - ( sin (x + ((2 * n) * PI ))))) by Th4

      .= ((( - ( - ( cos x))) - ( - ( cos x))) - (( sin (x + (((2 * n) + 1) * PI ))) - ( sin (x + ((2 * n) * PI ))))) by Th3

      .= ((( - ( - ( cos x))) - ( - ( cos x))) - (( - ( sin x)) - ( sin (x + ((2 * n) * PI ))))) by Th2

      .= ((( cos x) + ( cos x)) - (( - ( sin x)) - ( sin x))) by Th1

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

      hence thesis;

    end;

    theorem :: INTEGRA8:85

    ( integral ((r (#) sin ),A)) = ((r * (( - cos ) . ( upper_bound A))) - (r * (( - cos ) . ( lower_bound A))))

    proof

      ( sin | A) is bounded & ( [#] REAL ) is open Subset of REAL by Lm5, INTEGRA5: 10;

      hence thesis by Lm5, Th26, Th29, Th68, INTEGRA5: 11;

    end;

    theorem :: INTEGRA8:86

    ( integral ((r (#) cos ),A)) = ((r * ( sin . ( upper_bound A))) - (r * ( sin . ( lower_bound A))))

    proof

      

       A1: ( [#] REAL ) is open Subset of REAL ;

       cos is_integrable_on A & ( cos | A) is bounded by Lm11;

      hence thesis by A1, Th27, Th68, SIN_COS: 68;

    end;

    theorem :: INTEGRA8:87

    ( integral ((r (#) sinh ),A)) = ((r * ( cosh . ( upper_bound A))) - (r * ( cosh . ( lower_bound A))))

    proof

      

       A1: ( [#] REAL ) is open Subset of REAL ;

      ( sinh | A) is continuous & ( sinh | A) is bounded by Lm9, Lm14, INTEGRA5: 10;

      hence thesis by A1, Lm9, Th31, Th68, INTEGRA5: 11, SIN_COS2: 35;

    end;

    theorem :: INTEGRA8:88

    ( integral ((r (#) cosh ),A)) = ((r * ( sinh . ( upper_bound A))) - (r * ( sinh . ( lower_bound A))))

    proof

      

       A1: ( [#] REAL ) is open Subset of REAL ;

      ( cosh | A) is continuous & ( cosh | A) is bounded by Lm10, Lm16, INTEGRA5: 10;

      hence thesis by A1, Lm10, Th30, Th68, INTEGRA5: 11, SIN_COS2: 34;

    end;

    theorem :: INTEGRA8:89

    ( integral ((r (#) exp_R ),A)) = ((r * ( exp_R . ( upper_bound A))) - (r * ( exp_R . ( lower_bound A))))

    proof

      ( exp_R | A) is bounded & ( [#] REAL ) is open Subset of REAL by Lm8, INTEGRA5: 10;

      hence thesis by Lm8, Th32, Th68, INTEGRA5: 11, SIN_COS: 66;

    end;

    theorem :: INTEGRA8:90

    

     Th90: ( integral (( sin (#) cos ),A)) = ((1 / 2) * ((( cos . ( lower_bound A)) * ( cos . ( lower_bound A))) - (( cos . ( upper_bound A)) * ( cos . ( upper_bound A)))))

    proof

      

       A1: ( [#] REAL ) is open Subset of REAL ;

      ( sin | A) is continuous;

      then

       A2: (( - cos ) `| REAL ) is_integrable_on A by Lm5, Th29, INTEGRA5: 11;

      (( - sin ) | A) is continuous;

      then

       A3: ( cos `| REAL ) is_integrable_on A by Lm7, Th28, INTEGRA5: 11;

      ((( - cos ) `| REAL ) | A) is bounded & (( cos `| REAL ) | A) is bounded by Lm5, Lm7, Th28, Th29, INTEGRA5: 10;

      

      then ( integral (( sin (#) cos ),A)) = ((((( - cos ) . ( upper_bound A)) * ( cos . ( upper_bound A))) - ((( - cos ) . ( lower_bound A)) * ( cos . ( lower_bound A)))) - ( integral ((( - cos ) (#) ( - sin )),A))) by A2, A3, A1, Th26, Th28, Th29, INTEGRA5: 21, SIN_COS: 67

      .= ((((( - cos ) . ( upper_bound A)) * ( cos . ( upper_bound A))) - ((( - cos ) . ( lower_bound A)) * ( cos . ( lower_bound A)))) - ( integral (( sin (#) cos ),A))) by Lm4

      .= (((( - ( cos . ( upper_bound A))) * ( cos . ( upper_bound A))) - ((( - cos ) . ( lower_bound A)) * ( cos . ( lower_bound A)))) - ( integral (( sin (#) cos ),A))) by VALUED_1: 8

      .= (((( - ( cos . ( upper_bound A))) * ( cos . ( upper_bound A))) - (( - ( cos . ( lower_bound A))) * ( cos . ( lower_bound A)))) - ( integral (( sin (#) cos ),A))) by VALUED_1: 8

      .= (((( cos . ( lower_bound A)) * ( cos . ( lower_bound A))) - (( cos . ( upper_bound A)) * ( cos . ( upper_bound A)))) - ( integral (( sin (#) cos ),A)));

      hence thesis;

    end;

    theorem :: INTEGRA8:91

    A = [. 0 , ( PI / 2).] implies ( integral (( sin (#) cos ),A)) = (1 / 2)

    proof

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

      then ( upper_bound A) = ( PI / 2) & ( lower_bound A) = 0 by Th37;

      

      then ( integral (( sin (#) cos ),A)) = ((1 / 2) * ((( cos . 0 ) * ( cos . 0 )) - (( cos . ( PI / 2)) * ( cos . ( PI / 2))))) by Th90

      .= ((1 / 2) * ((( cos . ( 0 + (2 * PI ))) * ( cos . 0 )) - (( cos . ( PI / 2)) * ( cos . ( PI / 2))))) by SIN_COS: 78

      .= ((1 / 2) * ((1 * 1) - ( 0 * 0 ))) by SIN_COS: 76, SIN_COS: 78;

      hence thesis;

    end;

    theorem :: INTEGRA8:92

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

    proof

      assume A = [. 0 , PI .];

      then ( upper_bound A) = PI & ( lower_bound A) = 0 by Th37;

      

      then ( integral (( sin (#) cos ),A)) = ((1 / 2) * ((( cos . 0 ) * ( cos . 0 )) - (( cos . PI ) * ( cos . PI )))) by Th90

      .= ((1 / 2) * ((( cos . ( 0 + (2 * PI ))) * ( cos . 0 )) - (( cos . PI ) * ( cos . PI )))) by SIN_COS: 78

      .= ((1 / 2) * ((1 * 1) - (( - 1) * ( - 1)))) by SIN_COS: 76, SIN_COS: 78;

      hence thesis;

    end;

    theorem :: INTEGRA8:93

    A = [. 0 , ( PI * (3 / 2)).] implies ( integral (( sin (#) cos ),A)) = (1 / 2)

    proof

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

      then ( upper_bound A) = ( PI * (3 / 2)) & ( lower_bound A) = 0 by Th37;

      

      then ( integral (( sin (#) cos ),A)) = ((1 / 2) * ((( cos . 0 ) * ( cos . 0 )) - (( cos . ( PI * (3 / 2))) * ( cos . ( PI * (3 / 2)))))) by Th90

      .= ((1 / 2) * ((( cos . ( 0 + (2 * PI ))) * ( cos . 0 )) - (( cos . ( PI * (3 / 2))) * ( cos . ( PI * (3 / 2)))))) by SIN_COS: 78

      .= ((1 / 2) * ((1 * 1) - ( 0 * 0 ))) by SIN_COS: 76, SIN_COS: 78;

      hence thesis;

    end;

    theorem :: INTEGRA8:94

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

    proof

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

      then ( upper_bound A) = ( PI * 2) & ( lower_bound A) = 0 by Th37;

      

      then ( integral (( sin (#) cos ),A)) = ((1 / 2) * ((( cos . 0 ) * ( cos . 0 )) - (( cos . ( PI * 2)) * ( cos . ( PI * 2))))) by Th90

      .= ((1 / 2) * ((( cos . ( 0 + (2 * PI ))) * ( cos . 0 )) - (( cos . ( PI * 2)) * ( cos . ( PI * 2))))) by SIN_COS: 78

      .= ((1 / 2) * ((1 * 1) - (1 * 1))) by SIN_COS: 76, SIN_COS: 78;

      hence thesis;

    end;

    theorem :: INTEGRA8:95

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

    proof

      assume A = [.((2 * n) * PI ), (((2 * n) + 1) * PI ).];

      then ( upper_bound A) = (((2 * n) + 1) * PI ) & ( lower_bound A) = ((2 * n) * PI ) by Th37;

      

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

      .= ((1 / 2) * ((( cos 0 ) * ( cos ( 0 + ((2 * n) * PI )))) - (( cos . (((2 * n) + 1) * PI )) * ( cos . (((2 * n) + 1) * PI ))))) by Th3

      .= ((1 / 2) * ((( cos 0 ) * ( cos 0 )) - (( cos . (((2 * n) + 1) * PI )) * ( cos . (((2 * n) + 1) * PI ))))) by Th3

      .= ((1 / 2) * ((( cos ( 0 + (2 * PI ))) * ( cos 0 )) - (( cos . (((2 * n) + 1) * PI )) * ( cos . (((2 * n) + 1) * PI ))))) by SIN_COS: 79

      .= ((1 / 2) * ((1 * 1) - (( cos . (((2 * n) + 1) * PI )) * ( cos . (((2 * n) + 1) * PI ))))) by SIN_COS: 77, SIN_COS: 79

      .= ((1 / 2) * ((1 * 1) - (( - ( cos 0 )) * ( cos ( 0 + (((2 * n) + 1) * PI )))))) by Th4

      .= ((1 / 2) * ((1 * 1) - (( - ( cos 0 )) * ( - ( cos 0 ))))) by Th4

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

      .= ((1 / 2) * ((1 * 1) - (( cos ( 0 + (2 * PI ))) * ( cos 0 )))) by SIN_COS: 79

      .= ((1 / 2) * ((1 * 1) - (( cos ( 0 + (2 * PI ))) * ( cos ( 0 + (2 * PI )))))) by SIN_COS: 79;

      hence thesis by SIN_COS: 77;

    end;

    theorem :: INTEGRA8:96

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

    proof

      assume A = [.(x + ((2 * n) * PI )), (x + (((2 * n) + 1) * PI )).];

      then ( upper_bound A) = (x + (((2 * n) + 1) * PI )) & ( lower_bound A) = (x + ((2 * n) * PI )) by Th37;

      

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

      .= ((1 / 2) * ((( cos x) * ( cos (x + ((2 * n) * PI )))) - (( cos (x + (((2 * n) + 1) * PI ))) * ( cos (x + (((2 * n) + 1) * PI )))))) by Th3

      .= ((1 / 2) * ((( cos x) * ( cos x)) - (( cos (x + (((2 * n) + 1) * PI ))) * ( cos (x + (((2 * n) + 1) * PI )))))) by Th3

      .= ((1 / 2) * ((( cos x) * ( cos x)) - (( - ( cos x)) * ( cos (x + (((2 * n) + 1) * PI )))))) by Th4

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

      .= 0 ;

      hence thesis;

    end;

    

     Lm20: ( cos (#) cos ) is_integrable_on A & (( cos (#) cos ) | A) is bounded

    proof

      ( dom cos ) = REAL by FUNCT_2:def 1;

      then A c= (( dom cos ) /\ ( dom cos ));

      then

       A1: A c= ( dom ( cos (#) cos )) by VALUED_1:def 4;

      (( cos (#) cos ) | A) is continuous;

      hence thesis by A1, INTEGRA5: 10, INTEGRA5: 11;

    end;

    theorem :: INTEGRA8:97

    ( integral (( sin (#) sin ),A)) = (((( cos . ( lower_bound A)) * ( sin . ( lower_bound A))) - (( cos . ( upper_bound A)) * ( sin . ( upper_bound A)))) + ( integral (( cos (#) cos ),A)))

    proof

      

       A1: ( [#] REAL ) is open Subset of REAL ;

      

       A2: ((( cos (#) cos ) || A) | A) is bounded by Lm20, INTEGRA5: 9;

      ( sin | A) is continuous;

      then

       A3: (( - cos ) `| REAL ) is_integrable_on A by Lm5, Th29, INTEGRA5: 11;

      ( dom ( cos (#) cos )) = REAL by FUNCT_2:def 1;

      then

       A4: (( cos (#) cos ) || A) is Function of A, REAL by FUNCT_2: 68, INTEGRA5: 6;

      ( cos | A) is continuous;

      then

       A5: ( sin `| REAL ) is_integrable_on A by Lm6, Th27, INTEGRA5: 11;

      ( cos (#) cos ) is_integrable_on A by Lm20;

      then

       A6: (( cos (#) cos ) || A) is integrable;

      ((( - cos ) `| REAL ) | A) is bounded & (( sin `| REAL ) | A) is bounded by Lm5, Lm6, Th27, Th29, INTEGRA5: 10;

      

      then ( integral (( sin (#) sin ),A)) = ((((( - cos ) . ( upper_bound A)) * ( sin . ( upper_bound A))) - ((( - cos ) . ( lower_bound A)) * ( sin . ( lower_bound A)))) - ( integral ((( - cos ) (#) cos ),A))) by A3, A5, A1, Th26, Th27, Th29, INTEGRA5: 21, SIN_COS: 68

      .= (((( - ( cos . ( upper_bound A))) * ( sin . ( upper_bound A))) - ((( - cos ) . ( lower_bound A)) * ( sin . ( lower_bound A)))) - ( integral ((( - cos ) (#) cos ),A))) by VALUED_1: 8

      .= (((( - ( cos . ( upper_bound A))) * ( sin . ( upper_bound A))) - (( - ( cos . ( lower_bound A))) * ( sin . ( lower_bound A)))) - ( integral ((( - cos ) (#) cos ),A))) by VALUED_1: 8

      .= (((( cos . ( lower_bound A)) * ( sin . ( lower_bound A))) - (( cos . ( upper_bound A)) * ( sin . ( upper_bound A)))) - ( integral (( - ( cos (#) cos )),A))) by RFUNCT_1: 12

      .= (((( cos . ( lower_bound A)) * ( sin . ( lower_bound A))) - (( cos . ( upper_bound A)) * ( sin . ( upper_bound A)))) - ( integral (( - 1) (#) (( cos (#) cos ) || A)))) by RFUNCT_1: 49

      .= (((( cos . ( lower_bound A)) * ( sin . ( lower_bound A))) - (( cos . ( upper_bound A)) * ( sin . ( upper_bound A)))) - (( - 1) * ( integral (( cos (#) cos ),A)))) by A6, A2, A4, INTEGRA2: 31

      .= (((( cos . ( lower_bound A)) * ( sin . ( lower_bound A))) - (( cos . ( upper_bound A)) * ( sin . ( upper_bound A)))) + ( integral (( cos (#) cos ),A)));

      hence thesis;

    end;

    theorem :: INTEGRA8:98

    ( integral (( sinh (#) sinh ),A)) = (((( cosh . ( upper_bound A)) * ( sinh . ( upper_bound A))) - (( cosh . ( lower_bound A)) * ( sinh . ( lower_bound A)))) - ( integral (( cosh (#) cosh ),A)))

    proof

      

       A1: ( [#] REAL ) is open Subset of REAL ;

      

       A2: ( sinh `| REAL ) is_integrable_on A & (( sinh `| REAL ) | A) is bounded by Lm17, Th30;

      ( cosh `| REAL ) is_integrable_on A & (( cosh `| REAL ) | A) is bounded by Lm15, Th31;

      hence thesis by A2, A1, Th30, Th31, INTEGRA5: 21, SIN_COS2: 34, SIN_COS2: 35;

    end;

    theorem :: INTEGRA8:99

    ( integral (( sinh (#) cosh ),A)) = ((1 / 2) * ((( cosh . ( upper_bound A)) * ( cosh . ( upper_bound A))) - (( cosh . ( lower_bound A)) * ( cosh . ( lower_bound A)))))

    proof

      ( sinh | A) is continuous by Lm14;

      then

       A1: ( cosh `| REAL ) is_integrable_on A by Lm9, Th31, INTEGRA5: 11;

      (( cosh `| REAL ) | A) is bounded & ( [#] REAL ) is open Subset of REAL by Lm9, Lm14, Th31, INTEGRA5: 10;

      then ( integral (( sinh (#) cosh ),A)) = (((( cosh . ( upper_bound A)) * ( cosh . ( upper_bound A))) - (( cosh . ( lower_bound A)) * ( cosh . ( lower_bound A)))) - ( integral (( sinh (#) cosh ),A))) by A1, Th31, INTEGRA5: 21, SIN_COS2: 35;

      hence thesis;

    end;

    theorem :: INTEGRA8:100

    ( integral (( exp_R (#) exp_R ),A)) = ((1 / 2) * ((( exp_R . ( upper_bound A)) ^2 ) - (( exp_R . ( lower_bound A)) ^2 )))

    proof

      ( exp_R | A) is continuous;

      then

       A1: ( exp_R `| REAL ) is_integrable_on A by Lm8, Th32, INTEGRA5: 11;

      (( exp_R `| REAL ) | A) is bounded & ( [#] REAL ) is open Subset of REAL by Lm8, Th32, INTEGRA5: 10;

      

      then ( integral (( exp_R (#) exp_R ),A)) = (((( exp_R . ( upper_bound A)) * ( exp_R . ( upper_bound A))) - (( exp_R . ( lower_bound A)) * ( exp_R . ( lower_bound A)))) - ( integral (( exp_R (#) exp_R ),A))) by A1, Th32, INTEGRA5: 21, SIN_COS: 66

      .= (((( exp_R . ( upper_bound A)) ^2 ) - (( exp_R . ( lower_bound A)) * ( exp_R . ( lower_bound A)))) - ( integral (( exp_R (#) exp_R ),A)))

      .= (((( exp_R . ( upper_bound A)) ^2 ) - (( exp_R . ( lower_bound A)) ^2 )) - ( integral (( exp_R (#) exp_R ),A)));

      hence thesis;

    end;

    

     Lm21: ( exp_R (#) ( sin + cos )) is_integrable_on A & (( exp_R (#) ( sin + cos )) | A) is bounded

    proof

      

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

      ( dom sin ) = REAL & ( dom cos ) = REAL by FUNCT_2:def 1;

      then A c= (( dom exp_R ) /\ ( dom ( sin + cos ))) by A1, SIN_COS: 47;

      then

       A2: A c= ( dom ( exp_R (#) ( sin + cos ))) by VALUED_1:def 4;

      (( exp_R (#) ( sin + cos )) | A) is continuous;

      hence thesis by A2, INTEGRA5: 10, INTEGRA5: 11;

    end;

    

     Lm22: ( exp_R (#) ( cos - sin )) is_integrable_on A & (( exp_R (#) ( cos - sin )) | A) is bounded

    proof

      ( dom exp_R ) = REAL & ( dom ( cos - sin )) = REAL by FUNCT_2:def 1;

      then A c= (( dom exp_R ) /\ ( dom ( cos - sin )));

      then

       A1: A c= ( dom ( exp_R (#) ( cos - sin ))) by VALUED_1:def 4;

      (( exp_R (#) ( cos - sin )) | A) is continuous;

      hence thesis by A1, INTEGRA5: 10, INTEGRA5: 11;

    end;

    theorem :: INTEGRA8:101

    ( integral (( exp_R (#) ( sin + cos )),A)) = ((( exp_R (#) sin ) . ( upper_bound A)) - (( exp_R (#) sin ) . ( lower_bound A)))

    proof

      

       A1: ( dom ( sin + cos )) = REAL by FUNCT_2:def 1;

      

       A2: ( dom ( exp_R (#) ( sin + cos ))) = (( dom exp_R ) /\ ( dom ( sin + cos ))) by VALUED_1:def 4

      .= ( REAL /\ ( dom ( sin + cos ))) by SIN_COS: 47

      .= REAL by A1;

      

       A3: ( exp_R (#) ( sin + cos )) is_integrable_on A & (( exp_R (#) ( sin + cos )) | A) is bounded by Lm21;

      

       A4: ( dom ( exp_R (#) sin )) = REAL & ( [#] REAL ) is open Subset of REAL by FUNCT_2:def 1;

      

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

      proof

        let x be Element of REAL ;

        reconsider xx = x as Real;

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

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

        .= (( exp_R . x) * (( sin . xx) + ( cos . xx))) by VALUED_1: 1;

        hence thesis by A4, FDIFF_7: 44;

      end;

      ( exp_R (#) sin ) is_differentiable_on REAL by A4, FDIFF_7: 44;

      then ( dom (( exp_R (#) sin ) `| REAL )) = ( dom ( exp_R (#) ( sin + cos ))) by A2, FDIFF_1:def 7;

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

      hence thesis by A3, A4, FDIFF_7: 44, INTEGRA5: 13;

    end;

    theorem :: INTEGRA8:102

    ( integral (( exp_R (#) ( cos - sin )),A)) = ((( exp_R (#) cos ) . ( upper_bound A)) - (( exp_R (#) cos ) . ( lower_bound A)))

    proof

      

       A1: ( dom ( exp_R (#) cos )) = REAL & ( [#] REAL ) is open Subset of REAL by FUNCT_2:def 1;

      

       A2: ( dom ( cos - sin )) = REAL by FUNCT_2:def 1;

      

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

      proof

        let x be Element of REAL ;

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

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

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

        hence thesis by A1, FDIFF_7: 45;

      end;

      

       A4: ( exp_R (#) ( cos - sin )) is_integrable_on A & (( exp_R (#) ( cos - sin )) | A) is bounded by Lm22;

      

       A5: ( dom ( exp_R (#) ( cos - sin ))) = (( dom exp_R ) /\ ( dom ( cos - sin ))) by VALUED_1:def 4

      .= ( REAL /\ ( dom ( cos - sin ))) by SIN_COS: 47

      .= REAL by A2;

      ( exp_R (#) cos ) is_differentiable_on REAL by A1, FDIFF_7: 45;

      then ( dom (( exp_R (#) cos ) `| REAL )) = ( dom ( exp_R (#) ( cos - sin ))) by A5, FDIFF_1:def 7;

      then (( exp_R (#) cos ) `| REAL ) = ( exp_R (#) ( cos - sin )) by A3, PARTFUN1: 5;

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

    end;