integr12.miz



    begin

    reserve a,b,x,r for Real;

    reserve y for set;

    reserve n for Element of NAT ;

    reserve A for non empty closed_interval Subset of REAL ;

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

    reserve Z for open Subset of REAL ;

    theorem :: INTEGR12:1

    

     Th1: Z c= ( dom ((f1 + f2) ^ )) & (for x st x in Z holds (f1 . x) = 1) & f2 = ( #Z 2) implies ((f1 + f2) ^ ) is_differentiable_on Z & for x st x in Z holds ((((f1 + f2) ^ ) `| Z) . x) = ( - ((2 * x) / ((1 + (x |^ 2)) ^2 )))

    proof

      assume

       A1: Z c= ( dom ((f1 + f2) ^ )) & (for x st x in Z holds (f1 . x) = 1) & f2 = ( #Z 2);

      ( dom ((f1 + f2) ^ )) c= ( dom (f1 + f2)) by RFUNCT_1: 1;

      then

       A2: Z c= ( dom (f1 + f2)) by A1;

      then

       A3: (f1 + f2) is_differentiable_on Z & for x st x in Z holds (((f1 + f2) `| Z) . x) = (2 * x) by A1, SIN_COS9: 101;

      

       A4: for x st x in Z holds ((f1 + f2) . x) <> 0 by A1, RFUNCT_1: 3;

      then

       A5: ((f1 + f2) ^ ) is_differentiable_on Z by A3, FDIFF_2: 22;

      for x st x in Z holds ((((f1 + f2) ^ ) `| Z) . x) = ( - ((2 * x) / ((1 + (x |^ 2)) ^2 )))

      proof

        let x;

        assume

         A6: x in Z;

        then

         A7: ((f1 + f2) . x) <> 0 by A1, RFUNCT_1: 3;

        

         A8: (f1 + f2) is_differentiable_in x by A3, A6, FDIFF_1: 9;

        

         A9: (f2 . x) = (x #Z 2) by A1, TAYLOR_1:def 1

        .= (x |^ 2) by PREPOWER: 36;

        

         A10: ((f1 + f2) . x) = ((f1 . x) + (f2 . x)) by A2, A6, VALUED_1:def 1

        .= (1 + (x |^ 2)) by A1, A6, A9;

        ((((f1 + f2) ^ ) `| Z) . x) = ( diff (((f1 + f2) ^ ),x)) by A5, A6, FDIFF_1:def 7

        .= ( - (( diff ((f1 + f2),x)) / (((f1 + f2) . x) ^2 ))) by A7, A8, FDIFF_2: 15

        .= ( - ((((f1 + f2) `| Z) . x) / (((f1 + f2) . x) ^2 ))) by A3, A6, FDIFF_1:def 7

        .= ( - ((2 * x) / ((1 + (x |^ 2)) ^2 ))) by A1, A2, A6, A10, SIN_COS9: 101;

        hence thesis;

      end;

      hence thesis by A3, A4, FDIFF_2: 22;

    end;

    theorem :: INTEGR12:2

    A c= Z & f = (((g1 + g2) ^ ) / f2) & f2 = arccot & Z c= ].( - 1), 1.[ & g2 = ( #Z 2) & (for x st x in Z holds (g1 . x) = 1 & (f2 . x) > 0 ) & Z = ( dom f) implies ( integral (f,A)) = ((( - ( ln * arccot )) . ( upper_bound A)) - (( - ( ln * arccot )) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & f = (((g1 + g2) ^ ) / f2) & f2 = arccot & Z c= ].( - 1), 1.[ & g2 = ( #Z 2) & (for x st x in Z holds (g1 . x) = 1 & (f2 . x) > 0 ) & Z = ( dom f);

      then Z = (( dom ((g1 + g2) ^ )) /\ (( dom f2) \ (f2 " { 0 }))) by RFUNCT_1:def 1;

      then

       A2: Z c= ( dom ((g1 + g2) ^ )) & Z c= (( dom f2) \ (f2 " { 0 })) by XBOOLE_1: 18;

      ( dom ((g1 + g2) ^ )) c= ( dom (g1 + g2)) by RFUNCT_1: 1;

      then

       A3: Z c= ( dom (g1 + g2)) by A2;

      for x st x in Z holds (g1 . x) = 1 by A1;

      then

       A4: ((g1 + g2) ^ ) is_differentiable_on Z by A1, A2, Th1;

      

       A5: f2 is_differentiable_on Z by A1, SIN_COS9: 82;

      for x st x in Z holds (f2 . x) <> 0 by A1;

      then f is_differentiable_on Z by A1, A4, A5, FDIFF_2: 21;

      then (f | Z) is continuous by FDIFF_1: 25;

      then

       A6: (f | A) is continuous by A1, FCONT_1: 16;

      

       A7: Z c= ( dom (f2 ^ )) by A2, RFUNCT_1:def 2;

      ( dom (f2 ^ )) c= ( dom f2) by RFUNCT_1: 1;

      then

       A8: Z c= ( dom f2) by A7;

      

       A9: for x st x in Z holds (f2 . x) > 0 by A1;

      ( rng (f2 | Z)) c= ( right_open_halfline 0 )

      proof

        let x be object;

        assume x in ( rng (f2 | Z));

        then

        consider y be object such that

         A10: y in ( dom (f2 | Z)) & x = ((f2 | Z) . y) by FUNCT_1:def 3;

        y in Z by A10;

        then (f2 . y) > 0 by A1;

        then ((f2 | Z) . y) > 0 by A10, FUNCT_1: 47;

        hence thesis by A10, XXREAL_1: 235;

      end;

      then (f2 .: Z) c= ( dom ln ) by RELAT_1: 115, TAYLOR_1: 18;

      then

       A11: Z c= ( dom ( ln * arccot )) by A1, A8, FUNCT_1: 101;

      

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

      

       A13: ( ln * arccot ) is_differentiable_on Z by A1, A11, A9, SIN_COS9: 90;

      Z c= ( dom ( - ( ln * arccot ))) by A11, VALUED_1: 8;

      then

       A14: ( - ( ln * arccot )) is_differentiable_on Z by A13, FDIFF_1: 20;

      

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

      proof

        let x;

        assume

         A16: x in Z;

        then

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

         arccot is_differentiable_on Z by A1, SIN_COS9: 82;

        then

         A18: arccot is_differentiable_in x by A16, FDIFF_1: 9;

        

         A19: ( arccot . x) > 0 by A1, A16;

        

         A20: ( ln * arccot ) is_differentiable_in x by A13, A16, FDIFF_1: 9;

        ((( - ( ln * arccot )) `| Z) . x) = ( diff (( - ( ln * arccot )),x)) by A14, A16, FDIFF_1:def 7

        .= (( - 1) * ( diff (( ln * arccot ),x))) by A20, FDIFF_1: 15

        .= (( - 1) * (( diff ( arccot ,x)) / ( arccot . x))) by A18, A19, TAYLOR_1: 20

        .= (( - 1) * (( - (1 / (1 + (x ^2 )))) / ( arccot . x))) by A17, SIN_COS9: 76

        .= ((1 / (1 + (x ^2 ))) / ( arccot . x))

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

        hence thesis;

      end;

      

       A21: for x be Real st x in Z holds (f . x) = (1 / ((1 + (x ^2 )) * ( arccot . x)))

      proof

        let x be Real;

        assume

         A22: x in Z;

        

        then ((((g1 + g2) ^ ) / f2) . x) = ((((g1 + g2) ^ ) . x) / (f2 . x)) by A1, RFUNCT_1:def 1

        .= ((((g1 + g2) . x) " ) / (f2 . x)) by A2, A22, RFUNCT_1:def 2

        .= ((((g1 . x) + (g2 . x)) " ) / (f2 . x)) by A3, A22, VALUED_1:def 1

        .= (1 / (((g1 . x) + (g2 . x)) * (f2 . x))) by XCMPLX_1: 221

        .= (1 / ((1 + (( #Z 2) . x)) * (f2 . x))) by A1, A22

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

        .= (1 / ((1 + (x ^2 )) * ( arccot . x))) by A1, FDIFF_7: 1;

        hence thesis by A1;

      end;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

        then ((( - ( ln * arccot )) `| Z) . x) = (1 / ((1 + (x ^2 )) * ( arccot . x))) by A15

        .= (f . x) by A21, A24;

        hence thesis;

      end;

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

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

      hence thesis by A1, A12, A14, INTEGRA5: 13;

    end;

    theorem :: INTEGR12:3

    A c= Z & (for x st x in Z holds ( exp_R . x) < 1 & (f1 . x) = 1) & Z c= ( dom ( arctan * exp_R )) & Z = ( dom f) & f = ( exp_R / (f1 + ( exp_R ^2 ))) implies ( integral (f,A)) = ((( arctan * exp_R ) . ( upper_bound A)) - (( arctan * exp_R ) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & (for x st x in Z holds ( exp_R . x) < 1 & (f1 . x) = 1) & Z c= ( dom ( arctan * exp_R )) & Z = ( dom f) & f = ( exp_R / (f1 + ( exp_R ^2 )));

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

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

      then

       A2: Z c= ( dom ((f1 + ( exp_R ^2 )) ^ )) by RFUNCT_1:def 2;

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

      then

       A3: Z c= ( dom (f1 + ( exp_R ^2 ))) by A2;

      then

       A4: Z c= (( dom f1) /\ ( dom ( exp_R ^2 ))) by VALUED_1:def 1;

      then

       A5: Z c= ( dom f1) & Z c= ( dom ( exp_R ^2 )) by XBOOLE_1: 18;

      

       A6: Z c= ( dom ( exp_R (#) exp_R )) by A4, XBOOLE_1: 18;

      

       A7: exp_R is_differentiable_on Z by FDIFF_1: 26, TAYLOR_1: 16;

      then

       A8: ( exp_R (#) exp_R ) is_differentiable_on Z by A6, FDIFF_1: 21;

      for x st x in Z holds (f1 . x) = (( 0 * x) + 1) by A1;

      then f1 is_differentiable_on Z by A5, FDIFF_1: 23;

      then

       A9: (f1 + ( exp_R ^2 )) is_differentiable_on Z by A3, A8, FDIFF_1: 18;

      for x st x in Z holds ((f1 + ( exp_R ^2 )) . x) <> 0

      proof

        let x;

        assume x in Z;

        then x in (( dom exp_R ) /\ (( dom (f1 + ( exp_R ^2 ))) \ ((f1 + ( exp_R ^2 )) " { 0 }))) by A1, RFUNCT_1:def 1;

        then x in (( dom (f1 + ( exp_R ^2 ))) \ ((f1 + ( exp_R ^2 )) " { 0 })) by XBOOLE_0:def 4;

        then x in ( dom ((f1 + ( exp_R ^2 )) ^ )) by RFUNCT_1:def 2;

        hence thesis by RFUNCT_1: 3;

      end;

      then f is_differentiable_on Z by A1, A7, A9, FDIFF_2: 21;

      then (f | Z) is continuous by FDIFF_1: 25;

      then (f | A) is continuous by A1, FCONT_1: 16;

      then

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

      

       A11: for x st x in Z holds ( exp_R . x) < 1 by A1;

      then

       A12: ( arctan * exp_R ) is_differentiable_on Z by A1, SIN_COS9: 115;

      

       A13: for x st x in Z holds (f . x) = (( exp_R . x) / (1 + (( exp_R . x) ^2 )))

      proof

        let x;

        assume

         A14: x in Z;

        

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

        .= (( exp_R . x) * (((f1 . x) + (( exp_R ^2 ) . x)) " )) by A14, A3, VALUED_1:def 1

        .= (( exp_R . x) * (((f1 . x) + (( exp_R . x) ^2 )) " )) by VALUED_1: 11

        .= (( exp_R . x) / (1 + (( exp_R . x) ^2 ))) by A1, A14;

        hence thesis by A1;

      end;

      

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

      proof

        let x be Element of REAL ;

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

        then

         A16: x in Z by A12, FDIFF_1:def 7;

        

        then ((( arctan * exp_R ) `| Z) . x) = (( exp_R . x) / (1 + (( exp_R . x) ^2 ))) by A1, A11, SIN_COS9: 115

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

        hence thesis;

      end;

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

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

      hence thesis by A1, A10, A12, INTEGRA5: 13;

    end;

    theorem :: INTEGR12:4

    A c= Z & (for x st x in Z holds ( exp_R . x) < 1 & (f1 . x) = 1) & Z c= ( dom ( arccot * exp_R )) & Z = ( dom f) & f = (( - exp_R ) / (f1 + ( exp_R ^2 ))) implies ( integral (f,A)) = ((( arccot * exp_R ) . ( upper_bound A)) - (( arccot * exp_R ) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & (for x st x in Z holds ( exp_R . x) < 1 & (f1 . x) = 1) & Z c= ( dom ( arccot * exp_R )) & Z = ( dom f) & f = (( - exp_R ) / (f1 + ( exp_R ^2 )));

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

      then

       A2: Z c= ( dom ( - exp_R )) & Z c= (( dom (f1 + ( exp_R ^2 ))) \ ((f1 + ( exp_R ^2 )) " { 0 })) by XBOOLE_1: 18;

      then

       A3: Z c= ( dom ((f1 + ( exp_R ^2 )) ^ )) by RFUNCT_1:def 2;

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

      then

       A4: Z c= ( dom (f1 + ( exp_R ^2 ))) by A3;

      then

       A5: Z c= (( dom f1) /\ ( dom ( exp_R ^2 ))) by VALUED_1:def 1;

      then

       A6: Z c= ( dom f1) & Z c= ( dom ( exp_R ^2 )) by XBOOLE_1: 18;

      

       A7: Z c= ( dom ( exp_R (#) exp_R )) by A5, XBOOLE_1: 18;

      

       A8: exp_R is_differentiable_on Z by FDIFF_1: 26, TAYLOR_1: 16;

      then

       A9: (( - 1) (#) exp_R ) is_differentiable_on Z by A2, FDIFF_1: 20;

      

       A10: ( exp_R (#) exp_R ) is_differentiable_on Z by A7, A8, FDIFF_1: 21;

      for x st x in Z holds (f1 . x) = (( 0 * x) + 1) by A1;

      then f1 is_differentiable_on Z by A6, FDIFF_1: 23;

      then

       A11: (f1 + ( exp_R ^2 )) is_differentiable_on Z by A4, A10, FDIFF_1: 18;

      for x st x in Z holds ((f1 + ( exp_R ^2 )) . x) <> 0

      proof

        let x;

        assume x in Z;

        then x in (( dom ( - exp_R )) /\ (( dom (f1 + ( exp_R ^2 ))) \ ((f1 + ( exp_R ^2 )) " { 0 }))) by A1, RFUNCT_1:def 1;

        then x in (( dom (f1 + ( exp_R ^2 ))) \ ((f1 + ( exp_R ^2 )) " { 0 })) by XBOOLE_0:def 4;

        then x in ( dom ((f1 + ( exp_R ^2 )) ^ )) by RFUNCT_1:def 2;

        hence thesis by RFUNCT_1: 3;

      end;

      then f is_differentiable_on Z by A1, A9, A11, FDIFF_2: 21;

      then (f | Z) is continuous by FDIFF_1: 25;

      then (f | A) is continuous by A1, FCONT_1: 16;

      then

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

      

       A13: for x st x in Z holds ( exp_R . x) < 1 by A1;

      then

       A14: ( arccot * exp_R ) is_differentiable_on Z by A1, SIN_COS9: 116;

      

       A15: for x be Element of REAL st x in Z holds (f . x) = ( - (( exp_R . x) / (1 + (( exp_R . x) ^2 ))))

      proof

        let x be Element of REAL ;

        assume

         A16: x in Z;

        

        then ((( - exp_R ) / (f1 + ( exp_R ^2 ))) . x) = ((( - exp_R ) . x) * (((f1 + ( exp_R ^2 )) . x) " )) by A1, RFUNCT_1:def 1

        .= (( - ( exp_R . x)) * (((f1 + ( exp_R ^2 )) . x) " )) by RFUNCT_1: 58

        .= (( - ( exp_R . x)) * (((f1 . x) + (( exp_R ^2 ) . x)) " )) by A16, A4, VALUED_1:def 1

        .= (( - ( exp_R . x)) * (((f1 . x) + (( exp_R . x) ^2 )) " )) by VALUED_1: 11

        .= (( - ( exp_R . x)) / (1 + (( exp_R . x) ^2 ))) by A1, A16

        .= ( - (( exp_R . x) / (1 + (( exp_R . x) ^2 ))));

        hence thesis by A1;

      end;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

        then ((( arccot * exp_R ) `| Z) . x) = ( - (( exp_R . x) / (1 + (( exp_R . x) ^2 )))) by A1, A13, SIN_COS9: 116

        .= (f . x) by A18, A15;

        hence thesis;

      end;

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

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

      hence thesis by A1, A12, A14, INTEGRA5: 13;

    end;

    theorem :: INTEGR12:5

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

    proof

      assume

       A1: A c= Z & Z = ( dom f) & f = (( exp_R (#) ( sin / cos )) + ( exp_R / ( cos ^2 )));

      then Z = (( dom ( exp_R (#) ( sin / cos ))) /\ ( dom ( exp_R / ( cos ^2 )))) by VALUED_1:def 1;

      then

       A2: Z c= ( dom ( exp_R (#) ( sin / cos ))) & Z c= ( dom ( exp_R / ( cos ^2 ))) by XBOOLE_1: 18;

      

       A3: ( dom ( exp_R (#) ( sin / cos ))) c= (( dom exp_R ) /\ ( dom ( sin / cos ))) by VALUED_1:def 4;

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

      then ( dom ( exp_R (#) ( sin / cos ))) c= ( dom exp_R ) & ( dom ( exp_R (#) ( sin / cos ))) c= ( dom ( sin / cos )) & ( dom ( exp_R / ( cos ^2 ))) c= (( dom ( cos ^2 )) \ (( cos ^2 ) " { 0 })) by A3, XBOOLE_1: 18;

      then

       A4: Z c= ( dom exp_R ) & Z c= ( dom ( sin / cos )) & Z c= (( dom ( cos ^2 )) \ (( cos ^2 ) " { 0 })) by A2;

      

       A5: exp_R is_differentiable_on Z by FDIFF_1: 26, TAYLOR_1: 16;

      for x st x in Z holds ( sin / cos ) is_differentiable_in x

      proof

        let x;

        assume x in Z;

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

        hence thesis by FDIFF_7: 46;

      end;

      then ( sin / cos ) is_differentiable_on Z by A4, FDIFF_1: 9;

      then

       A6: ( exp_R (#) ( sin / cos )) is_differentiable_on Z by A2, A5, FDIFF_1: 21;

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

      then

       A7: ( cos ^2 ) is_differentiable_on Z by FDIFF_2: 20;

      x in Z implies (( cos ^2 ) . x) <> 0

      proof

        assume x in Z;

        then x in ( dom ( exp_R / ( cos ^2 ))) by A2;

        then x in (( dom exp_R ) /\ (( dom ( cos ^2 )) \ (( cos ^2 ) " { 0 }))) by RFUNCT_1:def 1;

        then x in (( dom ( cos ^2 )) \ (( cos ^2 ) " { 0 })) by XBOOLE_0:def 4;

        then x in ( dom (( cos ^2 ) ^ )) by RFUNCT_1:def 2;

        hence thesis by RFUNCT_1: 3;

      end;

      then ( exp_R / ( cos ^2 )) is_differentiable_on Z by A5, A7, FDIFF_2: 21;

      then (f | Z) is continuous by A1, A6, FDIFF_1: 18, FDIFF_1: 25;

      then (f | A) is continuous by A1, FCONT_1: 16;

      then

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

      

       A9: ( exp_R (#) tan ) is_differentiable_on Z by A2, FDIFF_8: 30;

      

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

      proof

        let x;

        assume

         A11: x in Z;

        

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

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

        .= ((( exp_R . x) * (( sin . x) * (( cos . x) " ))) + (( exp_R / ( cos ^2 )) . x)) by A4, A11, RFUNCT_1:def 1

        .= (((( exp_R . x) * ( sin . x)) / ( cos . x)) + (( exp_R . x) / (( cos ^2 ) . x))) by A2, A11, RFUNCT_1:def 1

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

        hence thesis by A1;

      end;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

        then ((( exp_R (#) tan ) `| Z) . x) = (((( exp_R . x) * ( sin . x)) / ( cos . x)) + (( exp_R . x) / (( cos . x) ^2 ))) by A2, FDIFF_8: 30

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

        hence thesis;

      end;

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

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

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

    end;

    theorem :: INTEGR12:6

    A c= Z & Z = ( dom f) & f = (( exp_R (#) ( cos / sin )) - ( exp_R / ( sin ^2 ))) implies ( integral (f,A)) = ((( exp_R (#) cot ) . ( upper_bound A)) - (( exp_R (#) cot ) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & Z = ( dom f) & f = (( exp_R (#) ( cos / sin )) - ( exp_R / ( sin ^2 )));

      then Z = (( dom ( exp_R (#) ( cos / sin ))) /\ ( dom ( exp_R / ( sin ^2 )))) by VALUED_1: 12;

      then

       A2: Z c= ( dom ( exp_R (#) ( cos / sin ))) & Z c= ( dom ( exp_R / ( sin ^2 ))) by XBOOLE_1: 18;

      

       A3: ( dom ( exp_R (#) ( cos / sin ))) c= (( dom exp_R ) /\ ( dom ( cos / sin ))) by VALUED_1:def 4;

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

      then ( dom ( exp_R (#) ( cos / sin ))) c= ( dom exp_R ) & ( dom ( exp_R (#) ( cos / sin ))) c= ( dom ( cos / sin )) & ( dom ( exp_R / ( sin ^2 ))) c= (( dom ( sin ^2 )) \ (( sin ^2 ) " { 0 })) by A3, XBOOLE_1: 18;

      then

       A4: Z c= ( dom exp_R ) & Z c= ( dom ( cos / sin )) & Z c= (( dom ( sin ^2 )) \ (( sin ^2 ) " { 0 })) by A2;

      

       A5: exp_R is_differentiable_on Z by FDIFF_1: 26, TAYLOR_1: 16;

      for x st x in Z holds ( cos / sin ) is_differentiable_in x

      proof

        let x;

        assume x in Z;

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

        hence thesis by FDIFF_7: 47;

      end;

      then ( cos / sin ) is_differentiable_on Z by A4, FDIFF_1: 9;

      then

       A6: ( exp_R (#) ( cos / sin )) is_differentiable_on Z by A2, A5, FDIFF_1: 21;

       sin is_differentiable_on Z by FDIFF_1: 26, SIN_COS: 68;

      then

       A7: ( sin ^2 ) is_differentiable_on Z by FDIFF_2: 20;

      x in Z implies (( sin ^2 ) . x) <> 0

      proof

        assume x in Z;

        then x in ( dom ( exp_R / ( sin ^2 ))) by A2;

        then x in (( dom exp_R ) /\ (( dom ( sin ^2 )) \ (( sin ^2 ) " { 0 }))) by RFUNCT_1:def 1;

        then x in (( dom ( sin ^2 )) \ (( sin ^2 ) " { 0 })) by XBOOLE_0:def 4;

        then x in ( dom (( sin ^2 ) ^ )) by RFUNCT_1:def 2;

        hence thesis by RFUNCT_1: 3;

      end;

      then ( exp_R / ( sin ^2 )) is_differentiable_on Z by A5, A7, FDIFF_2: 21;

      then (f | Z) is continuous by A1, A6, FDIFF_1: 19, FDIFF_1: 25;

      then (f | A) is continuous by A1, FCONT_1: 16;

      then

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

      

       A9: ( exp_R (#) cot ) is_differentiable_on Z by A2, FDIFF_8: 31;

      

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

      proof

        let x;

        assume

         A11: x in Z;

        

        then ((( exp_R (#) ( cos / sin )) - ( exp_R / ( sin ^2 ))) . x) = ((( exp_R (#) ( cos / sin )) . x) - (( exp_R / ( sin ^2 )) . x)) by A1, VALUED_1: 13

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

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

        .= (((( exp_R . x) * ( cos . x)) / ( sin . x)) - (( exp_R . x) / (( sin ^2 ) . x))) by A2, A11, RFUNCT_1:def 1

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

        hence thesis by A1;

      end;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

        then ((( exp_R (#) cot ) `| Z) . x) = (((( exp_R . x) * ( cos . x)) / ( sin . x)) - (( exp_R . x) / (( sin . x) ^2 ))) by A2, FDIFF_8: 31

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

        hence thesis;

      end;

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

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

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

    end;

    theorem :: INTEGR12:7

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

    proof

      assume

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

      then

       A2: Z = (( dom ( exp_R (#) arctan )) /\ ( dom ( exp_R / (f1 + ( #Z 2))))) by VALUED_1:def 1;

      

       A3: exp_R is_differentiable_on Z by FDIFF_1: 26, TAYLOR_1: 16;

      

       A4: ( exp_R (#) arctan ) is_differentiable_on Z by A1, SIN_COS9: 123;

      

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

      then

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

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

      then

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

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

      then

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

      ((f1 + ( #Z 2)) ^ ) is_differentiable_on Z by A1, A7, Th1;

      then ( exp_R (#) ((f1 + ( #Z 2)) ^ )) is_differentiable_on Z by A3, A6, FDIFF_1: 21;

      then ( exp_R / (f1 + ( #Z 2))) is_differentiable_on Z by RFUNCT_1: 31;

      then (f | Z) is continuous by A1, A4, FDIFF_1: 18, FDIFF_1: 25;

      then (f | A) is continuous by A1, FCONT_1: 16;

      then

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

      

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

      proof

        let x;

        assume

         A11: x in Z;

        

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

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

        .= ((( exp_R . x) * ( arctan . x)) + (( exp_R . x) / ((f1 + ( #Z 2)) . x))) by A5, A11, RFUNCT_1:def 1

        .= ((( exp_R . x) * ( arctan . x)) + (( exp_R . x) / ((f1 . x) + (( #Z 2) . x)))) by A8, A11, VALUED_1:def 1

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

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

        .= ((( exp_R . x) * ( arctan . x)) + (( exp_R . x) / (1 + (x ^2 )))) by A1, A11;

        hence thesis by A1;

      end;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

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

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

        hence thesis;

      end;

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

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

      hence thesis by A1, A9, INTEGRA5: 13, SIN_COS9: 123;

    end;

    theorem :: INTEGR12:8

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

    proof

      assume

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

      then

       A2: Z = (( dom ( exp_R (#) arccot )) /\ ( dom ( exp_R / (f1 + ( #Z 2))))) by VALUED_1: 12;

      

       A3: exp_R is_differentiable_on Z by FDIFF_1: 26, TAYLOR_1: 16;

      

       A4: ( exp_R (#) arccot ) is_differentiable_on Z by A1, SIN_COS9: 124;

      

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

      then

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

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

      then

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

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

      then

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

      ((f1 + ( #Z 2)) ^ ) is_differentiable_on Z by A1, A7, Th1;

      then ( exp_R (#) ((f1 + ( #Z 2)) ^ )) is_differentiable_on Z by A3, A6, FDIFF_1: 21;

      then ( exp_R / (f1 + ( #Z 2))) is_differentiable_on Z by RFUNCT_1: 31;

      then (f | Z) is continuous by A1, A4, FDIFF_1: 19, FDIFF_1: 25;

      then (f | A) is continuous by A1, FCONT_1: 16;

      then

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

      

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

      proof

        let x;

        assume

         A11: x in Z;

        

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

        .= ((( exp_R . x) * ( arccot . x)) - (( exp_R / (f1 + ( #Z 2))) . x)) by VALUED_1: 5

        .= ((( exp_R . x) * ( arccot . x)) - (( exp_R . x) / ((f1 + ( #Z 2)) . x))) by A5, A11, RFUNCT_1:def 1

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

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

        .= ((( exp_R . x) * ( arccot . x)) - (( exp_R . x) / ((f1 . x) + (x ^2 )))) by FDIFF_7: 1

        .= ((( exp_R . x) * ( arccot . x)) - (( exp_R . x) / (1 + (x ^2 )))) by A1, A11;

        hence thesis by A1;

      end;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

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

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

        hence thesis;

      end;

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

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

      hence thesis by A1, A9, INTEGRA5: 13, SIN_COS9: 124;

    end;

    theorem :: INTEGR12:9

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

    proof

      assume

       A1: A c= Z & Z = ( dom f) & f = (( exp_R * sin ) (#) cos );

      then Z = (( dom ( exp_R * sin )) /\ ( dom cos )) by VALUED_1:def 4;

      then

       A2: Z c= ( dom ( exp_R * sin )) by XBOOLE_1: 18;

      then

       A3: ( exp_R * sin ) is_differentiable_on Z by FDIFF_7: 37;

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

      then (f | Z) is continuous by A1, A3, FDIFF_1: 21, FDIFF_1: 25;

      then (f | A) is continuous by A1, FCONT_1: 16;

      then

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

      

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

      proof

        let x;

        assume

         A6: x in Z;

        

        then ((( exp_R * sin ) (#) cos ) . x) = ((( exp_R * sin ) . x) * ( cos . x)) by A1, VALUED_1:def 4

        .= (( exp_R . ( sin . x)) * ( cos . x)) by A2, A6, FUNCT_1: 12;

        hence thesis by A1;

      end;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

        then ((( exp_R * sin ) `| Z) . x) = (( exp_R . ( sin . x)) * ( cos . x)) by A2, FDIFF_7: 37

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

        hence thesis;

      end;

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

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

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

    end;

    theorem :: INTEGR12:10

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

    proof

      assume

       A1: A c= Z & Z = ( dom f) & f = (( exp_R * cos ) (#) sin );

      then Z = (( dom ( exp_R * cos )) /\ ( dom sin )) by VALUED_1:def 4;

      then

       A2: Z c= ( dom ( exp_R * cos )) by XBOOLE_1: 18;

      then

       A3: ( exp_R * cos ) is_differentiable_on Z by FDIFF_7: 36;

       sin is_differentiable_on Z by FDIFF_1: 26, SIN_COS: 68;

      then (f | Z) is continuous by A1, A3, FDIFF_1: 21, FDIFF_1: 25;

      then (f | A) is continuous by A1, FCONT_1: 16;

      then

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

      

       A5: Z c= ( dom ( - ( exp_R * cos ))) by A2, VALUED_1: 8;

      then

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

      

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

      proof

        let x;

        assume

         A8: x in Z;

        

         A9: cos is_differentiable_in x by SIN_COS: 63;

        

         A10: exp_R is_differentiable_in ( cos . x) by SIN_COS: 65;

        

         A11: ( exp_R * cos ) is_differentiable_in x by A3, A8, FDIFF_1: 9;

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

        .= (( - 1) * ( diff (( exp_R * cos ),x))) by A11, FDIFF_1: 15

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

        .= (( - 1) * (( diff ( exp_R ,( cos . x))) * ( - ( sin . x)))) by SIN_COS: 63

        .= (( - 1) * (( exp_R . ( cos . x)) * ( - ( sin . x)))) by SIN_COS: 65

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

        hence thesis;

      end;

      

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

      proof

        let x;

        assume

         A13: x in Z;

        

        then ((( exp_R * cos ) (#) sin ) . x) = ((( exp_R * cos ) . x) * ( sin . x)) by A1, VALUED_1:def 4

        .= (( exp_R . ( cos . x)) * ( sin . x)) by A2, A13, FUNCT_1: 12;

        hence thesis by A1;

      end;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

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

        .= (f . x) by A15, A12;

        hence thesis;

      end;

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

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

      hence thesis by A1, A4, A3, A5, FDIFF_1: 20, INTEGRA5: 13;

    end;

    theorem :: INTEGR12:11

    A c= Z & (for x st x in Z holds x > 0 ) & Z = ( dom f) & f = (( cos * ln ) (#) (( id Z) ^ )) implies ( integral (f,A)) = ((( sin * ln ) . ( upper_bound A)) - (( sin * ln ) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & (for x st x in Z holds x > 0 ) & Z = ( dom f) & f = (( cos * ln ) (#) (( id Z) ^ ));

      then

       A2: Z = ( dom (( cos * ln ) / ( id Z))) by RFUNCT_1: 31;

      Z = (( dom ( cos * ln )) /\ ( dom (( id Z) ^ ))) by A1, VALUED_1:def 4;

      then

       A3: Z c= ( dom ( cos * ln )) by XBOOLE_1: 18;

      for y be object st y in Z holds y in ( dom ( sin * ln ))

      proof

        let y be object;

        assume y in Z;

        then y in ( dom ln ) & ( ln . y) in ( dom sin ) by A3, FUNCT_1: 11, SIN_COS: 24;

        hence thesis by FUNCT_1: 11;

      end;

      then

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

      

       A5: ( cos * ln ) is_differentiable_on Z by A3, A1, FDIFF_7: 33;

       not 0 in Z by A1;

      then (( id Z) ^ ) is_differentiable_on Z by FDIFF_5: 4;

      then (f | Z) is continuous by A1, A5, FDIFF_1: 21, FDIFF_1: 25;

      then (f | A) is continuous by A1, FCONT_1: 16;

      then

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

      

       A7: ( sin * ln ) is_differentiable_on Z by A4, A1, FDIFF_7: 32;

      

       A8: for x st x in Z holds (f . x) = (( cos . ( ln . x)) / x)

      proof

        let x;

        assume

         A9: x in Z;

        ((( cos * ln ) (#) (( id Z) ^ )) . x) = ((( cos * ln ) / ( id Z)) . x) by RFUNCT_1: 31

        .= ((( cos * ln ) . x) * ((( id Z) . x) " )) by A2, A9, RFUNCT_1:def 1

        .= ((( cos * ln ) . x) / x) by A9, FUNCT_1: 18

        .= (( cos . ( ln . x)) / x) by A3, A9, FUNCT_1: 12;

        hence thesis by A1;

      end;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

        then ((( sin * ln ) `| Z) . x) = (( cos . ( ln . x)) / x) by A4, A1, FDIFF_7: 32

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

        hence thesis;

      end;

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

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

      hence thesis by A6, A4, A1, FDIFF_7: 32, INTEGRA5: 13;

    end;

    

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

    theorem :: INTEGR12:12

    A c= Z & (for x st x in Z holds x > 0 ) & Z = ( dom f) & f = (( sin * ln ) (#) (( id Z) ^ )) implies ( integral (f,A)) = ((( - ( cos * ln )) . ( upper_bound A)) - (( - ( cos * ln )) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & (for x st x in Z holds x > 0 ) & Z = ( dom f) & f = (( sin * ln ) (#) (( id Z) ^ ));

      then

       A2: Z = ( dom (( sin * ln ) / ( id Z))) by RFUNCT_1: 31;

      Z = (( dom ( sin * ln )) /\ ( dom (( id Z) ^ ))) by A1, VALUED_1:def 4;

      then

       A3: Z c= ( dom ( sin * ln )) by XBOOLE_1: 18;

      for y be object st y in Z holds y in ( dom ( cos * ln ))

      proof

        let y be object;

        assume y in Z;

        then y in ( dom ln ) & ( ln . y) in ( dom cos ) by A3, FUNCT_1: 11, SIN_COS: 24;

        hence thesis by FUNCT_1: 11;

      end;

      then

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

      

       A5: ( sin * ln ) is_differentiable_on Z by A3, A1, FDIFF_7: 32;

       not 0 in Z by A1;

      then (( id Z) ^ ) is_differentiable_on Z by FDIFF_5: 4;

      then (f | Z) is continuous by A1, A5, FDIFF_1: 21, FDIFF_1: 25;

      then (f | A) is continuous by A1, FCONT_1: 16;

      then

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

      

       A7: ( cos * ln ) is_differentiable_on Z by A4, A1, FDIFF_7: 33;

      

       A8: Z c= ( dom ( - ( cos * ln ))) by A4, VALUED_1: 8;

      then

       A9: (( - 1) (#) ( cos * ln )) is_differentiable_on Z by A7, FDIFF_1: 20;

      

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

      proof

        let x;

        assume

         A11: x in Z;

        then x > 0 by A1;

        then

         A12: x in ( right_open_halfline 0 ) by Lm1;

        

         A13: ln is_differentiable_in x by A11, A1, TAYLOR_1: 18;

        

         A14: cos is_differentiable_in ( ln . x) by SIN_COS: 63;

        

         A15: ( cos * ln ) is_differentiable_in x by A7, A11, FDIFF_1: 9;

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

        .= (( - 1) * ( diff (( cos * ln ),x))) by A15, FDIFF_1: 15

        .= (( - 1) * (( diff ( cos ,( ln . x))) * ( diff ( ln ,x)))) by A13, A14, FDIFF_2: 13

        .= (( - 1) * (( - ( sin . ( ln . x))) * ( diff ( ln ,x)))) by SIN_COS: 63

        .= (( - 1) * (( - ( sin . ( ln . x))) * (1 / x))) by A12, TAYLOR_1: 18

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

        hence thesis;

      end;

      

       A16: for x st x in Z holds (f . x) = (( sin . ( ln . x)) / x)

      proof

        let x;

        assume

         A17: x in Z;

        ((( sin * ln ) (#) (( id Z) ^ )) . x) = ((( sin * ln ) / ( id Z)) . x) by RFUNCT_1: 31

        .= ((( sin * ln ) . x) * ((( id Z) . x) " )) by A2, A17, RFUNCT_1:def 1

        .= ((( sin * ln ) . x) / x) by A17, FUNCT_1: 18

        .= (( sin . ( ln . x)) / x) by A3, A17, FUNCT_1: 12;

        hence thesis by A1;

      end;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

        then ((( - ( cos * ln )) `| Z) . x) = (( sin . ( ln . x)) / x) by A10

        .= (f . x) by A19, A16;

        hence thesis;

      end;

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

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

      hence thesis by A1, A6, A7, A8, FDIFF_1: 20, INTEGRA5: 13;

    end;

    theorem :: INTEGR12:13

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

    proof

      assume

       A1: A c= Z & Z = ( dom f) & f = ( exp_R (#) ( cos * exp_R ));

      then Z = (( dom exp_R ) /\ ( dom ( cos * exp_R ))) by VALUED_1:def 4;

      then

       A2: Z c= ( dom exp_R ) & Z c= ( dom ( cos * exp_R )) by XBOOLE_1: 18;

      for y be object st y in Z holds y in ( dom ( sin * exp_R ))

      proof

        let y be object;

        assume y in Z;

        then y in ( dom exp_R ) & ( exp_R . y) in ( dom sin ) by A2, SIN_COS: 24, XREAL_0:def 1;

        hence thesis by FUNCT_1: 11;

      end;

      then

       A3: Z c= ( dom ( sin * exp_R ));

      

       A4: ( cos * exp_R ) is_differentiable_on Z by A2, FDIFF_7: 35;

       exp_R is_differentiable_on Z by FDIFF_1: 26, TAYLOR_1: 16;

      then (f | Z) is continuous by A1, A4, FDIFF_1: 21, FDIFF_1: 25;

      then (f | A) is continuous by A1, FCONT_1: 16;

      then

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

      

       A6: ( sin * exp_R ) is_differentiable_on Z by A3, FDIFF_7: 34;

      

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

      proof

        let x;

        assume

         A8: x in Z;

        

        then (( exp_R (#) ( cos * exp_R )) . x) = (( exp_R . x) * (( cos * exp_R ) . x)) by A1, VALUED_1:def 4

        .= (( exp_R . x) * ( cos . ( exp_R . x))) by A2, A8, FUNCT_1: 12;

        hence thesis by A1;

      end;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

        then ((( sin * exp_R ) `| Z) . x) = (( exp_R . x) * ( cos . ( exp_R . x))) by A3, FDIFF_7: 34

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

        hence thesis;

      end;

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

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

      hence thesis by A1, A5, A3, FDIFF_7: 34, INTEGRA5: 13;

    end;

    theorem :: INTEGR12:14

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

    proof

      assume

       A1: A c= Z & Z = ( dom f) & f = ( exp_R (#) ( sin * exp_R ));

      then Z = (( dom exp_R ) /\ ( dom ( sin * exp_R ))) by VALUED_1:def 4;

      then

       A2: Z c= ( dom exp_R ) & Z c= ( dom ( sin * exp_R )) by XBOOLE_1: 18;

      for y be object st y in Z holds y in ( dom ( cos * exp_R ))

      proof

        let y be object;

        assume y in Z;

        then y in ( dom exp_R ) & ( exp_R . y) in ( dom cos ) by A2, SIN_COS: 24, XREAL_0:def 1;

        hence thesis by FUNCT_1: 11;

      end;

      then

       A3: Z c= ( dom ( cos * exp_R ));

      

       A4: ( sin * exp_R ) is_differentiable_on Z by A2, FDIFF_7: 34;

       exp_R is_differentiable_on Z by FDIFF_1: 26, TAYLOR_1: 16;

      then (f | Z) is continuous by A1, A4, FDIFF_1: 21, FDIFF_1: 25;

      then (f | A) is continuous by A1, FCONT_1: 16;

      then

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

      

       A6: ( cos * exp_R ) is_differentiable_on Z by A3, FDIFF_7: 35;

      

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

      then

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

      

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

      proof

        let x;

        assume

         A10: x in Z;

        

         A11: exp_R is_differentiable_in x by SIN_COS: 65;

        

         A12: cos is_differentiable_in ( exp_R . x) by SIN_COS: 63;

        

         A13: ( cos * exp_R ) is_differentiable_in x by A6, A10, FDIFF_1: 9;

        ((( - ( cos * exp_R )) `| Z) . x) = ( diff (( - ( cos * exp_R )),x)) by A8, A10, FDIFF_1:def 7

        .= (( - 1) * ( diff (( cos * exp_R ),x))) by A13, FDIFF_1: 15

        .= (( - 1) * (( diff ( cos ,( exp_R . x))) * ( diff ( exp_R ,x)))) by A11, A12, FDIFF_2: 13

        .= (( - 1) * (( - ( sin . ( exp_R . x))) * ( diff ( exp_R ,x)))) by SIN_COS: 63

        .= (( - 1) * (( - ( sin . ( exp_R . x))) * ( exp_R . x))) by SIN_COS: 65

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

        hence thesis;

      end;

      

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

      proof

        let x;

        assume

         A15: x in Z;

        

        then (( exp_R (#) ( sin * exp_R )) . x) = (( exp_R . x) * (( sin * exp_R ) . x)) by A1, VALUED_1:def 4

        .= (( exp_R . x) * ( sin . ( exp_R . x))) by A2, A15, FUNCT_1: 12;

        hence thesis by A1;

      end;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

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

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

        hence thesis;

      end;

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

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

      hence thesis by A1, A5, A6, A7, FDIFF_1: 20, INTEGRA5: 13;

    end;

    theorem :: INTEGR12:15

    A c= Z & Z c= ( dom ( ln * (f1 + f2))) & r <> 0 & (for x st x in Z holds (g . x) = (x / r) & (g . x) > ( - 1) & (g . x) < 1 & (f1 . x) = 1) & f2 = (( #Z 2) * g) & Z = ( dom f) & f = ( arctan * g) implies ( integral (f,A)) = ((((( id Z) (#) ( arctan * g)) - ((r / 2) (#) ( ln * (f1 + f2)))) . ( upper_bound A)) - (((( id Z) (#) ( arctan * g)) - ((r / 2) (#) ( ln * (f1 + f2)))) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & Z c= ( dom ( ln * (f1 + f2))) & r <> 0 & (for x st x in Z holds (g . x) = (x / r) & (g . x) > ( - 1) & (g . x) < 1 & (f1 . x) = 1) & f2 = (( #Z 2) * g) & Z = ( dom f) & f = ( arctan * g);

      Z c= (( dom ( id Z)) /\ ( dom f)) by A1;

      then

       A2: Z c= ( dom (( id Z) (#) ( arctan * g))) by A1, VALUED_1:def 4;

      Z c= ( dom ((r / 2) (#) ( ln * (f1 + f2)))) by A1, VALUED_1:def 5;

      then Z c= (( dom (( id Z) (#) ( arctan * g))) /\ ( dom ((r / 2) (#) ( ln * (f1 + f2))))) by A2, XBOOLE_1: 19;

      then

       A3: Z c= ( dom ((( id Z) (#) ( arctan * g)) - ((r / 2) (#) ( ln * (f1 + f2))))) by VALUED_1: 12;

      for x st x in Z holds (g . x) = (((1 / r) * x) + 0 )

      proof

        let x;

        assume x in Z;

        then (g . x) = (x / r) by A1;

        hence thesis;

      end;

      then for x st x in Z holds (g . x) = (((1 / r) * x) + 0 ) & (g . x) > ( - 1) & (g . x) < 1 by A1;

      then f is_differentiable_on Z by A1, SIN_COS9: 87;

      then (f | Z) is continuous by FDIFF_1: 25;

      then (f | A) is continuous by A1, FCONT_1: 16;

      then

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

      

       A5: (for x st x in Z holds (g . x) = (x / r) & (g . x) > ( - 1) & (g . x) < 1) & (for x st x in Z holds (f1 . x) = 1) & (for x st x in Z holds (g . x) = (x / r)) by A1;

      then

       A6: ((( id Z) (#) ( arctan * g)) - ((r / 2) (#) ( ln * (f1 + f2)))) is_differentiable_on Z by A1, A3, SIN_COS9: 109;

      

       A7: for x st x in Z holds (f . x) = ( arctan . (x / r))

      proof

        let x;

        assume

         A8: x in Z;

        

        then (( arctan * g) . x) = ( arctan . (g . x)) by A1, FUNCT_1: 12

        .= ( arctan . (x / r)) by A1, A8;

        hence thesis by A1;

      end;

      

       A9: for x be Element of REAL st x in ( dom (((( id Z) (#) ( arctan * g)) - ((r / 2) (#) ( ln * (f1 + f2)))) `| Z)) holds ((((( id Z) (#) ( arctan * g)) - ((r / 2) (#) ( ln * (f1 + f2)))) `| Z) . x) = (f . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom (((( id Z) (#) ( arctan * g)) - ((r / 2) (#) ( ln * (f1 + f2)))) `| Z));

        then

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

        

        then ((((( id Z) (#) ( arctan * g)) - ((r / 2) (#) ( ln * (f1 + f2)))) `| Z) . x) = ( arctan . (x / r)) by A1, A3, A5, SIN_COS9: 109

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

        hence thesis;

      end;

      ( dom (((( id Z) (#) ( arctan * g)) - ((r / 2) (#) ( ln * (f1 + f2)))) `| Z)) = ( dom f) by A1, A6, FDIFF_1:def 7;

      then (((( id Z) (#) ( arctan * g)) - ((r / 2) (#) ( ln * (f1 + f2)))) `| Z) = f by A9, PARTFUN1: 5;

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

    end;

    theorem :: INTEGR12:16

    A c= Z & Z c= ( dom ( ln * (f1 + f2))) & r <> 0 & (for x st x in Z holds (g . x) = (x / r) & (g . x) > ( - 1) & (g . x) < 1 & (f1 . x) = 1) & f2 = (( #Z 2) * g) & Z = ( dom f) & f = ( arccot * g) implies ( integral (f,A)) = ((((( id Z) (#) ( arccot * g)) + ((r / 2) (#) ( ln * (f1 + f2)))) . ( upper_bound A)) - (((( id Z) (#) ( arccot * g)) + ((r / 2) (#) ( ln * (f1 + f2)))) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & Z c= ( dom ( ln * (f1 + f2))) & r <> 0 & (for x st x in Z holds (g . x) = (x / r) & (g . x) > ( - 1) & (g . x) < 1 & (f1 . x) = 1) & f2 = (( #Z 2) * g) & Z = ( dom f) & f = ( arccot * g);

      Z c= (( dom ( id Z)) /\ ( dom f)) by A1;

      then

       A2: Z c= ( dom (( id Z) (#) ( arccot * g))) by A1, VALUED_1:def 4;

      Z c= ( dom ((r / 2) (#) ( ln * (f1 + f2)))) by A1, VALUED_1:def 5;

      then Z c= (( dom (( id Z) (#) ( arccot * g))) /\ ( dom ((r / 2) (#) ( ln * (f1 + f2))))) by A2, XBOOLE_1: 19;

      then

       A3: Z c= ( dom ((( id Z) (#) ( arccot * g)) + ((r / 2) (#) ( ln * (f1 + f2))))) by VALUED_1:def 1;

      

       A4: for x st x in Z holds (g . x) = (x / r) & (g . x) > ( - 1) & (g . x) < 1 by A1;

      for x st x in Z holds (g . x) = (((1 / r) * x) + 0 )

      proof

        let x;

        assume x in Z;

        then (g . x) = (x / r) by A1;

        hence thesis;

      end;

      then for x st x in Z holds (g . x) = (((1 / r) * x) + 0 ) & (g . x) > ( - 1) & (g . x) < 1 by A1;

      then f is_differentiable_on Z by A1, SIN_COS9: 88;

      then (f | Z) is continuous by FDIFF_1: 25;

      then (f | A) is continuous by A1, FCONT_1: 16;

      then

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

      

       A6: (for x st x in Z holds (f1 . x) = 1) & (for x st x in Z holds (g . x) = (x / r)) by A1;

      then

       A7: ((( id Z) (#) ( arccot * g)) + ((r / 2) (#) ( ln * (f1 + f2)))) is_differentiable_on Z by A1, A3, A4, SIN_COS9: 110;

      

       A8: for x st x in Z holds (f . x) = ( arccot . (x / r))

      proof

        let x;

        assume

         A9: x in Z;

        

        then (( arccot * g) . x) = ( arccot . (g . x)) by A1, FUNCT_1: 12

        .= ( arccot . (x / r)) by A1, A9;

        hence thesis by A1;

      end;

      

       A10: for x be Element of REAL st x in ( dom (((( id Z) (#) ( arccot * g)) + ((r / 2) (#) ( ln * (f1 + f2)))) `| Z)) holds ((((( id Z) (#) ( arccot * g)) + ((r / 2) (#) ( ln * (f1 + f2)))) `| Z) . x) = (f . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom (((( id Z) (#) ( arccot * g)) + ((r / 2) (#) ( ln * (f1 + f2)))) `| Z));

        then

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

        

        then ((((( id Z) (#) ( arccot * g)) + ((r / 2) (#) ( ln * (f1 + f2)))) `| Z) . x) = ( arccot . (x / r)) by A1, A3, A4, A6, SIN_COS9: 110

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

        hence thesis;

      end;

      ( dom (((( id Z) (#) ( arccot * g)) + ((r / 2) (#) ( ln * (f1 + f2)))) `| Z)) = ( dom f) by A1, A7, FDIFF_1:def 7;

      then (((( id Z) (#) ( arccot * g)) + ((r / 2) (#) ( ln * (f1 + f2)))) `| Z) = f by A10, PARTFUN1: 5;

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

    end;

    theorem :: INTEGR12:17

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

    proof

      assume

       A1: A c= Z & f = (( arctan * f1) + (( id Z) / (r (#) (g + (f1 ^2 ))))) & (for x st x in Z holds (g . x) = 1 & (f1 . x) = (x / r) & (f1 . x) > ( - 1) & (f1 . x) < 1) & Z = ( dom f) & (f | A) is continuous;

      then Z = (( dom ( arctan * f1)) /\ ( dom (( id Z) / (r (#) (g + (f1 ^2 )))))) by VALUED_1:def 1;

      then

       A2: Z c= ( dom ( arctan * f1)) & Z c= ( dom (( id Z) / (r (#) (g + (f1 ^2 ))))) by XBOOLE_1: 18;

      Z c= (( dom ( id Z)) /\ ( dom ( arctan * f1))) by A2, XBOOLE_1: 19;

      then

       A3: Z c= ( dom (( id Z) (#) ( arctan * f1))) by VALUED_1:def 4;

      Z c= (( dom ( id Z)) /\ (( dom (r (#) (g + (f1 ^2 )))) \ ((r (#) (g + (f1 ^2 ))) " { 0 }))) by A2, RFUNCT_1:def 1;

      then Z c= (( dom (r (#) (g + (f1 ^2 )))) \ ((r (#) (g + (f1 ^2 ))) " { 0 })) by XBOOLE_1: 18;

      then

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

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

      then Z c= ( dom (r (#) (g + (f1 ^2 )))) by A4;

      then

       A5: Z c= ( dom (g + (f1 ^2 ))) by VALUED_1:def 5;

      

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

      

       A7: for x st x in Z holds (f1 . x) = (x / r) & (f1 . x) > ( - 1) & (f1 . x) < 1 by A1;

      then

       A8: (( id Z) (#) ( arctan * f1)) is_differentiable_on Z by A3, SIN_COS9: 105;

      

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

      proof

        let x;

        assume

         A10: x in Z;

        

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

        .= (( arctan . (f1 . x)) + ((( id Z) / (r (#) (g + (f1 ^2 )))) . x)) by A2, A10, FUNCT_1: 12

        .= (( arctan . (f1 . x)) + ((( id Z) . x) / ((r (#) (g + (f1 ^2 ))) . x))) by A2, A10, RFUNCT_1:def 1

        .= (( arctan . (f1 . x)) + (x / ((r (#) (g + (f1 ^2 ))) . x))) by A10, FUNCT_1: 18

        .= (( arctan . (f1 . x)) + (x / (r * ((g + (f1 ^2 )) . x)))) by VALUED_1: 6

        .= (( arctan . (f1 . x)) + (x / (r * ((g . x) + ((f1 ^2 ) . x))))) by A5, A10, VALUED_1:def 1

        .= (( arctan . (f1 . x)) + (x / (r * ((g . x) + ((f1 . x) ^2 ))))) by VALUED_1: 11

        .= (( arctan . (x / r)) + (x / (r * ((g . x) + ((f1 . x) ^2 ))))) by A1, A10

        .= (( arctan . (x / r)) + (x / (r * (1 + ((f1 . x) ^2 ))))) by A1, A10

        .= (( arctan . (x / r)) + (x / (r * (1 + ((x / r) ^2 ))))) by A1, A10;

        hence thesis by A1;

      end;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

        then (((( id Z) (#) ( arctan * f1)) `| Z) . x) = (( arctan . (x / r)) + (x / (r * (1 + ((x / r) ^2 ))))) by A3, A7, SIN_COS9: 105

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

        hence thesis;

      end;

      ( dom ((( id Z) (#) ( arctan * f1)) `| Z)) = ( dom f) by A1, A8, FDIFF_1:def 7;

      then ((( id Z) (#) ( arctan * f1)) `| Z) = f by A11, PARTFUN1: 5;

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

    end;

    theorem :: INTEGR12:18

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

    proof

      assume

       A1: A c= Z & f = (( arccot * f1) - (( id Z) / (r (#) (g + (f1 ^2 ))))) & (for x st x in Z holds (g . x) = 1 & (f1 . x) = (x / r) & (f1 . x) > ( - 1) & (f1 . x) < 1) & Z = ( dom f) & (f | A) is continuous;

      then Z = (( dom ( arccot * f1)) /\ ( dom (( id Z) / (r (#) (g + (f1 ^2 )))))) by VALUED_1: 12;

      then

       A2: Z c= ( dom ( arccot * f1)) & Z c= ( dom (( id Z) / (r (#) (g + (f1 ^2 ))))) by XBOOLE_1: 18;

      Z c= (( dom ( id Z)) /\ ( dom ( arccot * f1))) by A2, XBOOLE_1: 19;

      then

       A3: Z c= ( dom (( id Z) (#) ( arccot * f1))) by VALUED_1:def 4;

      Z c= (( dom ( id Z)) /\ (( dom (r (#) (g + (f1 ^2 )))) \ ((r (#) (g + (f1 ^2 ))) " { 0 }))) by A2, RFUNCT_1:def 1;

      then Z c= (( dom (r (#) (g + (f1 ^2 )))) \ ((r (#) (g + (f1 ^2 ))) " { 0 })) by XBOOLE_1: 18;

      then

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

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

      then Z c= ( dom (r (#) (g + (f1 ^2 )))) by A4;

      then

       A5: Z c= ( dom (g + (f1 ^2 ))) by VALUED_1:def 5;

      

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

      

       A7: for x st x in Z holds (f1 . x) = (x / r) & (f1 . x) > ( - 1) & (f1 . x) < 1 by A1;

      then

       A8: (( id Z) (#) ( arccot * f1)) is_differentiable_on Z by A3, SIN_COS9: 106;

      

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

      proof

        let x;

        assume

         A10: x in Z;

        

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

        .= (( arccot . (f1 . x)) - ((( id Z) / (r (#) (g + (f1 ^2 )))) . x)) by A2, A10, FUNCT_1: 12

        .= (( arccot . (f1 . x)) - ((( id Z) . x) / ((r (#) (g + (f1 ^2 ))) . x))) by A2, A10, RFUNCT_1:def 1

        .= (( arccot . (f1 . x)) - (x / ((r (#) (g + (f1 ^2 ))) . x))) by A10, FUNCT_1: 18

        .= (( arccot . (f1 . x)) - (x / (r * ((g + (f1 ^2 )) . x)))) by VALUED_1: 6

        .= (( arccot . (f1 . x)) - (x / (r * ((g . x) + ((f1 ^2 ) . x))))) by A5, A10, VALUED_1:def 1

        .= (( arccot . (f1 . x)) - (x / (r * ((g . x) + ((f1 . x) ^2 ))))) by VALUED_1: 11

        .= (( arccot . (x / r)) - (x / (r * ((g . x) + ((f1 . x) ^2 ))))) by A1, A10

        .= (( arccot . (x / r)) - (x / (r * (1 + ((f1 . x) ^2 ))))) by A1, A10

        .= (( arccot . (x / r)) - (x / (r * (1 + ((x / r) ^2 ))))) by A1, A10;

        hence thesis by A1;

      end;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

        then (((( id Z) (#) ( arccot * f1)) `| Z) . x) = (( arccot . (x / r)) - (x / (r * (1 + ((x / r) ^2 ))))) by A3, A7, SIN_COS9: 106

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

        hence thesis;

      end;

      ( dom ((( id Z) (#) ( arccot * f1)) `| Z)) = ( dom f) by A1, A8, FDIFF_1:def 7;

      then ((( id Z) (#) ( arccot * f1)) `| Z) = f by A11, PARTFUN1: 5;

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

    end;

    theorem :: INTEGR12:19

    A c= Z & Z c= ].( - 1), 1.[ & (for x st x in Z holds (f1 . x) = 1) & Z = ( dom f) & Z c= ( dom (( #Z n) * arcsin )) & 1 < n & f = ((n (#) (( #Z (n - 1)) * arcsin )) / (( #R (1 / 2)) * (f1 - ( #Z 2)))) implies ( integral (f,A)) = (((( #Z n) * arcsin ) . ( upper_bound A)) - ((( #Z n) * arcsin ) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & Z c= ].( - 1), 1.[ & (for x st x in Z holds (f1 . x) = 1) & Z = ( dom f) & Z c= ( dom (( #Z n) * arcsin )) & 1 < n & f = ((n (#) (( #Z (n - 1)) * arcsin )) / (( #R (1 / 2)) * (f1 - ( #Z 2))));

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

      then

       A2: Z c= ( dom (n (#) (( #Z (n - 1)) * arcsin ))) & Z c= (( dom (( #R (1 / 2)) * (f1 - ( #Z 2)))) \ ((( #R (1 / 2)) * (f1 - ( #Z 2))) " { 0 })) by XBOOLE_1: 18;

      then

       A3: Z c= ( dom (( #Z (n - 1)) * arcsin )) by VALUED_1:def 5;

      

       A4: Z c= ( dom ((( #R (1 / 2)) * (f1 - ( #Z 2))) ^ )) by A2, RFUNCT_1:def 2;

      ( dom ((( #R (1 / 2)) * (f1 - ( #Z 2))) ^ )) c= ( dom (( #R (1 / 2)) * (f1 - ( #Z 2)))) by RFUNCT_1: 1;

      then

       A5: Z c= ( dom (( #R (1 / 2)) * (f1 - ( #Z 2)))) by A4;

      for x st x in Z holds (( #Z (n - 1)) * arcsin ) is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then

         A6: arcsin is_differentiable_in x by A1, FDIFF_1: 9, SIN_COS6: 83;

        consider m be Nat such that

         A7: n = (m + 1) by A1, NAT_1: 6;

        thus thesis by A6, A7, TAYLOR_1: 3;

      end;

      then (( #Z (n - 1)) * arcsin ) is_differentiable_on Z by A3, FDIFF_1: 9;

      then

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

      set f2 = ( #Z 2);

      for x st x in Z holds ((f1 - ( #Z 2)) . x) > 0

      proof

        let x;

        assume

         A9: x in Z;

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

        then 0 < (1 + x) & 0 < (1 - x) by XREAL_1: 50, XREAL_1: 148;

        then

         A10: 0 < ((1 + x) * (1 - x)) by XREAL_1: 129;

        for x st x in Z holds x in ( dom (f1 - f2)) by A5, FUNCT_1: 11;

        

        then ((f1 - f2) . x) = ((f1 . x) - (f2 . x)) by A9, VALUED_1: 13

        .= ((f1 . x) - (x #Z (1 + 1))) by TAYLOR_1:def 1

        .= ((f1 . x) - ((x #Z 1) * (x #Z 1))) by TAYLOR_1: 1

        .= ((f1 . x) - (x * (x #Z 1))) by PREPOWER: 35

        .= ((f1 . x) - (x * x)) by PREPOWER: 35

        .= (1 - (x * x)) by A1, A9;

        hence thesis by A10;

      end;

      then for x st x in Z holds (f1 . x) = 1 & ((f1 - ( #Z 2)) . x) > 0 by A1;

      then

       A11: (( #R (1 / 2)) * (f1 - ( #Z 2))) is_differentiable_on Z by A5, FDIFF_7: 22;

      x in Z implies ((( #R (1 / 2)) * (f1 - ( #Z 2))) . x) <> 0 by A4, RFUNCT_1: 3;

      then f is_differentiable_on Z by A1, A8, A11, FDIFF_2: 21;

      then (f | Z) is continuous by FDIFF_1: 25;

      then (f | A) is continuous by A1, FCONT_1: 16;

      then

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

      

       A13: (( #Z n) * arcsin ) is_differentiable_on Z by A1, FDIFF_7: 10;

      

       A14: for x st x in Z holds (f . x) = ((n * (( arcsin . x) #Z (n - 1))) / ( sqrt (1 - (x ^2 ))))

      proof

        let x;

        assume

         A15: x in Z;

        then

         A16: x in ( dom (f1 - ( #Z 2))) & ((f1 - ( #Z 2)) . x) in ( dom ( #R (1 / 2))) by A5, FUNCT_1: 11;

        then

         A17: ((f1 - ( #Z 2)) . x) in ( right_open_halfline 0 ) by TAYLOR_1:def 4;

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

        then 0 < (1 + x) & 0 < (1 - x) by XREAL_1: 50, XREAL_1: 148;

        then

         A18: 0 < ((1 + x) * (1 - x)) by XREAL_1: 129;

        (((n (#) (( #Z (n - 1)) * arcsin )) / (( #R (1 / 2)) * (f1 - ( #Z 2)))) . x) = (((n (#) (( #Z (n - 1)) * arcsin )) . x) / ((( #R (1 / 2)) * (f1 - ( #Z 2))) . x)) by A1, A15, RFUNCT_1:def 1

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

        .= ((n * (( #Z (n - 1)) . ( arcsin . x))) / ((( #R (1 / 2)) * (f1 - ( #Z 2))) . x)) by A3, A15, FUNCT_1: 12

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

        .= ((n * (( arcsin . x) #Z (n - 1))) / (( #R (1 / 2)) . ((f1 - ( #Z 2)) . x))) by A5, A15, FUNCT_1: 12

        .= ((n * (( arcsin . x) #Z (n - 1))) / (((f1 - ( #Z 2)) . x) #R (1 / 2))) by A17, TAYLOR_1:def 4

        .= ((n * (( arcsin . x) #Z (n - 1))) / (((f1 . x) - (( #Z 2) . x)) #R (1 / 2))) by A16, VALUED_1: 13

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

        .= ((n * (( arcsin . x) #Z (n - 1))) / (((f1 . x) - (x ^2 )) #R (1 / 2))) by FDIFF_7: 1

        .= ((n * (( arcsin . x) #Z (n - 1))) / ((1 - (x ^2 )) #R (1 / 2))) by A1, A15

        .= ((n * (( arcsin . x) #Z (n - 1))) / ( sqrt (1 - (x ^2 )))) by A18, FDIFF_7: 2;

        hence thesis by A1;

      end;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

        then (((( #Z n) * arcsin ) `| Z) . x) = ((n * (( arcsin . x) #Z (n - 1))) / ( sqrt (1 - (x ^2 )))) by A1, FDIFF_7: 10

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

        hence thesis;

      end;

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

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

      hence thesis by A1, A12, FDIFF_7: 10, INTEGRA5: 13;

    end;

    theorem :: INTEGR12:20

    A c= Z & Z c= ].( - 1), 1.[ & (for x st x in Z holds (f1 . x) = 1) & Z c= ( dom (( #Z n) * arccos )) & Z = ( dom f) & 1 < n & f = ((n (#) (( #Z (n - 1)) * arccos )) / (( #R (1 / 2)) * (f1 - ( #Z 2)))) implies ( integral (f,A)) = ((( - (( #Z n) * arccos )) . ( upper_bound A)) - (( - (( #Z n) * arccos )) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & Z c= ].( - 1), 1.[ & (for x st x in Z holds (f1 . x) = 1) & Z c= ( dom (( #Z n) * arccos )) & Z = ( dom f) & 1 < n & f = ((n (#) (( #Z (n - 1)) * arccos )) / (( #R (1 / 2)) * (f1 - ( #Z 2))));

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

      then

       A2: Z c= ( dom (n (#) (( #Z (n - 1)) * arccos ))) & Z c= (( dom (( #R (1 / 2)) * (f1 - ( #Z 2)))) \ ((( #R (1 / 2)) * (f1 - ( #Z 2))) " { 0 })) by XBOOLE_1: 18;

      then

       A3: Z c= ( dom (( #Z (n - 1)) * arccos )) by VALUED_1:def 5;

      

       A4: Z c= ( dom ((( #R (1 / 2)) * (f1 - ( #Z 2))) ^ )) by A2, RFUNCT_1:def 2;

      ( dom ((( #R (1 / 2)) * (f1 - ( #Z 2))) ^ )) c= ( dom (( #R (1 / 2)) * (f1 - ( #Z 2)))) by RFUNCT_1: 1;

      then

       A5: Z c= ( dom (( #R (1 / 2)) * (f1 - ( #Z 2)))) by A4;

      for x st x in Z holds (( #Z (n - 1)) * arccos ) is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then

         A6: arccos is_differentiable_in x by A1, FDIFF_1: 9, SIN_COS6: 106;

        consider m be Nat such that

         A7: n = (m + 1) by A1, NAT_1: 6;

        thus thesis by A6, A7, TAYLOR_1: 3;

      end;

      then (( #Z (n - 1)) * arccos ) is_differentiable_on Z by A3, FDIFF_1: 9;

      then

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

      set f2 = ( #Z 2);

      for x st x in Z holds ((f1 - ( #Z 2)) . x) > 0

      proof

        let x;

        assume

         A9: x in Z;

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

        then 0 < (1 + x) & 0 < (1 - x) by XREAL_1: 50, XREAL_1: 148;

        then

         A10: 0 < ((1 + x) * (1 - x)) by XREAL_1: 129;

        for x st x in Z holds x in ( dom (f1 - f2)) by A5, FUNCT_1: 11;

        

        then ((f1 - f2) . x) = ((f1 . x) - (f2 . x)) by A9, VALUED_1: 13

        .= ((f1 . x) - (x #Z (1 + 1))) by TAYLOR_1:def 1

        .= ((f1 . x) - ((x #Z 1) * (x #Z 1))) by TAYLOR_1: 1

        .= ((f1 . x) - (x * (x #Z 1))) by PREPOWER: 35

        .= ((f1 . x) - (x * x)) by PREPOWER: 35

        .= (1 - (x * x)) by A1, A9;

        hence thesis by A10;

      end;

      then for x st x in Z holds (f1 . x) = 1 & ((f1 - ( #Z 2)) . x) > 0 by A1;

      then

       A11: (( #R (1 / 2)) * (f1 - ( #Z 2))) is_differentiable_on Z by A5, FDIFF_7: 22;

      x in Z implies ((( #R (1 / 2)) * (f1 - ( #Z 2))) . x) <> 0 by A4, RFUNCT_1: 3;

      then f is_differentiable_on Z by A1, A8, A11, FDIFF_2: 21;

      then (f | Z) is continuous by FDIFF_1: 25;

      then (f | A) is continuous by A1, FCONT_1: 16;

      then

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

      

       A13: (( #Z n) * arccos ) is_differentiable_on Z by A1, FDIFF_7: 11;

      

       A14: Z c= ( dom ( - (( #Z n) * arccos ))) by A1, VALUED_1: 8;

      then

       A15: (( - 1) (#) (( #Z n) * arccos )) is_differentiable_on Z by A13, FDIFF_1: 20;

      

       A16: for x st x in Z holds (f . x) = ((n * (( arccos . x) #Z (n - 1))) / ( sqrt (1 - (x ^2 ))))

      proof

        let x;

        assume

         A17: x in Z;

        then

         A18: x in ( dom (f1 - ( #Z 2))) & ((f1 - ( #Z 2)) . x) in ( dom ( #R (1 / 2))) by A5, FUNCT_1: 11;

        then

         A19: ((f1 - ( #Z 2)) . x) in ( right_open_halfline 0 ) by TAYLOR_1:def 4;

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

        then 0 < (1 + x) & 0 < (1 - x) by XREAL_1: 50, XREAL_1: 148;

        then

         A20: 0 < ((1 + x) * (1 - x)) by XREAL_1: 129;

        (((n (#) (( #Z (n - 1)) * arccos )) / (( #R (1 / 2)) * (f1 - ( #Z 2)))) . x) = (((n (#) (( #Z (n - 1)) * arccos )) . x) / ((( #R (1 / 2)) * (f1 - ( #Z 2))) . x)) by A1, A17, RFUNCT_1:def 1

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

        .= ((n * (( #Z (n - 1)) . ( arccos . x))) / ((( #R (1 / 2)) * (f1 - ( #Z 2))) . x)) by A3, A17, FUNCT_1: 12

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

        .= ((n * (( arccos . x) #Z (n - 1))) / (( #R (1 / 2)) . ((f1 - ( #Z 2)) . x))) by A5, A17, FUNCT_1: 12

        .= ((n * (( arccos . x) #Z (n - 1))) / (((f1 - ( #Z 2)) . x) #R (1 / 2))) by A19, TAYLOR_1:def 4

        .= ((n * (( arccos . x) #Z (n - 1))) / (((f1 . x) - (( #Z 2) . x)) #R (1 / 2))) by A18, VALUED_1: 13

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

        .= ((n * (( arccos . x) #Z (n - 1))) / (((f1 . x) - (x ^2 )) #R (1 / 2))) by FDIFF_7: 1

        .= ((n * (( arccos . x) #Z (n - 1))) / ((1 - (x ^2 )) #R (1 / 2))) by A1, A17

        .= ((n * (( arccos . x) #Z (n - 1))) / ( sqrt (1 - (x ^2 )))) by A20, FDIFF_7: 2;

        hence thesis by A1;

      end;

      

       A21: for x st x in Z holds ((( - (( #Z n) * arccos )) `| Z) . x) = ((n * (( arccos . x) #Z (n - 1))) / ( sqrt (1 - (x ^2 ))))

      proof

        let x;

        assume

         A22: x in Z;

        then

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

        

         A24: arccos is_differentiable_in x by A1, A22, FDIFF_1: 9, SIN_COS6: 106;

        

         A25: (( #Z n) * arccos ) is_differentiable_in x by A13, A22, FDIFF_1: 9;

        ((( - (( #Z n) * arccos )) `| Z) . x) = ( diff (( - (( #Z n) * arccos )),x)) by A15, A22, FDIFF_1:def 7

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

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

        .= (( - 1) * ((n * (( arccos . x) #Z (n - 1))) * ( - (1 / ( sqrt (1 - (x ^2 ))))))) by A23, SIN_COS6: 106

        .= ((n * (( arccos . x) #Z (n - 1))) / ( sqrt (1 - (x ^2 ))));

        hence thesis;

      end;

      

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

      proof

        let x be Element of REAL ;

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

        then

         A27: x in Z by A15, FDIFF_1:def 7;

        

        then ((( - (( #Z n) * arccos )) `| Z) . x) = ((n * (( arccos . x) #Z (n - 1))) / ( sqrt (1 - (x ^2 )))) by A21

        .= (f . x) by A16, A27;

        hence thesis;

      end;

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

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

      hence thesis by A1, A12, A13, A14, FDIFF_1: 20, INTEGRA5: 13;

    end;

    theorem :: INTEGR12:21

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

    proof

      assume

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

      then Z = (( dom arcsin ) /\ ( dom (( id Z) / (( #R (1 / 2)) * (f1 - ( #Z 2)))))) by VALUED_1:def 1;

      then

       A2: Z c= ( dom arcsin ) & Z c= ( dom (( id Z) / (( #R (1 / 2)) * (f1 - ( #Z 2))))) by XBOOLE_1: 18;

      

       A3: Z = ( dom ( id Z));

      Z c= (( dom ( id Z)) /\ ( dom arcsin )) by A2, XBOOLE_1: 19;

      then

       A4: Z c= ( dom (( id Z) (#) arcsin )) by VALUED_1:def 4;

      

       A5: arcsin is_differentiable_on Z by A1, FDIFF_1: 26, SIN_COS6: 83;

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

      then

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

      Z c= (( dom ( id Z)) /\ (( dom (( #R (1 / 2)) * (f1 - ( #Z 2)))) \ ((( #R (1 / 2)) * (f1 - ( #Z 2))) " { 0 }))) by A2, RFUNCT_1:def 1;

      then Z c= (( dom (( #R (1 / 2)) * (f1 - ( #Z 2)))) \ ((( #R (1 / 2)) * (f1 - ( #Z 2))) " { 0 })) by XBOOLE_1: 18;

      then

       A7: Z c= ( dom ((( #R (1 / 2)) * (f1 - ( #Z 2))) ^ )) by RFUNCT_1:def 2;

      ( dom ((( #R (1 / 2)) * (f1 - ( #Z 2))) ^ )) c= ( dom (( #R (1 / 2)) * (f1 - ( #Z 2)))) by RFUNCT_1: 1;

      then

       A8: Z c= ( dom (( #R (1 / 2)) * (f1 - ( #Z 2)))) by A7;

      set f2 = ( #Z 2);

      for x st x in Z holds ((f1 - ( #Z 2)) . x) > 0

      proof

        let x;

        assume

         A9: x in Z;

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

        then 0 < (1 + x) & 0 < (1 - x) by XREAL_1: 50, XREAL_1: 148;

        then

         A10: 0 < ((1 + x) * (1 - x)) by XREAL_1: 129;

        for x st x in Z holds x in ( dom (f1 - f2)) by A8, FUNCT_1: 11;

        

        then ((f1 - f2) . x) = ((f1 . x) - (f2 . x)) by A9, VALUED_1: 13

        .= ((f1 . x) - (x #Z (1 + 1))) by TAYLOR_1:def 1

        .= ((f1 . x) - ((x #Z 1) * (x #Z 1))) by TAYLOR_1: 1

        .= ((f1 . x) - (x * (x #Z 1))) by PREPOWER: 35

        .= ((f1 . x) - (x * x)) by PREPOWER: 35

        .= (1 - (x * x)) by A1, A9;

        hence thesis by A10;

      end;

      then for x st x in Z holds (f1 . x) = 1 & ((f1 - ( #Z 2)) . x) > 0 by A1;

      then

       A11: (( #R (1 / 2)) * (f1 - ( #Z 2))) is_differentiable_on Z by A8, FDIFF_7: 22;

      x in Z implies ((( #R (1 / 2)) * (f1 - ( #Z 2))) . x) <> 0 by A7, RFUNCT_1: 3;

      then (( id Z) / (( #R (1 / 2)) * (f1 - ( #Z 2)))) is_differentiable_on Z by A6, A11, FDIFF_2: 21;

      then (f | Z) is continuous by A1, A5, FDIFF_1: 18, FDIFF_1: 25;

      then (f | A) is continuous by A1, FCONT_1: 16;

      then

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

      

       A13: (( id Z) (#) arcsin ) is_differentiable_on Z by A1, A4, FDIFF_7: 16;

      

       A14: for x st x in Z holds (f . x) = (( arcsin . x) + (x / ( sqrt (1 - (x ^2 )))))

      proof

        let x;

        assume

         A15: x in Z;

        then

         A16: x in ( dom (f1 - ( #Z 2))) & ((f1 - ( #Z 2)) . x) in ( dom ( #R (1 / 2))) by A8, FUNCT_1: 11;

        then

         A17: ((f1 - ( #Z 2)) . x) in ( right_open_halfline 0 ) by TAYLOR_1:def 4;

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

        then 0 < (1 + x) & 0 < (1 - x) by XREAL_1: 50, XREAL_1: 148;

        then

         A18: 0 < ((1 + x) * (1 - x)) by XREAL_1: 129;

        (( arcsin + (( id Z) / (( #R (1 / 2)) * (f1 - ( #Z 2))))) . x) = (( arcsin . x) + ((( id Z) / (( #R (1 / 2)) * (f1 - ( #Z 2)))) . x)) by A1, A15, VALUED_1:def 1

        .= (( arcsin . x) + ((( id Z) . x) / ((( #R (1 / 2)) * (f1 - ( #Z 2))) . x))) by A2, A15, RFUNCT_1:def 1

        .= (( arcsin . x) + (x / ((( #R (1 / 2)) * (f1 - ( #Z 2))) . x))) by A15, FUNCT_1: 18

        .= (( arcsin . x) + (x / (( #R (1 / 2)) . ((f1 - ( #Z 2)) . x)))) by A8, A15, FUNCT_1: 12

        .= (( arcsin . x) + (x / (((f1 - ( #Z 2)) . x) #R (1 / 2)))) by A17, TAYLOR_1:def 4

        .= (( arcsin . x) + (x / (((f1 . x) - (( #Z 2) . x)) #R (1 / 2)))) by A16, VALUED_1: 13

        .= (( arcsin . x) + (x / (((f1 . x) - (x #Z 2)) #R (1 / 2)))) by TAYLOR_1:def 1

        .= (( arcsin . x) + (x / (((f1 . x) - (x ^2 )) #R (1 / 2)))) by FDIFF_7: 1

        .= (( arcsin . x) + (x / ((1 - (x ^2 )) #R (1 / 2)))) by A1, A15

        .= (( arcsin . x) + (x / ( sqrt (1 - (x ^2 ))))) by A18, FDIFF_7: 2;

        hence thesis by A1;

      end;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

        then (((( id Z) (#) arcsin ) `| Z) . x) = (( arcsin . x) + (x / ( sqrt (1 - (x ^2 ))))) by A1, A4, FDIFF_7: 16

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

        hence thesis;

      end;

      ( dom ((( id Z) (#) arcsin ) `| Z)) = ( dom f) by A1, A13, FDIFF_1:def 7;

      then ((( id Z) (#) arcsin ) `| Z) = f by A19, PARTFUN1: 5;

      hence thesis by A1, A12, A4, FDIFF_7: 16, INTEGRA5: 13;

    end;

    theorem :: INTEGR12:22

    A c= Z & (for x st x in Z holds (f1 . x) = 1) & Z c= ].( - 1), 1.[ & Z = ( dom f) & f = ( arccos - (( id Z) / (( #R (1 / 2)) * (f1 - ( #Z 2))))) implies ( integral (f,A)) = (((( id Z) (#) arccos ) . ( upper_bound A)) - ((( id Z) (#) arccos ) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & (for x st x in Z holds (f1 . x) = 1) & Z c= ].( - 1), 1.[ & Z = ( dom f) & f = ( arccos - (( id Z) / (( #R (1 / 2)) * (f1 - ( #Z 2)))));

      then Z = (( dom arccos ) /\ ( dom (( id Z) / (( #R (1 / 2)) * (f1 - ( #Z 2)))))) by VALUED_1: 12;

      then

       A2: Z c= ( dom arccos ) & Z c= ( dom (( id Z) / (( #R (1 / 2)) * (f1 - ( #Z 2))))) by XBOOLE_1: 18;

      

       A3: Z = ( dom ( id Z));

      Z c= (( dom ( id Z)) /\ ( dom arccos )) by A2, XBOOLE_1: 19;

      then

       A4: Z c= ( dom (( id Z) (#) arccos )) by VALUED_1:def 4;

      

       A5: arccos is_differentiable_on Z by A1, FDIFF_1: 26, SIN_COS6: 106;

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

      then

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

      Z c= (( dom ( id Z)) /\ (( dom (( #R (1 / 2)) * (f1 - ( #Z 2)))) \ ((( #R (1 / 2)) * (f1 - ( #Z 2))) " { 0 }))) by A2, RFUNCT_1:def 1;

      then Z c= (( dom (( #R (1 / 2)) * (f1 - ( #Z 2)))) \ ((( #R (1 / 2)) * (f1 - ( #Z 2))) " { 0 })) by XBOOLE_1: 18;

      then

       A7: Z c= ( dom ((( #R (1 / 2)) * (f1 - ( #Z 2))) ^ )) by RFUNCT_1:def 2;

      ( dom ((( #R (1 / 2)) * (f1 - ( #Z 2))) ^ )) c= ( dom (( #R (1 / 2)) * (f1 - ( #Z 2)))) by RFUNCT_1: 1;

      then

       A8: Z c= ( dom (( #R (1 / 2)) * (f1 - ( #Z 2)))) by A7;

      set f2 = ( #Z 2);

      for x st x in Z holds ((f1 - ( #Z 2)) . x) > 0

      proof

        let x;

        assume

         A9: x in Z;

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

        then 0 < (1 + x) & 0 < (1 - x) by XREAL_1: 50, XREAL_1: 148;

        then

         A10: 0 < ((1 + x) * (1 - x)) by XREAL_1: 129;

        for x st x in Z holds x in ( dom (f1 - f2)) by A8, FUNCT_1: 11;

        

        then ((f1 - f2) . x) = ((f1 . x) - (f2 . x)) by A9, VALUED_1: 13

        .= ((f1 . x) - (x #Z (1 + 1))) by TAYLOR_1:def 1

        .= ((f1 . x) - ((x #Z 1) * (x #Z 1))) by TAYLOR_1: 1

        .= ((f1 . x) - (x * (x #Z 1))) by PREPOWER: 35

        .= ((f1 . x) - (x * x)) by PREPOWER: 35

        .= (1 - (x * x)) by A1, A9;

        hence thesis by A10;

      end;

      then for x st x in Z holds (f1 . x) = 1 & ((f1 - ( #Z 2)) . x) > 0 by A1;

      then

       A11: (( #R (1 / 2)) * (f1 - ( #Z 2))) is_differentiable_on Z by A8, FDIFF_7: 22;

      x in Z implies ((( #R (1 / 2)) * (f1 - ( #Z 2))) . x) <> 0 by A7, RFUNCT_1: 3;

      then (( id Z) / (( #R (1 / 2)) * (f1 - ( #Z 2)))) is_differentiable_on Z by A6, A11, FDIFF_2: 21;

      then (f | Z) is continuous by A1, A5, FDIFF_1: 19, FDIFF_1: 25;

      then (f | A) is continuous by A1, FCONT_1: 16;

      then

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

      

       A13: (( id Z) (#) arccos ) is_differentiable_on Z by A1, A4, FDIFF_7: 17;

      

       A14: for x st x in Z holds (f . x) = (( arccos . x) - (x / ( sqrt (1 - (x ^2 )))))

      proof

        let x;

        assume

         A15: x in Z;

        then

         A16: x in ( dom (f1 - ( #Z 2))) & ((f1 - ( #Z 2)) . x) in ( dom ( #R (1 / 2))) by A8, FUNCT_1: 11;

        then

         A17: ((f1 - ( #Z 2)) . x) in ( right_open_halfline 0 ) by TAYLOR_1:def 4;

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

        then 0 < (1 + x) & 0 < (1 - x) by XREAL_1: 50, XREAL_1: 148;

        then

         A18: 0 < ((1 + x) * (1 - x)) by XREAL_1: 129;

        (( arccos - (( id Z) / (( #R (1 / 2)) * (f1 - ( #Z 2))))) . x) = (( arccos . x) - ((( id Z) / (( #R (1 / 2)) * (f1 - ( #Z 2)))) . x)) by A1, A15, VALUED_1: 13

        .= (( arccos . x) - ((( id Z) . x) / ((( #R (1 / 2)) * (f1 - ( #Z 2))) . x))) by A2, A15, RFUNCT_1:def 1

        .= (( arccos . x) - (x / ((( #R (1 / 2)) * (f1 - ( #Z 2))) . x))) by A15, FUNCT_1: 18

        .= (( arccos . x) - (x / (( #R (1 / 2)) . ((f1 - ( #Z 2)) . x)))) by A8, A15, FUNCT_1: 12

        .= (( arccos . x) - (x / (((f1 - ( #Z 2)) . x) #R (1 / 2)))) by A17, TAYLOR_1:def 4

        .= (( arccos . x) - (x / (((f1 . x) - (( #Z 2) . x)) #R (1 / 2)))) by A16, VALUED_1: 13

        .= (( arccos . x) - (x / (((f1 . x) - (x #Z 2)) #R (1 / 2)))) by TAYLOR_1:def 1

        .= (( arccos . x) - (x / (((f1 . x) - (x ^2 )) #R (1 / 2)))) by FDIFF_7: 1

        .= (( arccos . x) - (x / ((1 - (x ^2 )) #R (1 / 2)))) by A1, A15

        .= (( arccos . x) - (x / ( sqrt (1 - (x ^2 ))))) by A18, FDIFF_7: 2;

        hence thesis by A1;

      end;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

        then (((( id Z) (#) arccos ) `| Z) . x) = (( arccos . x) - (x / ( sqrt (1 - (x ^2 ))))) by A1, A4, FDIFF_7: 17

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

        hence thesis;

      end;

      ( dom ((( id Z) (#) arccos ) `| Z)) = ( dom f) by A1, A13, FDIFF_1:def 7;

      then ((( id Z) (#) arccos ) `| Z) = f by A19, PARTFUN1: 5;

      hence thesis by A1, A12, A4, FDIFF_7: 17, INTEGRA5: 13;

    end;

    theorem :: INTEGR12:23

    A c= Z & Z c= ].( - 1), 1.[ & (for x st x in Z holds (f1 . x) = ((a * x) + b) & (f2 . x) = 1) & Z = ( dom f) & f = ((a (#) arcsin ) + (f1 / (( #R (1 / 2)) * (f2 - ( #Z 2))))) implies ( integral (f,A)) = (((f1 (#) arcsin ) . ( upper_bound A)) - ((f1 (#) arcsin ) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & Z c= ].( - 1), 1.[ & (for x st x in Z holds (f1 . x) = ((a * x) + b) & (f2 . x) = 1) & Z = ( dom f) & f = ((a (#) arcsin ) + (f1 / (( #R (1 / 2)) * (f2 - ( #Z 2)))));

      then Z = (( dom (a (#) arcsin )) /\ ( dom (f1 / (( #R (1 / 2)) * (f2 - ( #Z 2)))))) by VALUED_1:def 1;

      then

       A2: Z c= ( dom (a (#) arcsin )) & Z c= ( dom (f1 / (( #R (1 / 2)) * (f2 - ( #Z 2))))) by XBOOLE_1: 18;

      then

       A3: Z c= ( dom arcsin ) by VALUED_1:def 5;

      Z c= (( dom f1) /\ (( dom (( #R (1 / 2)) * (f2 - ( #Z 2)))) \ ((( #R (1 / 2)) * (f2 - ( #Z 2))) " { 0 }))) by A2, RFUNCT_1:def 1;

      then

       A4: Z c= ( dom f1) & Z c= (( dom (( #R (1 / 2)) * (f2 - ( #Z 2)))) \ ((( #R (1 / 2)) * (f2 - ( #Z 2))) " { 0 })) by XBOOLE_1: 18;

      then Z c= (( dom f1) /\ ( dom arcsin )) by A3, XBOOLE_1: 19;

      then

       A5: Z c= ( dom (f1 (#) arcsin )) by VALUED_1:def 4;

      

       A6: Z c= ( dom ((( #R (1 / 2)) * (f2 - ( #Z 2))) ^ )) by A4, RFUNCT_1:def 2;

      ( dom ((( #R (1 / 2)) * (f2 - ( #Z 2))) ^ )) c= ( dom (( #R (1 / 2)) * (f2 - ( #Z 2)))) by RFUNCT_1: 1;

      then

       A7: Z c= ( dom (( #R (1 / 2)) * (f2 - ( #Z 2)))) by A6;

      

       A8: arcsin is_differentiable_on Z by A1, FDIFF_1: 26, SIN_COS6: 83;

      then

       A9: (a (#) arcsin ) is_differentiable_on Z by A2, FDIFF_1: 20;

      

       A10: for x st x in Z holds (f1 . x) = ((a * x) + b) by A1;

      then

       A11: f1 is_differentiable_on Z by A4, FDIFF_1: 23;

      set f3 = ( #Z 2);

      for x st x in Z holds ((f2 - ( #Z 2)) . x) > 0

      proof

        let x;

        assume

         A12: x in Z;

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

        then 0 < (1 + x) & 0 < (1 - x) by XREAL_1: 50, XREAL_1: 148;

        then

         A13: 0 < ((1 + x) * (1 - x)) by XREAL_1: 129;

        for x st x in Z holds x in ( dom (f2 - f3)) by A7, FUNCT_1: 11;

        

        then ((f2 - f3) . x) = ((f2 . x) - (f3 . x)) by A12, VALUED_1: 13

        .= ((f2 . x) - (x #Z (1 + 1))) by TAYLOR_1:def 1

        .= ((f2 . x) - ((x #Z 1) * (x #Z 1))) by TAYLOR_1: 1

        .= ((f2 . x) - (x * (x #Z 1))) by PREPOWER: 35

        .= ((f2 . x) - (x * x)) by PREPOWER: 35

        .= (1 - (x * x)) by A1, A12;

        hence thesis by A13;

      end;

      then for x st x in Z holds (f2 . x) = 1 & ((f2 - ( #Z 2)) . x) > 0 by A1;

      then

       A14: (( #R (1 / 2)) * (f2 - ( #Z 2))) is_differentiable_on Z by A7, FDIFF_7: 22;

      x in Z implies ((( #R (1 / 2)) * (f2 - ( #Z 2))) . x) <> 0 by A6, RFUNCT_1: 3;

      then (f1 / (( #R (1 / 2)) * (f2 - ( #Z 2)))) is_differentiable_on Z by A11, A14, FDIFF_2: 21;

      then f is_differentiable_on Z by A1, A9, FDIFF_1: 18;

      then (f | Z) is continuous by FDIFF_1: 25;

      then (f | A) is continuous by A1, FCONT_1: 16;

      then

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

      

       A16: (f1 (#) arcsin ) is_differentiable_on Z by A5, A8, A11, FDIFF_1: 21;

      

       A17: for x st x in Z holds (f . x) = ((a * ( arcsin . x)) + (((a * x) + b) / ( sqrt (1 - (x ^2 )))))

      proof

        let x;

        assume

         A18: x in Z;

        then

         A19: x in ( dom (f2 - ( #Z 2))) & ((f2 - ( #Z 2)) . x) in ( dom ( #R (1 / 2))) by A7, FUNCT_1: 11;

        then

         A20: ((f2 - ( #Z 2)) . x) in ( right_open_halfline 0 ) by TAYLOR_1:def 4;

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

        then 0 < (1 + x) & 0 < (1 - x) by XREAL_1: 50, XREAL_1: 148;

        then

         A21: 0 < ((1 + x) * (1 - x)) by XREAL_1: 129;

        (((a (#) arcsin ) + (f1 / (( #R (1 / 2)) * (f2 - ( #Z 2))))) . x) = (((a (#) arcsin ) . x) + ((f1 / (( #R (1 / 2)) * (f2 - ( #Z 2)))) . x)) by A1, A18, VALUED_1:def 1

        .= ((a * ( arcsin . x)) + ((f1 / (( #R (1 / 2)) * (f2 - ( #Z 2)))) . x)) by VALUED_1: 6

        .= ((a * ( arcsin . x)) + ((f1 . x) / ((( #R (1 / 2)) * (f2 - ( #Z 2))) . x))) by A2, A18, RFUNCT_1:def 1

        .= ((a * ( arcsin . x)) + (((a * x) + b) / ((( #R (1 / 2)) * (f2 - ( #Z 2))) . x))) by A1, A18

        .= ((a * ( arcsin . x)) + (((a * x) + b) / (( #R (1 / 2)) . ((f2 - ( #Z 2)) . x)))) by A7, A18, FUNCT_1: 12

        .= ((a * ( arcsin . x)) + (((a * x) + b) / (((f2 - ( #Z 2)) . x) #R (1 / 2)))) by A20, TAYLOR_1:def 4

        .= ((a * ( arcsin . x)) + (((a * x) + b) / (((f2 . x) - (( #Z 2) . x)) #R (1 / 2)))) by A19, VALUED_1: 13

        .= ((a * ( arcsin . x)) + (((a * x) + b) / (((f2 . x) - (x #Z 2)) #R (1 / 2)))) by TAYLOR_1:def 1

        .= ((a * ( arcsin . x)) + (((a * x) + b) / (((f2 . x) - (x ^2 )) #R (1 / 2)))) by FDIFF_7: 1

        .= ((a * ( arcsin . x)) + (((a * x) + b) / ((1 - (x ^2 )) #R (1 / 2)))) by A1, A18

        .= ((a * ( arcsin . x)) + (((a * x) + b) / ( sqrt (1 - (x ^2 ))))) by A21, FDIFF_7: 2;

        hence thesis by A1;

      end;

      

       A22: for x be Element of REAL st x in ( dom ((f1 (#) arcsin ) `| Z)) holds (((f1 (#) arcsin ) `| Z) . x) = (f . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom ((f1 (#) arcsin ) `| Z));

        then

         A23: x in Z by A16, FDIFF_1:def 7;

        

        then (((f1 (#) arcsin ) `| Z) . x) = ((a * ( arcsin . x)) + (((a * x) + b) / ( sqrt (1 - (x ^2 ))))) by A1, A10, A5, FDIFF_7: 18

        .= (f . x) by A17, A23;

        hence thesis;

      end;

      ( dom ((f1 (#) arcsin ) `| Z)) = ( dom f) by A1, A16, FDIFF_1:def 7;

      then ((f1 (#) arcsin ) `| Z) = f by A22, PARTFUN1: 5;

      hence thesis by A1, A15, A16, INTEGRA5: 13;

    end;

    theorem :: INTEGR12:24

    A c= Z & Z c= ].( - 1), 1.[ & (for x st x in Z holds (f1 . x) = ((a * x) + b) & (f2 . x) = 1) & Z = ( dom f) & f = ((a (#) arccos ) - (f1 / (( #R (1 / 2)) * (f2 - ( #Z 2))))) implies ( integral (f,A)) = (((f1 (#) arccos ) . ( upper_bound A)) - ((f1 (#) arccos ) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & Z c= ].( - 1), 1.[ & (for x st x in Z holds (f1 . x) = ((a * x) + b) & (f2 . x) = 1) & Z = ( dom f) & f = ((a (#) arccos ) - (f1 / (( #R (1 / 2)) * (f2 - ( #Z 2)))));

      then Z = (( dom (a (#) arccos )) /\ ( dom (f1 / (( #R (1 / 2)) * (f2 - ( #Z 2)))))) by VALUED_1: 12;

      then

       A2: Z c= ( dom (a (#) arccos )) & Z c= ( dom (f1 / (( #R (1 / 2)) * (f2 - ( #Z 2))))) by XBOOLE_1: 18;

      then

       A3: Z c= ( dom arccos ) by VALUED_1:def 5;

      Z c= (( dom f1) /\ (( dom (( #R (1 / 2)) * (f2 - ( #Z 2)))) \ ((( #R (1 / 2)) * (f2 - ( #Z 2))) " { 0 }))) by A2, RFUNCT_1:def 1;

      then

       A4: Z c= ( dom f1) & Z c= (( dom (( #R (1 / 2)) * (f2 - ( #Z 2)))) \ ((( #R (1 / 2)) * (f2 - ( #Z 2))) " { 0 })) by XBOOLE_1: 18;

      then Z c= (( dom f1) /\ ( dom arccos )) by A3, XBOOLE_1: 19;

      then

       A5: Z c= ( dom (f1 (#) arccos )) by VALUED_1:def 4;

      

       A6: Z c= ( dom ((( #R (1 / 2)) * (f2 - ( #Z 2))) ^ )) by A4, RFUNCT_1:def 2;

      ( dom ((( #R (1 / 2)) * (f2 - ( #Z 2))) ^ )) c= ( dom (( #R (1 / 2)) * (f2 - ( #Z 2)))) by RFUNCT_1: 1;

      then

       A7: Z c= ( dom (( #R (1 / 2)) * (f2 - ( #Z 2)))) by A6;

      

       A8: arccos is_differentiable_on Z by A1, FDIFF_1: 26, SIN_COS6: 106;

      then

       A9: (a (#) arccos ) is_differentiable_on Z by A2, FDIFF_1: 20;

      

       A10: for x st x in Z holds (f1 . x) = ((a * x) + b) by A1;

      then

       A11: f1 is_differentiable_on Z by A4, FDIFF_1: 23;

      set f3 = ( #Z 2);

      for x st x in Z holds ((f2 - ( #Z 2)) . x) > 0

      proof

        let x;

        assume

         A12: x in Z;

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

        then 0 < (1 + x) & 0 < (1 - x) by XREAL_1: 50, XREAL_1: 148;

        then

         A13: 0 < ((1 + x) * (1 - x)) by XREAL_1: 129;

        for x st x in Z holds x in ( dom (f2 - f3)) by A7, FUNCT_1: 11;

        

        then ((f2 - f3) . x) = ((f2 . x) - (f3 . x)) by A12, VALUED_1: 13

        .= ((f2 . x) - (x #Z (1 + 1))) by TAYLOR_1:def 1

        .= ((f2 . x) - ((x #Z 1) * (x #Z 1))) by TAYLOR_1: 1

        .= ((f2 . x) - (x * (x #Z 1))) by PREPOWER: 35

        .= ((f2 . x) - (x * x)) by PREPOWER: 35

        .= (1 - (x * x)) by A1, A12;

        hence thesis by A13;

      end;

      then for x st x in Z holds (f2 . x) = 1 & ((f2 - ( #Z 2)) . x) > 0 by A1;

      then

       A14: (( #R (1 / 2)) * (f2 - ( #Z 2))) is_differentiable_on Z by A7, FDIFF_7: 22;

      x in Z implies ((( #R (1 / 2)) * (f2 - ( #Z 2))) . x) <> 0 by A6, RFUNCT_1: 3;

      then (f1 / (( #R (1 / 2)) * (f2 - ( #Z 2)))) is_differentiable_on Z by A11, A14, FDIFF_2: 21;

      then f is_differentiable_on Z by A1, A9, FDIFF_1: 19;

      then (f | Z) is continuous by FDIFF_1: 25;

      then (f | A) is continuous by A1, FCONT_1: 16;

      then

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

      

       A16: (f1 (#) arccos ) is_differentiable_on Z by A5, A8, A11, FDIFF_1: 21;

      

       A17: for x st x in Z holds (f . x) = ((a * ( arccos . x)) - (((a * x) + b) / ( sqrt (1 - (x ^2 )))))

      proof

        let x;

        assume

         A18: x in Z;

        then

         A19: x in ( dom (f2 - ( #Z 2))) & ((f2 - ( #Z 2)) . x) in ( dom ( #R (1 / 2))) by A7, FUNCT_1: 11;

        then

         A20: ((f2 - ( #Z 2)) . x) in ( right_open_halfline 0 ) by TAYLOR_1:def 4;

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

        then 0 < (1 + x) & 0 < (1 - x) by XREAL_1: 50, XREAL_1: 148;

        then

         A21: 0 < ((1 + x) * (1 - x)) by XREAL_1: 129;

        (((a (#) arccos ) - (f1 / (( #R (1 / 2)) * (f2 - ( #Z 2))))) . x) = (((a (#) arccos ) . x) - ((f1 / (( #R (1 / 2)) * (f2 - ( #Z 2)))) . x)) by A1, A18, VALUED_1: 13

        .= ((a * ( arccos . x)) - ((f1 / (( #R (1 / 2)) * (f2 - ( #Z 2)))) . x)) by VALUED_1: 6

        .= ((a * ( arccos . x)) - ((f1 . x) / ((( #R (1 / 2)) * (f2 - ( #Z 2))) . x))) by A2, A18, RFUNCT_1:def 1

        .= ((a * ( arccos . x)) - (((a * x) + b) / ((( #R (1 / 2)) * (f2 - ( #Z 2))) . x))) by A1, A18

        .= ((a * ( arccos . x)) - (((a * x) + b) / (( #R (1 / 2)) . ((f2 - ( #Z 2)) . x)))) by A7, A18, FUNCT_1: 12

        .= ((a * ( arccos . x)) - (((a * x) + b) / (((f2 - ( #Z 2)) . x) #R (1 / 2)))) by A20, TAYLOR_1:def 4

        .= ((a * ( arccos . x)) - (((a * x) + b) / (((f2 . x) - (( #Z 2) . x)) #R (1 / 2)))) by A19, VALUED_1: 13

        .= ((a * ( arccos . x)) - (((a * x) + b) / (((f2 . x) - (x #Z 2)) #R (1 / 2)))) by TAYLOR_1:def 1

        .= ((a * ( arccos . x)) - (((a * x) + b) / (((f2 . x) - (x ^2 )) #R (1 / 2)))) by FDIFF_7: 1

        .= ((a * ( arccos . x)) - (((a * x) + b) / ((1 - (x ^2 )) #R (1 / 2)))) by A1, A18

        .= ((a * ( arccos . x)) - (((a * x) + b) / ( sqrt (1 - (x ^2 ))))) by A21, FDIFF_7: 2;

        hence thesis by A1;

      end;

      

       A22: for x be Element of REAL st x in ( dom ((f1 (#) arccos ) `| Z)) holds (((f1 (#) arccos ) `| Z) . x) = (f . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom ((f1 (#) arccos ) `| Z));

        then

         A23: x in Z by A16, FDIFF_1:def 7;

        

        then (((f1 (#) arccos ) `| Z) . x) = ((a * ( arccos . x)) - (((a * x) + b) / ( sqrt (1 - (x ^2 ))))) by A1, A10, A5, FDIFF_7: 19

        .= (f . x) by A17, A23;

        hence thesis;

      end;

      ( dom ((f1 (#) arccos ) `| Z)) = ( dom f) by A1, A16, FDIFF_1:def 7;

      then ((f1 (#) arccos ) `| Z) = f by A22, PARTFUN1: 5;

      hence thesis by A1, A15, A16, INTEGRA5: 13;

    end;

    theorem :: INTEGR12:25

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

    proof

      assume

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

      then Z = (( dom ( arcsin * f1)) /\ ( dom (( id Z) / (a (#) (( #R (1 / 2)) * (g - (f1 ^2 ))))))) by VALUED_1:def 1;

      then

       A2: Z c= ( dom ( arcsin * f1)) & Z c= ( dom (( id Z) / (a (#) (( #R (1 / 2)) * (g - (f1 ^2 )))))) by XBOOLE_1: 18;

      Z c= (( dom ( id Z)) /\ ( dom ( arcsin * f1))) by A2, XBOOLE_1: 19;

      then

       A3: Z c= ( dom (( id Z) (#) ( arcsin * f1))) by VALUED_1:def 4;

      Z c= (( dom ( id Z)) /\ (( dom (a (#) (( #R (1 / 2)) * (g - (f1 ^2 ))))) \ ((a (#) (( #R (1 / 2)) * (g - (f1 ^2 )))) " { 0 }))) by A2, RFUNCT_1:def 1;

      then Z c= (( dom (a (#) (( #R (1 / 2)) * (g - (f1 ^2 ))))) \ ((a (#) (( #R (1 / 2)) * (g - (f1 ^2 )))) " { 0 })) by XBOOLE_1: 18;

      then

       A4: Z c= ( dom ((a (#) (( #R (1 / 2)) * (g - (f1 ^2 )))) ^ )) by RFUNCT_1:def 2;

      ( dom ((a (#) (( #R (1 / 2)) * (g - (f1 ^2 )))) ^ )) c= ( dom (a (#) (( #R (1 / 2)) * (g - (f1 ^2 ))))) by RFUNCT_1: 1;

      then Z c= ( dom (a (#) (( #R (1 / 2)) * (g - (f1 ^2 ))))) by A4;

      then

       A5: Z c= ( dom (( #R (1 / 2)) * (g - (f1 ^2 )))) by VALUED_1:def 5;

      

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

      

       A7: for x st x in Z holds (f1 . x) = (x / a) & (f1 . x) > ( - 1) & (f1 . x) < 1 by A1;

      then

       A8: (( id Z) (#) ( arcsin * f1)) is_differentiable_on Z by A3, FDIFF_7: 25;

      

       A9: for x st x in Z holds (f . x) = (( arcsin . (x / a)) + (x / (a * ( sqrt (1 - ((x / a) ^2 ))))))

      proof

        let x;

        assume

         A10: x in Z;

        then

         A11: x in ( dom (g - (f1 ^2 ))) & ((g - (f1 ^2 )) . x) in ( dom ( #R (1 / 2))) by A5, FUNCT_1: 11;

        then

         A12: ((g - (f1 ^2 )) . x) in ( right_open_halfline 0 ) by TAYLOR_1:def 4;

        ( - 1) < (f1 . x) & (f1 . x) < 1 by A1, A10;

        then 0 < (1 + (f1 . x)) & 0 < (1 - (f1 . x)) by XREAL_1: 50, XREAL_1: 148;

        then

         A13: 0 < ((1 + (f1 . x)) * (1 - (f1 . x))) by XREAL_1: 129;

        

         A14: (f1 . x) = (x / a) by A1, A10;

        ((( arcsin * f1) + (( id Z) / (a (#) (( #R (1 / 2)) * (g - (f1 ^2 )))))) . x) = ((( arcsin * f1) . x) + ((( id Z) / (a (#) (( #R (1 / 2)) * (g - (f1 ^2 ))))) . x)) by A1, A10, VALUED_1:def 1

        .= (( arcsin . (f1 . x)) + ((( id Z) / (a (#) (( #R (1 / 2)) * (g - (f1 ^2 ))))) . x)) by A2, A10, FUNCT_1: 12

        .= (( arcsin . (x / a)) + ((( id Z) / (a (#) (( #R (1 / 2)) * (g - (f1 ^2 ))))) . x)) by A1, A10

        .= (( arcsin . (x / a)) + ((( id Z) . x) / ((a (#) (( #R (1 / 2)) * (g - (f1 ^2 )))) . x))) by A2, A10, RFUNCT_1:def 1

        .= (( arcsin . (x / a)) + (x / ((a (#) (( #R (1 / 2)) * (g - (f1 ^2 )))) . x))) by A10, FUNCT_1: 18

        .= (( arcsin . (x / a)) + (x / (a * ((( #R (1 / 2)) * (g - (f1 ^2 ))) . x)))) by VALUED_1: 6

        .= (( arcsin . (x / a)) + (x / (a * (( #R (1 / 2)) . ((g - (f1 ^2 )) . x))))) by A5, A10, FUNCT_1: 12

        .= (( arcsin . (x / a)) + (x / (a * (((g - (f1 ^2 )) . x) #R (1 / 2))))) by A12, TAYLOR_1:def 4

        .= (( arcsin . (x / a)) + (x / (a * (((g . x) - ((f1 ^2 ) . x)) #R (1 / 2))))) by A11, VALUED_1: 13

        .= (( arcsin . (x / a)) + (x / (a * (((g . x) - ((f1 . x) ^2 )) #R (1 / 2))))) by VALUED_1: 11

        .= (( arcsin . (x / a)) + (x / (a * ((1 - ((f1 . x) ^2 )) #R (1 / 2))))) by A1, A10

        .= (( arcsin . (x / a)) + (x / (a * ((1 - ((x / a) ^2 )) #R (1 / 2))))) by A1, A10

        .= (( arcsin . (x / a)) + (x / (a * ( sqrt (1 - ((x / a) ^2 )))))) by A14, A13, FDIFF_7: 2;

        hence thesis by A1;

      end;

      

       A15: for x be Element of REAL st x in ( dom ((( id Z) (#) ( arcsin * f1)) `| Z)) holds (((( id Z) (#) ( arcsin * f1)) `| Z) . x) = (f . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom ((( id Z) (#) ( arcsin * f1)) `| Z));

        then

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

        

        then (((( id Z) (#) ( arcsin * f1)) `| Z) . x) = (( arcsin . (x / a)) + (x / (a * ( sqrt (1 - ((x / a) ^2 )))))) by A3, A7, FDIFF_7: 25

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

        hence thesis;

      end;

      ( dom ((( id Z) (#) ( arcsin * f1)) `| Z)) = ( dom f) by A1, A8, FDIFF_1:def 7;

      then ((( id Z) (#) ( arcsin * f1)) `| Z) = f by A15, PARTFUN1: 5;

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

    end;

    theorem :: INTEGR12:26

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

    proof

      assume

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

      then Z = (( dom ( arccos * f1)) /\ ( dom (( id Z) / (a (#) (( #R (1 / 2)) * (g - (f1 ^2 ))))))) by VALUED_1: 12;

      then

       A2: Z c= ( dom ( arccos * f1)) & Z c= ( dom (( id Z) / (a (#) (( #R (1 / 2)) * (g - (f1 ^2 )))))) by XBOOLE_1: 18;

      Z c= (( dom ( id Z)) /\ ( dom ( arccos * f1))) by A2, XBOOLE_1: 19;

      then

       A3: Z c= ( dom (( id Z) (#) ( arccos * f1))) by VALUED_1:def 4;

      Z c= (( dom ( id Z)) /\ (( dom (a (#) (( #R (1 / 2)) * (g - (f1 ^2 ))))) \ ((a (#) (( #R (1 / 2)) * (g - (f1 ^2 )))) " { 0 }))) by A2, RFUNCT_1:def 1;

      then Z c= (( dom (a (#) (( #R (1 / 2)) * (g - (f1 ^2 ))))) \ ((a (#) (( #R (1 / 2)) * (g - (f1 ^2 )))) " { 0 })) by XBOOLE_1: 18;

      then

       A4: Z c= ( dom ((a (#) (( #R (1 / 2)) * (g - (f1 ^2 )))) ^ )) by RFUNCT_1:def 2;

      ( dom ((a (#) (( #R (1 / 2)) * (g - (f1 ^2 )))) ^ )) c= ( dom (a (#) (( #R (1 / 2)) * (g - (f1 ^2 ))))) by RFUNCT_1: 1;

      then Z c= ( dom (a (#) (( #R (1 / 2)) * (g - (f1 ^2 ))))) by A4;

      then

       A5: Z c= ( dom (( #R (1 / 2)) * (g - (f1 ^2 )))) by VALUED_1:def 5;

      

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

      

       A7: for x st x in Z holds (f1 . x) = (x / a) & (f1 . x) > ( - 1) & (f1 . x) < 1 by A1;

      then

       A8: (( id Z) (#) ( arccos * f1)) is_differentiable_on Z by A3, FDIFF_7: 26;

      

       A9: for x st x in Z holds (f . x) = (( arccos . (x / a)) - (x / (a * ( sqrt (1 - ((x / a) ^2 ))))))

      proof

        let x;

        assume

         A10: x in Z;

        then

         A11: x in ( dom (g - (f1 ^2 ))) & ((g - (f1 ^2 )) . x) in ( dom ( #R (1 / 2))) by A5, FUNCT_1: 11;

        then

         A12: ((g - (f1 ^2 )) . x) in ( right_open_halfline 0 ) by TAYLOR_1:def 4;

        ( - 1) < (f1 . x) & (f1 . x) < 1 by A1, A10;

        then 0 < (1 + (f1 . x)) & 0 < (1 - (f1 . x)) by XREAL_1: 50, XREAL_1: 148;

        then

         A13: 0 < ((1 + (f1 . x)) * (1 - (f1 . x))) by XREAL_1: 129;

        

         A14: (f1 . x) = (x / a) by A1, A10;

        ((( arccos * f1) - (( id Z) / (a (#) (( #R (1 / 2)) * (g - (f1 ^2 )))))) . x) = ((( arccos * f1) . x) - ((( id Z) / (a (#) (( #R (1 / 2)) * (g - (f1 ^2 ))))) . x)) by A1, A10, VALUED_1: 13

        .= (( arccos . (f1 . x)) - ((( id Z) / (a (#) (( #R (1 / 2)) * (g - (f1 ^2 ))))) . x)) by A2, A10, FUNCT_1: 12

        .= (( arccos . (x / a)) - ((( id Z) / (a (#) (( #R (1 / 2)) * (g - (f1 ^2 ))))) . x)) by A1, A10

        .= (( arccos . (x / a)) - ((( id Z) . x) / ((a (#) (( #R (1 / 2)) * (g - (f1 ^2 )))) . x))) by A2, A10, RFUNCT_1:def 1

        .= (( arccos . (x / a)) - (x / ((a (#) (( #R (1 / 2)) * (g - (f1 ^2 )))) . x))) by A10, FUNCT_1: 18

        .= (( arccos . (x / a)) - (x / (a * ((( #R (1 / 2)) * (g - (f1 ^2 ))) . x)))) by VALUED_1: 6

        .= (( arccos . (x / a)) - (x / (a * (( #R (1 / 2)) . ((g - (f1 ^2 )) . x))))) by A5, A10, FUNCT_1: 12

        .= (( arccos . (x / a)) - (x / (a * (((g - (f1 ^2 )) . x) #R (1 / 2))))) by A12, TAYLOR_1:def 4

        .= (( arccos . (x / a)) - (x / (a * (((g . x) - ((f1 ^2 ) . x)) #R (1 / 2))))) by A11, VALUED_1: 13

        .= (( arccos . (x / a)) - (x / (a * (((g . x) - ((f1 . x) ^2 )) #R (1 / 2))))) by VALUED_1: 11

        .= (( arccos . (x / a)) - (x / (a * ((1 - ((f1 . x) ^2 )) #R (1 / 2))))) by A1, A10

        .= (( arccos . (x / a)) - (x / (a * ((1 - ((x / a) ^2 )) #R (1 / 2))))) by A1, A10

        .= (( arccos . (x / a)) - (x / (a * ( sqrt (1 - ((x / a) ^2 )))))) by A14, A13, FDIFF_7: 2;

        hence thesis by A1;

      end;

      

       A15: for x be Element of REAL st x in ( dom ((( id Z) (#) ( arccos * f1)) `| Z)) holds (((( id Z) (#) ( arccos * f1)) `| Z) . x) = (f . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom ((( id Z) (#) ( arccos * f1)) `| Z));

        then

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

        

        then (((( id Z) (#) ( arccos * f1)) `| Z) . x) = (( arccos . (x / a)) - (x / (a * ( sqrt (1 - ((x / a) ^2 )))))) by A3, A7, FDIFF_7: 26

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

        hence thesis;

      end;

      ( dom ((( id Z) (#) ( arccos * f1)) `| Z)) = ( dom f) by A1, A8, FDIFF_1:def 7;

      then ((( id Z) (#) ( arccos * f1)) `| Z) = f by A15, PARTFUN1: 5;

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

    end;

    theorem :: INTEGR12:27

    A c= Z & f = ((n (#) (( #Z (n - 1)) * sin )) / (( #Z (n + 1)) * cos )) & 1 <= n & Z c= ( dom (( #Z n) * tan )) & Z = ( dom f) implies ( integral (f,A)) = (((( #Z n) * tan ) . ( upper_bound A)) - ((( #Z n) * tan ) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & f = ((n (#) (( #Z (n - 1)) * sin )) / (( #Z (n + 1)) * cos )) & 1 <= n & Z c= ( dom (( #Z n) * tan )) & Z = ( dom f);

      then Z = (( dom (n (#) (( #Z (n - 1)) * sin ))) /\ (( dom (( #Z (n + 1)) * cos )) \ ((( #Z (n + 1)) * cos ) " { 0 }))) by RFUNCT_1:def 1;

      then

       A2: Z c= ( dom (n (#) (( #Z (n - 1)) * sin ))) & Z c= (( dom (( #Z (n + 1)) * cos )) \ ((( #Z (n + 1)) * cos ) " { 0 })) by XBOOLE_1: 18;

      then

       A3: Z c= ( dom ((( #Z (n + 1)) * cos ) ^ )) by RFUNCT_1:def 2;

      ( dom ((( #Z (n + 1)) * cos ) ^ )) c= ( dom (( #Z (n + 1)) * cos )) by RFUNCT_1: 1;

      then

       A4: Z c= ( dom (( #Z (n + 1)) * cos )) by A3;

      

       A5: x in Z implies ((( #Z (n + 1)) * cos ) . x) <> 0

      proof

        assume x in Z;

        then x in (( dom (n (#) (( #Z (n - 1)) * sin ))) /\ (( dom (( #Z (n + 1)) * cos )) \ ((( #Z (n + 1)) * cos ) " { 0 }))) by A1, RFUNCT_1:def 1;

        then x in (( dom (( #Z (n + 1)) * cos )) \ ((( #Z (n + 1)) * cos ) " { 0 })) by XBOOLE_0:def 4;

        then x in ( dom ((( #Z (n + 1)) * cos ) ^ )) by RFUNCT_1:def 2;

        hence thesis by RFUNCT_1: 3;

      end;

      

       A6: Z c= ( dom (( #Z (n - 1)) * sin )) by A2, VALUED_1:def 5;

      

       A7: (( #Z (n - 1)) * sin ) is_differentiable_in x

      proof

        consider m be Nat such that

         A8: n = (m + 1) by A1, NAT_1: 6;

         sin is_differentiable_in x by SIN_COS: 64;

        hence thesis by A8, TAYLOR_1: 3;

      end;

      (( #Z (n - 1)) * sin ) is_differentiable_on Z

      proof

        for x st x in Z holds (( #Z (n - 1)) * sin ) is_differentiable_in x by A7;

        hence thesis by A6, FDIFF_1: 9;

      end;

      then

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

      

       A10: (( #Z (n + 1)) * cos ) is_differentiable_in x

      proof

         cos is_differentiable_in x by SIN_COS: 63;

        hence thesis by TAYLOR_1: 3;

      end;

      (( #Z (n + 1)) * cos ) is_differentiable_on Z

      proof

        for x st x in Z holds (( #Z (n + 1)) * cos ) is_differentiable_in x by A10;

        hence thesis by A4, FDIFF_1: 9;

      end;

      then (f | Z) is continuous by A1, A5, A9, FDIFF_1: 25, FDIFF_2: 21;

      then (f | A) is continuous by A1, FCONT_1: 16;

      then

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

      

       A12: (( #Z n) * tan ) is_differentiable_on Z by A1, FDIFF_8: 20;

      

       A13: for x st x in Z holds (f . x) = ((n * (( sin . x) #Z (n - 1))) / (( cos . x) #Z (n + 1)))

      proof

        let x;

        assume

         A14: x in Z;

        

        then (((n (#) (( #Z (n - 1)) * sin )) / (( #Z (n + 1)) * cos )) . x) = (((n (#) (( #Z (n - 1)) * sin )) . x) / ((( #Z (n + 1)) * cos ) . x)) by A1, RFUNCT_1:def 1

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

        .= ((n * (( #Z (n - 1)) . ( sin . x))) / ((( #Z (n + 1)) * cos ) . x)) by A6, A14, FUNCT_1: 12

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

        .= ((n * (( sin . x) #Z (n - 1))) / (( #Z (n + 1)) . ( cos . x))) by A4, A14, FUNCT_1: 12

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

        hence thesis by A1;

      end;

      

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

      proof

        let x be Element of REAL ;

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

        then

         A16: x in Z by A12, FDIFF_1:def 7;

        

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

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

        hence thesis;

      end;

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

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

      hence thesis by A1, A11, FDIFF_8: 20, INTEGRA5: 13;

    end;

    theorem :: INTEGR12:28

    A c= Z & f = ((n (#) (( #Z (n - 1)) * cos )) / (( #Z (n + 1)) * sin )) & 1 <= n & Z c= ( dom (( #Z n) * cot )) & Z = ( dom f) implies ( integral (f,A)) = ((( - (( #Z n) * cot )) . ( upper_bound A)) - (( - (( #Z n) * cot )) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & f = ((n (#) (( #Z (n - 1)) * cos )) / (( #Z (n + 1)) * sin )) & 1 <= n & Z c= ( dom (( #Z n) * cot )) & Z = ( dom f);

      then Z = (( dom (n (#) (( #Z (n - 1)) * cos ))) /\ (( dom (( #Z (n + 1)) * sin )) \ ((( #Z (n + 1)) * sin ) " { 0 }))) by RFUNCT_1:def 1;

      then

       A2: Z c= ( dom (n (#) (( #Z (n - 1)) * cos ))) & Z c= (( dom (( #Z (n + 1)) * sin )) \ ((( #Z (n + 1)) * sin ) " { 0 })) by XBOOLE_1: 18;

      then

       A3: Z c= ( dom ((( #Z (n + 1)) * sin ) ^ )) by RFUNCT_1:def 2;

      ( dom ((( #Z (n + 1)) * sin ) ^ )) c= ( dom (( #Z (n + 1)) * sin )) by RFUNCT_1: 1;

      then

       A4: Z c= ( dom (( #Z (n + 1)) * sin )) by A3;

      

       A5: x in Z implies ((( #Z (n + 1)) * sin ) . x) <> 0

      proof

        assume x in Z;

        then x in (( dom (n (#) (( #Z (n - 1)) * cos ))) /\ (( dom (( #Z (n + 1)) * sin )) \ ((( #Z (n + 1)) * sin ) " { 0 }))) by A1, RFUNCT_1:def 1;

        then x in (( dom (( #Z (n + 1)) * sin )) \ ((( #Z (n + 1)) * sin ) " { 0 })) by XBOOLE_0:def 4;

        then x in ( dom ((( #Z (n + 1)) * sin ) ^ )) by RFUNCT_1:def 2;

        hence thesis by RFUNCT_1: 3;

      end;

      

       A6: Z c= ( dom (( #Z (n - 1)) * cos )) by A2, VALUED_1:def 5;

      

       A7: (( #Z (n - 1)) * cos ) is_differentiable_in x

      proof

        consider m be Nat such that

         A8: n = (m + 1) by A1, NAT_1: 6;

         cos is_differentiable_in x by SIN_COS: 63;

        hence thesis by A8, TAYLOR_1: 3;

      end;

      (( #Z (n - 1)) * cos ) is_differentiable_on Z

      proof

        for x st x in Z holds (( #Z (n - 1)) * cos ) is_differentiable_in x by A7;

        hence thesis by A6, FDIFF_1: 9;

      end;

      then

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

      

       A10: (( #Z (n + 1)) * sin ) is_differentiable_in x

      proof

         sin is_differentiable_in x by SIN_COS: 64;

        hence thesis by TAYLOR_1: 3;

      end;

      (( #Z (n + 1)) * sin ) is_differentiable_on Z

      proof

        for x st x in Z holds (( #Z (n + 1)) * sin ) is_differentiable_in x by A10;

        hence thesis by A4, FDIFF_1: 9;

      end;

      then (f | Z) is continuous by A1, A5, A9, FDIFF_1: 25, FDIFF_2: 21;

      then (f | A) is continuous by A1, FCONT_1: 16;

      then

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

      

       A12: (( #Z n) * cot ) is_differentiable_on Z by A1, FDIFF_8: 21;

      

       A13: ( dom (( #Z n) * cot )) c= ( dom cot ) by RELAT_1: 25;

      

       A14: Z c= ( dom ( - (( #Z n) * cot ))) by A1, VALUED_1: 8;

      then

       A15: (( - 1) (#) (( #Z n) * cot )) is_differentiable_on Z by A12, FDIFF_1: 20;

      

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

      proof

        let x;

        assume x in Z;

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

        hence thesis by FDIFF_8: 2;

      end;

      

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

      proof

        let x;

        assume

         A18: x in Z;

        then

         A19: ( sin . x) <> 0 by A16;

        then

         A20: cot is_differentiable_in x by FDIFF_7: 47;

        consider m be Nat such that

         A21: n = (m + 1) by A1, NAT_1: 6;

        set m = (n - 1);

        

         A22: (( #Z n) * cot ) is_differentiable_in x by A12, A18, FDIFF_1: 9;

        ((( - (( #Z n) * cot )) `| Z) . x) = ( diff (( - (( #Z n) * cot )),x)) by A15, A18, FDIFF_1:def 7

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

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

        .= (( - 1) * ((n * (( cot . x) #Z (n - 1))) * ( - (1 / (( sin . x) ^2 ))))) by A19, FDIFF_7: 47

        .= (( - 1) * ( - ((n * (( cot . x) #Z (n - 1))) / (( sin . x) ^2 ))))

        .= (( - 1) * ( - ((n * ((( cos . x) #Z m) / (( sin . x) #Z m))) / (( sin . x) ^2 )))) by A1, A13, A18, A21, FDIFF_8: 3, XBOOLE_1: 1

        .= (( - 1) * ( - (((n * (( cos . x) #Z (n - 1))) / (( sin . x) #Z (n - 1))) / (( sin . x) ^2 ))))

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

        .= (( - 1) * ( - ((n * (( cos . x) #Z (n - 1))) / ((( sin . x) #Z (n - 1)) * (( sin . x) #Z 2))))) by FDIFF_7: 1

        .= (( - 1) * ( - ((n * (( cos . x) #Z (n - 1))) / (( sin . x) #Z ((n - 1) + 2))))) by A16, A18, PREPOWER: 44

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

        hence thesis;

      end;

      

       A23: for x st x in Z holds (f . x) = ((n * (( cos . x) #Z (n - 1))) / (( sin . x) #Z (n + 1)))

      proof

        let x;

        assume

         A24: x in Z;

        

        then (((n (#) (( #Z (n - 1)) * cos )) / (( #Z (n + 1)) * sin )) . x) = (((n (#) (( #Z (n - 1)) * cos )) . x) / ((( #Z (n + 1)) * sin ) . x)) by A1, RFUNCT_1:def 1

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

        .= ((n * (( #Z (n - 1)) . ( cos . x))) / ((( #Z (n + 1)) * sin ) . x)) by A6, A24, FUNCT_1: 12

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

        .= ((n * (( cos . x) #Z (n - 1))) / (( #Z (n + 1)) . ( sin . x))) by A4, A24, FUNCT_1: 12

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

        hence thesis by A1;

      end;

      

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

      proof

        let x be Element of REAL ;

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

        then

         A26: x in Z by A15, FDIFF_1:def 7;

        

        then ((( - (( #Z n) * cot )) `| Z) . x) = ((n * (( cos . x) #Z (n - 1))) / (( sin . x) #Z (n + 1))) by A17

        .= (f . x) by A23, A26;

        hence thesis;

      end;

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

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

      hence thesis by A1, A11, A12, A14, FDIFF_1: 20, INTEGRA5: 13;

    end;

    theorem :: INTEGR12:29

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

    proof

      assume

       A1: A c= Z & Z c= ( dom ( tan * f1)) & f = ((( sin * f1) ^2 ) / (( cos * f1) ^2 )) & (for x st x in Z holds (f1 . x) = (a * x) & a <> 0 ) & Z = ( dom f);

      then

       A2: Z c= ( dom ((1 / a) (#) ( tan * f1))) by VALUED_1:def 5;

      Z c= (( dom ((1 / a) (#) ( tan * f1))) /\ ( dom ( id Z))) by A2, XBOOLE_1: 19;

      then

       A3: Z c= ( dom (((1 / a) (#) ( tan * f1)) - ( id Z))) by VALUED_1: 12;

      

       A4: for x st x in Z holds (f1 . x) = ((a * x) + 0 ) by A1;

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

      then

       A5: Z c= ( dom (( sin * f1) ^2 )) & Z c= (( dom (( cos * f1) ^2 )) \ ((( cos * f1) ^2 ) " { 0 })) by XBOOLE_1: 18;

      then

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

      

       A7: Z c= ( dom ((( cos * f1) ^2 ) ^ )) by A5, RFUNCT_1:def 2;

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

      then Z c= ( dom (( cos * f1) ^2 )) by A7;

      then

       A8: Z c= ( dom ( cos * f1)) by VALUED_1: 11;

      

       A9: ( sin * f1) is_differentiable_on Z by A6, A4, FDIFF_4: 37;

      

       A10: ( cos * f1) is_differentiable_on Z by A4, A8, FDIFF_4: 38;

      

       A11: (( sin * f1) ^2 ) is_differentiable_on Z by A9, FDIFF_2: 20;

      

       A12: (( cos * f1) ^2 ) is_differentiable_on Z by A10, FDIFF_2: 20;

      x in Z implies ((( cos * f1) ^2 ) . x) <> 0

      proof

        assume x in Z;

        then x in (( dom (( sin * f1) ^2 )) /\ (( dom (( cos * f1) ^2 )) \ ((( cos * f1) ^2 ) " { 0 }))) by A1, RFUNCT_1:def 1;

        then x in (( dom (( cos * f1) ^2 )) \ ((( cos * f1) ^2 ) " { 0 })) by XBOOLE_0:def 4;

        then x in ( dom ((( cos * f1) ^2 ) ^ )) by RFUNCT_1:def 2;

        hence thesis by RFUNCT_1: 3;

      end;

      then f is_differentiable_on Z by A1, A11, A12, FDIFF_2: 21;

      then (f | Z) is continuous by FDIFF_1: 25;

      then (f | A) is continuous by A1, FCONT_1: 16;

      then

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

      

       A14: (((1 / a) (#) ( tan * f1)) - ( id Z)) is_differentiable_on Z by A1, A3, FDIFF_8: 26;

      

       A15: for x st x in Z holds (f . x) = ((( sin . (a * x)) ^2 ) / (( cos . (a * x)) ^2 ))

      proof

        let x;

        assume

         A16: x in Z;

        

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

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

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

        .= ((( sin . (f1 . x)) ^2 ) / ((( cos * f1) . x) ^2 )) by A6, A16, FUNCT_1: 12

        .= ((( sin . (f1 . x)) ^2 ) / (( cos . (f1 . x)) ^2 )) by A8, A16, FUNCT_1: 12

        .= ((( sin . (a * x)) ^2 ) / (( cos . (f1 . x)) ^2 )) by A16, A1

        .= ((( sin . (a * x)) ^2 ) / (( cos . (a * x)) ^2 )) by A16, A1;

        hence thesis by A1;

      end;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

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

        .= (f . x) by A15, A18;

        hence thesis;

      end;

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

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

      hence thesis by A1, A13, A14, INTEGRA5: 13;

    end;

    theorem :: INTEGR12:30

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

    proof

      assume

       A1: A c= Z & Z c= ( dom ( cot * f1)) & f = ((( cos * f1) ^2 ) / (( sin * f1) ^2 )) & (for x st x in Z holds (f1 . x) = (a * x) & a <> 0 ) & Z = ( dom f);

      then

       A2: Z c= ( dom (( - (1 / a)) (#) ( cot * f1))) by VALUED_1:def 5;

      Z c= (( dom (( - (1 / a)) (#) ( cot * f1))) /\ ( dom ( id Z))) by A2, XBOOLE_1: 19;

      then

       A3: Z c= ( dom ((( - (1 / a)) (#) ( cot * f1)) - ( id Z))) by VALUED_1: 12;

      

       A4: for x st x in Z holds (f1 . x) = ((a * x) + 0 ) by A1;

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

      then

       A5: Z c= ( dom (( cos * f1) ^2 )) & Z c= (( dom (( sin * f1) ^2 )) \ ((( sin * f1) ^2 ) " { 0 })) by XBOOLE_1: 18;

      then

       A6: Z c= ( dom ( cos * f1)) by VALUED_1: 11;

      

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

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

      then Z c= ( dom (( sin * f1) ^2 )) by A7;

      then

       A8: Z c= ( dom ( sin * f1)) by VALUED_1: 11;

      then

       A9: ( sin * f1) is_differentiable_on Z by A4, FDIFF_4: 37;

      

       A10: ( cos * f1) is_differentiable_on Z by A4, A6, FDIFF_4: 38;

      

       A11: (( sin * f1) ^2 ) is_differentiable_on Z by A9, FDIFF_2: 20;

      

       A12: (( cos * f1) ^2 ) is_differentiable_on Z by A10, FDIFF_2: 20;

      x in Z implies ((( sin * f1) ^2 ) . x) <> 0

      proof

        assume x in Z;

        then x in (( dom (( cos * f1) ^2 )) /\ (( dom (( sin * f1) ^2 )) \ ((( sin * f1) ^2 ) " { 0 }))) by A1, RFUNCT_1:def 1;

        then x in (( dom (( sin * f1) ^2 )) \ ((( sin * f1) ^2 ) " { 0 })) by XBOOLE_0:def 4;

        then x in ( dom ((( sin * f1) ^2 ) ^ )) by RFUNCT_1:def 2;

        hence thesis by RFUNCT_1: 3;

      end;

      then f is_differentiable_on Z by A1, A11, A12, FDIFF_2: 21;

      then (f | Z) is continuous by FDIFF_1: 25;

      then (f | A) is continuous by A1, FCONT_1: 16;

      then

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

      

       A14: ((( - (1 / a)) (#) ( cot * f1)) - ( id Z)) is_differentiable_on Z by A1, A3, FDIFF_8: 27;

      

       A15: for x st x in Z holds (f . x) = ((( cos . (a * x)) ^2 ) / (( sin . (a * x)) ^2 ))

      proof

        let x;

        assume

         A16: x in Z;

        

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

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

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

        .= ((( cos . (f1 . x)) ^2 ) / ((( sin * f1) . x) ^2 )) by A6, A16, FUNCT_1: 12

        .= ((( cos . (f1 . x)) ^2 ) / (( sin . (f1 . x)) ^2 )) by A8, A16, FUNCT_1: 12

        .= ((( cos . (a * x)) ^2 ) / (( sin . (f1 . x)) ^2 )) by A16, A1

        .= ((( cos . (a * x)) ^2 ) / (( sin . (a * x)) ^2 )) by A16, A1;

        hence thesis by A1;

      end;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

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

        .= (f . x) by A15, A18;

        hence thesis;

      end;

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

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

      hence thesis by A1, A13, A14, INTEGRA5: 13;

    end;

    theorem :: INTEGR12:31

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

    proof

      assume

       A1: A c= Z & (for x st x in Z holds (f1 . x) = ((a * x) + b)) & Z = ( dom f) & f = ((a (#) ( sin / cos )) + (f1 / ( cos ^2 )));

      then

       A2: Z = (( dom (a (#) ( sin / cos ))) /\ ( dom (f1 / ( cos ^2 )))) by VALUED_1:def 1;

      then

       A3: Z c= ( dom (a (#) ( sin / cos ))) by XBOOLE_1: 18;

      then

       A4: Z c= ( dom ( sin / cos )) by VALUED_1:def 5;

      

       A5: Z c= ( dom (f1 / ( cos ^2 ))) by A2, XBOOLE_1: 18;

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

      then

       A6: Z c= ( dom f1) by A5, XBOOLE_1: 18;

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

      then

       A7: Z c= ( dom (f1 (#) tan )) by VALUED_1:def 4;

      for x st x in Z holds ( sin / cos ) is_differentiable_in x

      proof

        let x;

        assume x in Z;

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

        hence thesis by FDIFF_7: 46;

      end;

      then ( sin / cos ) is_differentiable_on Z by A4, FDIFF_1: 9;

      then

       A8: (a (#) ( sin / cos )) is_differentiable_on Z by A3, FDIFF_1: 20;

      

       A9: f1 is_differentiable_on Z by A1, A6, FDIFF_1: 23;

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

      then

       A10: ( cos ^2 ) is_differentiable_on Z by FDIFF_2: 20;

      x in Z implies (( cos ^2 ) . x) <> 0

      proof

        assume x in Z;

        then x in ( dom (f1 / ( cos ^2 ))) by A5;

        then x in (( dom f1) /\ (( dom ( cos ^2 )) \ (( cos ^2 ) " { 0 }))) by RFUNCT_1:def 1;

        then x in (( dom ( cos ^2 )) \ (( cos ^2 ) " { 0 })) by XBOOLE_0:def 4;

        then x in ( dom (( cos ^2 ) ^ )) by RFUNCT_1:def 2;

        hence thesis by RFUNCT_1: 3;

      end;

      then (f1 / ( cos ^2 )) is_differentiable_on Z by A9, A10, FDIFF_2: 21;

      then (f | Z) is continuous by A1, A8, FDIFF_1: 18, FDIFF_1: 25;

      then (f | A) is continuous by A1, FCONT_1: 16;

      then

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

      

       A12: (f1 (#) tan ) is_differentiable_on Z by A1, A7, FDIFF_8: 28;

      

       A13: for x st x in Z holds (f . x) = (((a * ( sin . x)) / ( cos . x)) + (((a * x) + b) / (( cos . x) ^2 )))

      proof

        let x;

        assume

         A14: x in Z;

        

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

        .= ((a * (( sin / cos ) . x)) + ((f1 / ( cos ^2 )) . x)) by VALUED_1: 6

        .= ((a * (( sin . x) / ( cos . x))) + ((f1 / ( cos ^2 )) . x)) by A14, A4, RFUNCT_1:def 1

        .= (((a * ( sin . x)) / ( cos . x)) + ((f1 . x) / (( cos ^2 ) . x))) by A14, A5, RFUNCT_1:def 1

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

        .= (((a * ( sin . x)) / ( cos . x)) + (((a * x) + b) / (( cos . x) ^2 ))) by A1, A14;

        hence thesis by A1;

      end;

      

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

      proof

        let x be Element of REAL ;

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

        then

         A16: x in Z by A12, FDIFF_1:def 7;

        

        then (((f1 (#) tan ) `| Z) . x) = (((a * ( sin . x)) / ( cos . x)) + (((a * x) + b) / (( cos . x) ^2 ))) by A1, A7, FDIFF_8: 28

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

        hence thesis;

      end;

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

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

      hence thesis by A1, A11, A7, FDIFF_8: 28, INTEGRA5: 13;

    end;

    theorem :: INTEGR12:32

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

    proof

      assume

       A1: A c= Z & (for x st x in Z holds (f1 . x) = ((a * x) + b)) & Z = ( dom f) & f = ((a (#) ( cos / sin )) - (f1 / ( sin ^2 )));

      then

       A2: Z = (( dom (a (#) ( cos / sin ))) /\ ( dom ( - (f1 / ( sin ^2 ))))) by VALUED_1:def 1;

      then

       A3: Z c= ( dom (a (#) ( cos / sin ))) by XBOOLE_1: 18;

      then

       A4: Z c= ( dom ( cos / sin )) by VALUED_1:def 5;

      Z c= ( dom ( - (f1 / ( sin ^2 )))) by A2, XBOOLE_1: 18;

      then

       A5: Z c= ( dom (f1 / ( sin ^2 ))) by VALUED_1: 8;

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

      then

       A6: Z c= ( dom f1) by A5, XBOOLE_1: 18;

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

      then

       A7: Z c= ( dom (f1 (#) cot )) by VALUED_1:def 4;

      for x st x in Z holds ( cos / sin ) is_differentiable_in x

      proof

        let x;

        assume x in Z;

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

        hence thesis by FDIFF_7: 47;

      end;

      then ( cos / sin ) is_differentiable_on Z by A4, FDIFF_1: 9;

      then

       A8: (a (#) ( cos / sin )) is_differentiable_on Z by A3, FDIFF_1: 20;

      

       A9: f1 is_differentiable_on Z by A1, A6, FDIFF_1: 23;

       sin is_differentiable_on Z by FDIFF_1: 26, SIN_COS: 68;

      then

       A10: ( sin ^2 ) is_differentiable_on Z by FDIFF_2: 20;

      x in Z implies (( sin ^2 ) . x) <> 0

      proof

        assume x in Z;

        then x in ( dom (f1 / ( sin ^2 ))) by A5;

        then x in (( dom f1) /\ (( dom ( sin ^2 )) \ (( sin ^2 ) " { 0 }))) by RFUNCT_1:def 1;

        then x in (( dom ( sin ^2 )) \ (( sin ^2 ) " { 0 })) by XBOOLE_0:def 4;

        then x in ( dom (( sin ^2 ) ^ )) by RFUNCT_1:def 2;

        hence thesis by RFUNCT_1: 3;

      end;

      then (f1 / ( sin ^2 )) is_differentiable_on Z by A9, A10, FDIFF_2: 21;

      then (f | Z) is continuous by A1, A8, FDIFF_1: 19, FDIFF_1: 25;

      then (f | A) is continuous by A1, FCONT_1: 16;

      then

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

      

       A12: (f1 (#) cot ) is_differentiable_on Z by A1, A7, FDIFF_8: 29;

      

       A13: for x st x in Z holds (f . x) = (((a * ( cos . x)) / ( sin . x)) - (((a * x) + b) / (( sin . x) ^2 )))

      proof

        let x;

        assume

         A14: x in Z;

        

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

        .= ((a * (( cos / sin ) . x)) - ((f1 / ( sin ^2 )) . x)) by VALUED_1: 6

        .= ((a * (( cos . x) / ( sin . x))) - ((f1 / ( sin ^2 )) . x)) by A14, A4, RFUNCT_1:def 1

        .= (((a * ( cos . x)) / ( sin . x)) - ((f1 . x) / (( sin ^2 ) . x))) by A14, A5, RFUNCT_1:def 1

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

        .= (((a * ( cos . x)) / ( sin . x)) - (((a * x) + b) / (( sin . x) ^2 ))) by A1, A14;

        hence thesis by A1;

      end;

      

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

      proof

        let x be Element of REAL ;

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

        then

         A16: x in Z by A12, FDIFF_1:def 7;

        

        then (((f1 (#) cot ) `| Z) . x) = (((a * ( cos . x)) / ( sin . x)) - (((a * x) + b) / (( sin . x) ^2 ))) by A1, A7, FDIFF_8: 29

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

        hence thesis;

      end;

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

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

      hence thesis by A1, A11, A7, FDIFF_8: 29, INTEGRA5: 13;

    end;

    theorem :: INTEGR12:33

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

    proof

      assume

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

      then

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

      

       A3: ( tan - ( id Z)) is_differentiable_on Z by A1, FDIFF_8: 24;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

        then ((( tan - ( id Z)) `| Z) . x) = ((( sin . x) ^2 ) / (( cos . x) ^2 )) by A1, FDIFF_8: 24

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

        hence thesis;

      end;

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

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

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

    end;

    theorem :: INTEGR12:34

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

    proof

      assume

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

      then

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

      

       A3: (( - cot ) - ( id Z)) is_differentiable_on Z by A1, FDIFF_8: 25;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

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

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

        hence thesis;

      end;

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

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

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

    end;

    theorem :: INTEGR12:35

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

    proof

      assume

       A1: A c= Z & (for x st x in Z holds (f . x) = (1 / (x * (1 + (( ln . x) ^2 )))) & ( ln . x) > ( - 1) & ( ln . x) < 1) & Z c= ( dom ( arctan * ln )) & Z = ( dom f) & (f | A) is continuous;

      then

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

      

       A3: for x st x in Z holds ( ln . x) > ( - 1) & ( ln . x) < 1 by A1;

      then

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

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

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

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

        hence thesis;

      end;

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

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

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

    end;

    theorem :: INTEGR12:36

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

    proof

      assume

       A1: A c= Z & (for x st x in Z holds (f . x) = ( - (1 / (x * (1 + (( ln . x) ^2 ))))) & ( ln . x) > ( - 1) & ( ln . x) < 1) & Z c= ( dom ( arccot * ln )) & Z = ( dom f) & (f | A) is continuous;

      then

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

      

       A3: for x st x in Z holds ( ln . x) > ( - 1) & ( ln . x) < 1 by A1;

      then

       A4: ( arccot * ln ) is_differentiable_on Z by A1, SIN_COS9: 118;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

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

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

        hence thesis;

      end;

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

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

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

    end;

    theorem :: INTEGR12:37

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

    proof

      assume

       A1: A c= Z & (for x st x in Z holds (f . x) = (a / ( sqrt (1 - (((a * x) + b) ^2 )))) & (f1 . x) = ((a * x) + b) & (f1 . x) > ( - 1) & (f1 . x) < 1) & Z c= ( dom ( arcsin * f1)) & Z = ( dom f) & (f | A) is continuous;

      then

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

      

       A3: for x st x in Z holds (f1 . x) = ((a * x) + b) & (f1 . x) > ( - 1) & (f1 . x) < 1 by A1;

      then

       A4: ( arcsin * f1) is_differentiable_on Z by A1, FDIFF_7: 14;

      

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

      proof

        let x be Element of REAL ;

        assume x in ( dom (( arcsin * f1) `| Z));

        then

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

        

        then ((( arcsin * f1) `| Z) . x) = (a / ( sqrt (1 - (((a * x) + b) ^2 )))) by A1, A3, FDIFF_7: 14

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

        hence thesis;

      end;

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

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

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

    end;

    theorem :: INTEGR12:38

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

    proof

      assume

       A1: A c= Z & (for x st x in Z holds (f . x) = (a / ( sqrt (1 - (((a * x) + b) ^2 )))) & (f1 . x) = ((a * x) + b) & (f1 . x) > ( - 1) & (f1 . x) < 1) & Z c= ( dom ( arccos * f1)) & Z = ( dom f) & (f | A) is continuous;

      then

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

      

       A3: for x st x in Z holds (f1 . x) = ((a * x) + b) by A1;

      

       A4: for x st x in Z holds (f1 . x) = ((a * x) + b) & (f1 . x) > ( - 1) & (f1 . x) < 1 by A1;

      

       A5: Z c= ( dom ( - ( arccos * f1))) by A1, VALUED_1: 8;

      

       A6: ( arccos * f1) is_differentiable_on Z by A1, A4, FDIFF_7: 15;

      then

       A7: (( - 1) (#) ( arccos * f1)) is_differentiable_on Z by A5, FDIFF_1: 20;

      for y be object st y in Z holds y in ( dom f1) by A1, FUNCT_1: 11;

      then

       A8: Z c= ( dom f1);

      then

       A9: f1 is_differentiable_on Z & for x st x in Z holds ((f1 `| Z) . x) = a by A3, FDIFF_1: 23;

      

       A10: for x st x in Z holds ((( - ( arccos * f1)) `| Z) . x) = (a / ( sqrt (1 - (((a * x) + b) ^2 ))))

      proof

        let x;

        assume

         A11: x in Z;

        then

         A12: f1 is_differentiable_in x by A9, FDIFF_1: 9;

        

         A13: (f1 . x) > ( - 1) & (f1 . x) < 1 by A1, A11;

        

         A14: ( arccos * f1) is_differentiable_in x by A6, A11, FDIFF_1: 9;

        ((( - ( arccos * f1)) `| Z) . x) = ( diff (( - ( arccos * f1)),x)) by A7, A11, FDIFF_1:def 7

        .= (( - 1) * ( diff (( arccos * f1),x))) by A14, FDIFF_1: 15

        .= (( - 1) * ( - (( diff (f1,x)) / ( sqrt (1 - ((f1 . x) ^2 )))))) by A12, A13, FDIFF_7: 7

        .= (( - 1) * ( - (((f1 `| Z) . x) / ( sqrt (1 - ((f1 . x) ^2 )))))) by A9, A11, FDIFF_1:def 7

        .= (( - 1) * ( - (a / ( sqrt (1 - ((f1 . x) ^2 )))))) by A3, A8, A11, FDIFF_1: 23

        .= (a / ( sqrt (1 - (((a * x) + b) ^2 )))) by A1, A11;

        hence thesis;

      end;

      

       A15: for x be Element of REAL st x in ( dom (( - ( arccos * f1)) `| Z)) holds ((( - ( arccos * f1)) `| Z) . x) = (f . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom (( - ( arccos * f1)) `| Z));

        then

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

        

        then ((( - ( arccos * f1)) `| Z) . x) = (a / ( sqrt (1 - (((a * x) + b) ^2 )))) by A10

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

        hence thesis;

      end;

      ( dom (( - ( arccos * f1)) `| Z)) = ( dom f) by A1, A7, FDIFF_1:def 7;

      then (( - ( arccos * f1)) `| Z) = f by A15, PARTFUN1: 5;

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

    end;

    theorem :: INTEGR12:39

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

    proof

      assume

       A1: A c= Z & f1 = (g - f2) & f2 = ( #Z 2) & (for x st x in Z holds (f . x) = (x * ((1 - (x #Z 2)) #R ( - (1 / 2)))) & (g . x) = 1 & (f1 . x) > 0 ) & Z c= ( dom (( #R (1 / 2)) * f1)) & Z = ( dom f) & (f | A) is continuous;

      then

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

      

       A3: for x st x in Z holds (g . x) = 1 & (f1 . x) > 0 by A1;

      

       A4: Z c= ( dom ( - (( #R (1 / 2)) * f1))) by A1, VALUED_1: 8;

      for y be object st y in Z holds y in ( dom f1) by A1, FUNCT_1: 11;

      then

       A5: Z c= ( dom (g + (( - 1) (#) f2))) by A1;

      

       A6: (( #R (1 / 2)) * f1) is_differentiable_on Z by A1, A3, FDIFF_7: 22;

      then

       A7: (( - 1) (#) (( #R (1 / 2)) * f1)) is_differentiable_on Z by A4, FDIFF_1: 20;

      

       A8: f2 = ( #Z 2) & for x st x in Z holds (g . x) = (1 + ( 0 * x)) by A1;

      then

       A9: f1 is_differentiable_on Z & for x st x in Z holds ((f1 `| Z) . x) = ( 0 + ((2 * ( - 1)) * x)) by A1, A5, FDIFF_4: 12;

      

       A10: for x st x in Z holds ((( - (( #R (1 / 2)) * f1)) `| Z) . x) = (x * ((1 - (x #Z 2)) #R ( - (1 / 2))))

      proof

        let x;

        assume

         A11: x in Z;

        then

         A12: x in ( dom (g - f2)) by A1, FUNCT_1: 11;

        

         A13: f1 is_differentiable_in x by A9, A11, FDIFF_1: 9;

        

         A14: ((g - f2) . x) = ((g . x) - (f2 . x)) by A12, VALUED_1: 13

        .= (1 - (f2 . x)) by A1, A11

        .= (1 - (x #Z 2)) by A1, TAYLOR_1:def 1;

        then

         A15: (f1 . x) = (1 - (x #Z 2)) & (f1 . x) > 0 by A1, A11;

        

         A16: (( #R (1 / 2)) * f1) is_differentiable_in x by A6, A11, FDIFF_1: 9;

        ((( - (( #R (1 / 2)) * f1)) `| Z) . x) = ( diff (( - (( #R (1 / 2)) * f1)),x)) by A7, A11, FDIFF_1:def 7

        .= (( - 1) * ( diff ((( #R (1 / 2)) * f1),x))) by A16, FDIFF_1: 15

        .= (( - 1) * (((1 / 2) * ((f1 . x) #R ((1 / 2) - 1))) * ( diff (f1,x)))) by A13, A15, TAYLOR_1: 22

        .= (( - 1) * (((1 / 2) * ((f1 . x) #R ((1 / 2) - 1))) * ((f1 `| Z) . x))) by A9, A11, FDIFF_1:def 7

        .= (( - 1) * (((1 / 2) * ((f1 . x) #R ((1 / 2) - 1))) * ( 0 + ((2 * ( - 1)) * x)))) by A1, A5, A8, A11, FDIFF_4: 12

        .= (x * ((1 - (x #Z 2)) #R ( - (1 / 2)))) by A1, A14;

        hence thesis;

      end;

      

       A17: for x be Element of REAL st x in ( dom (( - (( #R (1 / 2)) * f1)) `| Z)) holds ((( - (( #R (1 / 2)) * f1)) `| Z) . x) = (f . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom (( - (( #R (1 / 2)) * f1)) `| Z));

        then

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

        

        then ((( - (( #R (1 / 2)) * f1)) `| Z) . x) = (x * ((1 - (x #Z 2)) #R ( - (1 / 2)))) by A10

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

        hence thesis;

      end;

      ( dom (( - (( #R (1 / 2)) * f1)) `| Z)) = ( dom f) by A1, A7, FDIFF_1:def 7;

      then (( - (( #R (1 / 2)) * f1)) `| Z) = f by A17, PARTFUN1: 5;

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

    end;

    theorem :: INTEGR12:40

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

    proof

      assume

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

      then

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

      

       A3: for x st x in Z holds (f1 . x) = (a ^2 ) & (g . x) > 0 by A1;

      

       A4: Z c= ( dom ( - (( #R (1 / 2)) * g))) by A1, VALUED_1: 8;

      for y be object st y in Z holds y in ( dom g) by A1, FUNCT_1: 11;

      then

       A5: Z c= ( dom (f1 + (( - 1) (#) f2))) by A1;

      

       A6: (( #R (1 / 2)) * g) is_differentiable_on Z by A1, A3, FDIFF_7: 27;

      then

       A7: (( - 1) (#) (( #R (1 / 2)) * g)) is_differentiable_on Z by A4, FDIFF_1: 20;

      

       A8: f2 = ( #Z 2) & for x st x in Z holds (f1 . x) = ((a ^2 ) + ( 0 * x)) by A1;

      then

       A9: g is_differentiable_on Z & for x st x in Z holds ((g `| Z) . x) = ( 0 + ((2 * ( - 1)) * x)) by A1, A5, FDIFF_4: 12;

      

       A10: for x st x in Z holds ((( - (( #R (1 / 2)) * g)) `| Z) . x) = (x * (((a ^2 ) - (x #Z 2)) #R ( - (1 / 2))))

      proof

        let x;

        assume

         A11: x in Z;

        then

         A12: x in ( dom (f1 - f2)) by A1, FUNCT_1: 11;

        

         A13: g is_differentiable_in x by A9, A11, FDIFF_1: 9;

        

         A14: ((f1 - f2) . x) = ((f1 . x) - (f2 . x)) by A12, VALUED_1: 13

        .= ((a ^2 ) - (f2 . x)) by A1, A11

        .= ((a ^2 ) - (x #Z 2)) by A1, TAYLOR_1:def 1;

        then

         A15: (g . x) = ((a ^2 ) - (x #Z 2)) & (g . x) > 0 by A1, A11;

        

         A16: (( #R (1 / 2)) * g) is_differentiable_in x by A6, A11, FDIFF_1: 9;

        ((( - (( #R (1 / 2)) * g)) `| Z) . x) = ( diff (( - (( #R (1 / 2)) * g)),x)) by A7, A11, FDIFF_1:def 7

        .= (( - 1) * ( diff ((( #R (1 / 2)) * g),x))) by A16, FDIFF_1: 15

        .= (( - 1) * (((1 / 2) * ((g . x) #R ((1 / 2) - 1))) * ( diff (g,x)))) by A13, A15, TAYLOR_1: 22

        .= (( - 1) * (((1 / 2) * ((g . x) #R ((1 / 2) - 1))) * ((g `| Z) . x))) by A9, A11, FDIFF_1:def 7

        .= (( - 1) * (((1 / 2) * ((g . x) #R ((1 / 2) - 1))) * ( 0 + ((2 * ( - 1)) * x)))) by A1, A5, A8, A11, FDIFF_4: 12

        .= (x * (((a ^2 ) - (x #Z 2)) #R ( - (1 / 2)))) by A1, A14;

        hence thesis;

      end;

      

       A17: for x be Element of REAL st x in ( dom (( - (( #R (1 / 2)) * g)) `| Z)) holds ((( - (( #R (1 / 2)) * g)) `| Z) . x) = (f . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom (( - (( #R (1 / 2)) * g)) `| Z));

        then

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

        

        then ((( - (( #R (1 / 2)) * g)) `| Z) . x) = (x * (((a ^2 ) - (x #Z 2)) #R ( - (1 / 2)))) by A10

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

        hence thesis;

      end;

      ( dom (( - (( #R (1 / 2)) * g)) `| Z)) = ( dom f) by A1, A7, FDIFF_1:def 7;

      then (( - (( #R (1 / 2)) * g)) `| Z) = f by A17, PARTFUN1: 5;

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

    end;

    theorem :: INTEGR12:41

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

    proof

      assume

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

      then

       A2: Z c= ( dom (( - (1 / n)) (#) (( #Z n) * ( sin ^ )))) by VALUED_1:def 5;

      

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

      

       A4: for x st x in Z holds ( sin . x) <> 0 by A1;

      then

       A5: (( - (1 / n)) (#) (( #Z n) * ( sin ^ ))) is_differentiable_on Z by A1, A2, FDIFF_7: 30;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

        then (((( - (1 / n)) (#) (( #Z n) * ( sin ^ ))) `| Z) . x) = (( cos . x) / (( sin . x) #Z (n + 1))) by A1, A2, A4, FDIFF_7: 30

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

        hence thesis;

      end;

      ( dom ((( - (1 / n)) (#) (( #Z n) * ( sin ^ ))) `| Z)) = ( dom f) by A1, A5, FDIFF_1:def 7;

      then ((( - (1 / n)) (#) (( #Z n) * ( sin ^ ))) `| Z) = f by A6, PARTFUN1: 5;

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

    end;

    theorem :: INTEGR12:42

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

    proof

      assume

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

      then

       A2: Z c= ( dom ((1 / n) (#) (( #Z n) * ( cos ^ )))) by VALUED_1:def 5;

      

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

      

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

      then

       A5: ((1 / n) (#) (( #Z n) * ( cos ^ ))) is_differentiable_on Z by A1, A2, FDIFF_7: 31;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

        then ((((1 / n) (#) (( #Z n) * ( cos ^ ))) `| Z) . x) = (( sin . x) / (( cos . x) #Z (n + 1))) by A1, A2, A4, FDIFF_7: 31

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

        hence thesis;

      end;

      ( dom (((1 / n) (#) (( #Z n) * ( cos ^ ))) `| Z)) = ( dom f) by A1, A5, FDIFF_1:def 7;

      then (((1 / n) (#) (( #Z n) * ( cos ^ ))) `| Z) = f by A6, PARTFUN1: 5;

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

    end;

    theorem :: INTEGR12:43

    A c= Z & f = (((g1 + g2) ^ ) / f2) & f2 = arccot & Z c= ].( - 1), 1.[ & g2 = ( #Z 2) & (for x st x in Z holds (f . x) = (1 / ((1 + (x ^2 )) * ( arccot . x))) & (g1 . x) = 1 & (f2 . x) > 0 ) & Z = ( dom f) implies ( integral (f,A)) = ((( - ( ln * arccot )) . ( upper_bound A)) - (( - ( ln * arccot )) . ( lower_bound A)))

    proof

      assume

       A1: A c= Z & f = (((g1 + g2) ^ ) / f2) & f2 = arccot & Z c= ].( - 1), 1.[ & g2 = ( #Z 2) & (for x st x in Z holds (f . x) = (1 / ((1 + (x ^2 )) * ( arccot . x))) & (g1 . x) = 1 & (f2 . x) > 0 ) & Z = ( dom f);

      then Z = (( dom ((g1 + g2) ^ )) /\ (( dom f2) \ (f2 " { 0 }))) by RFUNCT_1:def 1;

      then

       A2: Z c= ( dom ((g1 + g2) ^ )) & Z c= (( dom f2) \ (f2 " { 0 })) by XBOOLE_1: 18;

      for x st x in Z holds (g1 . x) = 1 by A1;

      then

       A3: ((g1 + g2) ^ ) is_differentiable_on Z by A1, A2, Th1;

      

       A4: f2 is_differentiable_on Z by A1, SIN_COS9: 82;

      for x st x in Z holds (f2 . x) <> 0 by A1;

      then f is_differentiable_on Z by A1, A3, A4, FDIFF_2: 21;

      then (f | Z) is continuous by FDIFF_1: 25;

      then

       A5: (f | A) is continuous by A1, FCONT_1: 16;

      

       A6: Z c= ( dom (f2 ^ )) by A2, RFUNCT_1:def 2;

      ( dom (f2 ^ )) c= ( dom f2) by RFUNCT_1: 1;

      then

       A7: Z c= ( dom f2) by A6;

      

       A8: for x st x in Z holds (f2 . x) > 0 by A1;

      ( rng (f2 | Z)) c= ( right_open_halfline 0 )

      proof

        let x be object;

        assume x in ( rng (f2 | Z));

        then

        consider y be object such that

         A9: y in ( dom (f2 | Z)) & x = ((f2 | Z) . y) by FUNCT_1:def 3;

        y in Z by A9;

        then (f2 . y) > 0 by A1;

        then ((f2 | Z) . y) > 0 by A9, FUNCT_1: 47;

        hence thesis by A9, XXREAL_1: 235;

      end;

      then (f2 .: Z) c= ( dom ln ) by RELAT_1: 115, TAYLOR_1: 18;

      then

       A10: Z c= ( dom ( ln * arccot )) by A1, A7, FUNCT_1: 101;

      

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

      

       A12: ( ln * arccot ) is_differentiable_on Z by A1, A10, A8, SIN_COS9: 90;

      Z c= ( dom ( - ( ln * arccot ))) by A10, VALUED_1: 8;

      then

       A13: ( - ( ln * arccot )) is_differentiable_on Z by A12, FDIFF_1: 20;

      

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

      proof

        let x;

        assume

         A15: x in Z;

        then

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

         arccot is_differentiable_on Z by A1, SIN_COS9: 82;

        then

         A17: arccot is_differentiable_in x by A15, FDIFF_1: 9;

        

         A18: ( arccot . x) > 0 by A1, A15;

        

         A19: ( ln * arccot ) is_differentiable_in x by A12, A15, FDIFF_1: 9;

        ((( - ( ln * arccot )) `| Z) . x) = ( diff (( - ( ln * arccot )),x)) by A13, A15, FDIFF_1:def 7

        .= (( - 1) * ( diff (( ln * arccot ),x))) by A19, FDIFF_1: 15

        .= (( - 1) * (( diff ( arccot ,x)) / ( arccot . x))) by A17, A18, TAYLOR_1: 20

        .= (( - 1) * (( - (1 / (1 + (x ^2 )))) / ( arccot . x))) by A16, SIN_COS9: 76

        .= ((1 / (1 + (x ^2 ))) / ( arccot . x))

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

        hence thesis;

      end;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

        then ((( - ( ln * arccot )) `| Z) . x) = (1 / ((1 + (x ^2 )) * ( arccot . x))) by A14

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

        hence thesis;

      end;

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

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

      hence thesis by A1, A11, A13, INTEGRA5: 13;

    end;

    theorem :: INTEGR12:44

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

    proof

      assume

       A1: A c= Z & Z c= ].( - 1), 1.[ & (for x st x in Z holds ( arcsin . x) > 0 & (f1 . x) = 1) & Z c= ( dom ( ln * arcsin )) & Z = ( dom f) & f = (((( #R (1 / 2)) * (f1 - ( #Z 2))) (#) arcsin ) ^ );

      set g = ((( #R (1 / 2)) * (f1 - ( #Z 2))) (#) arcsin );

      

       A2: Z c= ( dom g) by A1, RFUNCT_1: 1;

      ( dom g) = (( dom (( #R (1 / 2)) * (f1 - ( #Z 2)))) /\ ( dom arcsin )) by VALUED_1:def 4;

      then

       A3: Z c= ( dom (( #R (1 / 2)) * (f1 - ( #Z 2)))) & Z c= ( dom arcsin ) by A2, XBOOLE_1: 18;

      

       A4: arcsin is_differentiable_on Z by A1, FDIFF_1: 26, SIN_COS6: 83;

      set f2 = ( #Z 2);

      for x st x in Z holds ((f1 - ( #Z 2)) . x) > 0

      proof

        let x;

        assume

         A5: x in Z;

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

        then 0 < (1 + x) & 0 < (1 - x) by XREAL_1: 50, XREAL_1: 148;

        then

         A6: 0 < ((1 + x) * (1 - x)) by XREAL_1: 129;

        for x st x in Z holds x in ( dom (f1 - f2)) by A3, FUNCT_1: 11;

        

        then ((f1 - f2) . x) = ((f1 . x) - (f2 . x)) by A5, VALUED_1: 13

        .= ((f1 . x) - (x #Z (1 + 1))) by TAYLOR_1:def 1

        .= ((f1 . x) - ((x #Z 1) * (x #Z 1))) by TAYLOR_1: 1

        .= ((f1 . x) - (x * (x #Z 1))) by PREPOWER: 35

        .= ((f1 . x) - (x * x)) by PREPOWER: 35

        .= (1 - (x * x)) by A1, A5;

        hence thesis by A6;

      end;

      then for x st x in Z holds (f1 . x) = 1 & ((f1 - ( #Z 2)) . x) > 0 by A1;

      then (( #R (1 / 2)) * (f1 - ( #Z 2))) is_differentiable_on Z by A3, FDIFF_7: 22;

      then

       A7: g is_differentiable_on Z by A2, A4, FDIFF_1: 21;

      for x st x in Z holds (g . x) <> 0 by A1, RFUNCT_1: 3;

      then f is_differentiable_on Z by A1, A7, FDIFF_2: 22;

      then (f | Z) is continuous by FDIFF_1: 25;

      then (f | A) is continuous by A1, FCONT_1: 16;

      then

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

      

       A9: for x st x in Z holds ( arcsin . x) > 0 by A1;

      then

       A10: ( ln * arcsin ) is_differentiable_on Z by A1, FDIFF_7: 8;

      

       A11: for x st x in Z holds (f . x) = (1 / (( sqrt (1 - (x ^2 ))) * ( arcsin . x)))

      proof

        let x;

        assume

         A12: x in Z;

        then

         A13: x in ( dom (f1 - ( #Z 2))) & ((f1 - ( #Z 2)) . x) in ( dom ( #R (1 / 2))) by A3, FUNCT_1: 11;

        then

         A14: ((f1 - ( #Z 2)) . x) in ( right_open_halfline 0 ) by TAYLOR_1:def 4;

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

        then 0 < (1 + x) & 0 < (1 - x) by XREAL_1: 50, XREAL_1: 148;

        then

         A15: 0 < ((1 + x) * (1 - x)) by XREAL_1: 129;

        ((((( #R (1 / 2)) * (f1 - ( #Z 2))) (#) arcsin ) ^ ) . x) = (1 / (((( #R (1 / 2)) * (f1 - ( #Z 2))) (#) arcsin ) . x)) by A1, A12, RFUNCT_1:def 2

        .= (1 / (((( #R (1 / 2)) * (f1 - ( #Z 2))) . x) * ( arcsin . x))) by VALUED_1: 5

        .= (1 / ((( #R (1 / 2)) . ((f1 - ( #Z 2)) . x)) * ( arcsin . x))) by A3, A12, FUNCT_1: 12

        .= (1 / ((((f1 - ( #Z 2)) . x) #R (1 / 2)) * ( arcsin . x))) by A14, TAYLOR_1:def 4

        .= (1 / ((((f1 . x) - (( #Z 2) . x)) #R (1 / 2)) * ( arcsin . x))) by A13, VALUED_1: 13

        .= (1 / ((((f1 . x) - (x #Z 2)) #R (1 / 2)) * ( arcsin . x))) by TAYLOR_1:def 1

        .= (1 / ((((f1 . x) - (x ^2 )) #R (1 / 2)) * ( arcsin . x))) by FDIFF_7: 1

        .= (1 / (((1 - (x ^2 )) #R (1 / 2)) * ( arcsin . x))) by A1, A12

        .= (1 / (( sqrt (1 - (x ^2 ))) * ( arcsin . x))) by A15, FDIFF_7: 2;

        hence thesis by A1;

      end;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

        then ((( ln * arcsin ) `| Z) . x) = (1 / (( sqrt (1 - (x ^2 ))) * ( arcsin . x))) by A1, A9, FDIFF_7: 8

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

        hence thesis;

      end;

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

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

      hence thesis by A1, A8, A10, INTEGRA5: 13;

    end;

    theorem :: INTEGR12:45

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

    proof

      assume

       A1: A c= Z & Z c= ].( - 1), 1.[ & (for x st x in Z holds (f1 . x) = 1 & ( arccos . x) > 0 ) & Z c= ( dom ( ln * arccos )) & Z = ( dom f) & f = (((( #R (1 / 2)) * (f1 - ( #Z 2))) (#) arccos ) ^ );

      set g = ((( #R (1 / 2)) * (f1 - ( #Z 2))) (#) arccos );

      

       A2: Z c= ( dom g) by A1, RFUNCT_1: 1;

      ( dom g) = (( dom (( #R (1 / 2)) * (f1 - ( #Z 2)))) /\ ( dom arccos )) by VALUED_1:def 4;

      then

       A3: Z c= ( dom (( #R (1 / 2)) * (f1 - ( #Z 2)))) & Z c= ( dom arccos ) by A2, XBOOLE_1: 18;

      

       A4: arccos is_differentiable_on Z by A1, FDIFF_1: 26, SIN_COS6: 106;

      set f2 = ( #Z 2);

      for x st x in Z holds ((f1 - ( #Z 2)) . x) > 0

      proof

        let x;

        assume

         A5: x in Z;

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

        then 0 < (1 + x) & 0 < (1 - x) by XREAL_1: 50, XREAL_1: 148;

        then

         A6: 0 < ((1 + x) * (1 - x)) by XREAL_1: 129;

        for x st x in Z holds x in ( dom (f1 - f2)) by A3, FUNCT_1: 11;

        

        then ((f1 - f2) . x) = ((f1 . x) - (f2 . x)) by A5, VALUED_1: 13

        .= ((f1 . x) - (x #Z (1 + 1))) by TAYLOR_1:def 1

        .= ((f1 . x) - ((x #Z 1) * (x #Z 1))) by TAYLOR_1: 1

        .= ((f1 . x) - (x * (x #Z 1))) by PREPOWER: 35

        .= ((f1 . x) - (x * x)) by PREPOWER: 35

        .= (1 - (x * x)) by A1, A5;

        hence thesis by A6;

      end;

      then for x st x in Z holds (f1 . x) = 1 & ((f1 - ( #Z 2)) . x) > 0 by A1;

      then (( #R (1 / 2)) * (f1 - ( #Z 2))) is_differentiable_on Z by A3, FDIFF_7: 22;

      then

       A7: g is_differentiable_on Z by A2, A4, FDIFF_1: 21;

      for x st x in Z holds (g . x) <> 0 by A1, RFUNCT_1: 3;

      then f is_differentiable_on Z by A1, A7, FDIFF_2: 22;

      then (f | Z) is continuous by FDIFF_1: 25;

      then (f | A) is continuous by A1, FCONT_1: 16;

      then

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

      for x st x in Z holds ( arccos . x) > 0 by A1;

      then

       A9: ( ln * arccos ) is_differentiable_on Z by A1, FDIFF_7: 9;

      Z c= ( dom ( - ( ln * arccos ))) by A1, VALUED_1: 8;

      then

       A10: (( - 1) (#) ( ln * arccos )) is_differentiable_on Z by A9, FDIFF_1: 20;

      

       A11: for x st x in Z holds ((( - ( ln * arccos )) `| Z) . x) = (1 / (( sqrt (1 - (x ^2 ))) * ( arccos . x)))

      proof

        let x;

        assume

         A12: x in Z;

        then

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

        

         A14: arccos is_differentiable_in x by A1, A12, FDIFF_1: 9, SIN_COS6: 106;

        

         A15: ( arccos . x) > 0 by A1, A12;

        

         A16: ( ln * arccos ) is_differentiable_in x by A9, A12, FDIFF_1: 9;

        ((( - ( ln * arccos )) `| Z) . x) = ( diff (( - ( ln * arccos )),x)) by A10, A12, FDIFF_1:def 7

        .= (( - 1) * ( diff (( ln * arccos ),x))) by A16, FDIFF_1: 15

        .= (( - 1) * (( diff ( arccos ,x)) / ( arccos . x))) by A14, A15, TAYLOR_1: 20

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

        .= (( - 1) * ( - ((1 / ( sqrt (1 - (x ^2 )))) / ( arccos . x))))

        .= (1 / (( sqrt (1 - (x ^2 ))) * ( arccos . x))) by XCMPLX_1: 78;

        hence thesis;

      end;

      

       A17: for x st x in Z holds (f . x) = (1 / (( sqrt (1 - (x ^2 ))) * ( arccos . x)))

      proof

        let x;

        assume

         A18: x in Z;

        then

         A19: x in ( dom (f1 - ( #Z 2))) & ((f1 - ( #Z 2)) . x) in ( dom ( #R (1 / 2))) by A3, FUNCT_1: 11;

        then

         A20: ((f1 - ( #Z 2)) . x) in ( right_open_halfline 0 ) by TAYLOR_1:def 4;

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

        then 0 < (1 + x) & 0 < (1 - x) by XREAL_1: 50, XREAL_1: 148;

        then

         A21: 0 < ((1 + x) * (1 - x)) by XREAL_1: 129;

        ((((( #R (1 / 2)) * (f1 - ( #Z 2))) (#) arccos ) ^ ) . x) = (1 / (((( #R (1 / 2)) * (f1 - ( #Z 2))) (#) arccos ) . x)) by A1, A18, RFUNCT_1:def 2

        .= (1 / (((( #R (1 / 2)) * (f1 - ( #Z 2))) . x) * ( arccos . x))) by VALUED_1: 5

        .= (1 / ((( #R (1 / 2)) . ((f1 - ( #Z 2)) . x)) * ( arccos . x))) by A3, A18, FUNCT_1: 12

        .= (1 / ((((f1 - ( #Z 2)) . x) #R (1 / 2)) * ( arccos . x))) by A20, TAYLOR_1:def 4

        .= (1 / ((((f1 . x) - (( #Z 2) . x)) #R (1 / 2)) * ( arccos . x))) by A19, VALUED_1: 13

        .= (1 / ((((f1 . x) - (x #Z 2)) #R (1 / 2)) * ( arccos . x))) by TAYLOR_1:def 1

        .= (1 / ((((f1 . x) - (x ^2 )) #R (1 / 2)) * ( arccos . x))) by FDIFF_7: 1

        .= (1 / (((1 - (x ^2 )) #R (1 / 2)) * ( arccos . x))) by A1, A18

        .= (1 / (( sqrt (1 - (x ^2 ))) * ( arccos . x))) by A21, FDIFF_7: 2;

        hence thesis by A1;

      end;

      

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

      proof

        let x be Element of REAL ;

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

        then

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

        

        then ((( - ( ln * arccos )) `| Z) . x) = (1 / (( sqrt (1 - (x ^2 ))) * ( arccos . x))) by A11

        .= (f . x) by A17, A23;

        hence thesis;

      end;

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

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

      hence thesis by A1, A8, A10, INTEGRA5: 13;

    end;