integra9.miz



    begin

    reserve r,p,x for Real;

    reserve n for Element of NAT ;

    reserve A for non empty closed_interval Subset of REAL ;

    reserve Z for open Subset of REAL ;

    

     Lm1: ( dom ( - ( exp_R * ( AffineMap (( - 1), 0 ))))) = ( [#] REAL ) by FUNCT_2:def 1;

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

    theorem :: INTEGRA9:1

    ( - ( exp_R * ( AffineMap (( - 1), 0 )))) is_differentiable_on REAL & for x holds ((( - ( exp_R * ( AffineMap (( - 1), 0 )))) `| REAL ) . x) = ( exp_R ( - x))

    proof

      

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

      

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

      

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

      then

       A4: ( AffineMap (( - jj), 0 )) is_differentiable_on REAL by A2, FDIFF_1: 23;

      for x st x in REAL holds ( exp_R * ( AffineMap (( - 1), 0 ))) qua PartFunc of REAL , REAL is_differentiable_in x

      proof

        let x;

        assume x in REAL ;

        then ( AffineMap (( - jj), 0 )) is_differentiable_in x by A2, A4, FDIFF_1: 9;

        hence thesis by TAYLOR_1: 19;

      end;

      then

       A5: ( exp_R * ( AffineMap (( - 1), 0 ))) is_differentiable_on REAL by A1, FDIFF_1: 9;

      hence ( - ( exp_R * ( AffineMap (( - 1), 0 )))) is_differentiable_on REAL by Lm1, FDIFF_1: 20;

      

       A6: for x st x in REAL holds ((( - ( exp_R * ( AffineMap (( - 1), 0 )))) `| REAL ) . x) = ( exp_R ( - x))

      proof

        let x;

        assume

         A7: x in REAL ;

        then

         A8: ( AffineMap (( - 1), 0 )) is_differentiable_in x by A2, A4, FDIFF_1: 9;

        ((( - ( exp_R * ( AffineMap (( - 1), 0 )))) `| REAL ) . x) = (( - 1) * ( diff (( exp_R * ( AffineMap (( - 1), 0 ))),x))) by A5, Lm1, FDIFF_1: 20, A7

        .= (( - 1) * (( exp_R . (( AffineMap (( - 1), 0 )) . x)) * ( diff (( AffineMap (( - 1), 0 )),x)))) by A8, TAYLOR_1: 19

        .= (( - 1) * (( exp_R . (( AffineMap (( - 1), 0 )) . x)) * ((( AffineMap (( - 1), 0 )) `| REAL ) . x))) by A4, FDIFF_1:def 7, A7

        .= (( - 1) * (( exp_R . (( AffineMap (( - 1), 0 )) . x)) * ( - 1))) by A2, A3, FDIFF_1: 23, A7

        .= (( - 1) * (( exp_R . ((( - 1) * x) + 0 )) * ( - 1))) by FCONT_1:def 4

        .= ( exp_R ( - x));

        hence thesis;

      end;

      let x;

      x in REAL by XREAL_0:def 1;

      hence ((( - ( exp_R * ( AffineMap (( - 1), 0 )))) `| REAL ) . x) = ( exp_R ( - x)) by A6;

    end;

    theorem :: INTEGRA9:2

    

     Th2: r <> 0 implies ((1 / r) (#) ( exp_R * ( AffineMap (r, 0 )))) is_differentiable_on REAL & for x holds ((((1 / r) (#) ( exp_R * ( AffineMap (r, 0 )))) `| REAL ) . x) = (( exp_R * ( AffineMap (r, 0 ))) . x)

    proof

      assume

       A1: r <> 0 ;

      

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

      

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

      

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

      then

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

      for x st x in REAL holds ( exp_R * ( AffineMap (r, 0 ))) is_differentiable_in x

      proof

        let x;

        assume x in REAL ;

        then ( AffineMap (r, 0 )) is_differentiable_in x by A3, A5, FDIFF_1: 9;

        hence thesis by TAYLOR_1: 19;

      end;

      then

       A6: ( [#] REAL ) = ( dom ((1 / r) (#) ( exp_R * ( AffineMap (r, 0 ))))) & ( exp_R * ( AffineMap (r, 0 ))) is_differentiable_on REAL by A2, FDIFF_1: 9, FUNCT_2:def 1;

      hence ((1 / r) (#) ( exp_R * ( AffineMap (r, 0 )))) is_differentiable_on REAL by FDIFF_1: 20;

      

       A7: for x st x in REAL holds ((((1 / r) (#) ( exp_R * ( AffineMap (r, 0 )))) `| REAL ) . x) = (( exp_R * ( AffineMap (r, 0 ))) . x)

      proof

        let x;

        assume

         A8: x in REAL ;

        then

         A9: ( AffineMap (r, 0 )) is_differentiable_in x by A3, A5, FDIFF_1: 9;

        ((((1 / r) (#) ( exp_R * ( AffineMap (r, 0 )))) `| REAL ) . x) = ((1 / r) * ( diff (( exp_R * ( AffineMap (r, 0 ))),x))) by A6, FDIFF_1: 20, A8

        .= ((1 / r) * (( exp_R . (( AffineMap (r, 0 )) . x)) * ( diff (( AffineMap (r, 0 )),x)))) by A9, TAYLOR_1: 19

        .= ((1 / r) * (( exp_R . (( AffineMap (r, 0 )) . x)) * ((( AffineMap (r, 0 )) `| REAL ) . x))) by A5, FDIFF_1:def 7, A8

        .= ((1 / r) * (( exp_R . (( AffineMap (r, 0 )) . x)) * r)) by A3, A4, FDIFF_1: 23, A8

        .= ((r * (1 / r)) * ( exp_R . (( AffineMap (r, 0 )) . x)))

        .= ((r / r) * ( exp_R . (( AffineMap (r, 0 )) . x))) by XCMPLX_1: 99

        .= (1 * ( exp_R . (( AffineMap (r, 0 )) . x))) by A1, XCMPLX_1: 60

        .= (( exp_R * ( AffineMap (r, 0 ))) . x) by A2, FUNCT_1: 12, A8;

        hence thesis;

      end;

      let x;

      x in REAL by XREAL_0:def 1;

      hence thesis by A7;

    end;

    theorem :: INTEGRA9:3

    r <> 0 implies ( integral (( exp_R * ( AffineMap (r, 0 ))),A)) = ((((1 / r) (#) ( exp_R * ( AffineMap (r, 0 )))) . ( upper_bound A)) - (((1 / r) (#) ( exp_R * ( AffineMap (r, 0 )))) . ( lower_bound A)))

    proof

      

       A1: ( dom ( exp_R * ( AffineMap (r, 0 )))) = REAL by FUNCT_2:def 1;

      assume

       A2: r <> 0 ;

      then ((1 / r) (#) ( exp_R * ( AffineMap (r, 0 )))) is_differentiable_on REAL by Th2;

      then

       A3: ( dom (((1 / r) (#) ( exp_R * ( AffineMap (r, 0 )))) `| REAL )) = ( dom ( exp_R * ( AffineMap (r, 0 )))) by A1, FDIFF_1:def 7;

      (( exp_R * ( AffineMap (r, 0 ))) | A) is continuous;

      then

       A4: ( exp_R * ( AffineMap (r, 0 ))) is_integrable_on A by A1, INTEGRA5: 11;

      for x be Element of REAL st x in ( dom (((1 / r) (#) ( exp_R * ( AffineMap (r, 0 )))) `| REAL )) holds ((((1 / r) (#) ( exp_R * ( AffineMap (r, 0 )))) `| REAL ) . x) = (( exp_R * ( AffineMap (r, 0 ))) . x) by A2, Th2;

      then

       A5: (((1 / r) (#) ( exp_R * ( AffineMap (r, 0 )))) `| REAL ) = ( exp_R * ( AffineMap (r, 0 ))) by A3, PARTFUN1: 5;

      (( exp_R * ( AffineMap (r, 0 ))) | A) is bounded by A1, INTEGRA5: 10;

      hence thesis by A2, A4, A5, Th2, INTEGRA5: 13;

    end;

    theorem :: INTEGRA9:4

    

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

    proof

      assume

       A1: n <> 0 ;

      

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

      

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

      then

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

      hence (( - (1 / n)) (#) ( cos * ( AffineMap (n, 0 )))) is_differentiable_on REAL by A2, FDIFF_1: 20;

      

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

      proof

        let x;

        assume

         A6: x in REAL ;

        

        then (((( - (1 / n)) (#) ( cos * ( AffineMap (n, 0 )))) `| REAL ) . x) = (( - (1 / n)) * ( diff (( cos * ( AffineMap (n, 0 ))),x))) by A2, A4, FDIFF_1: 20

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

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

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

        .= ((n / n) * ( sin . ((n * x) + 0 ))) by XCMPLX_1: 99

        .= (1 * ( sin . ((n * x) + 0 ))) by A1, XCMPLX_1: 60

        .= ( sin (n * x));

        hence thesis;

      end;

      let x;

      x in REAL by XREAL_0:def 1;

      hence thesis by A5;

    end;

    theorem :: INTEGRA9:5

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

    proof

      assume

       A1: n <> 0 ;

      

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

      

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

      

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

      proof

        let x be Element of REAL ;

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

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

        .= ( sin . (( AffineMap (n, 0 )) . x)) by A3

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

        hence thesis;

      end;

      (( - (1 / n)) (#) ( cos * ( AffineMap (n, 0 )))) is_differentiable_on REAL by A1, Th4;

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

      then

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

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

      then

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

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

      hence thesis by A1, A6, A5, Th4, INTEGRA5: 13;

    end;

    theorem :: INTEGRA9:6

    

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

    proof

      assume

       A1: n <> 0 ;

      

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

      

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

      then

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

      hence ((1 / n) (#) ( sin * ( AffineMap (n, 0 )))) is_differentiable_on REAL by A2, FDIFF_1: 20;

      

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

      proof

        let x;

        assume

         A6: x in REAL ;

        ((((1 / n) (#) ( sin * ( AffineMap (n, 0 )))) `| REAL ) . x) = ((1 / n) * ( diff (( sin * ( AffineMap (n, 0 ))),x))) by A2, A4, FDIFF_1: 20, A6

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

        .= ((1 / n) * (n * ( cos . ((n * x) + 0 )))) by A3, FDIFF_4: 37, A6

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

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

        .= (1 * ( cos . ((n * x) + 0 ))) by A1, XCMPLX_1: 60

        .= ( cos (n * x));

        hence thesis;

      end;

      let x;

      x in REAL by XREAL_0:def 1;

      hence thesis by A5;

    end;

    theorem :: INTEGRA9:7

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

    proof

      assume

       A1: n <> 0 ;

      

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

      

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

      

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

      proof

        let x be Element of REAL ;

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

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

        .= ( cos . (( AffineMap (n, 0 )) . x)) by A3

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

        hence thesis;

      end;

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

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

      then

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

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

      then

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

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

      hence thesis by A1, A6, A5, Th6, INTEGRA5: 13;

    end;

    theorem :: INTEGRA9:8

    A c= Z implies ( integral ((( id Z) (#) sin ),A)) = ((((( - ( id Z)) (#) cos ) + sin ) . ( upper_bound A)) - (((( - ( id Z)) (#) cos ) + sin ) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z;

      

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

      

       A3: ( dom ((( - ( id Z)) (#) cos ) + sin )) = (( dom (( - ( id Z)) (#) cos )) /\ REAL ) by SIN_COS: 24, VALUED_1:def 1

      .= ( dom (( - ( id Z)) (#) cos )) by XBOOLE_1: 28

      .= (( dom ( - ( id Z))) /\ REAL ) by SIN_COS: 24, VALUED_1:def 4

      .= ( dom ( - ( id Z))) by XBOOLE_1: 28

      .= Z by A2, RELAT_1: 45;

      then

       A4: ((( - ( id Z)) (#) cos ) + sin ) is_differentiable_on Z by FDIFF_4: 46;

      

       A5: for x st x in Z holds ((( id Z) (#) sin ) . x) = (x * ( sin . x))

      proof

        let x;

        assume

         A6: x in Z;

        ((( id Z) (#) sin ) . x) = ((( id Z) . x) * ( sin . x)) by VALUED_1: 5

        .= (x * ( sin . x)) by A6, FUNCT_1: 18;

        hence thesis;

      end;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

        then ((((( - ( id Z)) (#) cos ) + sin ) `| Z) . x) = (x * ( sin . x)) by A3, FDIFF_4: 46

        .= ((( id Z) (#) sin ) . x) by A5, A8;

        hence thesis;

      end;

      

       A9: ( dom (( id Z) (#) sin )) = (( dom ( id Z)) /\ REAL ) by SIN_COS: 24, VALUED_1:def 4

      .= ( dom ( id Z)) by XBOOLE_1: 28

      .= Z by RELAT_1: 45;

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

      then

       A10: (((( - ( id Z)) (#) cos ) + sin ) `| Z) = (( id Z) (#) sin ) by A7, PARTFUN1: 5;

      ((( id Z) (#) sin ) | A) is continuous;

      then

       A11: (( id Z) (#) sin ) is_integrable_on A by A1, A9, INTEGRA5: 11;

      ((( id Z) (#) sin ) | A) is bounded by A1, A9, INTEGRA5: 10;

      hence thesis by A1, A3, A11, A10, FDIFF_4: 46, INTEGRA5: 13;

    end;

    theorem :: INTEGRA9:9

    A c= Z implies ( integral ((( id Z) (#) cos ),A)) = ((((( id Z) (#) sin ) + cos ) . ( upper_bound A)) - (((( id Z) (#) sin ) + cos ) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z;

      ( dom ((( id Z) (#) sin ) + cos )) = (( dom (( id Z) (#) sin )) /\ REAL ) by SIN_COS: 24, VALUED_1:def 1

      .= ( dom (( id Z) (#) sin )) by XBOOLE_1: 28

      .= (( dom ( id Z)) /\ REAL ) by SIN_COS: 24, VALUED_1:def 4

      .= ( dom ( id Z)) by XBOOLE_1: 28;

      then

       A2: ( dom ((( id Z) (#) sin ) + cos )) = Z by RELAT_1: 45;

      then

       A3: ((( id Z) (#) sin ) + cos ) is_differentiable_on Z by FDIFF_4: 47;

      

       A4: for x st x in Z holds ((( id Z) (#) cos ) . x) = (x * ( cos . x))

      proof

        let x;

        assume

         A5: x in Z;

        ((( id Z) (#) cos ) . x) = ((( id Z) . x) * ( cos . x)) by VALUED_1: 5

        .= (x * ( cos . x)) by A5, FUNCT_1: 18;

        hence thesis;

      end;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

        then ((((( id Z) (#) sin ) + cos ) `| Z) . x) = (x * ( cos . x)) by A2, FDIFF_4: 47

        .= ((( id Z) (#) cos ) . x) by A4, A7;

        hence thesis;

      end;

      

       A8: ( dom (( id Z) (#) cos )) = (( dom ( id Z)) /\ REAL ) by SIN_COS: 24, VALUED_1:def 4

      .= ( dom ( id Z)) by XBOOLE_1: 28

      .= Z by RELAT_1: 45;

      then ( dom (((( id Z) (#) sin ) + cos ) `| Z)) = ( dom (( id Z) (#) cos )) by A3, FDIFF_1:def 7;

      then

       A9: (((( id Z) (#) sin ) + cos ) `| Z) = (( id Z) (#) cos ) by A6, PARTFUN1: 5;

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

      then

       A10: (( id Z) (#) cos ) is_integrable_on A by A1, A8, INTEGRA5: 11;

      ((( id Z) (#) cos ) | A) is bounded by A1, A8, INTEGRA5: 10;

      hence thesis by A1, A2, A10, A9, FDIFF_4: 47, INTEGRA5: 13;

    end;

    theorem :: INTEGRA9:10

    

     Th10: (( id Z) (#) cos ) is_differentiable_on Z & for x st x in Z holds (((( id Z) (#) cos ) `| Z) . x) = (( cos . x) - (x * ( sin . x)))

    proof

      

       A1: cos is_differentiable_on Z by FDIFF_1: 26, SIN_COS: 67;

      

       A2: ( dom (( id Z) (#) cos )) = (( dom ( id Z)) /\ REAL ) by SIN_COS: 24, VALUED_1:def 4

      .= ( dom ( id Z)) by XBOOLE_1: 28

      .= Z by RELAT_1: 45;

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

      then

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

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

      then

       A4: ( id Z) is_differentiable_on Z by A3, FDIFF_1: 23;

      

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

      now

        let x;

        assume

         A6: x in Z;

        

        hence (((( id Z) (#) cos ) `| Z) . x) = ((( cos . x) * ( diff (( id Z),x))) + ((( id Z) . x) * ( diff ( cos ,x)))) by A2, A4, A1, FDIFF_1: 21

        .= ((( cos . x) * ((( id Z) `| Z) . x)) + ((( id Z) . x) * ( diff ( cos ,x)))) by A4, A6, FDIFF_1:def 7

        .= ((( cos . x) * 1) + ((( id Z) . x) * ( diff ( cos ,x)))) by A3, A5, A6, FDIFF_1: 23

        .= ((( cos . x) * 1) + ((( id Z) . x) * ( - ( sin . x)))) by SIN_COS: 63

        .= (( cos . x) + (x * ( - ( sin . x)))) by A6, FUNCT_1: 18

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

      end;

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

    end;

    

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

    proof

      

       A1: sin is_differentiable_in x by SIN_COS: 64;

      

      then ( diff (( - sin ),x)) = ( - ( diff ( sin ,x))) by INTEGRA8: 22

      .= ( - ( cos . x)) by SIN_COS: 64;

      hence thesis by A1, INTEGRA8: 22;

    end;

    theorem :: INTEGRA9:11

    

     Th11: (( - sin ) + (( id Z) (#) cos )) is_differentiable_on Z & for x st x in Z holds (((( - sin ) + (( id Z) (#) cos )) `| Z) . x) = ( - (x * ( sin . x)))

    proof

      ( dom (( - sin ) + (( id Z) (#) cos ))) = (( dom ( - sin )) /\ ( dom (( id Z) (#) cos ))) by VALUED_1:def 1

      .= ( REAL /\ ( dom (( id Z) (#) cos ))) by SIN_COS: 24, VALUED_1: 8

      .= ( dom (( id Z) (#) cos )) by XBOOLE_1: 28

      .= (( dom ( id Z)) /\ REAL ) by SIN_COS: 24, VALUED_1:def 4

      .= ( dom ( id Z)) by XBOOLE_1: 28;

      then

       A1: Z = ( dom (( - sin ) + (( id Z) (#) cos ))) by RELAT_1: 45;

      

       A2: (( id Z) (#) cos ) is_differentiable_on Z by Th10;

      

       A3: ( - sin ) is_differentiable_on Z by FDIFF_1: 26, INTEGRA8: 24;

      now

        let x;

        assume

         A4: x in Z;

        

        hence (((( - sin ) + (( id Z) (#) cos )) `| Z) . x) = (( diff (( - sin ),x)) + ( diff ((( id Z) (#) cos ),x))) by A1, A2, A3, FDIFF_1: 18

        .= ((((( id Z) (#) cos ) `| Z) . x) + ( diff (( - sin ),x))) by A2, A4, FDIFF_1:def 7

        .= ((( cos . x) - (x * ( sin . x))) + ( diff (( - sin ),x))) by A4, Th10

        .= ((( cos . x) - (x * ( sin . x))) + ( - ( cos . x))) by Lm2

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

      end;

      hence thesis by A1, A2, A3, FDIFF_1: 18;

    end;

    theorem :: INTEGRA9:12

    A c= Z implies ( integral ((( - ( id Z)) (#) sin ),A)) = (((( - sin ) + (( id Z) (#) cos )) . ( upper_bound A)) - ((( - sin ) + (( id Z) (#) cos )) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z;

      

       A2: (( - sin ) + (( id Z) (#) cos )) is_differentiable_on Z by Th11;

      

       A3: for x st x in Z holds (( - ( id Z)) . x) = ((( - 1) * x) + 0 )

      proof

        let x;

        assume

         A4: x in Z;

        (( - ( id Z)) . x) = ( - (( id Z) . x)) by VALUED_1: 8

        .= ( - x) by A4, FUNCT_1: 18

        .= ((( - 1) * x) + 0 );

        hence thesis;

      end;

      

       A5: for x st x in Z holds ((( - ( id Z)) (#) sin ) . x) = ( - (x * ( sin . x)))

      proof

        let x;

        assume

         A6: x in Z;

        ((( - ( id Z)) (#) sin ) . x) = ((( - ( id Z)) . x) * ( sin . x)) by VALUED_1: 5

        .= (((( - 1) * x) + 0 ) * ( sin . x)) by A3, A6

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

        hence thesis;

      end;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

        then (((( - sin ) + (( id Z) (#) cos )) `| Z) . x) = ( - (x * ( sin . x))) by Th11

        .= ((( - ( id Z)) (#) sin ) . x) by A5, A8;

        hence thesis;

      end;

      ( dom (( - ( id Z)) (#) sin )) = (( dom ( - ( id Z))) /\ REAL ) by SIN_COS: 24, VALUED_1:def 4

      .= ( dom ( - ( id Z))) by XBOOLE_1: 28

      .= ( dom ( id Z)) by VALUED_1: 8;

      then

       A9: Z = ( dom (( - ( id Z)) (#) sin )) by RELAT_1: 45;

      then ( dom ((( - sin ) + (( id Z) (#) cos )) `| Z)) = ( dom (( - ( id Z)) (#) sin )) by A2, FDIFF_1:def 7;

      then

       A10: ((( - sin ) + (( id Z) (#) cos )) `| Z) = (( - ( id Z)) (#) sin ) by A7, PARTFUN1: 5;

      ((( - ( id Z)) (#) sin ) | A) is continuous;

      then

       A11: (( - ( id Z)) (#) sin ) is_integrable_on A by A1, A9, INTEGRA5: 11;

      ((( - ( id Z)) (#) sin ) | A) is bounded by A1, A9, INTEGRA5: 10;

      hence thesis by A1, A11, A10, Th11, INTEGRA5: 13;

    end;

    theorem :: INTEGRA9:13

    

     Th13: (( - cos ) - (( id Z) (#) sin )) is_differentiable_on Z & for x st x in Z holds (((( - cos ) - (( id Z) (#) sin )) `| Z) . x) = ( - (x * ( cos . x)))

    proof

      ( dom (( - cos ) - (( id Z) (#) sin ))) = (( dom ( - cos )) /\ ( dom (( id Z) (#) sin ))) by VALUED_1: 12

      .= ( REAL /\ ( dom (( id Z) (#) sin ))) by SIN_COS: 24, VALUED_1: 8

      .= ( dom (( id Z) (#) sin )) by XBOOLE_1: 28

      .= (( dom ( id Z)) /\ REAL ) by SIN_COS: 24, VALUED_1:def 4

      .= ( dom ( id Z)) by XBOOLE_1: 28;

      then

       A1: Z = ( dom (( - cos ) - (( id Z) (#) sin ))) by RELAT_1: 45;

      then Z c= (( dom ( - cos )) /\ ( dom (( id Z) (#) sin ))) by VALUED_1: 12;

      then

       A2: Z c= ( dom (( id Z) (#) sin )) by XBOOLE_1: 18;

      then

       A3: (( id Z) (#) sin ) is_differentiable_on Z by FDIFF_4: 45;

      

       A4: ( - cos ) is_differentiable_on Z by FDIFF_1: 26, INTEGRA8: 26;

      now

        let x;

        assume

         A5: x in Z;

        

        hence (((( - cos ) - (( id Z) (#) sin )) `| Z) . x) = (( diff (( - cos ),x)) - ( diff ((( id Z) (#) sin ),x))) by A1, A3, A4, FDIFF_1: 19

        .= (( sin . x) - ( diff ((( id Z) (#) sin ),x))) by INTEGRA8: 26, A5

        .= (( sin . x) - (((( id Z) (#) sin ) `| Z) . x)) by A3, A5, FDIFF_1:def 7

        .= (( sin . x) - (( sin . x) + (x * ( cos . x)))) by A2, A5, FDIFF_4: 45

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

      end;

      hence thesis by A1, A3, A4, FDIFF_1: 19;

    end;

    theorem :: INTEGRA9:14

    A c= Z implies ( integral ((( - ( id Z)) (#) cos ),A)) = (((( - cos ) - (( id Z) (#) sin )) . ( upper_bound A)) - ((( - cos ) - (( id Z) (#) sin )) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z;

      

       A2: (( - cos ) - (( id Z) (#) sin )) is_differentiable_on Z by Th13;

      

       A3: for x st x in Z holds (( - ( id Z)) . x) = ((( - 1) * x) + 0 )

      proof

        let x;

        assume

         A4: x in Z;

        (( - ( id Z)) . x) = ( - (( id Z) . x)) by VALUED_1: 8

        .= ( - x) by A4, FUNCT_1: 18

        .= ((( - 1) * x) + 0 );

        hence thesis;

      end;

      

       A5: for x st x in Z holds ((( - ( id Z)) (#) cos ) . x) = ( - (x * ( cos . x)))

      proof

        let x;

        assume

         A6: x in Z;

        ((( - ( id Z)) (#) cos ) . x) = ((( - ( id Z)) . x) * ( cos . x)) by VALUED_1: 5

        .= (((( - 1) * x) + 0 ) * ( cos . x)) by A3, A6

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

        hence thesis;

      end;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

        then (((( - cos ) - (( id Z) (#) sin )) `| Z) . x) = ( - (x * ( cos . x))) by Th13

        .= ((( - ( id Z)) (#) cos ) . x) by A5, A8;

        hence thesis;

      end;

      ( dom (( - ( id Z)) (#) cos )) = (( dom ( - ( id Z))) /\ REAL ) by SIN_COS: 24, VALUED_1:def 4

      .= ( dom ( - ( id Z))) by XBOOLE_1: 28

      .= ( dom ( id Z)) by VALUED_1: 8;

      then

       A9: Z = ( dom (( - ( id Z)) (#) cos )) by RELAT_1: 45;

      then ( dom ((( - cos ) - (( id Z) (#) sin )) `| Z)) = ( dom (( - ( id Z)) (#) cos )) by A2, FDIFF_1:def 7;

      then

       A10: ((( - cos ) - (( id Z) (#) sin )) `| Z) = (( - ( id Z)) (#) cos ) by A7, PARTFUN1: 5;

      ((( - ( id Z)) (#) cos ) | A) is continuous;

      then

       A11: (( - ( id Z)) (#) cos ) is_integrable_on A by A1, A9, INTEGRA5: 11;

      ((( - ( id Z)) (#) cos ) | A) is bounded by A1, A9, INTEGRA5: 10;

      hence thesis by A1, A11, A10, Th13, INTEGRA5: 13;

    end;

    theorem :: INTEGRA9:15

    A c= Z implies ( integral (( sin + (( id Z) (#) cos )),A)) = (((( id Z) (#) sin ) . ( upper_bound A)) - ((( id Z) (#) sin ) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z;

      ( dom ( sin + (( id Z) (#) cos ))) = ( REAL /\ ( dom (( id Z) (#) cos ))) by SIN_COS: 24, VALUED_1:def 1

      .= ( dom (( id Z) (#) cos )) by XBOOLE_1: 28

      .= (( dom ( id Z)) /\ REAL ) by SIN_COS: 24, VALUED_1:def 4

      .= ( dom ( id Z)) by XBOOLE_1: 28;

      then

       A2: Z = ( dom ( sin + (( id Z) (#) cos ))) by RELAT_1: 45;

      (( sin + (( id Z) (#) cos )) | A) is continuous;

      then

       A3: ( sin + (( id Z) (#) cos )) is_integrable_on A by A1, A2, INTEGRA5: 11;

      

       A4: ( dom (( id Z) (#) sin )) = (( dom ( id Z)) /\ REAL ) by SIN_COS: 24, VALUED_1:def 4

      .= ( dom ( id Z)) by XBOOLE_1: 28

      .= Z by RELAT_1: 45;

      then

       A5: (( id Z) (#) sin ) is_differentiable_on Z by FDIFF_4: 45;

      

       A6: for x st x in Z holds (( sin + (( id Z) (#) cos )) . x) = (( sin . x) + (x * ( cos . x)))

      proof

        let x;

        assume

         A7: x in Z;

        

        then (( sin + (( id Z) (#) cos )) . x) = (( sin . x) + ((( id Z) (#) cos ) . x)) by A2, VALUED_1:def 1

        .= (( sin . x) + ((( id Z) . x) * ( cos . x))) by VALUED_1: 5

        .= (( sin . x) + (x * ( cos . x))) by A7, FUNCT_1: 18;

        hence thesis;

      end;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

        then (((( id Z) (#) sin ) `| Z) . x) = (( sin . x) + (x * ( cos . x))) by A4, FDIFF_4: 45

        .= (( sin + (( id Z) (#) cos )) . x) by A6, A9;

        hence thesis;

      end;

      ( dom ((( id Z) (#) sin ) `| Z)) = ( dom ( sin + (( id Z) (#) cos ))) by A2, A5, FDIFF_1:def 7;

      then

       A10: ((( id Z) (#) sin ) `| Z) = ( sin + (( id Z) (#) cos )) by A8, PARTFUN1: 5;

      (( sin + (( id Z) (#) cos )) | A) is bounded by A1, A2, INTEGRA5: 10;

      hence thesis by A1, A4, A3, A10, FDIFF_4: 45, INTEGRA5: 13;

    end;

    theorem :: INTEGRA9:16

    A c= Z implies ( integral ((( - cos ) + (( id Z) (#) sin )),A)) = (((( - ( id Z)) (#) cos ) . ( upper_bound A)) - ((( - ( id Z)) (#) cos ) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z;

      ( dom (( - cos ) + (( id Z) (#) sin ))) = (( dom ( - cos )) /\ ( dom (( id Z) (#) sin ))) by VALUED_1:def 1

      .= ( REAL /\ ( dom (( id Z) (#) sin ))) by SIN_COS: 24, VALUED_1: 8

      .= ( dom (( id Z) (#) sin )) by XBOOLE_1: 28

      .= (( dom ( id Z)) /\ REAL ) by SIN_COS: 24, VALUED_1:def 4

      .= ( dom ( id Z)) by XBOOLE_1: 28;

      then

       A2: Z = ( dom (( - cos ) + (( id Z) (#) sin ))) by RELAT_1: 45;

      ((( - cos ) + (( id Z) (#) sin )) | A) is continuous;

      then

       A3: (( - cos ) + (( id Z) (#) sin )) is_integrable_on A by A1, A2, INTEGRA5: 11;

      ( dom (( - ( id Z)) (#) cos )) = (( dom ( - ( id Z))) /\ REAL ) by SIN_COS: 24, VALUED_1:def 4

      .= ( dom ( - ( id Z))) by XBOOLE_1: 28

      .= ( dom ( id Z)) by VALUED_1: 8;

      then

       A4: ( dom (( - ( id Z)) (#) cos )) = Z by RELAT_1: 45;

      then

       A5: (( - ( id Z)) (#) cos ) is_differentiable_on Z by FDIFF_4: 44;

      

       A6: for x st x in Z holds ((( - cos ) + (( id Z) (#) sin )) . x) = (( - ( cos . x)) + (x * ( sin . x)))

      proof

        let x;

        assume

         A7: x in Z;

        

        then ((( - cos ) + (( id Z) (#) sin )) . x) = ((( - cos ) . x) + ((( id Z) (#) sin ) . x)) by A2, VALUED_1:def 1

        .= ((( - cos ) . x) + ((( id Z) . x) * ( sin . x))) by VALUED_1: 5

        .= ((( - cos ) . x) + (x * ( sin . x))) by A7, FUNCT_1: 18

        .= (( - ( cos . x)) + (x * ( sin . x))) by VALUED_1: 8;

        hence thesis;

      end;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

        then (((( - ( id Z)) (#) cos ) `| Z) . x) = (( - ( cos . x)) + (x * ( sin . x))) by A4, FDIFF_4: 44

        .= ((( - cos ) + (( id Z) (#) sin )) . x) by A6, A9;

        hence thesis;

      end;

      ( dom ((( - ( id Z)) (#) cos ) `| Z)) = ( dom (( - cos ) + (( id Z) (#) sin ))) by A2, A5, FDIFF_1:def 7;

      then

       A10: ((( - ( id Z)) (#) cos ) `| Z) = (( - cos ) + (( id Z) (#) sin )) by A8, PARTFUN1: 5;

      ((( - cos ) + (( id Z) (#) sin )) | A) is bounded by A1, A2, INTEGRA5: 10;

      hence thesis by A1, A4, A3, A10, FDIFF_4: 44, INTEGRA5: 13;

    end;

    theorem :: INTEGRA9:17

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

    proof

      

       A1: for x st x in REAL holds (( AffineMap (1,( - 1))) . x) = (x - 1)

      proof

        let x;

        assume x in REAL ;

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

        .= (x - 1);

        hence thesis;

      end;

      

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

      

       A3: for x st x in REAL holds ((( AffineMap (1, 0 )) (#) exp_R ) . x) = (x * ( exp_R . x))

      proof

        let x;

        assume x in REAL ;

        ((( AffineMap (1, 0 )) (#) exp_R ) . x) = ((( AffineMap (1, 0 )) . x) * ( exp_R . x)) by VALUED_1: 5

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

        .= (x * ( exp_R . x));

        hence thesis;

      end;

      

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

      proof

        let x be Element of REAL ;

        assume x in ( dom (( exp_R (#) ( AffineMap (1,( - 1)))) `| REAL ));

        ((( exp_R (#) ( AffineMap (1,( - 1)))) `| REAL ) . x) = (x * ( exp_R . x)) by A2, A1, FDIFF_4: 55

        .= ((( AffineMap (1, 0 )) (#) exp_R ) . x) by A3;

        hence thesis;

      end;

      

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

      ((( AffineMap (1, 0 )) (#) exp_R ) | A) is continuous;

      then

       A6: (( AffineMap (1, 0 )) (#) exp_R ) is_integrable_on A by A5, INTEGRA5: 11;

      ( exp_R (#) ( AffineMap (1,( - 1)))) is_differentiable_on REAL by A2, A1, FDIFF_4: 55;

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

      then

       A7: (( exp_R (#) ( AffineMap (1,( - 1)))) `| REAL ) = (( AffineMap (1, 0 )) (#) exp_R ) by A4, PARTFUN1: 5;

      ((( AffineMap (1, 0 )) (#) exp_R ) | A) is bounded by A5, INTEGRA5: 10;

      hence thesis by A2, A1, A6, A7, FDIFF_4: 55, INTEGRA5: 13;

    end;

    theorem :: INTEGRA9:18

    

     Th18: ((1 / (n + 1)) (#) ( #Z (n + 1))) is_differentiable_on REAL & for x holds ((((1 / (n + 1)) (#) ( #Z (n + 1))) `| REAL ) . x) = (x #Z n)

    proof

      

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

      ( [#] REAL ) = ( dom ( #Z (n + 1))) & for x st x in REAL holds ( #Z (n + 1)) is_differentiable_in x by FUNCT_2:def 1, TAYLOR_1: 2;

      then

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

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

      

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

      proof

        set m = (n + 1);

        let x;

        assume

         A4: x in REAL ;

        ( diff (( #Z m),x)) = (m * (x #Z (m - 1))) by TAYLOR_1: 2;

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

      end;

      

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

      proof

        let x;

        assume

         A6: x in REAL ;

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

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

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

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

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

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

        hence thesis;

      end;

      let x;

      x in REAL by XREAL_0:def 1;

      hence thesis by A5;

    end;

    theorem :: INTEGRA9:19

    ( integral (( #Z n),A)) = (((1 / (n + 1)) * (( upper_bound A) |^ (n + 1))) - ((1 / (n + 1)) * (( lower_bound A) |^ (n + 1))))

    proof

      

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

      

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

      proof

        let x be Element of REAL ;

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

        ((((1 / (n + 1)) (#) ( #Z (n + 1))) `| REAL ) . x) = (x #Z n) by Th18

        .= (( #Z n) . x) by TAYLOR_1:def 1;

        hence thesis;

      end;

      ( dom ( #Z (n + 1))) = ( [#] REAL ) & for x st x in REAL holds ( #Z (n + 1)) is_differentiable_in x by FUNCT_2:def 1, TAYLOR_1: 2;

      then ( [#] REAL ) = ( dom ((1 / (n + 1)) (#) ( #Z (n + 1)))) & ( #Z (n + 1)) is_differentiable_on REAL by FDIFF_1: 9, FUNCT_2:def 1;

      then ((1 / (n + 1)) (#) ( #Z (n + 1))) is_differentiable_on REAL by FDIFF_1: 20;

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

      then

       A3: (((1 / (n + 1)) (#) ( #Z (n + 1))) `| REAL ) = ( #Z n) by A2, PARTFUN1: 5;

      

       A4: (( #Z (n + 1)) . ( upper_bound A)) = (( upper_bound A) #Z (n + 1)) by TAYLOR_1:def 1

      .= (( upper_bound A) |^ (n + 1)) by PREPOWER: 36;

      for x st x in REAL holds ( #Z n) is_differentiable_in x by TAYLOR_1: 2;

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

      then

       A5: (( #Z n) | REAL ) is continuous by FDIFF_1: 25;

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

      then

       A6: ( #Z n) is_integrable_on A by A1, INTEGRA5: 11;

      

       A7: (( #Z (n + 1)) . ( lower_bound A)) = (( lower_bound A) #Z (n + 1)) by TAYLOR_1:def 1

      .= (( lower_bound A) |^ (n + 1)) by PREPOWER: 36;

      (( #Z n) | A) is bounded by A1, A5, FCONT_1: 16, INTEGRA5: 10;

      

      then ( integral (( #Z n),A)) = ((((1 / (n + 1)) (#) ( #Z (n + 1))) . ( upper_bound A)) - (((1 / (n + 1)) (#) ( #Z (n + 1))) . ( lower_bound A))) by A6, A3, Th18, INTEGRA5: 13

      .= (((1 / (n + 1)) * (( #Z (n + 1)) . ( upper_bound A))) - (((1 / (n + 1)) (#) ( #Z (n + 1))) . ( lower_bound A))) by VALUED_1: 6

      .= (((1 / (n + 1)) * (( #Z (n + 1)) . ( upper_bound A))) - ((1 / (n + 1)) * (( #Z (n + 1)) . ( lower_bound A)))) by VALUED_1: 6

      .= (((1 / (n + 1)) * (( upper_bound A) |^ (n + 1))) - ((1 / (n + 1)) * (( lower_bound A) |^ (n + 1)))) by A4, A7;

      hence thesis;

    end;

    begin

    theorem :: INTEGRA9:20

    

     Th20: for f,g be PartFunc of REAL , REAL , C be non empty Subset of REAL holds ((f - g) || C) = ((f || C) - (g || C))

    proof

      let f,g be PartFunc of REAL , REAL ;

      let C be non empty Subset of REAL ;

      

       A1: ( dom ((f || C) - (g || C))) = (( dom (f | C)) /\ ( dom (g | C))) by VALUED_1: 12

      .= ((( dom f) /\ C) /\ ( dom (g | C))) by RELAT_1: 61

      .= ((( dom f) /\ C) /\ (( dom g) /\ C)) by RELAT_1: 61

      .= (( dom f) /\ (C /\ (( dom g) /\ C))) by XBOOLE_1: 16

      .= (( dom f) /\ (( dom g) /\ (C /\ C))) by XBOOLE_1: 16

      .= (( dom f) /\ (( dom g) /\ C));

      

       A2: ( dom ((f - g) || C)) = (( dom (f - g)) /\ C) by RELAT_1: 61

      .= ((( dom f) /\ ( dom g)) /\ C) by VALUED_1: 12;

      then

       A3: ( dom ((f - g) || C)) = ( dom ((f || C) - (g || C))) by A1, XBOOLE_1: 16;

      for c be Element of C st c in ( dom ((f - g) || C)) holds (((f - g) || C) . c) = (((f || C) - (g || C)) . c)

      proof

        let c be Element of C;

        assume

         A4: c in ( dom ((f - g) || C));

        then c in (( dom (f - g)) /\ C) by RELAT_1: 61;

        then

         A5: c in ( dom (f - g)) by XBOOLE_0:def 4;

        

         A6: c in (( dom (f || C)) /\ ( dom (g || C))) by A3, A4, VALUED_1: 12;

        then

         A7: c in ( dom (f | C)) by XBOOLE_0:def 4;

        

         A8: (((f - g) || C) . c) = ((f - g) . c) by A4, FUNCT_1: 47

        .= ((f . c) - (g . c)) by A5, VALUED_1: 13;

        

         A9: c in ( dom (g | C)) by A6, XBOOLE_0:def 4;

        (((f || C) - (g || C)) . c) = (((f || C) . c) - ((g || C) . c)) by A3, A4, VALUED_1: 13

        .= ((f . c) - ((g | C) . c)) by A7, FUNCT_1: 47;

        hence thesis by A8, A9, FUNCT_1: 47;

      end;

      hence thesis by A2, A1, PARTFUN1: 5, XBOOLE_1: 16;

    end;

    theorem :: INTEGRA9:21

    

     Th21: for f1,f2,g be PartFunc of REAL , REAL , C be non empty Subset of REAL holds (((f1 + f2) || C) (#) (g || C)) = (((f1 (#) g) + (f2 (#) g)) || C)

    proof

      let f1,f2,g be PartFunc of REAL , REAL ;

      let C be non empty Subset of REAL ;

      

       A1: ( dom (((f1 (#) g) + (f2 (#) g)) || C)) = (( dom ((f1 (#) g) + (f2 (#) g))) /\ C) by RELAT_1: 61

      .= ((( dom (f1 (#) g)) /\ ( dom (f2 (#) g))) /\ C) by VALUED_1:def 1

      .= (((( dom f1) /\ ( dom g)) /\ ( dom (f2 (#) g))) /\ C) by VALUED_1:def 4

      .= (((( dom f1) /\ ( dom g)) /\ (( dom f2) /\ ( dom g))) /\ C) by VALUED_1:def 4

      .= ((( dom f1) /\ ((( dom g) /\ ( dom f2)) /\ ( dom g))) /\ C) by XBOOLE_1: 16

      .= ((( dom f1) /\ (( dom f2) /\ (( dom g) /\ ( dom g)))) /\ C) by XBOOLE_1: 16

      .= (((( dom f1) /\ ( dom f2)) /\ ( dom g)) /\ C) by XBOOLE_1: 16;

      

       A2: ( dom (((f1 + f2) || C) (#) (g || C))) = (( dom ((f1 + f2) || C)) /\ ( dom (g || C))) by VALUED_1:def 4

      .= ((( dom (f1 + f2)) /\ C) /\ ( dom (g | C))) by RELAT_1: 61

      .= ((( dom (f1 + f2)) /\ C) /\ (( dom g) /\ C)) by RELAT_1: 61

      .= (((( dom f1) /\ ( dom f2)) /\ C) /\ (( dom g) /\ C)) by VALUED_1:def 1

      .= ((( dom f1) /\ ( dom f2)) /\ ((C /\ ( dom g)) /\ C)) by XBOOLE_1: 16

      .= ((( dom f1) /\ ( dom f2)) /\ (( dom g) /\ (C /\ C))) by XBOOLE_1: 16

      .= (((( dom f1) /\ ( dom f2)) /\ ( dom g)) /\ C) by XBOOLE_1: 16;

      for c be Element of C st c in ( dom (((f1 + f2) || C) (#) (g || C))) holds ((((f1 + f2) || C) (#) (g || C)) . c) = ((((f1 (#) g) + (f2 (#) g)) || C) . c)

      proof

        let c be Element of C;

        assume

         A3: c in ( dom (((f1 + f2) || C) (#) (g || C)));

        then

         A4: c in (( dom ((f1 + f2) || C)) /\ ( dom (g || C))) by VALUED_1:def 4;

        then

         A5: c in ( dom (g | C)) by XBOOLE_0:def 4;

        c in (( dom ((f1 (#) g) + (f2 (#) g))) /\ C) by A2, A1, A3, RELAT_1: 61;

        then

         A6: c in ( dom ((f1 (#) g) + (f2 (#) g))) by XBOOLE_0:def 4;

        then

         A7: c in (( dom (f1 (#) g)) /\ ( dom (f2 (#) g))) by VALUED_1:def 1;

        then

         A8: c in ( dom (f1 (#) g)) by XBOOLE_0:def 4;

        

         A9: c in ( dom ((f1 + f2) | C)) by A4, XBOOLE_0:def 4;

        then c in (( dom (f1 + f2)) /\ C) by RELAT_1: 61;

        then

         A10: c in ( dom (f1 + f2)) by XBOOLE_0:def 4;

        

         A11: ((((f1 + f2) || C) (#) (g || C)) . c) = ((((f1 + f2) || C) . c) * ((g || C) . c)) by A3, VALUED_1:def 4

        .= (((f1 + f2) . c) * ((g | C) . c)) by A9, FUNCT_1: 47

        .= (((f1 . c) + (f2 . c)) * ((g | C) . c)) by A10, VALUED_1:def 1;

        

         A12: c in ( dom (f2 (#) g)) by A7, XBOOLE_0:def 4;

        ((((f1 (#) g) + (f2 (#) g)) || C) . c) = (((f1 (#) g) + (f2 (#) g)) . c) by A2, A1, A3, FUNCT_1: 47

        .= (((f1 (#) g) . c) + ((f2 (#) g) . c)) by A6, VALUED_1:def 1

        .= (((f1 . c) * (g . c)) + ((f2 (#) g) . c)) by A8, VALUED_1:def 4

        .= (((f1 . c) * (g . c)) + ((f2 . c) * (g . c))) by A12, VALUED_1:def 4

        .= (((f1 . c) + (f2 . c)) * (g . c));

        hence thesis by A5, A11, FUNCT_1: 47;

      end;

      hence thesis by A2, A1, PARTFUN1: 5;

    end;

    theorem :: INTEGRA9:22

    

     Th22: for f1,f2,g be PartFunc of REAL , REAL , C be non empty Subset of REAL holds (((f1 - f2) || C) (#) (g || C)) = (((f1 (#) g) - (f2 (#) g)) || C)

    proof

      let f1,f2,g be PartFunc of REAL , REAL ;

      let C be non empty Subset of REAL ;

      

       A1: ( dom (((f1 (#) g) - (f2 (#) g)) || C)) = (( dom ((f1 (#) g) - (f2 (#) g))) /\ C) by RELAT_1: 61

      .= ((( dom (f1 (#) g)) /\ ( dom (f2 (#) g))) /\ C) by VALUED_1: 12

      .= (((( dom f1) /\ ( dom g)) /\ ( dom (f2 (#) g))) /\ C) by VALUED_1:def 4

      .= (((( dom f1) /\ ( dom g)) /\ (( dom f2) /\ ( dom g))) /\ C) by VALUED_1:def 4

      .= ((( dom f1) /\ ((( dom g) /\ ( dom f2)) /\ ( dom g))) /\ C) by XBOOLE_1: 16

      .= ((( dom f1) /\ (( dom f2) /\ (( dom g) /\ ( dom g)))) /\ C) by XBOOLE_1: 16

      .= (((( dom f1) /\ ( dom f2)) /\ ( dom g)) /\ C) by XBOOLE_1: 16;

      

       A2: ( dom (((f1 - f2) || C) (#) (g || C))) = (( dom ((f1 - f2) | C)) /\ ( dom (g | C))) by VALUED_1:def 4

      .= ((( dom (f1 - f2)) /\ C) /\ ( dom (g | C))) by RELAT_1: 61

      .= ((( dom (f1 - f2)) /\ C) /\ (( dom g) /\ C)) by RELAT_1: 61

      .= (((( dom f1) /\ ( dom f2)) /\ C) /\ (( dom g) /\ C)) by VALUED_1: 12

      .= ((( dom f1) /\ ( dom f2)) /\ ((C /\ ( dom g)) /\ C)) by XBOOLE_1: 16

      .= ((( dom f1) /\ ( dom f2)) /\ (( dom g) /\ (C /\ C))) by XBOOLE_1: 16

      .= (((( dom f1) /\ ( dom f2)) /\ ( dom g)) /\ C) by XBOOLE_1: 16;

      for c be Element of C st c in ( dom (((f1 - f2) || C) (#) (g || C))) holds ((((f1 - f2) || C) (#) (g || C)) . c) = ((((f1 (#) g) - (f2 (#) g)) || C) . c)

      proof

        let c be Element of C;

        assume

         A3: c in ( dom (((f1 - f2) || C) (#) (g || C)));

        then

         A4: c in (( dom ((f1 - f2) || C)) /\ ( dom (g || C))) by VALUED_1:def 4;

        then

         A5: c in ( dom (g | C)) by XBOOLE_0:def 4;

        c in (( dom ((f1 (#) g) - (f2 (#) g))) /\ C) by A2, A1, A3, RELAT_1: 61;

        then

         A6: c in ( dom ((f1 (#) g) - (f2 (#) g))) by XBOOLE_0:def 4;

        then

         A7: c in (( dom (f1 (#) g)) /\ ( dom (f2 (#) g))) by VALUED_1: 12;

        then

         A8: c in ( dom (f1 (#) g)) by XBOOLE_0:def 4;

        

         A9: c in ( dom ((f1 - f2) | C)) by A4, XBOOLE_0:def 4;

        then c in (( dom (f1 - f2)) /\ C) by RELAT_1: 61;

        then

         A10: c in ( dom (f1 - f2)) by XBOOLE_0:def 4;

        

         A11: ((((f1 - f2) || C) (#) (g || C)) . c) = ((((f1 - f2) | C) . c) * ((g | C) . c)) by A3, VALUED_1:def 4

        .= (((f1 - f2) . c) * ((g | C) . c)) by A9, FUNCT_1: 47

        .= (((f1 . c) - (f2 . c)) * ((g | C) . c)) by A10, VALUED_1: 13;

        

         A12: c in ( dom (f2 (#) g)) by A7, XBOOLE_0:def 4;

        ((((f1 (#) g) - (f2 (#) g)) || C) . c) = (((f1 (#) g) - (f2 (#) g)) . c) by A2, A1, A3, FUNCT_1: 47

        .= (((f1 (#) g) . c) - ((f2 (#) g) . c)) by A6, VALUED_1: 13

        .= (((f1 . c) * (g . c)) - ((f2 (#) g) . c)) by A8, VALUED_1:def 4

        .= (((f1 . c) * (g . c)) - ((f2 . c) * (g . c))) by A12, VALUED_1:def 4

        .= (((f1 . c) - (f2 . c)) * (g . c));

        hence thesis by A5, A11, FUNCT_1: 47;

      end;

      hence thesis by A2, A1, PARTFUN1: 5;

    end;

    theorem :: INTEGRA9:23

    for f1,f2,g be PartFunc of REAL , REAL , C be non empty Subset of REAL holds (((f1 (#) f2) || C) (#) (g || C)) = ((f1 || C) (#) ((f2 (#) g) || C))

    proof

      let f1,f2,g be PartFunc of REAL , REAL ;

      let C be non empty Subset of REAL ;

      (((f1 (#) f2) || C) (#) (g || C)) = (((f1 || C) (#) (f2 || C)) (#) (g || C)) & ((f1 || C) (#) ((f2 (#) g) || C)) = ((f1 || C) (#) ((f2 || C) (#) (g || C))) by INTEGRA5: 4;

      hence thesis by RFUNCT_1: 9;

    end;

    definition

      let A be non empty closed_interval Subset of REAL ;

      let f,g be PartFunc of REAL , REAL ;

      :: INTEGRA9:def1

      func |||(f,g,A)||| -> Real equals ( integral ((f (#) g),A));

      correctness ;

    end

    theorem :: INTEGRA9:24

    for f,g be PartFunc of REAL , REAL , A be non empty closed_interval Subset of REAL holds |||(f, g, A)||| = |||(g, f, A)|||;

    theorem :: INTEGRA9:25

    for f1,f2,g be PartFunc of REAL , REAL , A be non empty closed_interval Subset of REAL st ((f1 (#) g) || A) is total & ((f2 (#) g) || A) is total & (((f1 (#) g) || A) | A) is bounded & ((f1 (#) g) || A) is integrable & (((f2 (#) g) || A) | A) is bounded & ((f2 (#) g) || A) is integrable holds |||((f1 + f2), g, A)||| = ( |||(f1, g, A)||| + |||(f2, g, A)|||)

    proof

      let f1,f2,g be PartFunc of REAL , REAL ;

      let A be non empty closed_interval Subset of REAL ;

      assume

       A1: ((f1 (#) g) || A) is total & ((f2 (#) g) || A) is total;

      assume

       A2: (((f1 (#) g) || A) | A) is bounded & ((f1 (#) g) || A) is integrable & (((f2 (#) g) || A) | A) is bounded & ((f2 (#) g) || A) is integrable;

       |||((f1 + f2), g, A)||| = ( integral (((f1 + f2) || A) (#) (g || A))) by INTEGRA5: 4

      .= ( integral (((f1 (#) g) + (f2 (#) g)) || A)) by Th21

      .= ( integral (((f1 (#) g) || A) + ((f2 (#) g) || A))) by INTEGRA5: 5

      .= (( integral ((f1 (#) g) || A)) + ( integral ((f2 (#) g) || A))) by A1, A2, INTEGRA1: 57;

      hence thesis;

    end;

    theorem :: INTEGRA9:26

    for f1,f2,g be PartFunc of REAL , REAL , A be non empty closed_interval Subset of REAL st ((f1 (#) g) || A) is total & ((f2 (#) g) || A) is total & (((f1 (#) g) || A) | A) is bounded & ((f1 (#) g) || A) is integrable & (((f2 (#) g) || A) | A) is bounded & ((f2 (#) g) || A) is integrable holds |||((f1 - f2), g, A)||| = ( |||(f1, g, A)||| - |||(f2, g, A)|||)

    proof

      let f1,f2,g be PartFunc of REAL , REAL ;

      let A be non empty closed_interval Subset of REAL ;

      assume

       A1: ((f1 (#) g) || A) is total & ((f2 (#) g) || A) is total;

      assume

       A2: (((f1 (#) g) || A) | A) is bounded & ((f1 (#) g) || A) is integrable & (((f2 (#) g) || A) | A) is bounded & ((f2 (#) g) || A) is integrable;

       |||((f1 - f2), g, A)||| = ( integral (((f1 - f2) || A) (#) (g || A))) by INTEGRA5: 4

      .= ( integral (((f1 (#) g) - (f2 (#) g)) || A)) by Th22

      .= ( integral (((f1 (#) g) || A) - ((f2 (#) g) || A))) by Th20

      .= (( integral ((f1 (#) g) || A)) - ( integral ((f2 (#) g) || A))) by A1, A2, INTEGRA2: 33;

      hence thesis;

    end;

    theorem :: INTEGRA9:27

    for f,g be PartFunc of REAL , REAL , A be non empty closed_interval Subset of REAL st ((f (#) g) | A) is bounded & (f (#) g) is_integrable_on A & A c= ( dom (f (#) g)) holds |||(( - f), g, A)||| = ( - |||(f, g, A)|||)

    proof

      let f,g be PartFunc of REAL , REAL ;

      let A be non empty closed_interval Subset of REAL ;

      assume

       A1: ((f (#) g) | A) is bounded & (f (#) g) is_integrable_on A & A c= ( dom (f (#) g));

       |||(( - f), g, A)||| = ( integral ((( - 1) (#) (f (#) g)),A)) by RFUNCT_1: 12

      .= (( - 1) * ( integral ((f (#) g),A))) by A1, INTEGRA6: 9

      .= ( - |||(f, g, A)|||);

      hence thesis;

    end;

    theorem :: INTEGRA9:28

    for f,g be PartFunc of REAL , REAL , A be non empty closed_interval Subset of REAL st ((f (#) g) | A) is bounded & (f (#) g) is_integrable_on A & A c= ( dom (f (#) g)) holds |||((r (#) f), g, A)||| = (r * |||(f, g, A)|||)

    proof

      let f,g be PartFunc of REAL , REAL ;

      let A be non empty closed_interval Subset of REAL ;

      assume

       A1: ((f (#) g) | A) is bounded & (f (#) g) is_integrable_on A & A c= ( dom (f (#) g));

       |||((r (#) f), g, A)||| = ( integral ((r (#) (f (#) g)),A)) by RFUNCT_1: 12

      .= (r * ( integral ((f (#) g),A))) by A1, INTEGRA6: 9;

      hence thesis;

    end;

    theorem :: INTEGRA9:29

    for f,g be PartFunc of REAL , REAL , A be non empty closed_interval Subset of REAL st ((f (#) g) | A) is bounded & (f (#) g) is_integrable_on A & A c= ( dom (f (#) g)) holds |||((r (#) f), (p (#) g), A)||| = ((r * p) * |||(f, g, A)|||)

    proof

      let f,g be PartFunc of REAL , REAL ;

      let A be non empty closed_interval Subset of REAL ;

      assume

       A1: ((f (#) g) | A) is bounded & (f (#) g) is_integrable_on A & A c= ( dom (f (#) g));

       |||((r (#) f), (p (#) g), A)||| = ( integral ((r (#) (f (#) (p (#) g))),A)) by RFUNCT_1: 12

      .= ( integral ((r (#) (p (#) (f (#) g))),A)) by RFUNCT_1: 13

      .= ( integral (((r * p) (#) (f (#) g)),A)) by RFUNCT_1: 17

      .= ((r * p) * ( integral ((f (#) g),A))) by A1, INTEGRA6: 9;

      hence thesis;

    end;

    theorem :: INTEGRA9:30

    for f,g,h be PartFunc of REAL , REAL , A be non empty closed_interval Subset of REAL holds |||((f (#) g), h, A)||| = |||(f, (g (#) h), A)||| by RFUNCT_1: 9;

    theorem :: INTEGRA9:31

    

     Th31: for f,g be PartFunc of REAL , REAL , A be non empty closed_interval Subset of REAL st ((f (#) f) || A) is total & ((f (#) g) || A) is total & ((g (#) g) || A) is total & (((f (#) f) || A) | A) is bounded & (((f (#) g) || A) | A) is bounded & (((g (#) g) || A) | A) is bounded & (f (#) f) is_integrable_on A & (f (#) g) is_integrable_on A & (g (#) g) is_integrable_on A holds |||((f + g), (f + g), A)||| = (( |||(f, f, A)||| + (2 * |||(f, g, A)|||)) + |||(g, g, A)|||)

    proof

      let f,g be PartFunc of REAL , REAL ;

      let A be non empty closed_interval Subset of REAL ;

      assume that

       A1: ((f (#) f) || A) is total and

       A2: ((f (#) g) || A) is total and

       A3: ((g (#) g) || A) is total;

      assume that

       A4: (((f (#) f) || A) | A) is bounded and

       A5: (((f (#) g) || A) | A) is bounded and

       A6: (((g (#) g) || A) | A) is bounded;

      assume that

       A7: (f (#) f) is_integrable_on A and

       A8: (f (#) g) is_integrable_on A and

       A9: (g (#) g) is_integrable_on A;

      

       A10: ((f (#) g) || A) is integrable by A8;

      

       A11: ((g (#) g) || A) is integrable by A9;

      then

       A12: (((f (#) g) || A) + ((g (#) g) || A)) is integrable by A2, A3, A5, A6, A10, INTEGRA1: 57;

      

       A13: ((f (#) f) || A) is integrable by A7;

      then

       A14: (((f (#) f) || A) + ((f (#) g) || A)) is integrable by A1, A2, A4, A5, A10, INTEGRA1: 57;

      

       A15: ((((f (#) f) || A) + ((f (#) g) || A)) | (A /\ A)) is bounded & ((((f (#) g) || A) + ((g (#) g) || A)) | (A /\ A)) is bounded by A4, A5, A6, RFUNCT_1: 83;

       |||((f + g), (f + g), A)||| = ( integral (((f (#) (f + g)) + (g (#) (f + g))) || A)) by RFUNCT_1: 10

      .= ( integral (((f (#) (f + g)) || A) + ((g (#) (f + g)) || A))) by INTEGRA5: 5

      .= ( integral ((((f (#) f) + (f (#) g)) || A) + ((g (#) (f + g)) || A))) by RFUNCT_1: 11

      .= ( integral ((((f (#) f) + (f (#) g)) || A) + (((g (#) f) + (g (#) g)) || A))) by RFUNCT_1: 11

      .= ( integral ((((f (#) f) || A) + ((f (#) g) || A)) + (((g (#) f) + (g (#) g)) || A))) by INTEGRA5: 5

      .= ( integral ((((f (#) f) || A) + ((f (#) g) || A)) + (((g (#) f) || A) + ((g (#) g) || A)))) by INTEGRA5: 5

      .= (( integral (((f (#) f) || A) + ((f (#) g) || A))) + ( integral (((f (#) g) || A) + ((g (#) g) || A)))) by A1, A2, A3, A15, A14, A12, INTEGRA1: 57

      .= ((( integral ((f (#) f) || A)) + ( integral ((f (#) g) || A))) + ( integral (((f (#) g) || A) + ((g (#) g) || A)))) by A1, A2, A4, A5, A13, A10, INTEGRA1: 57

      .= ((( integral ((f (#) f) || A)) + ( integral ((f (#) g) || A))) + (( integral ((f (#) g) || A)) + ( integral ((g (#) g) || A)))) by A2, A3, A5, A6, A10, A11, INTEGRA1: 57;

      hence thesis;

    end;

    begin

    definition

      let A be non empty closed_interval Subset of REAL ;

      let f,g be PartFunc of REAL , REAL ;

      :: INTEGRA9:def2

      pred f is_orthogonal_with g,A means |||(f, g, A)||| = 0 ;

    end

    theorem :: INTEGRA9:32

    

     Th32: for f,g be PartFunc of REAL , REAL , A be non empty closed_interval Subset of REAL st ((f (#) f) || A) is total & ((f (#) g) || A) is total & ((g (#) g) || A) is total & (((f (#) f) || A) | A) is bounded & (((f (#) g) || A) | A) is bounded & (((g (#) g) || A) | A) is bounded & (f (#) f) is_integrable_on A & (f (#) g) is_integrable_on A & (g (#) g) is_integrable_on A & f is_orthogonal_with (g,A) holds |||((f + g), (f + g), A)||| = ( |||(f, f, A)||| + |||(g, g, A)|||)

    proof

      let f,g be PartFunc of REAL , REAL ;

      let A be non empty closed_interval Subset of REAL ;

      assume ((f (#) f) || A) is total & ((f (#) g) || A) is total & ((g (#) g) || A) is total & (((f (#) f) || A) | A) is bounded & (((f (#) g) || A) | A) is bounded & (((g (#) g) || A) | A) is bounded & (f (#) f) is_integrable_on A & (f (#) g) is_integrable_on A & (g (#) g) is_integrable_on A;

      then

       A1: |||((f + g), (f + g), A)||| = (( |||(f, f, A)||| + (2 * |||(f, g, A)|||)) + |||(g, g, A)|||) by Th31;

      assume f is_orthogonal_with (g,A);

      then |||(f, g, A)||| = 0 ;

      hence thesis by A1;

    end;

    theorem :: INTEGRA9:33

    for f be PartFunc of REAL , REAL , A be non empty closed_interval Subset of REAL st ((f (#) f) || A) is total & (((f (#) f) || A) | A) is bounded & ((f (#) f) || A) is integrable & (for x st x in A holds (((f (#) f) || A) . x) >= 0 ) holds |||(f, f, A)||| >= 0 by INTEGRA2: 32;

    theorem :: INTEGRA9:34

    A = [. 0 , PI .] implies sin is_orthogonal_with ( cos ,A) by INTEGRA8: 92;

    theorem :: INTEGRA9:35

    A = [. 0 , ( PI * 2).] implies sin is_orthogonal_with ( cos ,A) by INTEGRA8: 94;

    theorem :: INTEGRA9:36

    A = [.((2 * n) * PI ), (((2 * n) + 1) * PI ).] implies sin is_orthogonal_with ( cos ,A) by INTEGRA8: 95;

    theorem :: INTEGRA9:37

    A = [.(x + ((2 * n) * PI )), (x + (((2 * n) + 1) * PI )).] implies sin is_orthogonal_with ( cos ,A) by INTEGRA8: 96;

    theorem :: INTEGRA9:38

    A = [.( - PI ), PI .] implies sin is_orthogonal_with ( cos ,A)

    proof

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

      then

       A1: ( upper_bound A) = PI & ( lower_bound A) = ( - PI ) by INTEGRA8: 37;

       |||( sin , cos , A)||| = ((1 / 2) * ((( cos . ( lower_bound A)) * ( cos . ( lower_bound A))) - (( cos . ( upper_bound A)) * ( cos . ( upper_bound A))))) by INTEGRA8: 90

      .= ((1 / 2) * ((( cos . PI ) * ( cos . ( - PI ))) - (( cos . PI ) * ( cos . PI )))) by A1, SIN_COS: 30

      .= ((1 / 2) * ((( cos . PI ) * ( cos . PI )) - (( cos . PI ) * ( cos . PI )))) by SIN_COS: 30;

      hence thesis;

    end;

    theorem :: INTEGRA9:39

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

    proof

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

      then

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

       |||( sin , cos , A)||| = ((1 / 2) * ((( cos . ( lower_bound A)) * ( cos . ( lower_bound A))) - (( cos . ( upper_bound A)) * ( cos . ( upper_bound A))))) by INTEGRA8: 90

      .= ((1 / 2) * ((( cos . ( PI / 2)) * ( cos . ( - ( PI / 2)))) - (( cos . ( PI / 2)) * ( cos . ( PI / 2))))) by A1, SIN_COS: 30

      .= ((1 / 2) * ((( cos . ( PI / 2)) * ( cos . ( PI / 2))) - (( cos . ( PI / 2)) * ( cos . ( PI / 2))))) by SIN_COS: 30;

      hence thesis;

    end;

    theorem :: INTEGRA9:40

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

    proof

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

      then

       A1: ( upper_bound A) = (2 * PI ) & ( lower_bound A) = ( - (2 * PI )) by INTEGRA8: 37;

       |||( sin , cos , A)||| = ((1 / 2) * ((( cos . ( lower_bound A)) * ( cos . ( lower_bound A))) - (( cos . ( upper_bound A)) * ( cos . ( upper_bound A))))) by INTEGRA8: 90

      .= ((1 / 2) * ((( cos . (2 * PI )) * ( cos . ( - (2 * PI )))) - (( cos . (2 * PI )) * ( cos . (2 * PI ))))) by A1, SIN_COS: 30

      .= ((1 / 2) * ((( cos . (2 * PI )) * ( cos . (2 * PI ))) - (( cos . (2 * PI )) * ( cos . (2 * PI ))))) by SIN_COS: 30;

      hence thesis;

    end;

    theorem :: INTEGRA9:41

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

    proof

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

      then

       A1: ( upper_bound A) = ((2 * n) * PI ) & ( lower_bound A) = ( - ((2 * n) * PI )) by INTEGRA8: 37;

       |||( sin , cos , A)||| = ((1 / 2) * ((( cos . ( lower_bound A)) * ( cos . ( lower_bound A))) - (( cos . ( upper_bound A)) * ( cos . ( upper_bound A))))) by INTEGRA8: 90

      .= ((1 / 2) * ((( cos . ((2 * n) * PI )) * ( cos . ( - ((2 * n) * PI )))) - (( cos . ((2 * n) * PI )) * ( cos . ((2 * n) * PI ))))) by A1, SIN_COS: 30

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

      hence thesis;

    end;

    theorem :: INTEGRA9:42

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

    proof

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

      then

       A1: ( upper_bound A) = (x + ((2 * n) * PI )) & ( lower_bound A) = (x - ((2 * n) * PI )) by INTEGRA8: 37;

       |||( sin , cos , A)||| = ((1 / 2) * ((( cos . ( lower_bound A)) * ( cos . ( lower_bound A))) - (( cos . ( upper_bound A)) * ( cos . ( upper_bound A))))) by INTEGRA8: 90

      .= ((1 / 2) * ((( cos . (((2 * n) * PI ) - x)) * ( cos . ( - (((2 * n) * PI ) - x)))) - (( cos . (x + ((2 * n) * PI ))) * ( cos . (x + ((2 * n) * PI )))))) by A1, SIN_COS: 30

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

      .= ((1 / 2) * ((( cos ( - x)) * ( cos (( - x) + ((2 * n) * PI )))) - (( cos . (x + ((2 * n) * PI ))) * ( cos . (x + ((2 * n) * PI )))))) by INTEGRA8: 3

      .= ((1 / 2) * ((( cos ( - x)) * ( cos ( - x))) - (( cos . (x + ((2 * n) * PI ))) * ( cos . (x + ((2 * n) * PI )))))) by INTEGRA8: 3

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

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

      .= ((1 / 2) * ((( cos x) * ( cos x)) - (( cos x) * ( cos (x + ((2 * n) * PI )))))) by INTEGRA8: 3

      .= ((1 / 2) * ((( cos x) * ( cos x)) - (( cos x) * ( cos x)))) by INTEGRA8: 3;

      hence thesis;

    end;

    begin

    definition

      let A be non empty closed_interval Subset of REAL ;

      let f be PartFunc of REAL , REAL ;

      :: INTEGRA9:def3

      func ||..f,A..|| -> Real equals ( sqrt |||(f, f, A)|||);

      correctness ;

    end

    theorem :: INTEGRA9:43

    for f be PartFunc of REAL , REAL , A be non empty closed_interval Subset of REAL st ((f (#) f) || A) is total & (((f (#) f) || A) | A) is bounded & (for x st x in A holds (((f (#) f) || A) . x) >= 0 ) holds 0 <= ||..f, A..||

    proof

      let f be PartFunc of REAL , REAL ;

      let A be non empty closed_interval Subset of REAL ;

      assume

       A1: ((f (#) f) || A) is total;

      assume (((f (#) f) || A) | A) is bounded & for x st x in A holds (((f (#) f) || A) . x) >= 0 ;

      then |||(f, f, A)||| >= 0 by A1, INTEGRA2: 32;

      hence thesis by SQUARE_1:def 2;

    end;

    theorem :: INTEGRA9:44

    for f be PartFunc of REAL , REAL , A be non empty closed_interval Subset of REAL holds ||..(1 (#) f), A..|| = ||..f, A..|| by RFUNCT_1: 21;

    theorem :: INTEGRA9:45

    for f,g be PartFunc of REAL , REAL , A be non empty closed_interval Subset of REAL st ((f (#) f) || A) is total & ((f (#) g) || A) is total & ((g (#) g) || A) is total & (((f (#) f) || A) | A) is bounded & (((f (#) g) || A) | A) is bounded & (((g (#) g) || A) | A) is bounded & (f (#) f) is_integrable_on A & (f (#) g) is_integrable_on A & (g (#) g) is_integrable_on A & f is_orthogonal_with (g,A) & (for x st x in A holds (((f (#) f) || A) . x) >= 0 ) & (for x st x in A holds (((g (#) g) || A) . x) >= 0 ) holds ( ||..(f + g), A..|| ^2 ) = (( ||..f, A..|| ^2 ) + ( ||..g, A..|| ^2 ))

    proof

      let f,g be PartFunc of REAL , REAL ;

      let A be non empty closed_interval Subset of REAL ;

      assume that

       A1: ((f (#) f) || A) is total and

       A2: ((f (#) g) || A) is total and

       A3: ((g (#) g) || A) is total and

       A4: (((f (#) f) || A) | A) is bounded and

       A5: (((f (#) g) || A) | A) is bounded and

       A6: (((g (#) g) || A) | A) is bounded and

       A7: (f (#) f) is_integrable_on A & (f (#) g) is_integrable_on A & (g (#) g) is_integrable_on A;

      assume

       A8: f is_orthogonal_with (g,A);

      assume for x st x in A holds (((f (#) f) || A) . x) >= 0 ;

      then

       A9: |||(f, f, A)||| >= 0 by A1, A4, INTEGRA2: 32;

      assume for x st x in A holds (((g (#) g) || A) . x) >= 0 ;

      then

       A10: |||(g, g, A)||| >= 0 by A3, A6, INTEGRA2: 32;

      then

       A11: ( ||..g, A..|| ^2 ) = |||(g, g, A)||| by SQUARE_1:def 2;

       |||((f + g), (f + g), A)||| = ( |||(f, f, A)||| + |||(g, g, A)|||) by A1, A2, A3, A4, A5, A6, A7, A8, Th32;

      then |||((f + g), (f + g), A)||| >= 0 by A9, A10, XREAL_1: 33;

      then

       A12: ( ||..(f + g), A..|| ^2 ) = |||((f + g), (f + g), A)||| by SQUARE_1:def 2;

      ( ||..f, A..|| ^2 ) = |||(f, f, A)||| by A9, SQUARE_1:def 2;

      hence thesis by A1, A2, A3, A4, A5, A6, A7, A8, A12, A11, Th32;

    end;

    begin

    reserve a,b,x for Real;

    reserve n for Element of NAT ;

    reserve A for non empty closed_interval Subset of REAL ;

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

    reserve Z for open Subset of REAL ;

    theorem :: INTEGRA9:46

     not ( - a) in A implies ((( AffineMap (1,a)) ^ ) | A) is continuous

    proof

      set g2 = ( AffineMap (1,a));

      assume

       A1: not ( - a) in A;

       not 0 in ( rng (g2 | A))

      proof

        set h2 = (g2 | A);

        assume 0 in ( rng (g2 | A));

        then

        consider x be object such that

         A2: x in ( dom h2) and

         A3: (h2 . x) = 0 by FUNCT_1:def 3;

        reconsider d = x as Element of REAL by A2;

        

         A4: (g2 . d) = (a + (1 * d)) by FCONT_1:def 4;

        d in A by A2, RELAT_1: 57;

        then ( dom h2) c= A & (a + d) = 0 by A3, A4, FUNCT_1: 49, RELAT_1: 58;

        hence thesis by A1, A2;

      end;

      then

       A5: ((g2 | A) " { 0 }) = {} by FUNCT_1: 72;

      thus thesis by A5, FCONT_1: 23;

    end;

    theorem :: INTEGRA9:47

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

    proof

      assume that

       A1: A c= Z and

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

       A3: Z = ( dom f) and

       A4: ( dom f) = ( dom f2) and

       A5: for x st x in Z holds (f2 . x) = ( - (1 / ((a + x) ^2 ))) and

       A6: (f2 | A) is continuous;

      

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

      

       A8: (f ^ ) is_differentiable_on Z by A2, A3, FDIFF_4: 14;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

        then (((f ^ ) `| Z) . x) = ( - (1 / ((a + x) ^2 ))) by A2, A3, FDIFF_4: 14

        .= (f2 . x) by A5, A10;

        hence thesis;

      end;

      ( dom ((f ^ ) `| Z)) = ( dom f2) by A3, A4, A8, FDIFF_1:def 7;

      then ((f ^ ) `| Z) = f2 by A9, PARTFUN1: 5;

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

    end;

    theorem :: INTEGRA9:48

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

    proof

      assume that

       A1: A c= Z and

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

       A3: ( dom (( - 1) (#) (f ^ ))) = Z and

       A4: ( dom (( - 1) (#) (f ^ ))) = ( dom f2) and

       A5: for x st x in Z holds (f2 . x) = (1 / ((a + x) ^2 )) and

       A6: (f2 | A) is continuous;

      

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

      

       A8: (( - 1) (#) (f ^ )) is_differentiable_on Z by A2, A3, FDIFF_4: 15;

      

       A9: for x be Element of REAL st x in ( dom ((( - 1) (#) (f ^ )) `| Z)) holds (((( - 1) (#) (f ^ )) `| Z) . x) = (f2 . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom ((( - 1) (#) (f ^ )) `| Z));

        then

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

        

        then (((( - 1) (#) (f ^ )) `| Z) . x) = (1 / ((a + x) ^2 )) by A2, A3, FDIFF_4: 15

        .= (f2 . x) by A5, A10;

        hence thesis;

      end;

      ( dom ((( - 1) (#) (f ^ )) `| Z)) = ( dom f2) by A3, A4, A8, FDIFF_1:def 7;

      then ((( - 1) (#) (f ^ )) `| Z) = f2 by A9, PARTFUN1: 5;

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

    end;

    theorem :: INTEGRA9:49

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

    proof

      assume that

       A1: A c= Z and

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

       A3: ( dom f) = Z and

       A4: ( dom f) = ( dom f2) and

       A5: for x st x in Z holds (f2 . x) = (1 / ((a - x) ^2 )) and

       A6: (f2 | A) is continuous;

      

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

      

       A8: (f ^ ) is_differentiable_on Z by A2, A3, FDIFF_4: 16;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

        then (((f ^ ) `| Z) . x) = (1 / ((a - x) ^2 )) by A2, A3, FDIFF_4: 16

        .= (f2 . x) by A5, A10;

        hence thesis;

      end;

      ( dom ((f ^ ) `| Z)) = ( dom f2) by A3, A4, A8, FDIFF_1:def 7;

      then ((f ^ ) `| Z) = f2 by A9, PARTFUN1: 5;

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

    end;

    theorem :: INTEGRA9:50

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

    proof

      assume that

       A1: A c= Z and

       A2: for x st x in Z holds (f . x) = (a + x) & (f . x) > 0 and

       A3: ( dom ( ln * f)) = Z and

       A4: ( dom ( ln * f)) = ( dom f2) and

       A5: for x st x in Z holds (f2 . x) = (1 / (a + x)) and

       A6: (f2 | A) is continuous;

      

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

      

       A8: ( ln * f) is_differentiable_on Z by A2, A3, FDIFF_4: 1;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

        then ((( ln * f) `| Z) . x) = (1 / (a + x)) by A2, A3, FDIFF_4: 1

        .= (f2 . x) by A5, A10;

        hence thesis;

      end;

      ( dom (( ln * f) `| Z)) = ( dom f2) by A3, A4, A8, FDIFF_1:def 7;

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

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

    end;

    theorem :: INTEGRA9:51

    A c= Z & (for x st x in Z holds (f . x) = (x - a) & (f . x) > 0 ) & ( dom ( ln * f)) = Z & ( dom ( ln * f)) = ( dom f2) & (for x st x in Z holds (f2 . x) = (1 / (x - a))) & (f2 | A) is continuous implies ( integral (f2,A)) = ((( ln * f) . ( upper_bound A)) - (( ln * f) . ( lower_bound A)))

    proof

      assume that

       A1: A c= Z and

       A2: for x st x in Z holds (f . x) = (x - a) & (f . x) > 0 and

       A3: ( dom ( ln * f)) = Z and

       A4: ( dom ( ln * f)) = ( dom f2) and

       A5: for x st x in Z holds (f2 . x) = (1 / (x - a)) and

       A6: (f2 | A) is continuous;

      

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

      

       A8: ( ln * f) is_differentiable_on Z by A2, A3, FDIFF_4: 2;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

        then ((( ln * f) `| Z) . x) = (1 / (x - a)) by A2, A3, FDIFF_4: 2

        .= (f2 . x) by A5, A10;

        hence thesis;

      end;

      ( dom (( ln * f) `| Z)) = ( dom f2) by A3, A4, A8, FDIFF_1:def 7;

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

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

    end;

    theorem :: INTEGRA9:52

    A c= Z & (for x st x in Z holds (f . x) = (a - x) & (f . x) > 0 ) & ( dom ( - ( ln * f))) = Z & ( dom ( - ( ln * f))) = ( dom f2) & (for x st x in Z holds (f2 . x) = (1 / (a - x))) & (f2 | A) is continuous implies ( integral (f2,A)) = ((( - ( ln * f)) . ( upper_bound A)) - (( - ( ln * f)) . ( lower_bound A)))

    proof

      assume that

       A1: A c= Z and

       A2: for x st x in Z holds (f . x) = (a - x) & (f . x) > 0 and

       A3: ( dom ( - ( ln * f))) = Z and

       A4: ( dom ( - ( ln * f))) = ( dom f2) and

       A5: for x st x in Z holds (f2 . x) = (1 / (a - x)) and

       A6: (f2 | A) is continuous;

      

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

      

       A8: ( - ( ln * f)) is_differentiable_on Z by A2, A3, FDIFF_4: 3;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

        then ((( - ( ln * f)) `| Z) . x) = (1 / (a - x)) by A2, A3, FDIFF_4: 3

        .= (f2 . x) by A5, A10;

        hence thesis;

      end;

      ( dom (( - ( ln * f)) `| Z)) = ( dom f2) by A3, A4, A8, FDIFF_1:def 7;

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

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

    end;

    theorem :: INTEGRA9:53

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

    proof

      assume that

       A1: A c= Z and

       A2: (f = ( ln * f1) & for x st x in Z holds (f1 . x) = (a + x) & (f1 . x) > 0 ) & ( dom (( id Z) - (a (#) f))) = Z and

       A3: Z = ( dom f2) and

       A4: for x st x in Z holds (f2 . x) = (x / (a + x)) and

       A5: (f2 | A) is continuous;

      

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

      

       A7: (( id Z) - (a (#) f)) is_differentiable_on Z by A2, FDIFF_4: 4;

      

       A8: for x be Element of REAL st x in ( dom ((( id Z) - (a (#) f)) `| Z)) holds (((( id Z) - (a (#) f)) `| Z) . x) = (f2 . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom ((( id Z) - (a (#) f)) `| Z));

        then

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

        

        then (((( id Z) - (a (#) f)) `| Z) . x) = (x / (a + x)) by A2, FDIFF_4: 4

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

        hence thesis;

      end;

      ( dom ((( id Z) - (a (#) f)) `| Z)) = ( dom f2) by A3, A7, FDIFF_1:def 7;

      then ((( id Z) - (a (#) f)) `| Z) = f2 by A8, PARTFUN1: 5;

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

    end;

    theorem :: INTEGRA9:54

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

    proof

      assume that

       A1: A c= Z and

       A2: (f = ( ln * f1) & for x st x in Z holds (f1 . x) = (a + x) & (f1 . x) > 0 ) & ( dom (((2 * a) (#) f) - ( id Z))) = Z and

       A3: Z = ( dom f2) and

       A4: for x st x in Z holds (f2 . x) = ((a - x) / (a + x)) and

       A5: (f2 | A) is continuous;

      

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

      

       A7: (((2 * a) (#) f) - ( id Z)) is_differentiable_on Z by A2, FDIFF_4: 5;

      

       A8: for x be Element of REAL st x in ( dom ((((2 * a) (#) f) - ( id Z)) `| Z)) holds (((((2 * a) (#) f) - ( id Z)) `| Z) . x) = (f2 . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom ((((2 * a) (#) f) - ( id Z)) `| Z));

        then

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

        

        then (((((2 * a) (#) f) - ( id Z)) `| Z) . x) = ((a - x) / (a + x)) by A2, FDIFF_4: 5

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

        hence thesis;

      end;

      ( dom ((((2 * a) (#) f) - ( id Z)) `| Z)) = ( dom f2) by A3, A7, FDIFF_1:def 7;

      then ((((2 * a) (#) f) - ( id Z)) `| Z) = f2 by A8, PARTFUN1: 5;

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

    end;

    theorem :: INTEGRA9:55

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

    proof

      assume that

       A1: A c= Z and

       A2: (f = ( ln * f1) & for x st x in Z holds (f1 . x) = (x + a) & (f1 . x) > 0 ) & ( dom (( id Z) - ((2 * a) (#) f))) = Z and

       A3: Z = ( dom f2) and

       A4: for x st x in Z holds (f2 . x) = ((x - a) / (x + a)) and

       A5: (f2 | A) is continuous;

      

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

      

       A7: (( id Z) - ((2 * a) (#) f)) is_differentiable_on Z by A2, FDIFF_4: 6;

      

       A8: for x be Element of REAL st x in ( dom ((( id Z) - ((2 * a) (#) f)) `| Z)) holds (((( id Z) - ((2 * a) (#) f)) `| Z) . x) = (f2 . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom ((( id Z) - ((2 * a) (#) f)) `| Z));

        then

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

        

        then (((( id Z) - ((2 * a) (#) f)) `| Z) . x) = ((x - a) / (x + a)) by A2, FDIFF_4: 6

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

        hence thesis;

      end;

      ( dom ((( id Z) - ((2 * a) (#) f)) `| Z)) = ( dom f2) by A3, A7, FDIFF_1:def 7;

      then ((( id Z) - ((2 * a) (#) f)) `| Z) = f2 by A8, PARTFUN1: 5;

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

    end;

    theorem :: INTEGRA9:56

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

    proof

      assume that

       A1: A c= Z and

       A2: (f = ( ln * f1) & for x st x in Z holds (f1 . x) = (x - a) & (f1 . x) > 0 ) & ( dom (( id Z) + ((2 * a) (#) f))) = Z and

       A3: Z = ( dom f2) and

       A4: for x st x in Z holds (f2 . x) = ((x + a) / (x - a)) and

       A5: (f2 | A) is continuous;

      

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

      

       A7: (( id Z) + ((2 * a) (#) f)) is_differentiable_on Z by A2, FDIFF_4: 7;

      

       A8: for x be Element of REAL st x in ( dom ((( id Z) + ((2 * a) (#) f)) `| Z)) holds (((( id Z) + ((2 * a) (#) f)) `| Z) . x) = (f2 . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom ((( id Z) + ((2 * a) (#) f)) `| Z));

        then

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

        

        then (((( id Z) + ((2 * a) (#) f)) `| Z) . x) = ((x + a) / (x - a)) by A2, FDIFF_4: 7

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

        hence thesis;

      end;

      ( dom ((( id Z) + ((2 * a) (#) f)) `| Z)) = ( dom f2) by A3, A7, FDIFF_1:def 7;

      then ((( id Z) + ((2 * a) (#) f)) `| Z) = f2 by A8, PARTFUN1: 5;

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

    end;

    theorem :: INTEGRA9:57

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

    proof

      assume that

       A1: A c= Z and

       A2: (f = ( ln * f1) & for x st x in Z holds (f1 . x) = (x + b) & (f1 . x) > 0 ) & ( dom (( id Z) + ((a - b) (#) f))) = Z and

       A3: Z = ( dom f2) and

       A4: for x st x in Z holds (f2 . x) = ((x + a) / (x + b)) and

       A5: (f2 | A) is continuous;

      

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

      

       A7: (( id Z) + ((a - b) (#) f)) is_differentiable_on Z by A2, FDIFF_4: 8;

      

       A8: for x be Element of REAL st x in ( dom ((( id Z) + ((a - b) (#) f)) `| Z)) holds (((( id Z) + ((a - b) (#) f)) `| Z) . x) = (f2 . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom ((( id Z) + ((a - b) (#) f)) `| Z));

        then

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

        

        then (((( id Z) + ((a - b) (#) f)) `| Z) . x) = ((x + a) / (x + b)) by A2, FDIFF_4: 8

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

        hence thesis;

      end;

      ( dom ((( id Z) + ((a - b) (#) f)) `| Z)) = ( dom f2) by A3, A7, FDIFF_1:def 7;

      then ((( id Z) + ((a - b) (#) f)) `| Z) = f2 by A8, PARTFUN1: 5;

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

    end;

    theorem :: INTEGRA9:58

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

    proof

      assume that

       A1: A c= Z and

       A2: (f = ( ln * f1) & for x st x in Z holds (f1 . x) = (x - b) & (f1 . x) > 0 ) & ( dom (( id Z) + ((a + b) (#) f))) = Z and

       A3: Z = ( dom f2) and

       A4: for x st x in Z holds (f2 . x) = ((x + a) / (x - b)) and

       A5: (f2 | A) is continuous;

      

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

      

       A7: (( id Z) + ((a + b) (#) f)) is_differentiable_on Z by A2, FDIFF_4: 9;

      

       A8: for x be Element of REAL st x in ( dom ((( id Z) + ((a + b) (#) f)) `| Z)) holds (((( id Z) + ((a + b) (#) f)) `| Z) . x) = (f2 . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom ((( id Z) + ((a + b) (#) f)) `| Z));

        then

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

        

        then (((( id Z) + ((a + b) (#) f)) `| Z) . x) = ((x + a) / (x - b)) by A2, FDIFF_4: 9

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

        hence thesis;

      end;

      ( dom ((( id Z) + ((a + b) (#) f)) `| Z)) = ( dom f2) by A3, A7, FDIFF_1:def 7;

      then ((( id Z) + ((a + b) (#) f)) `| Z) = f2 by A8, PARTFUN1: 5;

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

    end;

    theorem :: INTEGRA9:59

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

    proof

      assume that

       A1: A c= Z and

       A2: (f = ( ln * f1) & for x st x in Z holds (f1 . x) = (x + b) & (f1 . x) > 0 ) & ( dom (( id Z) - ((a + b) (#) f))) = Z and

       A3: Z = ( dom f2) and

       A4: for x st x in Z holds (f2 . x) = ((x - a) / (x + b)) and

       A5: (f2 | A) is continuous;

      

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

      

       A7: (( id Z) - ((a + b) (#) f)) is_differentiable_on Z by A2, FDIFF_4: 10;

      

       A8: for x be Element of REAL st x in ( dom ((( id Z) - ((a + b) (#) f)) `| Z)) holds (((( id Z) - ((a + b) (#) f)) `| Z) . x) = (f2 . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom ((( id Z) - ((a + b) (#) f)) `| Z));

        then

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

        

        then (((( id Z) - ((a + b) (#) f)) `| Z) . x) = ((x - a) / (x + b)) by A2, FDIFF_4: 10

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

        hence thesis;

      end;

      ( dom ((( id Z) - ((a + b) (#) f)) `| Z)) = ( dom f2) by A3, A7, FDIFF_1:def 7;

      then ((( id Z) - ((a + b) (#) f)) `| Z) = f2 by A8, PARTFUN1: 5;

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

    end;

    theorem :: INTEGRA9:60

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

    proof

      assume that

       A1: A c= Z and

       A2: (f = ( ln * f1) & for x st x in Z holds (f1 . x) = (x - b) & (f1 . x) > 0 ) & ( dom (( id Z) + ((b - a) (#) f))) = Z and

       A3: Z = ( dom f2) and

       A4: for x st x in Z holds (f2 . x) = ((x - a) / (x - b)) and

       A5: (f2 | A) is continuous;

      

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

      

       A7: (( id Z) + ((b - a) (#) f)) is_differentiable_on Z by A2, FDIFF_4: 11;

      

       A8: for x be Element of REAL st x in ( dom ((( id Z) + ((b - a) (#) f)) `| Z)) holds (((( id Z) + ((b - a) (#) f)) `| Z) . x) = (f2 . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom ((( id Z) + ((b - a) (#) f)) `| Z));

        then

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

        

        then (((( id Z) + ((b - a) (#) f)) `| Z) . x) = ((x - a) / (x - b)) by A2, FDIFF_4: 11

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

        hence thesis;

      end;

      ( dom ((( id Z) + ((b - a) (#) f)) `| Z)) = ( dom f2) by A3, A7, FDIFF_1:def 7;

      then ((( id Z) + ((b - a) (#) f)) `| Z) = f2 by A8, PARTFUN1: 5;

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

    end;

    theorem :: INTEGRA9:61

    A c= Z & ( dom ln ) = Z & Z = ( dom (( id Z) ^ )) & ((( id Z) ^ ) | A) is continuous implies ( integral ((( id Z) ^ ),A)) = (( ln . ( upper_bound A)) - ( ln . ( lower_bound A)))

    proof

      set f2 = (( id Z) ^ );

      assume that

       A1: A c= Z and

       A2: ( dom ln ) = Z and

       A3: Z = ( dom (( id Z) ^ )) and

       A4: ((( id Z) ^ ) | A) is continuous;

      

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

      

       A6: ln is_differentiable_on Z by A2, FDIFF_5: 19;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

        then (( ln `| Z) . x) = (1 / x) by A2, FDIFF_5: 19

        .= (x " ) by XCMPLX_1: 215

        .= ((( id Z) . x) " ) by A8, FUNCT_1: 18

        .= (f2 . x) by A3, A8, RFUNCT_1:def 2;

        hence thesis;

      end;

      ( dom ( ln `| Z)) = ( dom f2) by A3, A6, FDIFF_1:def 7;

      then ( ln `| Z) = f2 by A7, PARTFUN1: 5;

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

    end;

    theorem :: INTEGRA9:62

    A c= Z & (for x st x in Z holds x > 0 ) & ( dom ( ln * ( #Z n))) = Z & ( dom ( ln * ( #Z n))) = ( dom f2) & (for x st x in Z holds (f2 . x) = (n / x)) & (f2 | A) is continuous implies ( integral (f2,A)) = ((( ln * ( #Z n)) . ( upper_bound A)) - (( ln * ( #Z n)) . ( lower_bound A)))

    proof

      assume that

       A1: A c= Z and

       A2: for x st x in Z holds x > 0 and

       A3: ( dom ( ln * ( #Z n))) = Z and

       A4: ( dom ( ln * ( #Z n))) = ( dom f2) and

       A5: for x st x in Z holds (f2 . x) = (n / x) and

       A6: (f2 | A) is continuous;

      

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

      

       A8: ( ln * ( #Z n)) is_differentiable_on Z by A2, A3, FDIFF_6: 9;

      

       A9: for x be Element of REAL st x in ( dom (( ln * ( #Z n)) `| Z)) holds ((( ln * ( #Z n)) `| Z) . x) = (f2 . x)

      proof

        let x be Element of REAL ;

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

        then

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

        

        then ((( ln * ( #Z n)) `| Z) . x) = (n / x) by A2, A3, FDIFF_6: 9

        .= (f2 . x) by A5, A10;

        hence thesis;

      end;

      ( dom (( ln * ( #Z n)) `| Z)) = ( dom f2) by A3, A4, A8, FDIFF_1:def 7;

      then (( ln * ( #Z n)) `| Z) = f2 by A9, PARTFUN1: 5;

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

    end;

    theorem :: INTEGRA9:63

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

    proof

      set f = ( id Z);

      assume that

       A1: not 0 in Z and

       A2: A c= Z and

       A3: ( dom ( ln * (f ^ ))) = Z and

       A4: ( dom ( ln * (f ^ ))) = ( dom f2) and

       A5: for x st x in Z holds (f2 . x) = ( - (1 / x)) and

       A6: (f2 | A) is continuous;

      

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

      

       A8: ( ln * (f ^ )) is_differentiable_on Z by A1, A3, FDIFF_8: 5;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

        then ((( ln * (f ^ )) `| Z) . x) = ( - (1 / x)) by A1, A3, FDIFF_8: 5

        .= (f2 . x) by A5, A10;

        hence thesis;

      end;

      ( dom (( ln * (f ^ )) `| Z)) = ( dom f2) by A3, A4, A8, FDIFF_1:def 7;

      then (( ln * (f ^ )) `| Z) = f2 by A9, PARTFUN1: 5;

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

    end;

    theorem :: INTEGRA9:64

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

    proof

      assume that

       A1: A c= Z and

       A2: for x st x in Z holds (f . x) = (a + x) & (f . x) > 0 and

       A3: ( dom ((2 / 3) (#) (( #R (3 / 2)) * f))) = Z and

       A4: ( dom ((2 / 3) (#) (( #R (3 / 2)) * f))) = ( dom f2) and

       A5: for x st x in Z holds (f2 . x) = ((a + x) #R (1 / 2)) and

       A6: (f2 | A) is continuous;

      

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

      

       A8: ((2 / 3) (#) (( #R (3 / 2)) * f)) is_differentiable_on Z by A2, A3, FDIFF_4: 28;

      

       A9: for x be Element of REAL st x in ( dom (((2 / 3) (#) (( #R (3 / 2)) * f)) `| Z)) holds ((((2 / 3) (#) (( #R (3 / 2)) * f)) `| Z) . x) = (f2 . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom (((2 / 3) (#) (( #R (3 / 2)) * f)) `| Z));

        then

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

        

        then ((((2 / 3) (#) (( #R (3 / 2)) * f)) `| Z) . x) = ((a + x) #R (1 / 2)) by A2, A3, FDIFF_4: 28

        .= (f2 . x) by A5, A10;

        hence thesis;

      end;

      ( dom (((2 / 3) (#) (( #R (3 / 2)) * f)) `| Z)) = ( dom f2) by A3, A4, A8, FDIFF_1:def 7;

      then (((2 / 3) (#) (( #R (3 / 2)) * f)) `| Z) = f2 by A9, PARTFUN1: 5;

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

    end;

    theorem :: INTEGRA9:65

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

    proof

      assume that

       A1: A c= Z and

       A2: for x st x in Z holds (f . x) = (a - x) & (f . x) > 0 and

       A3: ( dom (( - (2 / 3)) (#) (( #R (3 / 2)) * f))) = Z and

       A4: ( dom (( - (2 / 3)) (#) (( #R (3 / 2)) * f))) = ( dom f2) and

       A5: for x st x in Z holds (f2 . x) = ((a - x) #R (1 / 2)) and

       A6: (f2 | A) is continuous;

      

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

      

       A8: (( - (2 / 3)) (#) (( #R (3 / 2)) * f)) is_differentiable_on Z by A2, A3, FDIFF_4: 29;

      

       A9: for x be Element of REAL st x in ( dom ((( - (2 / 3)) (#) (( #R (3 / 2)) * f)) `| Z)) holds (((( - (2 / 3)) (#) (( #R (3 / 2)) * f)) `| Z) . x) = (f2 . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom ((( - (2 / 3)) (#) (( #R (3 / 2)) * f)) `| Z));

        then

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

        

        then (((( - (2 / 3)) (#) (( #R (3 / 2)) * f)) `| Z) . x) = ((a - x) #R (1 / 2)) by A2, A3, FDIFF_4: 29

        .= (f2 . x) by A5, A10;

        hence thesis;

      end;

      ( dom ((( - (2 / 3)) (#) (( #R (3 / 2)) * f)) `| Z)) = ( dom f2) by A3, A4, A8, FDIFF_1:def 7;

      then ((( - (2 / 3)) (#) (( #R (3 / 2)) * f)) `| Z) = f2 by A9, PARTFUN1: 5;

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

    end;

    theorem :: INTEGRA9:66

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

    proof

      assume that

       A1: A c= Z and

       A2: for x st x in Z holds (f . x) = (a + x) & (f . x) > 0 and

       A3: ( dom (2 (#) (( #R (1 / 2)) * f))) = Z and

       A4: ( dom (2 (#) (( #R (1 / 2)) * f))) = ( dom f2) and

       A5: for x st x in Z holds (f2 . x) = ((a + x) #R ( - (1 / 2))) and

       A6: (f2 | A) is continuous;

      

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

      

       A8: (2 (#) (( #R (1 / 2)) * f)) is_differentiable_on Z by A2, A3, FDIFF_4: 30;

      

       A9: for x be Element of REAL st x in ( dom ((2 (#) (( #R (1 / 2)) * f)) `| Z)) holds (((2 (#) (( #R (1 / 2)) * f)) `| Z) . x) = (f2 . x)

      proof

        let x be Element of REAL ;

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

        then

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

        

        then (((2 (#) (( #R (1 / 2)) * f)) `| Z) . x) = ((a + x) #R ( - (1 / 2))) by A2, A3, FDIFF_4: 30

        .= (f2 . x) by A5, A10;

        hence thesis;

      end;

      ( dom ((2 (#) (( #R (1 / 2)) * f)) `| Z)) = ( dom f2) by A3, A4, A8, FDIFF_1:def 7;

      then ((2 (#) (( #R (1 / 2)) * f)) `| Z) = f2 by A9, PARTFUN1: 5;

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

    end;

    theorem :: INTEGRA9:67

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

    proof

      assume that

       A1: A c= Z and

       A2: for x st x in Z holds (f . x) = (a - x) & (f . x) > 0 and

       A3: ( dom (( - 2) (#) (( #R (1 / 2)) * f))) = Z and

       A4: ( dom (( - 2) (#) (( #R (1 / 2)) * f))) = ( dom f2) and

       A5: for x st x in Z holds (f2 . x) = ((a - x) #R ( - (1 / 2))) and

       A6: (f2 | A) is continuous;

      

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

      

       A8: (( - 2) (#) (( #R (1 / 2)) * f)) is_differentiable_on Z by A2, A3, FDIFF_4: 31;

      

       A9: for x be Element of REAL st x in ( dom ((( - 2) (#) (( #R (1 / 2)) * f)) `| Z)) holds (((( - 2) (#) (( #R (1 / 2)) * f)) `| Z) . x) = (f2 . x)

      proof

        let x be Element of REAL ;

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

        then

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

        

        then (((( - 2) (#) (( #R (1 / 2)) * f)) `| Z) . x) = ((a - x) #R ( - (1 / 2))) by A2, A3, FDIFF_4: 31

        .= (f2 . x) by A5, A10;

        hence thesis;

      end;

      ( dom ((( - 2) (#) (( #R (1 / 2)) * f)) `| Z)) = ( dom f2) by A3, A4, A8, FDIFF_1:def 7;

      then ((( - 2) (#) (( #R (1 / 2)) * f)) `| Z) = f2 by A9, PARTFUN1: 5;

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

    end;

    theorem :: INTEGRA9:68

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

    proof

      assume that

       A1: A c= Z and

       A2: ( dom ((( - ( id Z)) (#) cos ) + sin )) = Z and

       A3: for x st x in Z holds (f . x) = (x * ( sin . x)) and

       A4: Z = ( dom f) and

       A5: (f | A) is continuous;

      

       A6: ((( - ( id Z)) (#) cos ) + sin ) is_differentiable_on Z by A2, FDIFF_4: 46;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

        then ((((( - ( id Z)) (#) cos ) + sin ) `| Z) . x) = (x * ( sin . x)) by A2, FDIFF_4: 46

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

        hence thesis;

      end;

      ( dom (((( - ( id Z)) (#) cos ) + sin ) `| Z)) = ( dom f) by A4, A6, FDIFF_1:def 7;

      then

       A9: (((( - ( id Z)) (#) cos ) + 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, A9, FDIFF_4: 46, INTEGRA5: 13;

    end;

    theorem :: INTEGRA9:69

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

    proof

      assume that

       A1: A c= Z and

       A2: ( dom sec ) = Z and

       A3: for x st x in Z holds (f . x) = (( sin . x) / (( cos . x) ^2 )) and

       A4: Z = ( dom f) and

       A5: (f | A) is continuous;

      

       A6: sec is_differentiable_on Z by A2, FDIFF_9: 4;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

        then (( sec `| Z) . x) = (( sin . x) / (( cos . x) ^2 )) by A2, FDIFF_9: 4

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

        hence thesis;

      end;

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

      then

       A9: ( sec `| 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, FDIFF_9: 4, INTEGRA5: 13;

    end;

    theorem :: INTEGRA9:70

    

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

    proof

      

       A1: sin is_differentiable_on Z by FDIFF_1: 26, SIN_COS: 68;

      assume

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

      then

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

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

      then

       A4: cosec is_differentiable_on Z by A1, FDIFF_2: 22;

      

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

      proof

        let x;

        assume

         A6: x in Z;

        then

         A7: ( sin . x) <> 0 & sin is_differentiable_in x by A3, A1, FDIFF_1: 9, RFUNCT_1: 3;

        ((( - cosec ) `| Z) . x) = (( - 1) * ( diff (( sin ^ ),x))) by A2, A4, A6, FDIFF_1: 20

        .= (( - 1) * ( - (( diff ( sin ,x)) / (( sin . x) ^2 )))) by A7, FDIFF_2: 15

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

        hence thesis;

      end;

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

      hence thesis by A5;

    end;

    theorem :: INTEGRA9:71

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

    proof

      assume that

       A1: A c= Z and

       A2: ( dom ( - cosec )) = Z and

       A3: for x st x in Z holds (f . x) = (( cos . x) / (( sin . x) ^2 )) and

       A4: Z = ( dom f) and

       A5: (f | A) is continuous;

      

       A6: ( - cosec ) is_differentiable_on Z by A2, Th70;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

        then ((( - cosec ) `| Z) . x) = (( cos . x) / (( sin . x) ^2 )) by A2, Th70

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

        hence thesis;

      end;

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

      then

       A9: (( - cosec ) `| 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, Th70, INTEGRA5: 13;

    end;