fdiff_4.miz



    begin

    reserve y for set;

    reserve x,a,b,c for Real;

    reserve n for Element of NAT ;

    reserve Z for open Subset of REAL ;

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

    theorem :: FDIFF_4:1

    

     Th1: Z c= ( dom ( ln * f)) & (for x st x in Z holds (f . x) = (a + x) & (f . x) > 0 ) implies ( ln * f) is_differentiable_on Z & for x st x in Z holds ((( ln * f) `| Z) . x) = (1 / (a + x))

    proof

      assume that

       A1: Z c= ( dom ( ln * f)) and

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

      for y be object st y in Z holds y in ( dom f) by A1, FUNCT_1: 11;

      then

       A3: Z c= ( dom f) by TARSKI:def 3;

      

       A4: for x st x in Z holds (f . x) = ((1 * x) + a) by A2;

      then

       A5: f is_differentiable_on Z by A3, FDIFF_1: 23;

      

       A6: for x st x in Z holds ( ln * f) is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then f is_differentiable_in x & (f . x) > 0 by A2, A5, FDIFF_1: 9;

        hence thesis by TAYLOR_1: 20;

      end;

      then

       A7: ( ln * f) is_differentiable_on Z by A1, FDIFF_1: 9;

      for x st x in Z holds ((( ln * f) `| Z) . x) = (1 / (a + x))

      proof

        let x;

        assume

         A8: x in Z;

        then

         A9: (f . x) = (a + x) by A2;

        f is_differentiable_in x & (f . x) > 0 by A2, A5, A8, FDIFF_1: 9;

        

        then ( diff (( ln * f),x)) = (( diff (f,x)) / (f . x)) by TAYLOR_1: 20

        .= (((f `| Z) . x) / (f . x)) by A5, A8, FDIFF_1:def 7

        .= (1 / (a + x)) by A3, A4, A8, A9, FDIFF_1: 23;

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

      end;

      hence thesis by A1, A6, FDIFF_1: 9;

    end;

    theorem :: FDIFF_4:2

    

     Th2: Z c= ( dom ( ln * f)) & (for x st x in Z holds (f . x) = (x - a) & (f . x) > 0 ) implies ( ln * f) is_differentiable_on Z & for x st x in Z holds ((( ln * f) `| Z) . x) = (1 / (x - a))

    proof

      assume that

       A1: Z c= ( dom ( ln * f)) and

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

      

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

      proof

        let x;

        

         A4: ((1 * x) + ( - a)) = ((1 * x) - a);

        assume x in Z;

        hence thesis by A2, A4;

      end;

      for y be object st y in Z holds y in ( dom f) by A1, FUNCT_1: 11;

      then

       A5: Z c= ( dom f) by TARSKI:def 3;

      then

       A6: f is_differentiable_on Z by A3, FDIFF_1: 23;

      

       A7: for x st x in Z holds ( ln * f) is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then f is_differentiable_in x & (f . x) > 0 by A2, A6, FDIFF_1: 9;

        hence thesis by TAYLOR_1: 20;

      end;

      then

       A8: ( ln * f) is_differentiable_on Z by A1, FDIFF_1: 9;

      for x st x in Z holds ((( ln * f) `| Z) . x) = (1 / (x - a))

      proof

        let x;

        assume

         A9: x in Z;

        then

         A10: (f . x) = (x - a) by A2;

        f is_differentiable_in x & (f . x) > 0 by A2, A6, A9, FDIFF_1: 9;

        

        then ( diff (( ln * f),x)) = (( diff (f,x)) / (f . x)) by TAYLOR_1: 20

        .= (((f `| Z) . x) / (f . x)) by A6, A9, FDIFF_1:def 7

        .= (1 / (x - a)) by A5, A3, A9, A10, FDIFF_1: 23;

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

      end;

      hence thesis by A1, A7, FDIFF_1: 9;

    end;

    theorem :: FDIFF_4:3

    Z c= ( dom ( - ( ln * f))) & (for x st x in Z holds (f . x) = (a - x) & (f . x) > 0 ) implies ( - ( ln * f)) is_differentiable_on Z & for x st x in Z holds ((( - ( ln * f)) `| Z) . x) = (1 / (a - x))

    proof

      assume that

       A1: Z c= ( dom ( - ( ln * f))) and

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

      now

        let y be object;

        assume y in Z;

        then y in ( dom (( - 1) (#) ( ln * f))) by A1;

        hence y in ( dom ( ln * f)) by VALUED_1:def 5;

      end;

      then

       A3: Z c= ( dom ( ln * f)) by TARSKI:def 3;

      then for y be object st y in Z holds y in ( dom f) by FUNCT_1: 11;

      then

       A4: Z c= ( dom f) by TARSKI:def 3;

      

       A5: for x st x in Z holds (f . x) = ((( - 1) * x) + a)

      proof

        let x;

        assume x in Z;

        then (f . x) = (a - x) by A2;

        hence thesis;

      end;

      then

       A6: f is_differentiable_on Z by A4, FDIFF_1: 23;

      now

        let x;

        assume x in Z;

        then f is_differentiable_in x & (f . x) > 0 by A2, A6, FDIFF_1: 9;

        hence ( ln * f) is_differentiable_in x by TAYLOR_1: 20;

      end;

      then

       A7: ( ln * f) is_differentiable_on Z by A3, FDIFF_1: 9;

      

       A8: for x st x in Z holds ((( - ( ln * f)) `| Z) . x) = (1 / (a - x))

      proof

        let x;

        assume

         A9: x in Z;

        then

         A10: (f . x) = (a - x) by A2;

        (f . x) > 0 & f is_differentiable_in x by A2, A6, A9, FDIFF_1: 9;

        

        then ( diff (( ln * f),x)) = (( diff (f,x)) / (f . x)) by TAYLOR_1: 20

        .= (((f `| Z) . x) / (f . x)) by A6, A9, FDIFF_1:def 7

        .= (( - 1) / (a - x)) by A4, A5, A9, A10, FDIFF_1: 23;

        

        then (((( - 1) (#) ( ln * f)) `| Z) . x) = (( - 1) * (( - 1) / (a - x))) by A1, A7, A9, FDIFF_1: 20

        .= ((( - 1) * ( - 1)) / (a - x)) by XCMPLX_1: 74

        .= (1 / (a - x));

        hence thesis;

      end;

      Z c= ( dom (( - 1) (#) ( ln * f))) by A1;

      hence thesis by A7, A8, FDIFF_1: 20;

    end;

    theorem :: FDIFF_4:4

    Z c= ( dom (( id Z) - (a (#) f))) & f = ( ln * f1) & (for x st x in Z holds (f1 . x) = (a + x) & (f1 . x) > 0 ) implies (( id Z) - (a (#) f)) is_differentiable_on Z & for x st x in Z holds (((( id Z) - (a (#) f)) `| Z) . x) = (x / (a + x))

    proof

      assume that

       A1: Z c= ( dom (( id Z) - (a (#) f))) and

       A2: f = ( ln * f1) and

       A3: for x st x in Z holds (f1 . x) = (a + x) & (f1 . x) > 0 ;

      

       A4: Z c= (( dom ( id Z)) /\ ( dom (a (#) f))) by A1, VALUED_1: 12;

      then

       A5: Z c= ( dom (a (#) f)) by XBOOLE_1: 18;

      then

       A6: Z c= ( dom ( ln * f1)) by A2, VALUED_1:def 5;

      then

       A7: f is_differentiable_on Z by A2, A3, Th1;

      then

       A8: (a (#) f) is_differentiable_on Z by A5, FDIFF_1: 20;

      

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

      

       A10: Z c= ( dom ( id Z)) by A4, XBOOLE_1: 18;

      then

       A11: ( id Z) is_differentiable_on Z by A9, FDIFF_1: 23;

      

       A12: for x st x in Z holds (((a (#) f) `| Z) . x) = (a / (a + x))

      proof

        let x;

        assume

         A13: x in Z;

        

        hence (((a (#) f) `| Z) . x) = (a * ( diff (f,x))) by A5, A7, FDIFF_1: 20

        .= (a * ((f `| Z) . x)) by A7, A13, FDIFF_1:def 7

        .= (a * (1 / (a + x))) by A2, A3, A6, A13, Th1

        .= (a / (a + x)) by XCMPLX_1: 99;

      end;

      for x st x in Z holds (((( id Z) - (a (#) f)) `| Z) . x) = (x / (a + x))

      proof

        let x;

        assume

         A14: x in Z;

        then

         A15: (f1 . x) = (a + x) & (f1 . x) > 0 by A3;

        (((( id Z) - (a (#) f)) `| Z) . x) = (( diff (( id Z),x)) - ( diff ((a (#) f),x))) by A1, A11, A8, A14, FDIFF_1: 19

        .= (((( id Z) `| Z) . x) - ( diff ((a (#) f),x))) by A11, A14, FDIFF_1:def 7

        .= (((( id Z) `| Z) . x) - (((a (#) f) `| Z) . x)) by A8, A14, FDIFF_1:def 7

        .= (1 - (((a (#) f) `| Z) . x)) by A10, A9, A14, FDIFF_1: 23

        .= (1 - (a / (a + x))) by A12, A14

        .= (((1 * (a + x)) - a) / (a + x)) by A15, XCMPLX_1: 127

        .= (x / (a + x));

        hence thesis;

      end;

      hence thesis by A1, A11, A8, FDIFF_1: 19;

    end;

    theorem :: FDIFF_4:5

    Z c= ( dom (((2 * a) (#) f) - ( id Z))) & f = ( ln * f1) & (for x st x in Z holds (f1 . x) = (a + x) & (f1 . x) > 0 ) implies (((2 * a) (#) f) - ( id Z)) is_differentiable_on Z & for x st x in Z holds (((((2 * a) (#) f) - ( id Z)) `| Z) . x) = ((a - x) / (a + x))

    proof

      assume that

       A1: Z c= ( dom (((2 * a) (#) f) - ( id Z))) and

       A2: f = ( ln * f1) and

       A3: for x st x in Z holds (f1 . x) = (a + x) & (f1 . x) > 0 ;

      

       A4: Z c= (( dom ((2 * a) (#) f)) /\ ( dom ( id Z))) by A1, VALUED_1: 12;

      then

       A5: Z c= ( dom ((2 * a) (#) f)) by XBOOLE_1: 18;

      then

       A6: Z c= ( dom ( ln * f1)) by A2, VALUED_1:def 5;

      then

       A7: f is_differentiable_on Z by A2, A3, Th1;

      then

       A8: ((2 * a) (#) f) is_differentiable_on Z by A5, FDIFF_1: 20;

      

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

      

       A10: Z c= ( dom ( id Z)) by A4, XBOOLE_1: 18;

      then

       A11: ( id Z) is_differentiable_on Z by A9, FDIFF_1: 23;

      

       A12: for x st x in Z holds ((((2 * a) (#) f) `| Z) . x) = ((2 * a) / (a + x))

      proof

        let x;

        assume

         A13: x in Z;

        

        hence ((((2 * a) (#) f) `| Z) . x) = ((2 * a) * ( diff (f,x))) by A5, A7, FDIFF_1: 20

        .= ((2 * a) * ((f `| Z) . x)) by A7, A13, FDIFF_1:def 7

        .= ((2 * a) * (1 / (a + x))) by A2, A3, A6, A13, Th1

        .= ((2 * a) / (a + x)) by XCMPLX_1: 99;

      end;

      for x st x in Z holds (((((2 * a) (#) f) - ( id Z)) `| Z) . x) = ((a - x) / (a + x))

      proof

        let x;

        assume

         A14: x in Z;

        then

         A15: (f1 . x) = (a + x) & (f1 . x) > 0 by A3;

        (((((2 * a) (#) f) - ( id Z)) `| Z) . x) = (( diff (((2 * a) (#) f),x)) - ( diff (( id Z),x))) by A1, A11, A8, A14, FDIFF_1: 19

        .= (( diff (((2 * a) (#) f),x)) - ((( id Z) `| Z) . x)) by A11, A14, FDIFF_1:def 7

        .= (((((2 * a) (#) f) `| Z) . x) - ((( id Z) `| Z) . x)) by A8, A14, FDIFF_1:def 7

        .= (((((2 * a) (#) f) `| Z) . x) - 1) by A10, A9, A14, FDIFF_1: 23

        .= (((2 * a) / (a + x)) - 1) by A12, A14

        .= (((2 * a) - (1 * (a + x))) / (a + x)) by A15, XCMPLX_1: 126

        .= ((a - x) / (a + x));

        hence thesis;

      end;

      hence thesis by A1, A11, A8, FDIFF_1: 19;

    end;

    theorem :: FDIFF_4:6

    Z c= ( dom (( id Z) - ((2 * a) (#) f))) & f = ( ln * f1) & (for x st x in Z holds (f1 . x) = (x + a) & (f1 . x) > 0 ) implies (( id Z) - ((2 * a) (#) f)) is_differentiable_on Z & for x st x in Z holds (((( id Z) - ((2 * a) (#) f)) `| Z) . x) = ((x - a) / (x + a))

    proof

      assume that

       A1: Z c= ( dom (( id Z) - ((2 * a) (#) f))) and

       A2: f = ( ln * f1) and

       A3: for x st x in Z holds (f1 . x) = (x + a) & (f1 . x) > 0 ;

      

       A4: for x st x in Z holds (f1 . x) = (a + x) & (f1 . x) > 0 by A3;

      

       A5: Z c= (( dom ( id Z)) /\ ( dom ((2 * a) (#) f))) by A1, VALUED_1: 12;

      then

       A6: Z c= ( dom ((2 * a) (#) f)) by XBOOLE_1: 18;

      then

       A7: Z c= ( dom ( ln * f1)) by A2, VALUED_1:def 5;

      then

       A8: f is_differentiable_on Z by A2, A4, Th1;

      then

       A9: ((2 * a) (#) f) is_differentiable_on Z by A6, FDIFF_1: 20;

      

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

      

       A11: Z c= ( dom ( id Z)) by A5, XBOOLE_1: 18;

      then

       A12: ( id Z) is_differentiable_on Z by A10, FDIFF_1: 23;

      

       A13: for x st x in Z holds ((((2 * a) (#) f) `| Z) . x) = ((2 * a) / (x + a))

      proof

        let x;

        assume

         A14: x in Z;

        

        hence ((((2 * a) (#) f) `| Z) . x) = ((2 * a) * ( diff (f,x))) by A6, A8, FDIFF_1: 20

        .= ((2 * a) * ((f `| Z) . x)) by A8, A14, FDIFF_1:def 7

        .= ((2 * a) * (1 / (x + a))) by A2, A7, A4, A14, Th1

        .= ((2 * a) / (x + a)) by XCMPLX_1: 99;

      end;

      for x st x in Z holds (((( id Z) - ((2 * a) (#) f)) `| Z) . x) = ((x - a) / (x + a))

      proof

        let x;

        assume

         A15: x in Z;

        then

         A16: (f1 . x) = (x + a) & (f1 . x) > 0 by A3;

        (((( id Z) - ((2 * a) (#) f)) `| Z) . x) = (( diff (( id Z),x)) - ( diff (((2 * a) (#) f),x))) by A1, A12, A9, A15, FDIFF_1: 19

        .= (((( id Z) `| Z) . x) - ( diff (((2 * a) (#) f),x))) by A12, A15, FDIFF_1:def 7

        .= (((( id Z) `| Z) . x) - ((((2 * a) (#) f) `| Z) . x)) by A9, A15, FDIFF_1:def 7

        .= (1 - ((((2 * a) (#) f) `| Z) . x)) by A11, A10, A15, FDIFF_1: 23

        .= (1 - ((2 * a) / (x + a))) by A13, A15

        .= (((1 * (x + a)) - (2 * a)) / (x + a)) by A16, XCMPLX_1: 127

        .= ((x - a) / (x + a));

        hence thesis;

      end;

      hence thesis by A1, A12, A9, FDIFF_1: 19;

    end;

    theorem :: FDIFF_4:7

    Z c= ( dom (( id Z) + ((2 * a) (#) f))) & f = ( ln * f1) & (for x st x in Z holds (f1 . x) = (x - a) & (f1 . x) > 0 ) implies (( id Z) + ((2 * a) (#) f)) is_differentiable_on Z & for x st x in Z holds (((( id Z) + ((2 * a) (#) f)) `| Z) . x) = ((x + a) / (x - a))

    proof

      assume that

       A1: Z c= ( dom (( id Z) + ((2 * a) (#) f))) and

       A2: f = ( ln * f1) and

       A3: for x st x in Z holds (f1 . x) = (x - a) & (f1 . x) > 0 ;

      

       A4: Z c= (( dom ( id Z)) /\ ( dom ((2 * a) (#) f))) by A1, VALUED_1:def 1;

      then

       A5: Z c= ( dom ((2 * a) (#) f)) by XBOOLE_1: 18;

      then

       A6: Z c= ( dom ( ln * f1)) by A2, VALUED_1:def 5;

      then

       A7: f is_differentiable_on Z by A2, A3, Th2;

      then

       A8: ((2 * a) (#) f) is_differentiable_on Z by A5, FDIFF_1: 20;

      

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

      

       A10: Z c= ( dom ( id Z)) by A4, XBOOLE_1: 18;

      then

       A11: ( id Z) is_differentiable_on Z by A9, FDIFF_1: 23;

      

       A12: for x st x in Z holds ((((2 * a) (#) f) `| Z) . x) = ((2 * a) / (x - a))

      proof

        let x;

        assume

         A13: x in Z;

        

        hence ((((2 * a) (#) f) `| Z) . x) = ((2 * a) * ( diff (f,x))) by A5, A7, FDIFF_1: 20

        .= ((2 * a) * ((f `| Z) . x)) by A7, A13, FDIFF_1:def 7

        .= ((2 * a) * (1 / (x - a))) by A2, A3, A6, A13, Th2

        .= ((2 * a) / (x - a)) by XCMPLX_1: 99;

      end;

      for x st x in Z holds (((( id Z) + ((2 * a) (#) f)) `| Z) . x) = ((x + a) / (x - a))

      proof

        let x;

        assume

         A14: x in Z;

        then

         A15: (f1 . x) = (x - a) & (f1 . x) > 0 by A3;

        (((( id Z) + ((2 * a) (#) f)) `| Z) . x) = (( diff (( id Z),x)) + ( diff (((2 * a) (#) f),x))) by A1, A11, A8, A14, FDIFF_1: 18

        .= (((( id Z) `| Z) . x) + ( diff (((2 * a) (#) f),x))) by A11, A14, FDIFF_1:def 7

        .= (((( id Z) `| Z) . x) + ((((2 * a) (#) f) `| Z) . x)) by A8, A14, FDIFF_1:def 7

        .= (1 + ((((2 * a) (#) f) `| Z) . x)) by A10, A9, A14, FDIFF_1: 23

        .= (1 + ((2 * a) / (x - a))) by A12, A14

        .= (((1 * (x - a)) + (2 * a)) / (x - a)) by A15, XCMPLX_1: 113

        .= ((x + a) / (x - a));

        hence thesis;

      end;

      hence thesis by A1, A11, A8, FDIFF_1: 18;

    end;

    theorem :: FDIFF_4:8

    Z c= ( dom (( id Z) + ((a - b) (#) f))) & f = ( ln * f1) & (for x st x in Z holds (f1 . x) = (x + b) & (f1 . x) > 0 ) implies (( id Z) + ((a - b) (#) f)) is_differentiable_on Z & for x st x in Z holds (((( id Z) + ((a - b) (#) f)) `| Z) . x) = ((x + a) / (x + b))

    proof

      assume that

       A1: Z c= ( dom (( id Z) + ((a - b) (#) f))) and

       A2: f = ( ln * f1) and

       A3: for x st x in Z holds (f1 . x) = (x + b) & (f1 . x) > 0 ;

      

       A4: for x st x in Z holds (f1 . x) = (b + x) & (f1 . x) > 0 by A3;

      

       A5: Z c= (( dom ( id Z)) /\ ( dom ((a - b) (#) f))) by A1, VALUED_1:def 1;

      then

       A6: Z c= ( dom ((a - b) (#) f)) by XBOOLE_1: 18;

      then

       A7: Z c= ( dom ( ln * f1)) by A2, VALUED_1:def 5;

      then

       A8: f is_differentiable_on Z by A2, A4, Th1;

      then

       A9: ((a - b) (#) f) is_differentiable_on Z by A6, FDIFF_1: 20;

      

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

      

       A11: Z c= ( dom ( id Z)) by A5, XBOOLE_1: 18;

      then

       A12: ( id Z) is_differentiable_on Z by A10, FDIFF_1: 23;

      

       A13: for x st x in Z holds ((((a - b) (#) f) `| Z) . x) = ((a - b) / (x + b))

      proof

        let x;

        assume

         A14: x in Z;

        

        hence ((((a - b) (#) f) `| Z) . x) = ((a - b) * ( diff (f,x))) by A6, A8, FDIFF_1: 20

        .= ((a - b) * ((f `| Z) . x)) by A8, A14, FDIFF_1:def 7

        .= ((a - b) * (1 / (x + b))) by A2, A7, A4, A14, Th1

        .= ((a - b) / (x + b)) by XCMPLX_1: 99;

      end;

      for x st x in Z holds (((( id Z) + ((a - b) (#) f)) `| Z) . x) = ((x + a) / (x + b))

      proof

        let x;

        assume

         A15: x in Z;

        then

         A16: (f1 . x) = (x + b) & (f1 . x) > 0 by A3;

        (((( id Z) + ((a - b) (#) f)) `| Z) . x) = (( diff (( id Z),x)) + ( diff (((a - b) (#) f),x))) by A1, A12, A9, A15, FDIFF_1: 18

        .= (((( id Z) `| Z) . x) + ( diff (((a - b) (#) f),x))) by A12, A15, FDIFF_1:def 7

        .= (((( id Z) `| Z) . x) + ((((a - b) (#) f) `| Z) . x)) by A9, A15, FDIFF_1:def 7

        .= (1 + ((((a - b) (#) f) `| Z) . x)) by A11, A10, A15, FDIFF_1: 23

        .= (1 + ((a - b) / (x + b))) by A13, A15

        .= (((1 * (x + b)) + (a - b)) / (x + b)) by A16, XCMPLX_1: 113

        .= ((x + a) / (x + b));

        hence thesis;

      end;

      hence thesis by A1, A12, A9, FDIFF_1: 18;

    end;

    theorem :: FDIFF_4:9

    Z c= ( dom (( id Z) + ((a + b) (#) f))) & f = ( ln * f1) & (for x st x in Z holds (f1 . x) = (x - b) & (f1 . x) > 0 ) implies (( id Z) + ((a + b) (#) f)) is_differentiable_on Z & for x st x in Z holds (((( id Z) + ((a + b) (#) f)) `| Z) . x) = ((x + a) / (x - b))

    proof

      assume that

       A1: Z c= ( dom (( id Z) + ((a + b) (#) f))) and

       A2: f = ( ln * f1) and

       A3: for x st x in Z holds (f1 . x) = (x - b) & (f1 . x) > 0 ;

      

       A4: Z c= (( dom ( id Z)) /\ ( dom ((a + b) (#) f))) by A1, VALUED_1:def 1;

      then

       A5: Z c= ( dom ((a + b) (#) f)) by XBOOLE_1: 18;

      then

       A6: Z c= ( dom ( ln * f1)) by A2, VALUED_1:def 5;

      then

       A7: f is_differentiable_on Z by A2, A3, Th2;

      then

       A8: ((a + b) (#) f) is_differentiable_on Z by A5, FDIFF_1: 20;

      

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

      

       A10: Z c= ( dom ( id Z)) by A4, XBOOLE_1: 18;

      then

       A11: ( id Z) is_differentiable_on Z by A9, FDIFF_1: 23;

      

       A12: for x st x in Z holds ((((a + b) (#) f) `| Z) . x) = ((a + b) / (x - b))

      proof

        let x;

        assume

         A13: x in Z;

        

        hence ((((a + b) (#) f) `| Z) . x) = ((a + b) * ( diff (f,x))) by A5, A7, FDIFF_1: 20

        .= ((a + b) * ((f `| Z) . x)) by A7, A13, FDIFF_1:def 7

        .= ((a + b) * (1 / (x - b))) by A2, A3, A6, A13, Th2

        .= ((a + b) / (x - b)) by XCMPLX_1: 99;

      end;

      for x st x in Z holds (((( id Z) + ((a + b) (#) f)) `| Z) . x) = ((x + a) / (x - b))

      proof

        let x;

        assume

         A14: x in Z;

        then

         A15: (f1 . x) = (x - b) & (f1 . x) > 0 by A3;

        (((( id Z) + ((a + b) (#) f)) `| Z) . x) = (( diff (( id Z),x)) + ( diff (((a + b) (#) f),x))) by A1, A11, A8, A14, FDIFF_1: 18

        .= (((( id Z) `| Z) . x) + ( diff (((a + b) (#) f),x))) by A11, A14, FDIFF_1:def 7

        .= (((( id Z) `| Z) . x) + ((((a + b) (#) f) `| Z) . x)) by A8, A14, FDIFF_1:def 7

        .= (1 + ((((a + b) (#) f) `| Z) . x)) by A10, A9, A14, FDIFF_1: 23

        .= (1 + ((a + b) / (x - b))) by A12, A14

        .= (((1 * (x - b)) + (a + b)) / (x - b)) by A15, XCMPLX_1: 113

        .= ((x + a) / (x - b));

        hence thesis;

      end;

      hence thesis by A1, A11, A8, FDIFF_1: 18;

    end;

    theorem :: FDIFF_4:10

    Z c= ( dom (( id Z) - ((a + b) (#) f))) & f = ( ln * f1) & (for x st x in Z holds (f1 . x) = (x + b) & (f1 . x) > 0 ) implies (( id Z) - ((a + b) (#) f)) is_differentiable_on Z & for x st x in Z holds (((( id Z) - ((a + b) (#) f)) `| Z) . x) = ((x - a) / (x + b))

    proof

      assume that

       A1: Z c= ( dom (( id Z) - ((a + b) (#) f))) and

       A2: f = ( ln * f1) and

       A3: for x st x in Z holds (f1 . x) = (x + b) & (f1 . x) > 0 ;

      

       A4: for x st x in Z holds (f1 . x) = (b + x) & (f1 . x) > 0 by A3;

      

       A5: Z c= (( dom ( id Z)) /\ ( dom ((a + b) (#) f))) by A1, VALUED_1: 12;

      then

       A6: Z c= ( dom ((a + b) (#) f)) by XBOOLE_1: 18;

      then

       A7: Z c= ( dom ( ln * f1)) by A2, VALUED_1:def 5;

      then

       A8: f is_differentiable_on Z by A2, A4, Th1;

      then

       A9: ((a + b) (#) f) is_differentiable_on Z by A6, FDIFF_1: 20;

      

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

      

       A11: Z c= ( dom ( id Z)) by A5, XBOOLE_1: 18;

      then

       A12: ( id Z) is_differentiable_on Z by A10, FDIFF_1: 23;

      

       A13: for x st x in Z holds ((((a + b) (#) f) `| Z) . x) = ((a + b) / (x + b))

      proof

        let x;

        assume

         A14: x in Z;

        

        hence ((((a + b) (#) f) `| Z) . x) = ((a + b) * ( diff (f,x))) by A6, A8, FDIFF_1: 20

        .= ((a + b) * ((f `| Z) . x)) by A8, A14, FDIFF_1:def 7

        .= ((a + b) * (1 / (x + b))) by A2, A7, A4, A14, Th1

        .= ((a + b) / (x + b)) by XCMPLX_1: 99;

      end;

      for x st x in Z holds (((( id Z) - ((a + b) (#) f)) `| Z) . x) = ((x - a) / (x + b))

      proof

        let x;

        assume

         A15: x in Z;

        then

         A16: (f1 . x) = (x + b) & (f1 . x) > 0 by A3;

        (((( id Z) - ((a + b) (#) f)) `| Z) . x) = (( diff (( id Z),x)) - ( diff (((a + b) (#) f),x))) by A1, A12, A9, A15, FDIFF_1: 19

        .= (((( id Z) `| Z) . x) - ( diff (((a + b) (#) f),x))) by A12, A15, FDIFF_1:def 7

        .= (((( id Z) `| Z) . x) - ((((a + b) (#) f) `| Z) . x)) by A9, A15, FDIFF_1:def 7

        .= (1 - ((((a + b) (#) f) `| Z) . x)) by A11, A10, A15, FDIFF_1: 23

        .= (1 - ((a + b) / (x + b))) by A13, A15

        .= (((1 * (x + b)) - (a + b)) / (x + b)) by A16, XCMPLX_1: 127

        .= ((x - a) / (x + b));

        hence thesis;

      end;

      hence thesis by A1, A12, A9, FDIFF_1: 19;

    end;

    theorem :: FDIFF_4:11

    Z c= ( dom (( id Z) + ((b - a) (#) f))) & f = ( ln * f1) & (for x st x in Z holds (f1 . x) = (x - b) & (f1 . x) > 0 ) implies (( id Z) + ((b - a) (#) f)) is_differentiable_on Z & for x st x in Z holds (((( id Z) + ((b - a) (#) f)) `| Z) . x) = ((x - a) / (x - b))

    proof

      assume that

       A1: Z c= ( dom (( id Z) + ((b - a) (#) f))) and

       A2: f = ( ln * f1) and

       A3: for x st x in Z holds (f1 . x) = (x - b) & (f1 . x) > 0 ;

      

       A4: Z c= (( dom ( id Z)) /\ ( dom ((b - a) (#) f))) by A1, VALUED_1:def 1;

      then

       A5: Z c= ( dom ((b - a) (#) f)) by XBOOLE_1: 18;

      then

       A6: Z c= ( dom ( ln * f1)) by A2, VALUED_1:def 5;

      then

       A7: f is_differentiable_on Z by A2, A3, Th2;

      then

       A8: ((b - a) (#) f) is_differentiable_on Z by A5, FDIFF_1: 20;

      

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

      

       A10: Z c= ( dom ( id Z)) by A4, XBOOLE_1: 18;

      then

       A11: ( id Z) is_differentiable_on Z by A9, FDIFF_1: 23;

      

       A12: for x st x in Z holds ((((b - a) (#) f) `| Z) . x) = ((b - a) / (x - b))

      proof

        let x;

        assume

         A13: x in Z;

        

        hence ((((b - a) (#) f) `| Z) . x) = ((b - a) * ( diff (f,x))) by A5, A7, FDIFF_1: 20

        .= ((b - a) * ((f `| Z) . x)) by A7, A13, FDIFF_1:def 7

        .= ((b - a) * (1 / (x - b))) by A2, A3, A6, A13, Th2

        .= ((b - a) / (x - b)) by XCMPLX_1: 99;

      end;

      for x st x in Z holds (((( id Z) + ((b - a) (#) f)) `| Z) . x) = ((x - a) / (x - b))

      proof

        let x;

        assume

         A14: x in Z;

        then

         A15: (f1 . x) = (x - b) & (f1 . x) > 0 by A3;

        (((( id Z) + ((b - a) (#) f)) `| Z) . x) = (( diff (( id Z),x)) + ( diff (((b - a) (#) f),x))) by A1, A11, A8, A14, FDIFF_1: 18

        .= (((( id Z) `| Z) . x) + ( diff (((b - a) (#) f),x))) by A11, A14, FDIFF_1:def 7

        .= (((( id Z) `| Z) . x) + ((((b - a) (#) f) `| Z) . x)) by A8, A14, FDIFF_1:def 7

        .= (1 + ((((b - a) (#) f) `| Z) . x)) by A10, A9, A14, FDIFF_1: 23

        .= (1 + ((b - a) / (x - b))) by A12, A14

        .= (((1 * (x - b)) + (b - a)) / (x - b)) by A15, XCMPLX_1: 113

        .= ((x - a) / (x - b));

        hence thesis;

      end;

      hence thesis by A1, A11, A8, FDIFF_1: 18;

    end;

    theorem :: FDIFF_4:12

    

     Th12: Z c= ( dom (f1 + (c (#) f2))) & (for x st x in Z holds (f1 . x) = (a + (b * x))) & f2 = ( #Z 2) implies (f1 + (c (#) f2)) is_differentiable_on Z & for x st x in Z holds (((f1 + (c (#) f2)) `| Z) . x) = (b + ((2 * c) * x))

    proof

      assume that

       A1: Z c= ( dom (f1 + (c (#) f2))) and

       A2: for x st x in Z holds (f1 . x) = (a + (b * x)) and

       A3: f2 = ( #Z 2);

      

       A4: for x st x in Z holds f2 is_differentiable_in x by A3, TAYLOR_1: 2;

      

       A5: Z c= (( dom f1) /\ ( dom (c (#) f2))) by A1, VALUED_1:def 1;

      then

       A6: Z c= ( dom f1) by XBOOLE_1: 18;

      

       A7: for x st x in Z holds (f1 . x) = ((b * x) + a) by A2;

      then

       A8: f1 is_differentiable_on Z by A6, FDIFF_1: 23;

      

       A9: Z c= ( dom (c (#) f2)) by A5, XBOOLE_1: 18;

      then Z c= ( dom f2) by VALUED_1:def 5;

      then

       A10: f2 is_differentiable_on Z by A4, FDIFF_1: 9;

      then

       A11: (c (#) f2) is_differentiable_on Z by A9, FDIFF_1: 20;

      

       A12: for x st x in Z holds ((f2 `| Z) . x) = (2 * x)

      proof

        let x;

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

        then

         A13: ( diff (f2,x)) = (2 * x) by A3, TAYLOR_1: 2;

        assume x in Z;

        hence thesis by A10, A13, FDIFF_1:def 7;

      end;

      

       A14: for x st x in Z holds (((c (#) f2) `| Z) . x) = ((2 * c) * x)

      proof

        let x;

        assume

         A15: x in Z;

        

        hence (((c (#) f2) `| Z) . x) = (c * ( diff (f2,x))) by A9, A10, FDIFF_1: 20

        .= (c * ((f2 `| Z) . x)) by A10, A15, FDIFF_1:def 7

        .= (c * (2 * x)) by A12, A15

        .= ((2 * c) * x);

      end;

      for x st x in Z holds (((f1 + (c (#) f2)) `| Z) . x) = (b + ((2 * c) * x))

      proof

        let x;

        assume

         A16: x in Z;

        

        then (((f1 + (c (#) f2)) `| Z) . x) = (( diff (f1,x)) + ( diff ((c (#) f2),x))) by A1, A8, A11, FDIFF_1: 18

        .= (((f1 `| Z) . x) + ( diff ((c (#) f2),x))) by A8, A16, FDIFF_1:def 7

        .= (((f1 `| Z) . x) + (((c (#) f2) `| Z) . x)) by A11, A16, FDIFF_1:def 7

        .= (b + (((c (#) f2) `| Z) . x)) by A6, A7, A16, FDIFF_1: 23

        .= (b + ((2 * c) * x)) by A14, A16;

        hence thesis;

      end;

      hence thesis by A1, A8, A11, FDIFF_1: 18;

    end;

    theorem :: FDIFF_4:13

    

     Th13: Z c= ( dom ( ln * (f1 + (c (#) f2)))) & f2 = ( #Z 2) & (for x st x in Z holds (f1 . x) = (a + (b * x)) & ((f1 + (c (#) f2)) . x) > 0 ) implies ( ln * (f1 + (c (#) f2))) is_differentiable_on Z & for x st x in Z holds ((( ln * (f1 + (c (#) f2))) `| Z) . x) = ((b + ((2 * c) * x)) / ((a + (b * x)) + (c * (x |^ 2))))

    proof

      assume that

       A1: Z c= ( dom ( ln * (f1 + (c (#) f2)))) and

       A2: f2 = ( #Z 2) and

       A3: for x st x in Z holds (f1 . x) = (a + (b * x)) & ((f1 + (c (#) f2)) . x) > 0 ;

      for y be object st y in Z holds y in ( dom (f1 + (c (#) f2))) by A1, FUNCT_1: 11;

      then

       A4: Z c= ( dom (f1 + (c (#) f2))) by TARSKI:def 3;

      then Z c= (( dom f1) /\ ( dom (c (#) f2))) by VALUED_1:def 1;

      then

       A5: Z c= ( dom (c (#) f2)) by XBOOLE_1: 18;

      

       A6: for x st x in Z holds (f1 . x) = (a + (b * x)) by A3;

      then

       A7: (f1 + (c (#) f2)) is_differentiable_on Z by A2, A4, Th12;

      

       A8: for x st x in Z holds ( ln * (f1 + (c (#) f2))) is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then (f1 + (c (#) f2)) is_differentiable_in x & ((f1 + (c (#) f2)) . x) > 0 by A3, A7, FDIFF_1: 9;

        hence thesis by TAYLOR_1: 20;

      end;

      then

       A9: ( ln * (f1 + (c (#) f2))) is_differentiable_on Z by A1, FDIFF_1: 9;

      for x st x in Z holds ((( ln * (f1 + (c (#) f2))) `| Z) . x) = ((b + ((2 * c) * x)) / ((a + (b * x)) + (c * (x |^ 2))))

      proof

        let x;

        assume

         A10: x in Z;

        then x in ( dom (f1 + (c (#) f2))) by A1, FUNCT_1: 11;

        

        then

         A11: ((f1 + (c (#) f2)) . x) = ((f1 . x) + ((c (#) f2) . x)) by VALUED_1:def 1

        .= ((f1 . x) + (c * (f2 . x))) by A5, A10, VALUED_1:def 5

        .= ((a + (b * x)) + (c * (f2 . x))) by A3, A10

        .= ((a + (b * x)) + (c * (x #Z 2))) by A2, TAYLOR_1:def 1

        .= ((a + (b * x)) + (c * (x |^ 2))) by PREPOWER: 36;

        (f1 + (c (#) f2)) is_differentiable_in x & ((f1 + (c (#) f2)) . x) > 0 by A3, A7, A10, FDIFF_1: 9;

        

        then ( diff (( ln * (f1 + (c (#) f2))),x)) = (( diff ((f1 + (c (#) f2)),x)) / ((f1 + (c (#) f2)) . x)) by TAYLOR_1: 20

        .= ((((f1 + (c (#) f2)) `| Z) . x) / ((f1 + (c (#) f2)) . x)) by A7, A10, FDIFF_1:def 7

        .= ((b + ((2 * c) * x)) / ((a + (b * x)) + (c * (x |^ 2)))) by A2, A4, A6, A10, A11, Th12;

        hence thesis by A9, A10, FDIFF_1:def 7;

      end;

      hence thesis by A1, A8, FDIFF_1: 9;

    end;

    theorem :: FDIFF_4:14

    

     Th14: Z c= ( dom f) & (for x st x in Z holds (f . x) = (a + x) & (f . x) <> 0 ) implies (f ^ ) is_differentiable_on Z & for x st x in Z holds (((f ^ ) `| Z) . x) = ( - (1 / ((a + x) ^2 )))

    proof

      assume that

       A1: Z c= ( dom f) and

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

      

       A3: for x st x in Z holds (f . x) = ((1 * x) + a) by A2;

      then

       A4: f is_differentiable_on Z by A1, FDIFF_1: 23;

      

       A5: for x st x in Z holds (f . x) <> 0 by A2;

      then

       A6: (f ^ ) is_differentiable_on Z by A4, FDIFF_2: 22;

      now

        let x;

        assume

         A7: x in Z;

        then

         A8: (f . x) <> 0 & f is_differentiable_in x by A2, A4, FDIFF_1: 9;

        (((f ^ ) `| Z) . x) = ( diff ((f ^ ),x)) by A6, A7, FDIFF_1:def 7

        .= ( - (( diff (f,x)) / ((f . x) ^2 ))) by A8, FDIFF_2: 15

        .= ( - (((f `| Z) . x) / ((f . x) ^2 ))) by A4, A7, FDIFF_1:def 7

        .= ( - (1 / ((f . x) ^2 ))) by A1, A3, A7, FDIFF_1: 23

        .= ( - (1 / ((a + x) ^2 ))) by A2, A7;

        hence (((f ^ ) `| Z) . x) = ( - (1 / ((a + x) ^2 )));

      end;

      hence thesis by A4, A5, FDIFF_2: 22;

    end;

    theorem :: FDIFF_4:15

    Z c= ( dom (( - 1) (#) (f ^ ))) & (for x st x in Z holds (f . x) = (a + x) & (f . x) <> 0 ) implies (( - 1) (#) (f ^ )) is_differentiable_on Z & for x st x in Z holds (((( - 1) (#) (f ^ )) `| Z) . x) = (1 / ((a + x) ^2 ))

    proof

      assume that

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

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

      

       A3: ( dom (f ^ )) c= ( dom f) by RFUNCT_1: 1;

      Z c= ( dom (f ^ )) by A1, VALUED_1:def 5;

      then

       A4: Z c= ( dom f) by A3, XBOOLE_1: 1;

      then

       A5: (f ^ ) is_differentiable_on Z by A2, Th14;

      now

        let x;

        assume

         A6: x in Z;

        

        hence (((( - 1) (#) (f ^ )) `| Z) . x) = (( - 1) * ( diff ((f ^ ),x))) by A1, A5, FDIFF_1: 20

        .= (( - 1) * (((f ^ ) `| Z) . x)) by A5, A6, FDIFF_1:def 7

        .= (( - 1) * ( - (1 / ((a + x) ^2 )))) by A2, A4, A6, Th14

        .= (1 / ((a + x) ^2 ));

      end;

      hence thesis by A1, A5, FDIFF_1: 20;

    end;

    theorem :: FDIFF_4:16

    Z c= ( dom f) & (for x st x in Z holds (f . x) = (a - x) & (f . x) <> 0 ) implies (f ^ ) is_differentiable_on Z & for x st x in Z holds (((f ^ ) `| Z) . x) = (1 / ((a - x) ^2 ))

    proof

      assume that

       A1: Z c= ( dom f) and

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

      

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

      proof

        let x;

        assume x in Z;

        then (f . x) = (a - x) by A2;

        hence thesis;

      end;

      then

       A4: f is_differentiable_on Z by A1, FDIFF_1: 23;

      

       A5: for x st x in Z holds (f . x) <> 0 by A2;

      then

       A6: (f ^ ) is_differentiable_on Z by A4, FDIFF_2: 22;

      now

        let x;

        assume

         A7: x in Z;

        then

         A8: (f . x) <> 0 & f is_differentiable_in x by A2, A4, FDIFF_1: 9;

        (((f ^ ) `| Z) . x) = ( diff ((f ^ ),x)) by A6, A7, FDIFF_1:def 7

        .= ( - (( diff (f,x)) / ((f . x) ^2 ))) by A8, FDIFF_2: 15

        .= ( - (((f `| Z) . x) / ((f . x) ^2 ))) by A4, A7, FDIFF_1:def 7

        .= ( - (( - 1) / ((f . x) ^2 ))) by A1, A3, A7, FDIFF_1: 23

        .= ( - ( - (1 / ((f . x) ^2 )))) by XCMPLX_1: 187

        .= (1 / ((a - x) ^2 )) by A2, A7;

        hence (((f ^ ) `| Z) . x) = (1 / ((a - x) ^2 ));

      end;

      hence thesis by A4, A5, FDIFF_2: 22;

    end;

    theorem :: FDIFF_4:17

    

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

    proof

      assume that

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

       A2: f2 = ( #Z 2);

      

       A3: Z c= ( dom (f1 + (1 (#) f2))) & for x st x in Z holds (f1 . x) = ((a ^2 ) + ( 0 * x)) by A1, RFUNCT_1: 21;

      

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

      proof

        let x;

        assume

         A5: x in Z;

        (((f1 + f2) `| Z) . x) = (((f1 + (1 (#) f2)) `| Z) . x) by RFUNCT_1: 21

        .= ( 0 + ((2 * 1) * x)) by A2, A3, A5, Th12

        .= (2 * x);

        hence thesis;

      end;

      (f1 + (1 (#) f2)) is_differentiable_on Z by A2, A3, Th12;

      hence thesis by A4, RFUNCT_1: 21;

    end;

    theorem :: FDIFF_4:18

    Z c= ( dom ( ln * (f1 + f2))) & f2 = ( #Z 2) & (for x st x in Z holds (f1 . x) = (a ^2 ) & ((f1 + f2) . x) > 0 ) implies ( ln * (f1 + f2)) is_differentiable_on Z & for x st x in Z holds ((( ln * (f1 + f2)) `| Z) . x) = ((2 * x) / ((a ^2 ) + (x |^ 2)))

    proof

      assume that

       A1: Z c= ( dom ( ln * (f1 + f2))) and

       A2: f2 = ( #Z 2) and

       A3: for x st x in Z holds (f1 . x) = (a ^2 ) & ((f1 + f2) . x) > 0 ;

      f2 = (1 (#) f2) by RFUNCT_1: 21;

      then

       A4: for x st x in Z holds (f1 . x) = ((a ^2 ) + ( 0 * x)) & ((f1 + (1 (#) f2)) . x) > 0 by A3;

      

       A5: Z c= ( dom ( ln * (f1 + (1 (#) f2)))) by A1, RFUNCT_1: 21;

      

       A6: for x st x in Z holds ((( ln * (f1 + f2)) `| Z) . x) = ((2 * x) / ((a ^2 ) + (x |^ 2)))

      proof

        let x;

        assume

         A7: x in Z;

        ((( ln * (f1 + f2)) `| Z) . x) = ((( ln * (f1 + (1 (#) f2))) `| Z) . x) by RFUNCT_1: 21

        .= (( 0 + ((2 * 1) * x)) / (((a ^2 ) + ( 0 * x)) + (1 * (x |^ 2)))) by A2, A5, A4, A7, Th13

        .= ((2 * x) / ((a ^2 ) + (x |^ 2)));

        hence thesis;

      end;

      ( ln * (f1 + (1 (#) f2))) is_differentiable_on Z by A2, A5, A4, Th13;

      hence thesis by A6, RFUNCT_1: 21;

    end;

    theorem :: FDIFF_4:19

    Z c= ( dom ( - ( ln * (f1 - f2)))) & f2 = ( #Z 2) & (for x st x in Z holds (f1 . x) = (a ^2 ) & ((f1 - f2) . x) > 0 ) implies ( - ( ln * (f1 - f2))) is_differentiable_on Z & for x st x in Z holds ((( - ( ln * (f1 - f2))) `| Z) . x) = ((2 * x) / ((a ^2 ) - (x |^ 2)))

    proof

      assume that

       A1: Z c= ( dom ( - ( ln * (f1 - f2)))) and

       A2: f2 = ( #Z 2) and

       A3: for x st x in Z holds (f1 . x) = (a ^2 ) & ((f1 - f2) . x) > 0 ;

      

       A4: Z c= ( dom ( ln * (f1 + (( - 1) (#) f2)))) & for x st x in Z holds (f1 . x) = ((a ^2 ) + ( 0 * x)) & ((f1 + (( - 1) (#) f2)) . x) > 0 by A1, A3, VALUED_1: 8;

      then

       A5: ( ln * (f1 + (( - 1) (#) f2))) is_differentiable_on Z by A2, Th13;

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

      proof

        let x;

        assume

         A6: x in Z;

        

        then ((( - ( ln * (f1 - f2))) `| Z) . x) = (( - 1) * ( diff (( ln * (f1 + (( - 1) (#) f2))),x))) by A1, A5, FDIFF_1: 20

        .= (( - 1) * ((( ln * (f1 + (( - 1) (#) f2))) `| Z) . x)) by A5, A6, FDIFF_1:def 7

        .= (( - 1) * (( 0 + ((2 * ( - 1)) * x)) / (((a ^2 ) + ( 0 * x)) + (( - 1) * (x |^ 2))))) by A2, A4, A6, Th13

        .= ((( - 1) * ((2 * ( - 1)) * x)) / ((a ^2 ) + (( - 1) * (x |^ 2)))) by XCMPLX_1: 74

        .= ((2 * x) / ((a ^2 ) - (x |^ 2)));

        hence thesis;

      end;

      hence thesis by A1, A5, FDIFF_1: 20;

    end;

    theorem :: FDIFF_4:20

    

     Th20: Z c= ( dom (f1 + f2)) & (for x st x in Z holds (f1 . x) = a) & f2 = ( #Z 3) implies (f1 + f2) is_differentiable_on Z & for x st x in Z holds (((f1 + f2) `| Z) . x) = (3 * (x |^ 2))

    proof

      assume that

       A1: Z c= ( dom (f1 + f2)) and

       A2: for x st x in Z holds (f1 . x) = a and

       A3: f2 = ( #Z 3);

      

       A4: for x st x in Z holds f2 is_differentiable_in x by A3, TAYLOR_1: 2;

      

       A5: Z c= (( dom f1) /\ ( dom f2)) by A1, VALUED_1:def 1;

      then

       A6: Z c= ( dom f1) by XBOOLE_1: 18;

      

       A7: for x st x in Z holds (f1 . x) = (( 0 * x) + a) by A2;

      then

       A8: f1 is_differentiable_on Z by A6, FDIFF_1: 23;

      Z c= ( dom f2) by A5, XBOOLE_1: 18;

      then

       A9: f2 is_differentiable_on Z by A4, FDIFF_1: 9;

      

       A10: for x st x in Z holds ((f2 `| Z) . x) = (3 * (x #Z (3 - 1)))

      proof

        let x;

        assume

         A11: x in Z;

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

        hence thesis by A9, A11, FDIFF_1:def 7;

      end;

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

      proof

        let x;

        assume

         A12: x in Z;

        then (((f1 + f2) `| Z) . x) = (( diff (f1,x)) + ( diff (f2,x))) by A1, A8, A9, FDIFF_1: 18;

        

        hence (((f1 + f2) `| Z) . x) = (((f1 `| Z) . x) + ( diff (f2,x))) by A8, A12, FDIFF_1:def 7

        .= (((f1 `| Z) . x) + ((f2 `| Z) . x)) by A9, A12, FDIFF_1:def 7

        .= ( 0 + ((f2 `| Z) . x)) by A6, A7, A12, FDIFF_1: 23

        .= (3 * (x #Z (3 - 1))) by A10, A12

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

      end;

      hence thesis by A1, A8, A9, FDIFF_1: 18;

    end;

    theorem :: FDIFF_4:21

    Z c= ( dom ( ln * (f1 + f2))) & f2 = ( #Z 3) & (for x st x in Z holds (f1 . x) = a & ((f1 + f2) . x) > 0 ) implies ( ln * (f1 + f2)) is_differentiable_on Z & for x st x in Z holds ((( ln * (f1 + f2)) `| Z) . x) = ((3 * (x |^ 2)) / (a + (x |^ 3)))

    proof

      assume that

       A1: Z c= ( dom ( ln * (f1 + f2))) and

       A2: f2 = ( #Z 3) and

       A3: for x st x in Z holds (f1 . x) = a & ((f1 + f2) . x) > 0 ;

      for y be object st y in Z holds y in ( dom (f1 + f2)) by A1, FUNCT_1: 11;

      then

       A4: Z c= ( dom (f1 + f2)) by TARSKI:def 3;

      

       A5: for x st x in Z holds (f1 . x) = a by A3;

      then

       A6: (f1 + f2) is_differentiable_on Z by A2, A4, Th20;

      

       A7: for x st x in Z holds ( ln * (f1 + f2)) is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then (f1 + f2) is_differentiable_in x & ((f1 + f2) . x) > 0 by A3, A6, FDIFF_1: 9;

        hence thesis by TAYLOR_1: 20;

      end;

      then

       A8: ( ln * (f1 + f2)) is_differentiable_on Z by A1, FDIFF_1: 9;

      for x st x in Z holds ((( ln * (f1 + f2)) `| Z) . x) = ((3 * (x |^ 2)) / (a + (x |^ 3)))

      proof

        let x;

        assume

         A9: x in Z;

        then

         A10: x in ( dom (f1 + f2)) by A1, FUNCT_1: 11;

        (f1 + f2) is_differentiable_in x & ((f1 + f2) . x) > 0 by A3, A6, A9, FDIFF_1: 9;

        

        then ( diff (( ln * (f1 + f2)),x)) = (( diff ((f1 + f2),x)) / ((f1 + f2) . x)) by TAYLOR_1: 20

        .= ((((f1 + f2) `| Z) . x) / ((f1 + f2) . x)) by A6, A9, FDIFF_1:def 7

        .= ((3 * (x |^ 2)) / ((f1 + f2) . x)) by A2, A4, A5, A9, Th20

        .= ((3 * (x |^ 2)) / ((f1 . x) + (f2 . x))) by A10, VALUED_1:def 1

        .= ((3 * (x |^ 2)) / (a + (f2 . x))) by A3, A9

        .= ((3 * (x |^ 2)) / (a + (x #Z 3))) by A2, TAYLOR_1:def 1

        .= ((3 * (x |^ 2)) / (a + (x |^ 3))) by PREPOWER: 36;

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

      end;

      hence thesis by A1, A7, FDIFF_1: 9;

    end;

    theorem :: FDIFF_4:22

    Z c= ( dom ( ln * (f1 / f2))) & (for x st x in Z holds (f1 . x) = (a + x) & (f1 . x) > 0 & (f2 . x) = (a - x) & (f2 . x) > 0 ) implies ( ln * (f1 / f2)) is_differentiable_on Z & for x st x in Z holds ((( ln * (f1 / f2)) `| Z) . x) = ((2 * a) / ((a ^2 ) - (x ^2 )))

    proof

      assume that

       A1: Z c= ( dom ( ln * (f1 / f2))) and

       A2: for x st x in Z holds (f1 . x) = (a + x) & (f1 . x) > 0 & (f2 . x) = (a - x) & (f2 . x) > 0 ;

      for y be object st y in Z holds y in ( dom (f1 / f2)) by A1, FUNCT_1: 11;

      then Z c= ( dom (f1 / f2)) by TARSKI:def 3;

      then

       A3: Z c= (( dom f1) /\ (( dom f2) \ (f2 " { 0 }))) by RFUNCT_1:def 1;

      then

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

      

       A5: for x st x in Z holds (f1 . x) = ((1 * x) + a) by A2;

      then

       A6: f1 is_differentiable_on Z by A4, FDIFF_1: 23;

      

       A7: for x st x in Z holds (f2 . x) = ((( - 1) * x) + a)

      proof

        let x;

        assume x in Z;

        then (f2 . x) = (a - x) by A2;

        hence thesis;

      end;

      

       A8: Z c= ( dom f2) by A3, XBOOLE_1: 1;

      then

       A9: f2 is_differentiable_on Z by A7, FDIFF_1: 23;

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

      then

       A10: (f1 / f2) is_differentiable_on Z by A6, A9, FDIFF_2: 21;

      

       A11: for x st x in Z holds (((f1 / f2) `| Z) . x) = ((2 * a) / ((a - x) ^2 ))

      proof

        let x;

        assume

         A12: x in Z;

        then

         A13: (f2 . x) <> 0 by A2;

        

         A14: (f1 . x) = (a + x) & (f2 . x) = (a - x) by A2, A12;

        f1 is_differentiable_in x & f2 is_differentiable_in x by A6, A9, A12, FDIFF_1: 9;

        

        then ( diff ((f1 / f2),x)) = (((( diff (f1,x)) * (f2 . x)) - (( diff (f2,x)) * (f1 . x))) / ((f2 . x) ^2 )) by A13, FDIFF_2: 14

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

        .= (((((f1 `| Z) . x) * (f2 . x)) - (((f2 `| Z) . x) * (f1 . x))) / ((f2 . x) ^2 )) by A9, A12, FDIFF_1:def 7

        .= (((1 * (f2 . x)) - (((f2 `| Z) . x) * (f1 . x))) / ((f2 . x) ^2 )) by A4, A5, A12, FDIFF_1: 23

        .= (((1 * (f2 . x)) - (( - 1) * (f1 . x))) / ((f2 . x) ^2 )) by A8, A7, A12, FDIFF_1: 23

        .= ((2 * a) / ((a - x) ^2 )) by A14;

        hence thesis by A10, A12, FDIFF_1:def 7;

      end;

      

       A15: for x st x in Z holds ((f1 / f2) . x) > 0

      proof

        let x;

        assume

         A16: x in Z;

        then x in ( dom (f1 / f2)) by A1, FUNCT_1: 11;

        

        then

         A17: ((f1 / f2) . x) = ((f1 . x) * ((f2 . x) " )) by RFUNCT_1:def 1

        .= ((f1 . x) / (f2 . x)) by XCMPLX_0:def 9;

        (f1 . x) > 0 & (f2 . x) > 0 by A2, A16;

        hence thesis by A17, XREAL_1: 139;

      end;

      

       A18: for x st x in Z holds ( ln * (f1 / f2)) is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then (f1 / f2) is_differentiable_in x & ((f1 / f2) . x) > 0 by A10, A15, FDIFF_1: 9;

        hence thesis by TAYLOR_1: 20;

      end;

      then

       A19: ( ln * (f1 / f2)) is_differentiable_on Z by A1, FDIFF_1: 9;

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

      proof

        let x;

        assume

         A20: x in Z;

        then

         A21: (f2 . x) = (a - x) & (f2 . x) > 0 by A2;

        

         A22: (f1 . x) = (a + x) & (f2 . x) = (a - x) by A2, A20;

        

         A23: x in ( dom (f1 / f2)) by A1, A20, FUNCT_1: 11;

        (f1 / f2) is_differentiable_in x & ((f1 / f2) . x) > 0 by A10, A15, A20, FDIFF_1: 9;

        

        then ( diff (( ln * (f1 / f2)),x)) = (( diff ((f1 / f2),x)) / ((f1 / f2) . x)) by TAYLOR_1: 20

        .= ((((f1 / f2) `| Z) . x) / ((f1 / f2) . x)) by A10, A20, FDIFF_1:def 7

        .= (((2 * a) / ((a - x) ^2 )) / ((f1 / f2) . x)) by A11, A20

        .= (((2 * a) / ((a - x) ^2 )) / ((f1 . x) * ((f2 . x) " ))) by A23, RFUNCT_1:def 1

        .= (((2 * a) / ((a - x) * (a - x))) / ((a + x) / (a - x))) by A22, XCMPLX_0:def 9

        .= ((((2 * a) / (a - x)) / (a - x)) / ((a + x) / (a - x))) by XCMPLX_1: 78

        .= ((((2 * a) / (a - x)) / ((a + x) / (a - x))) / (a - x)) by XCMPLX_1: 48

        .= (((2 * a) / (a + x)) / (a - x)) by A21, XCMPLX_1: 55

        .= ((2 * a) / ((a + x) * (a - x))) by XCMPLX_1: 78

        .= ((2 * a) / ((a ^2 ) - (x ^2 )));

        hence thesis by A19, A20, FDIFF_1:def 7;

      end;

      hence thesis by A1, A18, FDIFF_1: 9;

    end;

    theorem :: FDIFF_4:23

    Z c= ( dom ( ln * (f1 / f2))) & (for x st x in Z holds (f1 . x) = (x - a) & (f1 . x) > 0 & (f2 . x) = (x + a) & (f2 . x) > 0 ) implies ( ln * (f1 / f2)) is_differentiable_on Z & for x st x in Z holds ((( ln * (f1 / f2)) `| Z) . x) = ((2 * a) / ((x ^2 ) - (a ^2 )))

    proof

      assume that

       A1: Z c= ( dom ( ln * (f1 / f2))) and

       A2: for x st x in Z holds (f1 . x) = (x - a) & (f1 . x) > 0 & (f2 . x) = (x + a) & (f2 . x) > 0 ;

      

       A3: for x st x in Z holds (f2 . x) = ((1 * x) + a) by A2;

      for y be object st y in Z holds y in ( dom (f1 / f2)) by A1, FUNCT_1: 11;

      then Z c= ( dom (f1 / f2)) by TARSKI:def 3;

      then

       A4: Z c= (( dom f1) /\ (( dom f2) \ (f2 " { 0 }))) by RFUNCT_1:def 1;

      then

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

      

       A6: Z c= ( dom f2) by A4, XBOOLE_1: 1;

      then

       A7: f2 is_differentiable_on Z by A3, FDIFF_1: 23;

      

       A8: for x st x in Z holds (f1 . x) = ((1 * x) + ( - a))

      proof

        let x;

        

         A9: ((1 * x) + ( - a)) = ((1 * x) - a);

        assume x in Z;

        hence thesis by A2, A9;

      end;

      then

       A10: f1 is_differentiable_on Z by A5, FDIFF_1: 23;

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

      then

       A11: (f1 / f2) is_differentiable_on Z by A10, A7, FDIFF_2: 21;

      

       A12: for x st x in Z holds (((f1 / f2) `| Z) . x) = ((2 * a) / ((x + a) ^2 ))

      proof

        let x;

        assume

         A13: x in Z;

        then

         A14: (f2 . x) <> 0 by A2;

        

         A15: (f1 . x) = (x - a) & (f2 . x) = (x + a) by A2, A13;

        f1 is_differentiable_in x & f2 is_differentiable_in x by A10, A7, A13, FDIFF_1: 9;

        

        then ( diff ((f1 / f2),x)) = (((( diff (f1,x)) * (f2 . x)) - (( diff (f2,x)) * (f1 . x))) / ((f2 . x) ^2 )) by A14, FDIFF_2: 14

        .= (((((f1 `| Z) . x) * (f2 . x)) - (( diff (f2,x)) * (f1 . x))) / ((f2 . x) ^2 )) by A10, A13, FDIFF_1:def 7

        .= (((((f1 `| Z) . x) * (f2 . x)) - (((f2 `| Z) . x) * (f1 . x))) / ((f2 . x) ^2 )) by A7, A13, FDIFF_1:def 7

        .= (((1 * (f2 . x)) - (((f2 `| Z) . x) * (f1 . x))) / ((f2 . x) ^2 )) by A5, A8, A13, FDIFF_1: 23

        .= (((1 * (f2 . x)) - (1 * (f1 . x))) / ((f2 . x) ^2 )) by A6, A3, A13, FDIFF_1: 23

        .= ((2 * a) / ((x + a) ^2 )) by A15;

        hence thesis by A11, A13, FDIFF_1:def 7;

      end;

      

       A16: for x st x in Z holds ((f1 / f2) . x) > 0

      proof

        let x;

        assume

         A17: x in Z;

        then x in ( dom (f1 / f2)) by A1, FUNCT_1: 11;

        

        then

         A18: ((f1 / f2) . x) = ((f1 . x) * ((f2 . x) " )) by RFUNCT_1:def 1

        .= ((f1 . x) / (f2 . x)) by XCMPLX_0:def 9;

        (f1 . x) > 0 & (f2 . x) > 0 by A2, A17;

        hence thesis by A18, XREAL_1: 139;

      end;

      

       A19: for x st x in Z holds ( ln * (f1 / f2)) is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then (f1 / f2) is_differentiable_in x & ((f1 / f2) . x) > 0 by A11, A16, FDIFF_1: 9;

        hence thesis by TAYLOR_1: 20;

      end;

      then

       A20: ( ln * (f1 / f2)) is_differentiable_on Z by A1, FDIFF_1: 9;

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

      proof

        let x;

        assume

         A21: x in Z;

        then

         A22: (f2 . x) = (x + a) & (f2 . x) > 0 by A2;

        

         A23: (f1 . x) = (x - a) & (f2 . x) = (x + a) by A2, A21;

        

         A24: x in ( dom (f1 / f2)) by A1, A21, FUNCT_1: 11;

        (f1 / f2) is_differentiable_in x & ((f1 / f2) . x) > 0 by A11, A16, A21, FDIFF_1: 9;

        

        then ( diff (( ln * (f1 / f2)),x)) = (( diff ((f1 / f2),x)) / ((f1 / f2) . x)) by TAYLOR_1: 20

        .= ((((f1 / f2) `| Z) . x) / ((f1 / f2) . x)) by A11, A21, FDIFF_1:def 7

        .= (((2 * a) / ((x + a) ^2 )) / ((f1 / f2) . x)) by A12, A21

        .= (((2 * a) / ((x + a) ^2 )) / ((f1 . x) * ((f2 . x) " ))) by A24, RFUNCT_1:def 1

        .= (((2 * a) / ((x + a) * (x + a))) / ((x - a) / (x + a))) by A23, XCMPLX_0:def 9

        .= ((((2 * a) / (x + a)) / (x + a)) / ((x - a) / (x + a))) by XCMPLX_1: 78

        .= ((((2 * a) / (x + a)) / ((x - a) / (x + a))) / (x + a)) by XCMPLX_1: 48

        .= (((2 * a) / (x - a)) / (x + a)) by A22, XCMPLX_1: 55

        .= ((2 * a) / ((x - a) * (x + a))) by XCMPLX_1: 78

        .= ((2 * a) / ((x ^2 ) - (a ^2 )));

        hence thesis by A20, A21, FDIFF_1:def 7;

      end;

      hence thesis by A1, A19, FDIFF_1: 9;

    end;

    theorem :: FDIFF_4:24

    

     Th24: Z c= ( dom ( ln * (f1 / f2))) & (for x st x in Z holds (f1 . x) = (x - a) & (f1 . x) > 0 & (f2 . x) = (x - b) & (f2 . x) > 0 ) implies ( ln * (f1 / f2)) is_differentiable_on Z & for x st x in Z holds ((( ln * (f1 / f2)) `| Z) . x) = ((a - b) / ((x - a) * (x - b)))

    proof

      assume that

       A1: Z c= ( dom ( ln * (f1 / f2))) and

       A2: for x st x in Z holds (f1 . x) = (x - a) & (f1 . x) > 0 & (f2 . x) = (x - b) & (f2 . x) > 0 ;

      

       A3: for x st x in Z holds (f1 . x) = ((1 * x) + ( - a)) & (f2 . x) = ((1 * x) + ( - b))

      proof

        let x;

        

         A4: ((1 * x) + ( - a)) = ((1 * x) - a) & ((1 * x) + ( - b)) = ((1 * x) - b);

        assume x in Z;

        hence thesis by A2, A4;

      end;

      then

       A5: for x st x in Z holds (f1 . x) = ((1 * x) + ( - a));

      for y be object st y in Z holds y in ( dom (f1 / f2)) by A1, FUNCT_1: 11;

      then Z c= ( dom (f1 / f2)) by TARSKI:def 3;

      then

       A6: Z c= (( dom f1) /\ (( dom f2) \ (f2 " { 0 }))) by RFUNCT_1:def 1;

      then

       A7: Z c= ( dom f1) by XBOOLE_1: 18;

      then

       A8: f1 is_differentiable_on Z by A5, FDIFF_1: 23;

      

       A9: for x st x in Z holds (f2 . x) = ((1 * x) + ( - b)) by A3;

      

       A10: Z c= ( dom f2) by A6, XBOOLE_1: 1;

      then

       A11: f2 is_differentiable_on Z by A9, FDIFF_1: 23;

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

      then

       A12: (f1 / f2) is_differentiable_on Z by A8, A11, FDIFF_2: 21;

      

       A13: for x st x in Z holds (((f1 / f2) `| Z) . x) = ((a - b) / ((x - b) ^2 ))

      proof

        let x;

        assume

         A14: x in Z;

        then

         A15: (f2 . x) <> 0 by A2;

        

         A16: (f1 . x) = (x - a) & (f2 . x) = (x - b) by A2, A14;

        f1 is_differentiable_in x & f2 is_differentiable_in x by A8, A11, A14, FDIFF_1: 9;

        

        then ( diff ((f1 / f2),x)) = (((( diff (f1,x)) * (f2 . x)) - (( diff (f2,x)) * (f1 . x))) / ((f2 . x) ^2 )) by A15, FDIFF_2: 14

        .= (((((f1 `| Z) . x) * (f2 . x)) - (( diff (f2,x)) * (f1 . x))) / ((f2 . x) ^2 )) by A8, A14, FDIFF_1:def 7

        .= (((((f1 `| Z) . x) * (f2 . x)) - (((f2 `| Z) . x) * (f1 . x))) / ((f2 . x) ^2 )) by A11, A14, FDIFF_1:def 7

        .= (((1 * (f2 . x)) - (((f2 `| Z) . x) * (f1 . x))) / ((f2 . x) ^2 )) by A7, A5, A14, FDIFF_1: 23

        .= (((1 * (f2 . x)) - (1 * (f1 . x))) / ((f2 . x) ^2 )) by A10, A9, A14, FDIFF_1: 23

        .= ((a - b) / ((x - b) ^2 )) by A16;

        hence thesis by A12, A14, FDIFF_1:def 7;

      end;

      

       A17: for x st x in Z holds ((f1 / f2) . x) > 0

      proof

        let x;

        assume

         A18: x in Z;

        then x in ( dom (f1 / f2)) by A1, FUNCT_1: 11;

        

        then

         A19: ((f1 / f2) . x) = ((f1 . x) * ((f2 . x) " )) by RFUNCT_1:def 1

        .= ((f1 . x) / (f2 . x)) by XCMPLX_0:def 9;

        (f1 . x) > 0 & (f2 . x) > 0 by A2, A18;

        hence thesis by A19, XREAL_1: 139;

      end;

      

       A20: for x st x in Z holds ( ln * (f1 / f2)) is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then (f1 / f2) is_differentiable_in x & ((f1 / f2) . x) > 0 by A12, A17, FDIFF_1: 9;

        hence thesis by TAYLOR_1: 20;

      end;

      then

       A21: ( ln * (f1 / f2)) is_differentiable_on Z by A1, FDIFF_1: 9;

      for x st x in Z holds ((( ln * (f1 / f2)) `| Z) . x) = ((a - b) / ((x - a) * (x - b)))

      proof

        let x;

        assume

         A22: x in Z;

        then

         A23: (f2 . x) = (x - b) & (f2 . x) > 0 by A2;

        

         A24: (f1 . x) = (x - a) & (f2 . x) = (x - b) by A2, A22;

        

         A25: x in ( dom (f1 / f2)) by A1, A22, FUNCT_1: 11;

        (f1 / f2) is_differentiable_in x & ((f1 / f2) . x) > 0 by A12, A17, A22, FDIFF_1: 9;

        

        then ( diff (( ln * (f1 / f2)),x)) = (( diff ((f1 / f2),x)) / ((f1 / f2) . x)) by TAYLOR_1: 20

        .= ((((f1 / f2) `| Z) . x) / ((f1 / f2) . x)) by A12, A22, FDIFF_1:def 7

        .= (((a - b) / ((x - b) ^2 )) / ((f1 / f2) . x)) by A13, A22

        .= (((a - b) / ((x - b) ^2 )) / ((f1 . x) * ((f2 . x) " ))) by A25, RFUNCT_1:def 1

        .= (((a - b) / ((x - b) * (x - b))) / ((x - a) / (x - b))) by A24, XCMPLX_0:def 9

        .= ((((a - b) / (x - b)) / (x - b)) / ((x - a) / (x - b))) by XCMPLX_1: 78

        .= ((((a - b) / (x - b)) / ((x - a) / (x - b))) / (x - b)) by XCMPLX_1: 48

        .= (((a - b) / (x - a)) / (x - b)) by A23, XCMPLX_1: 55

        .= ((a - b) / ((x - a) * (x - b))) by XCMPLX_1: 78;

        hence thesis by A21, A22, FDIFF_1:def 7;

      end;

      hence thesis by A1, A20, FDIFF_1: 9;

    end;

    theorem :: FDIFF_4:25

    Z c= ( dom ((1 / (a - b)) (#) f)) & f = ( ln * (f1 / f2)) & (for x st x in Z holds (f1 . x) = (x - a) & (f1 . x) > 0 & (f2 . x) = (x - b) & (f2 . x) > 0 & (a - b) <> 0 ) implies ((1 / (a - b)) (#) f) is_differentiable_on Z & for x st x in Z holds ((((1 / (a - b)) (#) f) `| Z) . x) = (1 / ((x - a) * (x - b)))

    proof

      assume that

       A1: Z c= ( dom ((1 / (a - b)) (#) f)) and

       A2: f = ( ln * (f1 / f2)) and

       A3: for x st x in Z holds (f1 . x) = (x - a) & (f1 . x) > 0 & (f2 . x) = (x - b) & (f2 . x) > 0 & (a - b) <> 0 ;

      

       A4: (for x st x in Z holds (f1 . x) = (x - a) & (f1 . x) > 0 & (f2 . x) = (x - b) & (f2 . x) > 0 ) & Z c= ( dom f) by A1, A3, VALUED_1:def 5;

      then

       A5: f is_differentiable_on Z by A2, Th24;

      for x st x in Z holds ((((1 / (a - b)) (#) f) `| Z) . x) = (1 / ((x - a) * (x - b)))

      proof

        let x;

        assume

         A6: x in Z;

        then

         A7: (a - b) <> 0 by A3;

        ((((1 / (a - b)) (#) f) `| Z) . x) = ((1 / (a - b)) * ( diff (f,x))) by A1, A5, A6, FDIFF_1: 20

        .= ((1 / (a - b)) * ((f `| Z) . x)) by A5, A6, FDIFF_1:def 7

        .= ((1 / (a - b)) * ((a - b) / ((x - a) * (x - b)))) by A2, A4, A6, Th24

        .= (((1 / (a - b)) * (a - b)) / ((x - a) * (x - b))) by XCMPLX_1: 74

        .= (1 / ((x - a) * (x - b))) by A7, XCMPLX_1: 106;

        hence thesis;

      end;

      hence thesis by A1, A5, FDIFF_1: 20;

    end;

    theorem :: FDIFF_4:26

    Z c= ( dom ( ln * (f1 / f2))) & f2 = ( #Z 2) & (for x st x in Z holds (f1 . x) = (x - a) & (f1 . x) > 0 & (f2 . x) > 0 & x <> 0 ) implies ( ln * (f1 / f2)) is_differentiable_on Z & for x st x in Z holds ((( ln * (f1 / f2)) `| Z) . x) = (((2 * a) - x) / (x * (x - a)))

    proof

      assume that

       A1: Z c= ( dom ( ln * (f1 / f2))) and

       A2: f2 = ( #Z 2) and

       A3: for x st x in Z holds (f1 . x) = (x - a) & (f1 . x) > 0 & (f2 . x) > 0 & x <> 0 ;

      

       A4: for x st x in Z holds f2 is_differentiable_in x by A2, TAYLOR_1: 2;

      for y be object st y in Z holds y in ( dom (f1 / f2)) by A1, FUNCT_1: 11;

      then Z c= ( dom (f1 / f2)) by TARSKI:def 3;

      then

       A5: Z c= (( dom f1) /\ (( dom f2) \ (f2 " { 0 }))) by RFUNCT_1:def 1;

      then

       A6: Z c= ( dom f1) by XBOOLE_1: 18;

      

       A7: for x st x in Z holds (f1 . x) = ((1 * x) + ( - a))

      proof

        let x;

        

         A8: ((1 * x) + ( - a)) = ((1 * x) - a);

        assume x in Z;

        hence thesis by A3, A8;

      end;

      then

       A9: f1 is_differentiable_on Z by A6, FDIFF_1: 23;

      

       A10: Z c= ( dom f2) by A5, XBOOLE_1: 1;

      then

       A11: f2 is_differentiable_on Z by A4, FDIFF_1: 9;

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

      then

       A12: (f1 / f2) is_differentiable_on Z by A9, A11, FDIFF_2: 21;

      

       A13: f2 is_differentiable_on Z by A10, A4, FDIFF_1: 9;

      

       A14: for x st x in Z holds ((f2 `| Z) . x) = (2 * x)

      proof

        let x;

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

        then

         A15: ( diff (f2,x)) = (2 * x) by A2, TAYLOR_1: 2;

        assume x in Z;

        hence thesis by A13, A15, FDIFF_1:def 7;

      end;

      

       A16: for x st x in Z holds (((f1 / f2) `| Z) . x) = (((2 * a) - x) / (x |^ 3))

      proof

        let x;

        

         A17: f2 is_differentiable_in x by A2, TAYLOR_1: 2;

        

         A18: (f2 . x) = (x #Z 2) by A2, TAYLOR_1:def 1

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

        assume

         A19: x in Z;

        then

         A20: x <> 0 by A3;

        f1 is_differentiable_in x & (f2 . x) <> 0 by A3, A9, A19, FDIFF_1: 9;

        

        then ( diff ((f1 / f2),x)) = (((( diff (f1,x)) * (f2 . x)) - (( diff (f2,x)) * (f1 . x))) / ((f2 . x) ^2 )) by A17, FDIFF_2: 14

        .= (((((f1 `| Z) . x) * (f2 . x)) - (( diff (f2,x)) * (f1 . x))) / ((f2 . x) ^2 )) by A9, A19, FDIFF_1:def 7

        .= (((((f1 `| Z) . x) * (f2 . x)) - (((f2 `| Z) . x) * (f1 . x))) / ((f2 . x) ^2 )) by A11, A19, FDIFF_1:def 7

        .= (((1 * (f2 . x)) - (((f2 `| Z) . x) * (f1 . x))) / ((f2 . x) ^2 )) by A6, A7, A19, FDIFF_1: 23

        .= (((1 * (f2 . x)) - ((2 * x) * (f1 . x))) / ((f2 . x) ^2 )) by A14, A19

        .= (((x |^ (1 + 1)) - ((2 * x) * (x - a))) / ((x |^ 2) ^2 )) by A3, A19, A18

        .= ((((x |^ 1) * x) - ((2 * x) * (x - a))) / ((x |^ 2) ^2 )) by NEWTON: 6

        .= (((x * x) - ((2 * x) * (x - a))) / ((x |^ 2) ^2 ))

        .= ((x * ((2 * a) - x)) / (x |^ (2 + 2))) by NEWTON: 8

        .= ((x * ((2 * a) - x)) / (x |^ (3 + 1)))

        .= ((x * ((2 * a) - x)) / ((x |^ 3) * x)) by NEWTON: 6

        .= (((2 * a) - x) / (x |^ 3)) by A20, XCMPLX_1: 91;

        hence thesis by A12, A19, FDIFF_1:def 7;

      end;

      

       A21: for x st x in Z holds ((f1 / f2) . x) > 0

      proof

        let x;

        assume

         A22: x in Z;

        then x in ( dom (f1 / f2)) by A1, FUNCT_1: 11;

        

        then

         A23: ((f1 / f2) . x) = ((f1 . x) * ((f2 . x) " )) by RFUNCT_1:def 1

        .= ((f1 . x) / (f2 . x)) by XCMPLX_0:def 9;

        (f1 . x) > 0 & (f2 . x) > 0 by A3, A22;

        hence thesis by A23, XREAL_1: 139;

      end;

      

       A24: for x st x in Z holds ( ln * (f1 / f2)) is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then (f1 / f2) is_differentiable_in x & ((f1 / f2) . x) > 0 by A12, A21, FDIFF_1: 9;

        hence thesis by TAYLOR_1: 20;

      end;

      then

       A25: ( ln * (f1 / f2)) is_differentiable_on Z by A1, FDIFF_1: 9;

      for x st x in Z holds ((( ln * (f1 / f2)) `| Z) . x) = (((2 * a) - x) / (x * (x - a)))

      proof

        let x;

        assume

         A26: x in Z;

        then

         A27: x in ( dom (f1 / f2)) by A1, FUNCT_1: 11;

        

         A28: (f2 . x) = (x #Z 2) by A2, TAYLOR_1:def 1

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

        then

         A29: (x |^ 2) > 0 by A3, A26;

        

         A30: (f1 . x) = (x - a) by A3, A26;

        (f1 / f2) is_differentiable_in x & ((f1 / f2) . x) > 0 by A12, A21, A26, FDIFF_1: 9;

        

        then ( diff (( ln * (f1 / f2)),x)) = (( diff ((f1 / f2),x)) / ((f1 / f2) . x)) by TAYLOR_1: 20

        .= ((((f1 / f2) `| Z) . x) / ((f1 / f2) . x)) by A12, A26, FDIFF_1:def 7

        .= ((((2 * a) - x) / (x |^ 3)) / ((f1 / f2) . x)) by A16, A26

        .= ((((2 * a) - x) / (x |^ 3)) / ((f1 . x) * ((f2 . x) " ))) by A27, RFUNCT_1:def 1

        .= ((((2 * a) - x) / (x |^ (2 + 1))) / ((x - a) / (x |^ 2))) by A28, A30, XCMPLX_0:def 9

        .= ((((2 * a) - x) / ((x |^ 2) * x)) / ((x - a) / (x |^ 2))) by NEWTON: 6

        .= (((((2 * a) - x) / (x |^ 2)) / x) / ((x - a) / (x |^ 2))) by XCMPLX_1: 78

        .= (((((2 * a) - x) / (x |^ 2)) / ((x - a) / (x |^ 2))) / x) by XCMPLX_1: 48

        .= ((((2 * a) - x) / (x - a)) / x) by A29, XCMPLX_1: 55

        .= (((2 * a) - x) / (x * (x - a))) by XCMPLX_1: 78;

        hence thesis by A25, A26, FDIFF_1:def 7;

      end;

      hence thesis by A1, A24, FDIFF_1: 9;

    end;

    theorem :: FDIFF_4:27

    

     Th27: Z c= ( dom (( #R (3 / 2)) * f)) & (for x st x in Z holds (f . x) = (a + x) & (f . x) > 0 ) implies (( #R (3 / 2)) * f) is_differentiable_on Z & for x st x in Z holds (((( #R (3 / 2)) * f) `| Z) . x) = ((3 / 2) * ((a + x) #R (1 / 2)))

    proof

      assume that

       A1: Z c= ( dom (( #R (3 / 2)) * f)) and

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

      for y be object st y in Z holds y in ( dom f) by A1, FUNCT_1: 11;

      then

       A3: Z c= ( dom f) by TARSKI:def 3;

      

       A4: for x st x in Z holds (f . x) = ((1 * x) + a) by A2;

      then

       A5: f is_differentiable_on Z by A3, FDIFF_1: 23;

      

       A6: for x st x in Z holds (( #R (3 / 2)) * f) is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then f is_differentiable_in x & (f . x) > 0 by A2, A5, FDIFF_1: 9;

        hence thesis by TAYLOR_1: 22;

      end;

      then

       A7: (( #R (3 / 2)) * f) is_differentiable_on Z by A1, FDIFF_1: 9;

      for x st x in Z holds (((( #R (3 / 2)) * f) `| Z) . x) = ((3 / 2) * ((a + x) #R (1 / 2)))

      proof

        let x;

        assume

         A8: x in Z;

        then

         A9: (f . x) = (a + x) by A2;

        f is_differentiable_in x & (f . x) > 0 by A2, A5, A8, FDIFF_1: 9;

        

        then ( diff ((( #R (3 / 2)) * f),x)) = (((3 / 2) * ((f . x) #R ((3 / 2) - 1))) * ( diff (f,x))) by TAYLOR_1: 22

        .= (((3 / 2) * ((f . x) #R ((3 / 2) - 1))) * ((f `| Z) . x)) by A5, A8, FDIFF_1:def 7

        .= (((3 / 2) * ((a + x) #R ((3 / 2) - 1))) * 1) by A3, A4, A8, A9, FDIFF_1: 23

        .= ((3 / 2) * ((a + x) #R (1 / 2)));

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

      end;

      hence thesis by A1, A6, FDIFF_1: 9;

    end;

    theorem :: FDIFF_4:28

    Z c= ( dom ((2 / 3) (#) (( #R (3 / 2)) * f))) & (for x st x in Z holds (f . x) = (a + x) & (f . x) > 0 ) implies ((2 / 3) (#) (( #R (3 / 2)) * f)) is_differentiable_on Z & for x st x in Z holds ((((2 / 3) (#) (( #R (3 / 2)) * f)) `| Z) . x) = ((a + x) #R (1 / 2))

    proof

      assume that

       A1: Z c= ( dom ((2 / 3) (#) (( #R (3 / 2)) * f))) and

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

      

       A3: Z c= ( dom (( #R (3 / 2)) * f)) by A1, VALUED_1:def 5;

      then

       A4: (( #R (3 / 2)) * f) is_differentiable_on Z by A2, Th27;

      for x st x in Z holds ((((2 / 3) (#) (( #R (3 / 2)) * f)) `| Z) . x) = ((a + x) #R (1 / 2))

      proof

        let x;

        assume

         A5: x in Z;

        

        hence ((((2 / 3) (#) (( #R (3 / 2)) * f)) `| Z) . x) = ((2 / 3) * ( diff ((( #R (3 / 2)) * f),x))) by A1, A4, FDIFF_1: 20

        .= ((2 / 3) * (((( #R (3 / 2)) * f) `| Z) . x)) by A4, A5, FDIFF_1:def 7

        .= ((2 / 3) * ((3 / 2) * ((a + x) #R (1 / 2)))) by A2, A3, A5, Th27

        .= ((a + x) #R (1 / 2));

      end;

      hence thesis by A1, A4, FDIFF_1: 20;

    end;

    theorem :: FDIFF_4:29

    Z c= ( dom (( - (2 / 3)) (#) (( #R (3 / 2)) * f))) & (for x st x in Z holds (f . x) = (a - x) & (f . x) > 0 ) implies (( - (2 / 3)) (#) (( #R (3 / 2)) * f)) is_differentiable_on Z & for x st x in Z holds (((( - (2 / 3)) (#) (( #R (3 / 2)) * f)) `| Z) . x) = ((a - x) #R (1 / 2))

    proof

      assume that

       A1: Z c= ( dom (( - (2 / 3)) (#) (( #R (3 / 2)) * f))) and

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

      

       A3: Z c= ( dom (( #R (3 / 2)) * f)) by A1, VALUED_1:def 5;

      then for y be object st y in Z holds y in ( dom f) by FUNCT_1: 11;

      then

       A4: Z c= ( dom f) by TARSKI:def 3;

      

       A5: for x st x in Z holds (f . x) = ((( - 1) * x) + a)

      proof

        let x;

        assume x in Z;

        then (f . x) = (a - x) by A2;

        hence thesis;

      end;

      then

       A6: f is_differentiable_on Z by A4, FDIFF_1: 23;

      now

        let x;

        assume x in Z;

        then f is_differentiable_in x & (f . x) > 0 by A2, A6, FDIFF_1: 9;

        hence (( #R (3 / 2)) * f) is_differentiable_in x by TAYLOR_1: 22;

      end;

      then

       A7: (( #R (3 / 2)) * f) is_differentiable_on Z by A3, FDIFF_1: 9;

      for x st x in Z holds (((( - (2 / 3)) (#) (( #R (3 / 2)) * f)) `| Z) . x) = ((a - x) #R (1 / 2))

      proof

        let x;

        assume

         A8: x in Z;

        then

         A9: (f . x) = (a - x) by A2;

        

         A10: f is_differentiable_in x & (f . x) > 0 by A2, A6, A8, FDIFF_1: 9;

        (((( - (2 / 3)) (#) (( #R (3 / 2)) * f)) `| Z) . x) = (( - (2 / 3)) * ( diff ((( #R (3 / 2)) * f),x))) by A1, A7, A8, FDIFF_1: 20

        .= (( - (2 / 3)) * (((3 / 2) * ((f . x) #R ((3 / 2) - 1))) * ( diff (f,x)))) by A10, TAYLOR_1: 22

        .= (( - (2 / 3)) * (((3 / 2) * ((f . x) #R ((3 / 2) - 1))) * ((f `| Z) . x))) by A6, A8, FDIFF_1:def 7

        .= (( - (2 / 3)) * (((3 / 2) * ((a - x) #R ((3 / 2) - 1))) * ( - 1))) by A4, A5, A8, A9, FDIFF_1: 23

        .= ((a - x) #R (1 / 2));

        hence thesis;

      end;

      hence thesis by A1, A7, FDIFF_1: 20;

    end;

    theorem :: FDIFF_4:30

    Z c= ( dom (2 (#) (( #R (1 / 2)) * f))) & (for x st x in Z holds (f . x) = (a + x) & (f . x) > 0 ) implies (2 (#) (( #R (1 / 2)) * f)) is_differentiable_on Z & for x st x in Z holds (((2 (#) (( #R (1 / 2)) * f)) `| Z) . x) = ((a + x) #R ( - (1 / 2)))

    proof

      assume that

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

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

      

       A3: Z c= ( dom (( #R (1 / 2)) * f)) by A1, VALUED_1:def 5;

      then for y be object st y in Z holds y in ( dom f) by FUNCT_1: 11;

      then

       A4: Z c= ( dom f) by TARSKI:def 3;

      

       A5: for x st x in Z holds (f . x) = ((1 * x) + a) by A2;

      then

       A6: f is_differentiable_on Z by A4, FDIFF_1: 23;

      now

        let x;

        assume x in Z;

        then f is_differentiable_in x & (f . x) > 0 by A2, A6, FDIFF_1: 9;

        hence (( #R (1 / 2)) * f) is_differentiable_in x by TAYLOR_1: 22;

      end;

      then

       A7: (( #R (1 / 2)) * f) is_differentiable_on Z by A3, FDIFF_1: 9;

      for x st x in Z holds (((2 (#) (( #R (1 / 2)) * f)) `| Z) . x) = ((a + x) #R ( - (1 / 2)))

      proof

        let x;

        assume

         A8: x in Z;

        then

         A9: (f . x) = (a + x) by A2;

        

         A10: f is_differentiable_in x & (f . x) > 0 by A2, A6, A8, FDIFF_1: 9;

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

        .= (2 * (((1 / 2) * ((f . x) #R ((1 / 2) - 1))) * ( diff (f,x)))) by A10, TAYLOR_1: 22

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

        .= (2 * (((1 / 2) * ((a + x) #R ((1 / 2) - 1))) * 1)) by A4, A5, A8, A9, FDIFF_1: 23

        .= ((a + x) #R ( - (1 / 2)));

        hence thesis;

      end;

      hence thesis by A1, A7, FDIFF_1: 20;

    end;

    theorem :: FDIFF_4:31

    Z c= ( dom (( - 2) (#) (( #R (1 / 2)) * f))) & (for x st x in Z holds (f . x) = (a - x) & (f . x) > 0 ) implies (( - 2) (#) (( #R (1 / 2)) * f)) is_differentiable_on Z & for x st x in Z holds (((( - 2) (#) (( #R (1 / 2)) * f)) `| Z) . x) = ((a - x) #R ( - (1 / 2)))

    proof

      assume that

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

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

      

       A3: Z c= ( dom (( #R (1 / 2)) * f)) by A1, VALUED_1:def 5;

      then for y be object st y in Z holds y in ( dom f) by FUNCT_1: 11;

      then

       A4: Z c= ( dom f) by TARSKI:def 3;

      

       A5: for x st x in Z holds (f . x) = ((( - 1) * x) + a)

      proof

        let x;

        assume x in Z;

        then (f . x) = (a - x) by A2;

        hence thesis;

      end;

      then

       A6: f is_differentiable_on Z by A4, FDIFF_1: 23;

      now

        let x;

        assume x in Z;

        then f is_differentiable_in x & (f . x) > 0 by A2, A6, FDIFF_1: 9;

        hence (( #R (1 / 2)) * f) is_differentiable_in x by TAYLOR_1: 22;

      end;

      then

       A7: (( #R (1 / 2)) * f) is_differentiable_on Z by A3, FDIFF_1: 9;

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

      proof

        let x;

        assume

         A8: x in Z;

        then

         A9: (f . x) = (a - x) by A2;

        

         A10: f is_differentiable_in x & (f . x) > 0 by A2, A6, A8, FDIFF_1: 9;

        (((( - 2) (#) (( #R (1 / 2)) * f)) `| Z) . x) = (( - 2) * ( diff ((( #R (1 / 2)) * f),x))) by A1, A7, A8, FDIFF_1: 20

        .= (( - 2) * (((1 / 2) * ((f . x) #R ((1 / 2) - 1))) * ( diff (f,x)))) by A10, TAYLOR_1: 22

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

        .= (( - 2) * (((1 / 2) * ((a - x) #R ((1 / 2) - 1))) * ( - 1))) by A4, A5, A8, A9, FDIFF_1: 23

        .= ((a - x) #R ( - (1 / 2)));

        hence thesis;

      end;

      hence thesis by A1, A7, FDIFF_1: 20;

    end;

    theorem :: FDIFF_4:32

    Z c= ( dom ((2 / (3 * b)) (#) (( #R (3 / 2)) * f))) & (for x st x in Z holds (f . x) = (a + (b * x)) & b <> 0 & (f . x) > 0 ) implies ((2 / (3 * b)) (#) (( #R (3 / 2)) * f)) is_differentiable_on Z & for x st x in Z holds ((((2 / (3 * b)) (#) (( #R (3 / 2)) * f)) `| Z) . x) = ((a + (b * x)) #R (1 / 2))

    proof

      assume that

       A1: Z c= ( dom ((2 / (3 * b)) (#) (( #R (3 / 2)) * f))) and

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

      

       A3: Z c= ( dom (( #R (3 / 2)) * f)) by A1, VALUED_1:def 5;

      then for y be object st y in Z holds y in ( dom f) by FUNCT_1: 11;

      then

       A4: Z c= ( dom f) by TARSKI:def 3;

      

       A5: for x st x in Z holds (f . x) = ((b * x) + a) by A2;

      then

       A6: f is_differentiable_on Z by A4, FDIFF_1: 23;

      now

        let x;

        assume x in Z;

        then f is_differentiable_in x & (f . x) > 0 by A2, A6, FDIFF_1: 9;

        hence (( #R (3 / 2)) * f) is_differentiable_in x by TAYLOR_1: 22;

      end;

      then

       A7: (( #R (3 / 2)) * f) is_differentiable_on Z by A3, FDIFF_1: 9;

      for x st x in Z holds ((((2 / (3 * b)) (#) (( #R (3 / 2)) * f)) `| Z) . x) = ((a + (b * x)) #R (1 / 2))

      proof

        let x;

        assume

         A8: x in Z;

        then

         A9: (3 * b) <> 0 by A2;

        

         A10: (f . x) = (a + (b * x)) by A2, A8;

        

         A11: f is_differentiable_in x & (f . x) > 0 by A2, A6, A8, FDIFF_1: 9;

        ((((2 / (3 * b)) (#) (( #R (3 / 2)) * f)) `| Z) . x) = ((2 / (3 * b)) * ( diff ((( #R (3 / 2)) * f),x))) by A1, A7, A8, FDIFF_1: 20

        .= ((2 / (3 * b)) * (((3 / 2) * ((f . x) #R ((3 / 2) - 1))) * ( diff (f,x)))) by A11, TAYLOR_1: 22

        .= ((2 / (3 * b)) * (((3 / 2) * ((f . x) #R ((3 / 2) - 1))) * ((f `| Z) . x))) by A6, A8, FDIFF_1:def 7

        .= ((2 / (3 * b)) * (((3 / 2) * ((a + (b * x)) #R ((3 / 2) - 1))) * b)) by A4, A5, A8, A10, FDIFF_1: 23

        .= (((2 / (3 * b)) * ((3 * b) / 2)) * ((a + (b * x)) #R ((3 / 2) - 1)))

        .= (1 * ((a + (b * x)) #R ((3 / 2) - 1))) by A9, XCMPLX_1: 112

        .= ((a + (b * x)) #R (1 / 2));

        hence thesis;

      end;

      hence thesis by A1, A7, FDIFF_1: 20;

    end;

    theorem :: FDIFF_4:33

    Z c= ( dom (( - (2 / (3 * b))) (#) (( #R (3 / 2)) * f))) & (for x st x in Z holds (f . x) = (a - (b * x)) & b <> 0 & (f . x) > 0 ) implies (( - (2 / (3 * b))) (#) (( #R (3 / 2)) * f)) is_differentiable_on Z & for x st x in Z holds (((( - (2 / (3 * b))) (#) (( #R (3 / 2)) * f)) `| Z) . x) = ((a - (b * x)) #R (1 / 2))

    proof

      assume that

       A1: Z c= ( dom (( - (2 / (3 * b))) (#) (( #R (3 / 2)) * f))) and

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

      

       A3: Z c= ( dom (( #R (3 / 2)) * f)) by A1, VALUED_1:def 5;

      then for y be object st y in Z holds y in ( dom f) by FUNCT_1: 11;

      then

       A4: Z c= ( dom f) by TARSKI:def 3;

      

       A5: for x st x in Z holds (f . x) = ((( - b) * x) + a)

      proof

        let x;

        assume x in Z;

        then (f . x) = (a - (b * x)) by A2;

        hence thesis;

      end;

      then

       A6: f is_differentiable_on Z by A4, FDIFF_1: 23;

      now

        let x;

        assume x in Z;

        then f is_differentiable_in x & (f . x) > 0 by A2, A6, FDIFF_1: 9;

        hence (( #R (3 / 2)) * f) is_differentiable_in x by TAYLOR_1: 22;

      end;

      then

       A7: (( #R (3 / 2)) * f) is_differentiable_on Z by A3, FDIFF_1: 9;

      for x st x in Z holds (((( - (2 / (3 * b))) (#) (( #R (3 / 2)) * f)) `| Z) . x) = ((a - (b * x)) #R (1 / 2))

      proof

        let x;

        assume

         A8: x in Z;

        then

         A9: (3 * b) <> 0 by A2;

        

         A10: (f . x) = (a - (b * x)) by A2, A8;

        

         A11: f is_differentiable_in x & (f . x) > 0 by A2, A6, A8, FDIFF_1: 9;

        (((( - (2 / (3 * b))) (#) (( #R (3 / 2)) * f)) `| Z) . x) = (( - (2 / (3 * b))) * ( diff ((( #R (3 / 2)) * f),x))) by A1, A7, A8, FDIFF_1: 20

        .= (( - (2 / (3 * b))) * (((3 / 2) * ((f . x) #R ((3 / 2) - 1))) * ( diff (f,x)))) by A11, TAYLOR_1: 22

        .= (( - (2 / (3 * b))) * (((3 / 2) * ((f . x) #R ((3 / 2) - 1))) * ((f `| Z) . x))) by A6, A8, FDIFF_1:def 7

        .= (( - (2 / (3 * b))) * (((3 / 2) * ((a - (b * x)) #R ((3 / 2) - 1))) * ( - b))) by A4, A5, A8, A10, FDIFF_1: 23

        .= (((2 / (3 * b)) * ((3 * b) / 2)) * ((a - (b * x)) #R ((3 / 2) - 1)))

        .= (1 * ((a - (b * x)) #R ((3 / 2) - 1))) by A9, XCMPLX_1: 112

        .= ((a - (b * x)) #R (1 / 2));

        hence thesis;

      end;

      hence thesis by A1, A7, FDIFF_1: 20;

    end;

    theorem :: FDIFF_4:34

    Z c= ( dom (( #R (1 / 2)) * f)) & f = (f1 + f2) & f2 = ( #Z 2) & (for x st x in Z holds (f1 . x) = (a ^2 ) & (f . x) > 0 ) implies (( #R (1 / 2)) * f) is_differentiable_on Z & for x st x in Z holds (((( #R (1 / 2)) * f) `| Z) . x) = (x * (((a ^2 ) + (x |^ 2)) #R ( - (1 / 2))))

    proof

      assume that

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

       A2: f = (f1 + f2) and

       A3: f2 = ( #Z 2) and

       A4: for x st x in Z holds (f1 . x) = (a ^2 ) & (f . x) > 0 ;

      for y be object st y in Z holds y in ( dom f) by A1, FUNCT_1: 11;

      then

       A5: Z c= ( dom (f1 + f2)) by A2, TARSKI:def 3;

      

       A6: for x st x in Z holds (f1 . x) = (a ^2 ) by A4;

      then

       A7: f is_differentiable_on Z by A2, A3, A5, Th17;

      

       A8: for x st x in Z holds (( #R (1 / 2)) * f) is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then f is_differentiable_in x & (f . x) > 0 by A4, A7, FDIFF_1: 9;

        hence thesis by TAYLOR_1: 22;

      end;

      then

       A9: (( #R (1 / 2)) * f) is_differentiable_on Z by A1, FDIFF_1: 9;

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

      proof

        let x;

        assume

         A10: x in Z;

        then x in ( dom (f1 + f2)) by A1, A2, FUNCT_1: 11;

        

        then

         A11: ((f1 + f2) . x) = ((f1 . x) + (f2 . x)) by VALUED_1:def 1

        .= ((a ^2 ) + (f2 . x)) by A4, A10

        .= ((a ^2 ) + (x #Z 2)) by A3, TAYLOR_1:def 1

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

        f is_differentiable_in x & (f . x) > 0 by A4, A7, A10, FDIFF_1: 9;

        

        then ( diff ((( #R (1 / 2)) * f),x)) = (((1 / 2) * ((f . x) #R ((1 / 2) - 1))) * ( diff (f,x))) by TAYLOR_1: 22

        .= (((1 / 2) * ((f . x) #R ((1 / 2) - 1))) * ((f `| Z) . x)) by A7, A10, FDIFF_1:def 7

        .= (((1 / 2) * (((a ^2 ) + (x |^ 2)) #R ((1 / 2) - 1))) * (2 * x)) by A2, A3, A5, A6, A10, A11, Th17

        .= (x * (((a ^2 ) + (x |^ 2)) #R ( - (1 / 2))));

        hence thesis by A9, A10, FDIFF_1:def 7;

      end;

      hence thesis by A1, A8, FDIFF_1: 9;

    end;

    theorem :: FDIFF_4:35

    Z c= ( dom ( - (( #R (1 / 2)) * f))) & f = (f1 - f2) & f2 = ( #Z 2) & (for x st x in Z holds (f1 . x) = (a ^2 ) & (f . x) > 0 ) implies ( - (( #R (1 / 2)) * f)) is_differentiable_on Z & for x st x in Z holds ((( - (( #R (1 / 2)) * f)) `| Z) . x) = (x * (((a ^2 ) - (x |^ 2)) #R ( - (1 / 2))))

    proof

      assume that

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

       A2: f = (f1 - f2) and

       A3: f2 = ( #Z 2) and

       A4: for x st x in Z holds (f1 . x) = (a ^2 ) & (f . x) > 0 ;

      

       A5: for x st x in Z holds (f1 . x) = ((a ^2 ) + ( 0 * x)) by A4;

      

       A6: Z c= ( dom (( #R (1 / 2)) * f)) by A1, VALUED_1: 8;

      then for y be object st y in Z holds y in ( dom f) by FUNCT_1: 11;

      then

       A7: Z c= ( dom (f1 + (( - 1) (#) f2))) by A2, TARSKI:def 3;

      then

       A8: f is_differentiable_on Z by A2, A3, A5, Th12;

      now

        let x;

        assume x in Z;

        then f is_differentiable_in x & (f . x) > 0 by A4, A8, FDIFF_1: 9;

        hence (( #R (1 / 2)) * f) is_differentiable_in x by TAYLOR_1: 22;

      end;

      then

       A9: (( #R (1 / 2)) * f) is_differentiable_on Z by A6, FDIFF_1: 9;

      for x st x in Z holds (((( - 1) (#) (( #R (1 / 2)) * f)) `| Z) . x) = (x * (((a ^2 ) - (x |^ 2)) #R ( - (1 / 2))))

      proof

        let x;

        assume

         A10: x in Z;

        then

         A11: f is_differentiable_in x & (f . x) > 0 by A4, A8, FDIFF_1: 9;

        x in ( dom (f1 - f2)) by A2, A6, A10, FUNCT_1: 11;

        

        then

         A12: ((f1 - f2) . x) = ((f1 . x) - (f2 . x)) by VALUED_1: 13

        .= ((a ^2 ) - (f2 . x)) by A4, A10

        .= ((a ^2 ) - (x #Z 2)) by A3, TAYLOR_1:def 1

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

        (((( - 1) (#) (( #R (1 / 2)) * f)) `| Z) . x) = (( - 1) * ( diff ((( #R (1 / 2)) * f),x))) by A1, A9, A10, FDIFF_1: 20

        .= (( - 1) * (((1 / 2) * ((f . x) #R ((1 / 2) - 1))) * ( diff (f,x)))) by A11, TAYLOR_1: 22

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

        .= (( - 1) * (((1 / 2) * ((f . x) #R ((1 / 2) - 1))) * ( 0 + ((2 * ( - 1)) * x)))) by A2, A3, A7, A5, A10, Th12

        .= (x * (((a ^2 ) - (x |^ 2)) #R ( - (1 / 2)))) by A2, A12;

        hence thesis;

      end;

      hence thesis by A1, A9, FDIFF_1: 20;

    end;

    theorem :: FDIFF_4:36

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

    proof

      assume that

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

       A2: f = (f1 + f2) and

       A3: f2 = ( #Z 2) and

       A4: for x st x in Z holds (f1 . x) = x & (f . x) > 0 ;

      

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

      

       A6: f2 = (1 (#) f2) by RFUNCT_1: 21;

      

       A7: Z c= ( dom (( #R (1 / 2)) * f)) by A1, VALUED_1:def 5;

      then for y be object st y in Z holds y in ( dom f) by FUNCT_1: 11;

      then

       A8: Z c= ( dom (f1 + (1 (#) f2))) by A2, A6, TARSKI:def 3;

      then

       A9: (f1 + f2) is_differentiable_on Z by A3, A6, A5, Th12;

      now

        let x;

        assume x in Z;

        then f is_differentiable_in x & (f . x) > 0 by A2, A4, A9, FDIFF_1: 9;

        hence (( #R (1 / 2)) * f) is_differentiable_in x by TAYLOR_1: 22;

      end;

      then

       A10: (( #R (1 / 2)) * f) is_differentiable_on Z by A7, FDIFF_1: 9;

      

       A11: for x st x in Z holds (((f1 + f2) `| Z) . x) = (1 + ((2 * 1) * x)) by A3, A6, A8, A5, Th12;

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

      proof

        let x;

        assume

         A12: x in Z;

        then

         A13: f is_differentiable_in x & (f . x) > 0 by A2, A4, A9, FDIFF_1: 9;

        x in ( dom (f1 + f2)) by A2, A7, A12, FUNCT_1: 11;

        

        then

         A14: ((f1 + f2) . x) = ((f1 . x) + (f2 . x)) by VALUED_1:def 1

        .= (x + (f2 . x)) by A4, A12

        .= (x + (x #Z 2)) by A3, TAYLOR_1:def 1

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

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

        .= (2 * (((1 / 2) * ((f . x) #R ((1 / 2) - 1))) * ( diff (f,x)))) by A13, TAYLOR_1: 22

        .= (2 * (((1 / 2) * ((f . x) #R ((1 / 2) - 1))) * ((f `| Z) . x))) by A2, A9, A12, FDIFF_1:def 7

        .= (((2 * (1 / 2)) * ((f . x) #R ((1 / 2) - 1))) * ((f `| Z) . x))

        .= (((2 * x) + 1) * (((x |^ 2) + x) #R ( - (1 / 2)))) by A2, A11, A12, A14;

        hence thesis;

      end;

      hence thesis by A1, A10, FDIFF_1: 20;

    end;

    theorem :: FDIFF_4:37

    Z c= ( dom ( sin * f)) & (for x st x in Z holds (f . x) = ((a * x) + b)) implies ( sin * f) is_differentiable_on Z & for x st x in Z holds ((( sin * f) `| Z) . x) = (a * ( cos . ((a * x) + b)))

    proof

      assume that

       A1: Z c= ( dom ( sin * f)) and

       A2: for x st x in Z holds (f . x) = ((a * x) + b);

      for y be object st y in Z holds y in ( dom f) by A1, FUNCT_1: 11;

      then

       A3: Z c= ( dom f) by TARSKI:def 3;

      then

       A4: f is_differentiable_on Z by A2, FDIFF_1: 23;

      

       A5: for x st x in Z holds ( sin * f) is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then

         A6: f is_differentiable_in x by A4, FDIFF_1: 9;

         sin is_differentiable_in (f . x) by SIN_COS: 64;

        hence thesis by A6, FDIFF_2: 13;

      end;

      then

       A7: ( sin * f) is_differentiable_on Z by A1, FDIFF_1: 9;

      for x st x in Z holds ((( sin * f) `| Z) . x) = (a * ( cos . ((a * x) + b)))

      proof

        let x;

        

         A8: sin is_differentiable_in (f . x) by SIN_COS: 64;

        assume

         A9: x in Z;

        then f is_differentiable_in x by A4, FDIFF_1: 9;

        

        then ( diff (( sin * f),x)) = (( diff ( sin ,(f . x))) * ( diff (f,x))) by A8, FDIFF_2: 13

        .= (( cos . (f . x)) * ( diff (f,x))) by SIN_COS: 64

        .= (( cos . ((a * x) + b)) * ( diff (f,x))) by A2, A9

        .= (( cos . ((a * x) + b)) * ((f `| Z) . x)) by A4, A9, FDIFF_1:def 7

        .= (a * ( cos . ((a * x) + b))) by A2, A3, A9, FDIFF_1: 23;

        hence thesis by A7, A9, FDIFF_1:def 7;

      end;

      hence thesis by A1, A5, FDIFF_1: 9;

    end;

    theorem :: FDIFF_4:38

    Z c= ( dom ( cos * f)) & (for x st x in Z holds (f . x) = ((a * x) + b)) implies ( cos * f) is_differentiable_on Z & for x st x in Z holds ((( cos * f) `| Z) . x) = ( - (a * ( sin . ((a * x) + b))))

    proof

      assume that

       A1: Z c= ( dom ( cos * f)) and

       A2: for x st x in Z holds (f . x) = ((a * x) + b);

      for y be object st y in Z holds y in ( dom f) by A1, FUNCT_1: 11;

      then

       A3: Z c= ( dom f) by TARSKI:def 3;

      then

       A4: f is_differentiable_on Z by A2, FDIFF_1: 23;

      

       A5: for x st x in Z holds ( cos * f) is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then

         A6: f is_differentiable_in x by A4, FDIFF_1: 9;

         cos is_differentiable_in (f . x) by SIN_COS: 63;

        hence thesis by A6, FDIFF_2: 13;

      end;

      then

       A7: ( cos * f) is_differentiable_on Z by A1, FDIFF_1: 9;

      for x st x in Z holds ((( cos * f) `| Z) . x) = ( - (a * ( sin . ((a * x) + b))))

      proof

        let x;

        

         A8: ( diff ( cos ,(f . x))) = ( - ( sin . (f . x))) by SIN_COS: 63;

        

         A9: cos is_differentiable_in (f . x) by SIN_COS: 63;

        assume

         A10: x in Z;

        then f is_differentiable_in x by A4, FDIFF_1: 9;

        

        then ( diff (( cos * f),x)) = (( diff ( cos ,(f . x))) * ( diff (f,x))) by A9, FDIFF_2: 13

        .= ( - (( sin . (f . x)) * ( diff (f,x)))) by A8

        .= ( - (( sin . ((a * x) + b)) * ( diff (f,x)))) by A2, A10

        .= ( - (( sin . ((a * x) + b)) * ((f `| Z) . x))) by A4, A10, FDIFF_1:def 7

        .= ( - (a * ( sin . ((a * x) + b)))) by A2, A3, A10, FDIFF_1: 23;

        hence thesis by A7, A10, FDIFF_1:def 7;

      end;

      hence thesis by A1, A5, FDIFF_1: 9;

    end;

    theorem :: FDIFF_4:39

    (for x st x in Z holds ( cos . x) <> 0 ) implies ( cos ^ ) is_differentiable_on Z & for x st x in Z holds ((( cos ^ ) `| Z) . x) = (( sin . x) / (( cos . x) ^2 ))

    proof

      assume

       A1: for x st x in Z holds ( cos . x) <> 0 ;

      

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

      then

       A3: ( cos ^ ) is_differentiable_on Z by A1, FDIFF_2: 22;

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

      proof

        let x;

        

         A4: cos is_differentiable_in x by SIN_COS: 63;

        assume

         A5: x in Z;

        then

         A6: ( cos . x) <> 0 by A1;

        ((( cos ^ ) `| Z) . x) = ( diff (( cos ^ ),x)) by A3, A5, FDIFF_1:def 7

        .= ( - (( diff ( cos ,x)) / (( cos . x) ^2 ))) by A6, A4, FDIFF_2: 15

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

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

        .= (( sin . x) / (( cos . x) ^2 ));

        hence thesis;

      end;

      hence thesis by A1, A2, FDIFF_2: 22;

    end;

    theorem :: FDIFF_4:40

    (for x st x in Z holds ( sin . x) <> 0 ) implies ( sin ^ ) is_differentiable_on Z & for x st x in Z holds ((( sin ^ ) `| Z) . x) = ( - (( cos . x) / (( sin . x) ^2 )))

    proof

      

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

      assume

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

      then

       A3: ( sin ^ ) is_differentiable_on Z by A1, FDIFF_2: 22;

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

      proof

        let x;

        assume

         A4: x in Z;

        then

         A5: ( sin . x) <> 0 & sin is_differentiable_in x by A2, A1, FDIFF_1: 9;

        ((( sin ^ ) `| Z) . x) = ( diff (( sin ^ ),x)) by A3, A4, FDIFF_1:def 7

        .= ( - (( diff ( sin ,x)) / (( sin . x) ^2 ))) by A5, FDIFF_2: 15

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

        hence thesis;

      end;

      hence thesis by A2, A1, FDIFF_2: 22;

    end;

    theorem :: FDIFF_4:41

    Z c= ( dom ( sin (#) cos )) implies ( sin (#) cos ) is_differentiable_on Z & for x st x in Z holds ((( sin (#) cos ) `| Z) . x) = ( cos (2 * x))

    proof

      

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

      assume

       A2: Z c= ( dom ( sin (#) cos ));

      now

        let x;

        assume x in Z;

        

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

        .= ((( cos . x) * ( cos . x)) + (( sin . x) * ( diff ( cos ,x)))) by SIN_COS: 64

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

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

        .= ((( cos x) ^2 ) - (( sin . x) ^2 )) by SIN_COS:def 19

        .= ((( cos x) ^2 ) - (( sin x) ^2 )) by SIN_COS:def 17

        .= ( cos (2 * x)) by SIN_COS5: 7;

      end;

      hence thesis by A2, A1, FDIFF_1: 21;

    end;

    theorem :: FDIFF_4:42

    Z c= ( dom ( ln * cos )) & (for x st x in Z holds ( cos . x) > 0 ) implies ( ln * cos ) is_differentiable_on Z & for x st x in Z holds ((( ln * cos ) `| Z) . x) = ( - ( tan x))

    proof

      assume that

       A1: Z c= ( dom ( ln * cos )) and

       A2: for x st x in Z holds ( cos . x) > 0 ;

      

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

      

       A4: for x st x in Z holds ( ln * cos ) is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then cos is_differentiable_in x & ( cos . x) > 0 by A2, A3, FDIFF_1: 9;

        hence thesis by TAYLOR_1: 20;

      end;

      then

       A5: ( ln * cos ) is_differentiable_on Z by A1, FDIFF_1: 9;

      for x st x in Z holds ((( ln * cos ) `| Z) . x) = ( - ( tan x))

      proof

        let x;

        assume

         A6: x in Z;

        then cos is_differentiable_in x & ( cos . x) > 0 by A2, A3, FDIFF_1: 9;

        

        then ( diff (( ln * cos ),x)) = (( diff ( cos ,x)) / ( cos . x)) by TAYLOR_1: 20

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

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

        .= ( - (( sin x) / ( cos . x))) by SIN_COS:def 17

        .= ( - (( sin x) / ( cos x))) by SIN_COS:def 19

        .= ( - ( tan x)) by SIN_COS4:def 1;

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

      end;

      hence thesis by A1, A4, FDIFF_1: 9;

    end;

    theorem :: FDIFF_4:43

    Z c= ( dom ( ln * sin )) & (for x st x in Z holds ( sin . x) > 0 ) implies ( ln * sin ) is_differentiable_on Z & for x st x in Z holds ((( ln * sin ) `| Z) . x) = ( cot x)

    proof

      assume that

       A1: Z c= ( dom ( ln * sin )) and

       A2: for x st x in Z holds ( sin . x) > 0 ;

      

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

      

       A4: for x st x in Z holds ( ln * sin ) is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then sin is_differentiable_in x & ( sin . x) > 0 by A2, A3, FDIFF_1: 9;

        hence thesis by TAYLOR_1: 20;

      end;

      then

       A5: ( ln * sin ) is_differentiable_on Z by A1, FDIFF_1: 9;

      for x st x in Z holds ((( ln * sin ) `| Z) . x) = ( cot x)

      proof

        let x;

        assume

         A6: x in Z;

        then sin is_differentiable_in x & ( sin . x) > 0 by A2, A3, FDIFF_1: 9;

        

        then ( diff (( ln * sin ),x)) = (( diff ( sin ,x)) / ( sin . x)) by TAYLOR_1: 20

        .= (( cos . x) / ( sin . x)) by SIN_COS: 64

        .= (( cos x) / ( sin . x)) by SIN_COS:def 19

        .= (( cos x) / ( sin x)) by SIN_COS:def 17

        .= ( cot x) by SIN_COS4:def 2;

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

      end;

      hence thesis by A1, A4, FDIFF_1: 9;

    end;

    theorem :: FDIFF_4:44

    

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

    proof

      

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

      proof

        let x;

        assume

         A2: x in Z;

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

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

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

        hence thesis;

      end;

      assume

       A3: Z c= ( dom (( - ( id Z)) (#) cos ));

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

      then

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

      then

       A5: ( - ( id Z)) is_differentiable_on Z by A1, FDIFF_1: 23;

      

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

      now

        let x;

        assume

         A7: x in Z;

        

        hence (((( - ( id Z)) (#) cos ) `| Z) . x) = ((( cos . x) * ( diff (( - ( id Z)),x))) + ((( - ( id Z)) . x) * ( diff ( cos ,x)))) by A3, A5, A6, FDIFF_1: 21

        .= ((( cos . x) * ((( - ( id Z)) `| Z) . x)) + ((( - ( id Z)) . x) * ( diff ( cos ,x)))) by A5, A7, FDIFF_1:def 7

        .= ((( cos . x) * ( - 1)) + ((( - ( id Z)) . x) * ( diff ( cos ,x)))) by A4, A1, A7, FDIFF_1: 23

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

        .= (( - ( cos . x)) + (((( - 1) * x) + 0 ) * ( - ( sin . x)))) by A1, A7

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

      end;

      hence thesis by A3, A5, A6, FDIFF_1: 21;

    end;

    theorem :: FDIFF_4:45

    

     Th45: Z c= ( dom (( id Z) (#) sin )) implies (( id Z) (#) sin ) is_differentiable_on Z & for x st x in Z holds (((( id Z) (#) sin ) `| Z) . x) = (( sin . x) + (x * ( cos . x)))

    proof

      

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

      assume

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

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

      then

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

      then

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

      

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

      now

        let x;

        assume

         A6: x in Z;

        

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

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

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

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

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

      end;

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

    end;

    theorem :: FDIFF_4:46

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

    proof

      assume

       A1: Z c= ( dom ((( - ( id Z)) (#) cos ) + sin ));

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

      then

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

      then

       A3: (( - ( id Z)) (#) cos ) is_differentiable_on Z by Th44;

      

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

      now

        let x;

        assume

         A5: x in Z;

        

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

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

        .= ((( - ( cos . x)) + (x * ( sin . x))) + ( diff ( sin ,x))) by A2, A5, Th44

        .= ((( - ( cos . x)) + (x * ( sin . x))) + ( cos . x)) by SIN_COS: 64

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

      end;

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

    end;

    theorem :: FDIFF_4:47

    Z c= ( dom ((( id Z) (#) sin ) + cos )) implies ((( id Z) (#) sin ) + cos ) is_differentiable_on Z & for x st x in Z holds ((((( id Z) (#) sin ) + cos ) `| Z) . x) = (x * ( cos . x))

    proof

      assume

       A1: Z c= ( dom ((( id Z) (#) sin ) + cos ));

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

      then

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

      then

       A3: (( id Z) (#) sin ) is_differentiable_on Z by Th45;

      

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

      now

        let x;

        assume

         A5: x in Z;

        

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

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

        .= ((( sin . x) + (x * ( cos . x))) + ( diff ( cos ,x))) by A2, A5, Th45

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

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

      end;

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

    end;

    theorem :: FDIFF_4:48

    Z c= ( dom (2 (#) (( #R (1 / 2)) * sin ))) & (for x st x in Z holds ( sin . x) > 0 ) implies (2 (#) (( #R (1 / 2)) * sin )) is_differentiable_on Z & for x st x in Z holds (((2 (#) (( #R (1 / 2)) * sin )) `| Z) . x) = (( cos . x) * (( sin . x) #R ( - (1 / 2))))

    proof

      assume that

       A1: Z c= ( dom (2 (#) (( #R (1 / 2)) * sin ))) and

       A2: for x st x in Z holds ( sin . x) > 0 ;

       A3:

      now

        let x;

        assume x in Z;

        then sin is_differentiable_in x & ( sin . x) > 0 by A2, SIN_COS: 64;

        hence (( #R (1 / 2)) * sin ) is_differentiable_in x by TAYLOR_1: 22;

      end;

      Z c= ( dom (( #R (1 / 2)) * sin )) by A1, VALUED_1:def 5;

      then

       A4: (( #R (1 / 2)) * sin ) is_differentiable_on Z by A3, FDIFF_1: 9;

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

      proof

        let x;

        assume

         A5: x in Z;

        then

         A6: sin is_differentiable_in x & ( sin . x) > 0 by A2, SIN_COS: 64;

        (((2 (#) (( #R (1 / 2)) * sin )) `| Z) . x) = (2 * ( diff ((( #R (1 / 2)) * sin ),x))) by A1, A4, A5, FDIFF_1: 20

        .= (2 * (((1 / 2) * (( sin . x) #R ((1 / 2) - 1))) * ( diff ( sin ,x)))) by A6, TAYLOR_1: 22

        .= (2 * (((1 / 2) * (( sin . x) #R ((1 / 2) - 1))) * ( cos . x))) by SIN_COS: 64

        .= (( cos . x) * (( sin . x) #R ( - (1 / 2))));

        hence thesis;

      end;

      hence thesis by A1, A4, FDIFF_1: 20;

    end;

    theorem :: FDIFF_4:49

    

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

    proof

       A1:

      now

        let x;

        assume x in Z;

         sin is_differentiable_in x by SIN_COS: 64;

        hence (( #Z 2) * sin ) is_differentiable_in x by TAYLOR_1: 3;

      end;

      assume

       A2: Z c= ( dom ((1 / 2) (#) (( #Z 2) * sin )));

      then Z c= ( dom (( #Z 2) * sin )) by VALUED_1:def 5;

      then

       A3: (( #Z 2) * sin ) is_differentiable_on Z by A1, FDIFF_1: 9;

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

      proof

        let x;

        

         A4: sin is_differentiable_in x by SIN_COS: 64;

        assume x in Z;

        

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

        .= ((1 / 2) * ((2 * (( sin . x) #Z (2 - 1))) * ( diff ( sin ,x)))) by A4, TAYLOR_1: 3

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

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

        .= (( sin . x) * ( cos . x)) by PREPOWER: 35;

        hence thesis;

      end;

      hence thesis by A2, A3, FDIFF_1: 20;

    end;

    theorem :: FDIFF_4:50

    Z c= ( dom ( sin + ((1 / 2) (#) (( #Z 2) * sin )))) & (for x st x in Z holds ( sin . x) > 0 & ( sin . x) < 1) implies ( sin + ((1 / 2) (#) (( #Z 2) * sin ))) is_differentiable_on Z & for x st x in Z holds ((( sin + ((1 / 2) (#) (( #Z 2) * sin ))) `| Z) . x) = ((( cos . x) |^ 3) / (1 - ( sin . x)))

    proof

      assume that

       A1: Z c= ( dom ( sin + ((1 / 2) (#) (( #Z 2) * sin )))) and

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

      Z c= (( dom ((1 / 2) (#) (( #Z 2) * sin ))) /\ ( dom sin )) by A1, VALUED_1:def 1;

      then

       A3: Z c= ( dom ((1 / 2) (#) (( #Z 2) * sin ))) by XBOOLE_1: 18;

      then

       A4: ((1 / 2) (#) (( #Z 2) * sin )) is_differentiable_on Z by Th49;

      

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

      now

        let x;

        assume

         A6: x in Z;

        then ( sin . x) < 1 by A2;

        then

         A7: (1 - ( sin . x)) > 0 by XREAL_1: 50;

        ((( sin + ((1 / 2) (#) (( #Z 2) * sin ))) `| Z) . x) = (( diff ( sin ,x)) + ( diff (((1 / 2) (#) (( #Z 2) * sin )),x))) by A1, A4, A5, A6, FDIFF_1: 18

        .= (( cos . x) + ( diff (((1 / 2) (#) (( #Z 2) * sin )),x))) by SIN_COS: 64

        .= (( cos . x) + ((((1 / 2) (#) (( #Z 2) * sin )) `| Z) . x)) by A4, A6, FDIFF_1:def 7

        .= (( cos . x) + (( sin . x) * ( cos . x))) by A3, A6, Th49

        .= (((( cos . x) * (1 + ( sin . x))) * (1 - ( sin . x))) / (1 - ( sin . x))) by A7, XCMPLX_1: 89

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

        .= ((( cos . x) * (1 - (( sin x) ^2 ))) / (1 - ( sin . x))) by SIN_COS:def 17

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

        .= ((( cos . x) * (( cos x) |^ 2)) / (1 - ( sin . x))) by WSIERP_1: 1

        .= ((( cos . x) * (( cos . x) |^ 2)) / (1 - ( sin . x))) by SIN_COS:def 19

        .= ((( cos . x) |^ (2 + 1)) / (1 - ( sin . x))) by NEWTON: 6

        .= ((( cos . x) |^ 3) / (1 - ( sin . x)));

        hence ((( sin + ((1 / 2) (#) (( #Z 2) * sin ))) `| Z) . x) = ((( cos . x) |^ 3) / (1 - ( sin . x)));

      end;

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

    end;

    theorem :: FDIFF_4:51

    Z c= ( dom (((1 / 2) (#) (( #Z 2) * sin )) - cos )) & (for x st x in Z holds ( sin . x) > 0 & ( cos . x) < 1) implies (((1 / 2) (#) (( #Z 2) * sin )) - cos ) is_differentiable_on Z & for x st x in Z holds (((((1 / 2) (#) (( #Z 2) * sin )) - cos ) `| Z) . x) = ((( sin . x) |^ 3) / (1 - ( cos . x)))

    proof

      assume that

       A1: Z c= ( dom (((1 / 2) (#) (( #Z 2) * sin )) - cos )) and

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

      Z c= (( dom ((1 / 2) (#) (( #Z 2) * sin ))) /\ ( dom cos )) by A1, VALUED_1: 12;

      then

       A3: Z c= ( dom ((1 / 2) (#) (( #Z 2) * sin ))) by XBOOLE_1: 18;

      then

       A4: ((1 / 2) (#) (( #Z 2) * sin )) is_differentiable_on Z by Th49;

      

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

      now

        let x;

        assume

         A6: x in Z;

        then

         A7: (1 - ( cos . x)) > 0 by A2, XREAL_1: 50;

        (((((1 / 2) (#) (( #Z 2) * sin )) - cos ) `| Z) . x) = (( diff (((1 / 2) (#) (( #Z 2) * sin )),x)) - ( diff ( cos ,x))) by A1, A4, A5, A6, FDIFF_1: 19

        .= (( diff (((1 / 2) (#) (( #Z 2) * sin )),x)) - ( - ( sin . x))) by SIN_COS: 63

        .= (((((1 / 2) (#) (( #Z 2) * sin )) `| Z) . x) - ( - ( sin . x))) by A4, A6, FDIFF_1:def 7

        .= ((( sin . x) * ( cos . x)) - ( - ( sin . x))) by A3, A6, Th49

        .= (((( sin . x) * (1 + ( cos . x))) * (1 - ( cos . x))) / (1 - ( cos . x))) by A7, XCMPLX_1: 89

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

        .= ((( sin . x) * (1 - (( cos x) ^2 ))) / (1 - ( cos . x))) by SIN_COS:def 19

        .= ((( sin . x) * (( sin x) * ( sin x))) / (1 - ( cos . x))) by SIN_COS4: 4

        .= ((( sin . x) * (( sin x) |^ 2)) / (1 - ( cos . x))) by WSIERP_1: 1

        .= ((( sin . x) * (( sin . x) |^ 2)) / (1 - ( cos . x))) by SIN_COS:def 17

        .= ((( sin . x) |^ (2 + 1)) / (1 - ( cos . x))) by NEWTON: 6

        .= ((( sin . x) |^ 3) / (1 - ( cos . x)));

        hence (((((1 / 2) (#) (( #Z 2) * sin )) - cos ) `| Z) . x) = ((( sin . x) |^ 3) / (1 - ( cos . x)));

      end;

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

    end;

    theorem :: FDIFF_4:52

    Z c= ( dom ( sin - ((1 / 2) (#) (( #Z 2) * sin )))) & (for x st x in Z holds ( sin . x) > 0 & ( sin . x) > ( - 1)) implies ( sin - ((1 / 2) (#) (( #Z 2) * sin ))) is_differentiable_on Z & for x st x in Z holds ((( sin - ((1 / 2) (#) (( #Z 2) * sin ))) `| Z) . x) = ((( cos . x) |^ 3) / (1 + ( sin . x)))

    proof

      assume that

       A1: Z c= ( dom ( sin - ((1 / 2) (#) (( #Z 2) * sin )))) and

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

      Z c= (( dom ((1 / 2) (#) (( #Z 2) * sin ))) /\ ( dom sin )) by A1, VALUED_1: 12;

      then

       A3: Z c= ( dom ((1 / 2) (#) (( #Z 2) * sin ))) by XBOOLE_1: 18;

      then

       A4: ((1 / 2) (#) (( #Z 2) * sin )) is_differentiable_on Z by Th49;

      

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

      now

        let x;

        assume

         A6: x in Z;

        then ( sin . x) > ( - 1) by A2;

        then

         A7: (( sin . x) - ( - 1)) > 0 by XREAL_1: 50;

        ((( sin - ((1 / 2) (#) (( #Z 2) * sin ))) `| Z) . x) = (( diff ( sin ,x)) - ( diff (((1 / 2) (#) (( #Z 2) * sin )),x))) by A1, A4, A5, A6, FDIFF_1: 19

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

        .= (( cos . x) - ((((1 / 2) (#) (( #Z 2) * sin )) `| Z) . x)) by A4, A6, FDIFF_1:def 7

        .= (( cos . x) - (( sin . x) * ( cos . x))) by A3, A6, Th49

        .= (((( cos . x) * (1 - ( sin . x))) * (1 + ( sin . x))) / (1 + ( sin . x))) by A7, XCMPLX_1: 89

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

        .= ((( cos . x) * (1 - (( sin x) ^2 ))) / (1 + ( sin . x))) by SIN_COS:def 17

        .= ((( cos . x) * (( cos x) * ( cos x))) / (1 + ( sin . x))) by SIN_COS4: 5

        .= ((( cos . x) * (( cos x) |^ 2)) / (1 + ( sin . x))) by WSIERP_1: 1

        .= ((( cos . x) * (( cos . x) |^ 2)) / (1 + ( sin . x))) by SIN_COS:def 19

        .= ((( cos . x) |^ (2 + 1)) / (1 + ( sin . x))) by NEWTON: 6

        .= ((( cos . x) |^ 3) / (1 + ( sin . x)));

        hence ((( sin - ((1 / 2) (#) (( #Z 2) * sin ))) `| Z) . x) = ((( cos . x) |^ 3) / (1 + ( sin . x)));

      end;

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

    end;

    theorem :: FDIFF_4:53

    Z c= ( dom (( - cos ) - ((1 / 2) (#) (( #Z 2) * sin )))) & (for x st x in Z holds ( sin . x) > 0 & ( cos . x) > ( - 1)) implies (( - cos ) - ((1 / 2) (#) (( #Z 2) * sin ))) is_differentiable_on Z & for x st x in Z holds (((( - cos ) - ((1 / 2) (#) (( #Z 2) * sin ))) `| Z) . x) = ((( sin . x) |^ 3) / (1 + ( cos . x)))

    proof

      assume that

       A1: Z c= ( dom (( - cos ) - ((1 / 2) (#) (( #Z 2) * sin )))) and

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

      

       A3: Z c= (( dom ((1 / 2) (#) (( #Z 2) * sin ))) /\ ( dom ( - cos ))) by A1, VALUED_1: 12;

      then

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

      

       A5: Z c= ( dom ((1 / 2) (#) (( #Z 2) * sin ))) by A3, XBOOLE_1: 18;

      then

       A6: ((1 / 2) (#) (( #Z 2) * sin )) is_differentiable_on Z by Th49;

      

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

      

       A8: ( - cos ) is_differentiable_on Z by A4, A7, FDIFF_1: 20;

      now

        let x;

        assume

         A9: x in Z;

        then

         A10: (( cos . x) - ( - 1)) > 0 by A2, XREAL_1: 50;

        (((( - cos ) - ((1 / 2) (#) (( #Z 2) * sin ))) `| Z) . x) = (( diff (( - cos ),x)) - ( diff (((1 / 2) (#) (( #Z 2) * sin )),x))) by A1, A6, A8, A9, FDIFF_1: 19

        .= (((( - cos ) `| Z) . x) - ( diff (((1 / 2) (#) (( #Z 2) * sin )),x))) by A8, A9, FDIFF_1:def 7

        .= ((( - 1) * ( diff ( cos ,x))) - ( diff (((1 / 2) (#) (( #Z 2) * sin )),x))) by A4, A7, A9, FDIFF_1: 20

        .= ((( - 1) * ( - ( sin . x))) - ( diff (((1 / 2) (#) (( #Z 2) * sin )),x))) by SIN_COS: 63

        .= (( sin . x) - ((((1 / 2) (#) (( #Z 2) * sin )) `| Z) . x)) by A6, A9, FDIFF_1:def 7

        .= (( sin . x) - (( sin . x) * ( cos . x))) by A5, A9, Th49

        .= (((( sin . x) * (1 - ( cos . x))) * (1 + ( cos . x))) / (1 + ( cos . x))) by A10, XCMPLX_1: 89

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

        .= ((( sin . x) * (1 - (( cos x) ^2 ))) / (1 + ( cos . x))) by SIN_COS:def 19

        .= ((( sin . x) * (( sin x) * ( sin x))) / (1 + ( cos . x))) by SIN_COS4: 4

        .= ((( sin . x) * (( sin x) |^ 2)) / (1 + ( cos . x))) by WSIERP_1: 1

        .= ((( sin . x) * (( sin . x) |^ 2)) / (1 + ( cos . x))) by SIN_COS:def 17

        .= ((( sin . x) |^ (2 + 1)) / (1 + ( cos . x))) by NEWTON: 6

        .= ((( sin . x) |^ 3) / (1 + ( cos . x)));

        hence (((( - cos ) - ((1 / 2) (#) (( #Z 2) * sin ))) `| Z) . x) = ((( sin . x) |^ 3) / (1 + ( cos . x)));

      end;

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

    end;

    theorem :: FDIFF_4:54

    Z c= ( dom ((1 / n) (#) (( #Z n) * sin ))) & n > 0 implies ((1 / n) (#) (( #Z n) * sin )) is_differentiable_on Z & for x st x in Z holds ((((1 / n) (#) (( #Z n) * sin )) `| Z) . x) = ((( sin . x) #Z (n - 1)) * ( cos . x))

    proof

      assume that

       A1: Z c= ( dom ((1 / n) (#) (( #Z n) * sin ))) and

       A2: n > 0 ;

       A3:

      now

        let x;

        assume x in Z;

         sin is_differentiable_in x by SIN_COS: 64;

        hence (( #Z n) * sin ) is_differentiable_in x by TAYLOR_1: 3;

      end;

      Z c= ( dom (( #Z n) * sin )) by A1, VALUED_1:def 5;

      then

       A4: (( #Z n) * sin ) is_differentiable_on Z by A3, FDIFF_1: 9;

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

      proof

        let x;

        

         A5: sin is_differentiable_in x by SIN_COS: 64;

        assume x in Z;

        

        then ((((1 / n) (#) (( #Z n) * sin )) `| Z) . x) = ((1 / n) * ( diff ((( #Z n) * sin ),x))) by A1, A4, FDIFF_1: 20

        .= ((1 / n) * ((n * (( sin . x) #Z (n - 1))) * ( diff ( sin ,x)))) by A5, TAYLOR_1: 3

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

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

        .= ((((n " ) * n) * (( sin . x) #Z (n - 1))) * ( cos . x)) by XCMPLX_1: 215

        .= ((1 * (( sin . x) #Z (n - 1))) * ( cos . x)) by A2, XCMPLX_0:def 7

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

        hence thesis;

      end;

      hence thesis by A1, A4, FDIFF_1: 20;

    end;

    theorem :: FDIFF_4:55

    Z c= ( dom ( exp_R (#) f)) & (for x st x in Z holds (f . x) = (x - 1)) implies ( exp_R (#) f) is_differentiable_on Z & for x st x in Z holds ((( exp_R (#) f) `| Z) . x) = (x * ( exp_R . x))

    proof

      assume that

       A1: Z c= ( dom ( exp_R (#) f)) and

       A2: for x st x in Z holds (f . x) = (x - 1);

      

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

      proof

        let x;

        

         A4: ((1 * x) + ( - 1)) = ((1 * x) - 1);

        assume x in Z;

        hence thesis by A2, A4;

      end;

      Z c= (( dom f) /\ ( dom exp_R )) by A1, VALUED_1:def 4;

      then

       A5: Z c= ( dom f) by XBOOLE_1: 18;

      then

       A6: f is_differentiable_on Z by A3, FDIFF_1: 23;

      

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

      now

        let x;

        assume

         A8: x in Z;

        

        hence ((( exp_R (#) f) `| Z) . x) = (((f . x) * ( diff ( exp_R ,x))) + (( exp_R . x) * ( diff (f,x)))) by A1, A6, A7, FDIFF_1: 21

        .= (((x - 1) * ( diff ( exp_R ,x))) + (( exp_R . x) * ( diff (f,x)))) by A2, A8

        .= (((x - 1) * ( exp_R . x)) + (( exp_R . x) * ( diff (f,x)))) by TAYLOR_1: 16

        .= (((x - 1) * ( exp_R . x)) + (( exp_R . x) * ((f `| Z) . x))) by A6, A8, FDIFF_1:def 7

        .= (((x - 1) * ( exp_R . x)) + (( exp_R . x) * 1)) by A5, A3, A8, FDIFF_1: 23

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

      end;

      hence thesis by A1, A6, A7, FDIFF_1: 21;

    end;

    theorem :: FDIFF_4:56

    Z c= ( dom ( ln * ( exp_R / ( exp_R + f)))) & (for x st x in Z holds (f . x) = 1) implies ( ln * ( exp_R / ( exp_R + f))) is_differentiable_on Z & for x st x in Z holds ((( ln * ( exp_R / ( exp_R + f))) `| Z) . x) = (1 / (( exp_R . x) + 1))

    proof

      assume that

       A1: Z c= ( dom ( ln * ( exp_R / ( exp_R + f)))) and

       A2: for x st x in Z holds (f . x) = 1;

      

       A3: for x st x in Z holds (f . x) = (( 0 * x) + 1) by A2;

      for y be object st y in Z holds y in ( dom ( exp_R / ( exp_R + f))) by A1, FUNCT_1: 11;

      then Z c= ( dom ( exp_R / ( exp_R + f))) by TARSKI:def 3;

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

      then

       A4: Z c= ( dom ( exp_R + f)) by XBOOLE_1: 1;

      then Z c= (( dom exp_R ) /\ ( dom f)) by VALUED_1:def 1;

      then

       A5: Z c= ( dom f) by XBOOLE_1: 18;

      then

       A6: f is_differentiable_on Z by A3, FDIFF_1: 23;

      

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

      then

       A8: ( exp_R + f) is_differentiable_on Z by A4, A6, FDIFF_1: 18;

      

       A9: for x st x in Z holds (( exp_R + f) . x) > 0

      proof

        let x;

        assume

         A10: x in Z;

        

        then (( exp_R + f) . x) = (( exp_R . x) + (f . x)) by A4, VALUED_1:def 1

        .= (( exp_R . x) + 1) by A2, A10;

        hence thesis by SIN_COS: 54, XREAL_1: 34;

      end;

      then for x st x in Z holds (( exp_R + f) . x) <> 0 ;

      then

       A11: ( exp_R / ( exp_R + f)) is_differentiable_on Z by A7, A8, FDIFF_2: 21;

      

       A12: for x st x in Z holds ((( exp_R + f) `| Z) . x) = ( exp_R . x)

      proof

        let x;

        assume

         A13: x in Z;

        

        hence ((( exp_R + f) `| Z) . x) = (( diff ( exp_R ,x)) + ( diff (f,x))) by A4, A6, A7, FDIFF_1: 18

        .= (( exp_R . x) + ( diff (f,x))) by SIN_COS: 65

        .= (( exp_R . x) + ((f `| Z) . x)) by A6, A13, FDIFF_1:def 7

        .= (( exp_R . x) + 0 ) by A5, A3, A13, FDIFF_1: 23

        .= ( exp_R . x);

      end;

      

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

      proof

        let x;

        

         A15: exp_R is_differentiable_in x by SIN_COS: 65;

        assume

         A16: x in Z;

        

        then

         A17: (( exp_R + f) . x) = (( exp_R . x) + (f . x)) by A4, VALUED_1:def 1

        .= (( exp_R . x) + 1) by A2, A16;

        ( exp_R + f) is_differentiable_in x & (( exp_R + f) . x) <> 0 by A8, A9, A16, FDIFF_1: 9;

        

        then ( diff (( exp_R / ( exp_R + f)),x)) = (((( diff ( exp_R ,x)) * (( exp_R + f) . x)) - (( diff (( exp_R + f),x)) * ( exp_R . x))) / ((( exp_R + f) . x) ^2 )) by A15, FDIFF_2: 14

        .= (((( exp_R . x) * (( exp_R + f) . x)) - (( diff (( exp_R + f),x)) * ( exp_R . x))) / ((( exp_R + f) . x) ^2 )) by SIN_COS: 65

        .= (((( exp_R . x) * (( exp_R . x) + 1)) - (((( exp_R + f) `| Z) . x) * ( exp_R . x))) / ((( exp_R . x) + 1) ^2 )) by A8, A16, A17, FDIFF_1:def 7

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

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

        hence thesis by A11, A16, FDIFF_1:def 7;

      end;

      

       A18: for x st x in Z holds (( exp_R / ( exp_R + f)) . x) > 0

      proof

        let x;

        

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

        assume

         A20: x in Z;

        then x in ( dom ( exp_R / ( exp_R + f))) by A1, FUNCT_1: 11;

        

        then

         A21: (( exp_R / ( exp_R + f)) . x) = (( exp_R . x) * ((( exp_R + f) . x) " )) by RFUNCT_1:def 1

        .= (( exp_R . x) * (1 / (( exp_R + f) . x))) by XCMPLX_1: 215

        .= (( exp_R . x) / (( exp_R + f) . x)) by XCMPLX_1: 99;

        (( exp_R + f) . x) > 0 by A9, A20;

        hence thesis by A21, A19, XREAL_1: 139;

      end;

      

       A22: for x st x in Z holds ( ln * ( exp_R / ( exp_R + f))) is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then ( exp_R / ( exp_R + f)) is_differentiable_in x & (( exp_R / ( exp_R + f)) . x) > 0 by A11, A18, FDIFF_1: 9;

        hence thesis by TAYLOR_1: 20;

      end;

      then

       A23: ( ln * ( exp_R / ( exp_R + f))) is_differentiable_on Z by A1, FDIFF_1: 9;

      for x st x in Z holds ((( ln * ( exp_R / ( exp_R + f))) `| Z) . x) = (1 / (( exp_R . x) + 1))

      proof

        let x;

        assume

         A24: x in Z;

        then x in ( dom ( exp_R / ( exp_R + f))) by A1, FUNCT_1: 11;

        

        then

         A25: (( exp_R / ( exp_R + f)) . x) = (( exp_R . x) * ((( exp_R + f) . x) " )) by RFUNCT_1:def 1

        .= (( exp_R . x) * (1 / (( exp_R + f) . x))) by XCMPLX_1: 215

        .= (( exp_R . x) / (( exp_R + f) . x)) by XCMPLX_1: 99

        .= (( exp_R . x) / (( exp_R . x) + (f . x))) by A4, A24, VALUED_1:def 1

        .= (( exp_R . x) / (( exp_R . x) + 1)) by A2, A24;

        then

         A26: (( exp_R . x) / (( exp_R . x) + 1)) > 0 by A18, A24;

        ( exp_R / ( exp_R + f)) is_differentiable_in x & (( exp_R / ( exp_R + f)) . x) > 0 by A11, A18, A24, FDIFF_1: 9;

        

        then ( diff (( ln * ( exp_R / ( exp_R + f))),x)) = (( diff (( exp_R / ( exp_R + f)),x)) / (( exp_R / ( exp_R + f)) . x)) by TAYLOR_1: 20

        .= (((( exp_R / ( exp_R + f)) `| Z) . x) / (( exp_R / ( exp_R + f)) . x)) by A11, A24, FDIFF_1:def 7

        .= ((( exp_R . x) / ((( exp_R . x) + 1) ^2 )) / (( exp_R . x) / (( exp_R . x) + 1))) by A14, A24, A25

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

        .= (((( exp_R . x) / (( exp_R . x) + 1)) / (( exp_R . x) / (( exp_R . x) + 1))) / (( exp_R . x) + 1)) by XCMPLX_1: 48

        .= (1 / (( exp_R . x) + 1)) by A26, XCMPLX_1: 60;

        hence thesis by A23, A24, FDIFF_1:def 7;

      end;

      hence thesis by A1, A22, FDIFF_1: 9;

    end;

    theorem :: FDIFF_4:57

    Z c= ( dom ( ln * (( exp_R - f) / exp_R ))) & (for x st x in Z holds (f . x) = 1 & (( exp_R - f) . x) > 0 ) implies ( ln * (( exp_R - f) / exp_R )) is_differentiable_on Z & for x st x in Z holds ((( ln * (( exp_R - f) / exp_R )) `| Z) . x) = (1 / (( exp_R . x) - 1))

    proof

      assume that

       A1: Z c= ( dom ( ln * (( exp_R - f) / exp_R ))) and

       A2: for x st x in Z holds (f . x) = 1 & (( exp_R - f) . x) > 0 ;

      

       A3: for x st x in Z holds (f . x) = (( 0 * x) + 1) by A2;

      for y be object st y in Z holds y in ( dom (( exp_R - f) / exp_R )) by A1, FUNCT_1: 11;

      then Z c= ( dom (( exp_R - f) / exp_R )) by TARSKI:def 3;

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

      then

       A4: Z c= ( dom ( exp_R - f)) by XBOOLE_1: 18;

      then Z c= (( dom exp_R ) /\ ( dom f)) by VALUED_1: 12;

      then

       A5: Z c= ( dom f) by XBOOLE_1: 18;

      then

       A6: f is_differentiable_on Z by A3, FDIFF_1: 23;

      

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

      then

       A8: ( exp_R - f) is_differentiable_on Z by A4, A6, FDIFF_1: 19;

      for x st x in Z holds ( exp_R . x) <> 0 by SIN_COS: 54;

      then

       A9: (( exp_R - f) / exp_R ) is_differentiable_on Z by A7, A8, FDIFF_2: 21;

      

       A10: for x st x in Z holds ((( exp_R - f) `| Z) . x) = ( exp_R . x)

      proof

        let x;

        assume

         A11: x in Z;

        

        hence ((( exp_R - f) `| Z) . x) = (( diff ( exp_R ,x)) - ( diff (f,x))) by A4, A6, A7, FDIFF_1: 19

        .= (( exp_R . x) - ( diff (f,x))) by SIN_COS: 65

        .= (( exp_R . x) - ((f `| Z) . x)) by A6, A11, FDIFF_1:def 7

        .= (( exp_R . x) - 0 ) by A5, A3, A11, FDIFF_1: 23

        .= ( exp_R . x);

      end;

      

       A12: for x st x in Z holds (((( exp_R - f) / exp_R ) `| Z) . x) = (1 / ( exp_R . x))

      proof

        let x;

        

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

        assume

         A14: x in Z;

        

        then

         A15: (( exp_R - f) . x) = (( exp_R . x) - (f . x)) by A4, VALUED_1: 13

        .= (( exp_R . x) - 1) by A2, A14;

         exp_R is_differentiable_in x & ( exp_R - f) is_differentiable_in x by A8, A14, FDIFF_1: 9, SIN_COS: 65;

        

        then ( diff ((( exp_R - f) / exp_R ),x)) = (((( diff (( exp_R - f),x)) * ( exp_R . x)) - (( diff ( exp_R ,x)) * (( exp_R - f) . x))) / (( exp_R . x) ^2 )) by A13, FDIFF_2: 14

        .= (((((( exp_R - f) `| Z) . x) * ( exp_R . x)) - (( diff ( exp_R ,x)) * (( exp_R - f) . x))) / (( exp_R . x) ^2 )) by A8, A14, FDIFF_1:def 7

        .= (((( exp_R . x) * ( exp_R . x)) - (( diff ( exp_R ,x)) * (( exp_R - f) . x))) / (( exp_R . x) ^2 )) by A10, A14

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

        .= ((( exp_R . x) / ( exp_R . x)) / ( exp_R . x)) by XCMPLX_1: 78

        .= (1 / ( exp_R . x)) by A13, XCMPLX_1: 60;

        hence thesis by A9, A14, FDIFF_1:def 7;

      end;

      

       A16: for x st x in Z holds ((( exp_R - f) / exp_R ) . x) > 0

      proof

        let x;

        

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

        assume

         A18: x in Z;

        then x in ( dom (( exp_R - f) / exp_R )) by A1, FUNCT_1: 11;

        

        then

         A19: ((( exp_R - f) / exp_R ) . x) = ((( exp_R - f) . x) * (( exp_R . x) " )) by RFUNCT_1:def 1

        .= ((( exp_R - f) . x) * (1 / ( exp_R . x))) by XCMPLX_1: 215

        .= ((( exp_R - f) . x) / ( exp_R . x)) by XCMPLX_1: 99;

        (( exp_R - f) . x) > 0 by A2, A18;

        hence thesis by A19, A17, XREAL_1: 139;

      end;

      

       A20: for x st x in Z holds ( ln * (( exp_R - f) / exp_R )) is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then (( exp_R - f) / exp_R ) is_differentiable_in x & ((( exp_R - f) / exp_R ) . x) > 0 by A9, A16, FDIFF_1: 9;

        hence thesis by TAYLOR_1: 20;

      end;

      then

       A21: ( ln * (( exp_R - f) / exp_R )) is_differentiable_on Z by A1, FDIFF_1: 9;

      for x st x in Z holds ((( ln * (( exp_R - f) / exp_R )) `| Z) . x) = (1 / (( exp_R . x) - 1))

      proof

        let x;

        

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

        assume

         A23: x in Z;

        then x in ( dom (( exp_R - f) / exp_R )) by A1, FUNCT_1: 11;

        

        then

         A24: ((( exp_R - f) / exp_R ) . x) = ((( exp_R - f) . x) * (( exp_R . x) " )) by RFUNCT_1:def 1

        .= ((( exp_R - f) . x) * (1 / ( exp_R . x))) by XCMPLX_1: 215

        .= ((( exp_R - f) . x) / ( exp_R . x)) by XCMPLX_1: 99

        .= ((( exp_R . x) - (f . x)) / ( exp_R . x)) by A4, A23, VALUED_1: 13

        .= ((( exp_R . x) - 1) / ( exp_R . x)) by A2, A23;

        (( exp_R - f) / exp_R ) is_differentiable_in x & ((( exp_R - f) / exp_R ) . x) > 0 by A9, A16, A23, FDIFF_1: 9;

        

        then ( diff (( ln * (( exp_R - f) / exp_R )),x)) = (( diff ((( exp_R - f) / exp_R ),x)) / ((( exp_R - f) / exp_R ) . x)) by TAYLOR_1: 20

        .= ((((( exp_R - f) / exp_R ) `| Z) . x) / ((( exp_R - f) / exp_R ) . x)) by A9, A23, FDIFF_1:def 7

        .= ((1 / ( exp_R . x)) / ((( exp_R . x) - 1) / ( exp_R . x))) by A12, A23, A24

        .= (1 / (( exp_R . x) - 1)) by A22, XCMPLX_1: 55;

        hence thesis by A21, A23, FDIFF_1:def 7;

      end;

      hence thesis by A1, A20, FDIFF_1: 9;

    end;