fdiff_6.miz



    begin

    reserve y for set,

x,a for Real,

n for Element of NAT ,

Z for open Subset of REAL ,

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

    

     Lm1: (1 - ( cos (2 * x))) = (2 * (( sin x) ^2 ))

    proof

      (1 - ( cos (2 * x))) = (1 - ( cos (x + x)))

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

      .= (((( cos x) ^2 ) + (( sin x) ^2 )) - ((( cos x) ^2 ) - (( sin x) ^2 ))) by SIN_COS: 29

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

      hence thesis;

    end;

    

     Lm2: (1 + ( cos (2 * x))) = (2 * (( cos x) ^2 ))

    proof

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

      .= (1 + ((( cos x) ^2 ) - (( sin x) ^2 ))) by SIN_COS: 75

      .= (((( cos x) ^2 ) + (( sin x) ^2 )) + ((( cos x) ^2 ) - (( sin x) ^2 ))) by SIN_COS: 29

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

      hence thesis;

    end;

    

     Lm3: ( sin . x) > 0 implies ( sin . x) = (((1 - ( cos . x)) * (1 + ( cos . x))) #R (1 / 2))

    proof

      assume

       A1: ( sin . x) > 0 ;

      

      then ( sin . x) = (( sin . x) #R (2 * (1 / 2))) by PREPOWER: 72

      .= ((( sin . x) #R (1 + 1)) #R (1 / 2)) by A1, PREPOWER: 91

      .= (((( sin . x) #R 1) * (( sin . x) #R 1)) #R (1 / 2)) by A1, PREPOWER: 75

      .= ((( sin . x) * (( sin . x) #R 1)) #R (1 / 2)) by A1, PREPOWER: 72

      .= ((((( sin . x) ^2 ) + (( cos . x) ^2 )) - (( cos . x) ^2 )) #R (1 / 2)) by A1, PREPOWER: 72

      .= (((1 ^2 ) - (( cos . x) ^2 )) #R (1 / 2)) by SIN_COS: 28

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

      hence thesis;

    end;

    

     Lm4: ( sin . x) > 0 & ( cos . x) < 1 & ( cos . x) > ( - 1) implies (( sin . x) / ((1 - ( cos . x)) #R (1 / 2))) = ((1 + ( cos . x)) #R (1 / 2))

    proof

      assume that

       A1: ( sin . x) > 0 and

       A2: ( cos . x) < 1 and

       A3: ( cos . x) > ( - 1);

      

       A4: (1 - ( cos . x)) > (1 - 1) by A2, XREAL_1: 15;

      (1 + ( cos . x)) > (1 + ( - 1)) by A3, XREAL_1: 8;

      then

       A5: ((1 - ( cos . x)) * (1 + ( cos . x))) > 0 by A4, XREAL_1: 129;

      (( sin . x) / ((1 - ( cos . x)) #R (1 / 2))) = ((((1 - ( cos . x)) * (1 + ( cos . x))) #R (1 / 2)) / ((1 - ( cos . x)) #R (1 / 2))) by A1, Lm3

      .= ((((1 - ( cos . x)) * (1 + ( cos . x))) / (1 - ( cos . x))) #R (1 / 2)) by A4, A5, PREPOWER: 80

      .= ((1 + ( cos . x)) #R (1 / 2)) by A4, XCMPLX_1: 89;

      hence thesis;

    end;

    theorem :: FDIFF_6:1

    

     Th1: a > 0 implies ( exp_R . (x * ( log ( number_e ,a)))) = (a #R x)

    proof

      assume

       A1: a > 0 ;

       number_e <> 1 by TAYLOR_1: 11;

      

      then ( exp_R . (x * ( log ( number_e ,a)))) = ( exp_R . ( log ( number_e ,(a to_power x)))) by A1, POWER: 55, TAYLOR_1: 11

      .= ( exp_R . ( log ( number_e ,(a #R x)))) by A1, POWER:def 2

      .= (a #R x) by A1, PREPOWER: 81, TAYLOR_1: 15;

      hence thesis;

    end;

    theorem :: FDIFF_6:2

    

     Th2: a > 0 implies ( exp_R . ( - (x * ( log ( number_e ,a))))) = (a #R ( - x))

    proof

      

       A1: number_e <> 1 by TAYLOR_1: 11;

      assume

       A2: a > 0 ;

      ( exp_R . ( - (x * ( log ( number_e ,a))))) = ( exp_R . (( - x) * ( log ( number_e ,a))))

      .= ( exp_R . ( log ( number_e ,(a to_power ( - x))))) by A2, A1, POWER: 55, TAYLOR_1: 11

      .= ( exp_R . ( log ( number_e ,(a #R ( - x))))) by A2, POWER:def 2

      .= (a #R ( - x)) by A2, PREPOWER: 81, TAYLOR_1: 15;

      hence thesis;

    end;

    

     Lm5: ( sin . x) > 0 & ( cos . x) < 1 & ( cos . x) > ( - 1) implies (( sin . x) / ((1 + ( cos . x)) #R (1 / 2))) = ((1 - ( cos . x)) #R (1 / 2))

    proof

      assume that

       A1: ( sin . x) > 0 and

       A2: ( cos . x) < 1 and

       A3: ( cos . x) > ( - 1);

      

       A4: (1 + ( cos . x)) > (1 + ( - 1)) by A3, XREAL_1: 8;

      (1 - ( cos . x)) > (1 - 1) by A2, XREAL_1: 15;

      then

       A5: ((1 - ( cos . x)) * (1 + ( cos . x))) > 0 by A4, XREAL_1: 129;

      (( sin . x) / ((1 + ( cos . x)) #R (1 / 2))) = ((((1 - ( cos . x)) * (1 + ( cos . x))) #R (1 / 2)) / ((1 + ( cos . x)) #R (1 / 2))) by A1, Lm3

      .= ((((1 - ( cos . x)) * (1 + ( cos . x))) / (1 + ( cos . x))) #R (1 / 2)) by A4, A5, PREPOWER: 80

      .= ((1 - ( cos . x)) #R (1 / 2)) by A4, XCMPLX_1: 89;

      hence thesis;

    end;

    theorem :: FDIFF_6:3

    

     Th3: 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)) and

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

       A3: f2 = ( #Z 2);

      

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

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

      proof

        let x;

        assume x in Z;

        

        hence (((f1 - f2) `| Z) . x) = ( 0 + ((2 * ( - 1)) * x)) by A1, A3, A4, FDIFF_4: 12

        .= ( - (2 * x));

      end;

      hence thesis by A1, A3, A4, FDIFF_4: 12;

    end;

    theorem :: FDIFF_6:4

    

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

    proof

      assume that

       A1: Z c= ( dom ((f1 + f2) / (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: for x st x in Z holds (f1 . x) = (a ^2 ) by A3;

      

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

      then

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

      then

       A7: (f1 + f2) is_differentiable_on Z by A2, A4, FDIFF_4: 17;

      

       A8: Z c= ( dom (f1 - f2)) by A5, XBOOLE_1: 1;

      then

       A9: (f1 - f2) is_differentiable_on Z by A2, A4, Th3;

      

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

      then

       A11: ((f1 + f2) / (f1 - f2)) is_differentiable_on Z by A7, A9, FDIFF_2: 21;

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

      proof

        let x;

        

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

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

        assume

         A13: x in Z;

        then

         A14: ((f1 - f2) . x) <> 0 by A3;

        

         A15: ((f1 - f2) . x) = ((f1 . x) - (f2 . x)) by A8, A13, VALUED_1: 13

        .= ((a ^2 ) - (x |^ 2)) by A3, A13, A12;

        

         A16: ((f1 + f2) . x) = ((f1 . x) + (f2 . x)) by A6, A13, VALUED_1:def 1

        .= ((a ^2 ) + (x |^ 2)) by A3, A13, A12;

        (f1 + f2) is_differentiable_in x & (f1 - f2) is_differentiable_in x by A7, A9, A13, FDIFF_1: 9;

        

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

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

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

        .= ((((2 * x) * ((f1 - f2) . x)) - ((((f1 - f2) `| Z) . x) * ((f1 + f2) . x))) / (((f1 - f2) . x) ^2 )) by A2, A6, A4, A13, FDIFF_4: 17

        .= ((((2 * x) * ((f1 - f2) . x)) - (( - (2 * x)) * ((f1 + f2) . x))) / (((f1 - f2) . x) ^2 )) by A2, A8, A4, A13, Th3

        .= (((4 * (a ^2 )) * x) / (((a ^2 ) - (x |^ 2)) ^2 )) by A16, A15;

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

      end;

      hence thesis by A7, A9, A10, FDIFF_2: 21;

    end;

    theorem :: FDIFF_6:5

    

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

    proof

      assume that

       A1: Z c= ( dom f) and

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

       A3: f2 = ( #Z 2) and

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

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

      then

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

      then

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

      then

       A7: Z c= ( dom (f1 - f2)) by XBOOLE_1: 1;

      

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

      then

       A9: ((f1 + f2) / (f1 - f2)) is_differentiable_on Z by A3, A5, Th4;

      

       A10: Z c= ( dom (f1 + f2)) by A6, XBOOLE_1: 18;

      

       A11: for x st x in Z holds (((f1 + f2) / (f1 - f2)) . x) > 0

      proof

        let x;

        

         A12: (f2 . x) = (x #Z 2) by A3, TAYLOR_1:def 1

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

        assume

         A13: x in Z;

        then

         A14: ((f1 - f2) . x) > 0 by A4;

        a <> 0 by A4, A13;

        then

         A15: (a ^2 ) > 0 by SQUARE_1: 12;

        (x |^ 2) = (x ^2 ) by NEWTON: 81;

        then

         A16: ((a ^2 ) + (x |^ 2)) > ( 0 + 0 ) by A15, XREAL_1: 8, XREAL_1: 63;

        

         A17: (((f1 + f2) / (f1 - f2)) . x) = (((f1 + f2) . x) * (((f1 - f2) . x) " )) by A5, A13, RFUNCT_1:def 1

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

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

        .= ((a ^2 ) + (x |^ 2)) by A4, A13, A12;

        hence thesis by A14, A16, A17, XREAL_1: 139;

      end;

      

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

      proof

        let x;

        assume x in Z;

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

        hence thesis by TAYLOR_1: 20;

      end;

      then

       A19: f is_differentiable_on Z by A1, A2, FDIFF_1: 9;

      for x st x in Z holds ((f `| Z) . x) = (((4 * (a ^2 )) * x) / ((a |^ 4) - (x |^ 4)))

      proof

        let x;

        

         A20: ((a ^2 ) ^2 ) = ((a |^ 2) * (a ^2 )) by NEWTON: 81

        .= ((a |^ 2) * (a |^ 2)) by NEWTON: 81

        .= ((a |^ 2) |^ 2) by WSIERP_1: 1

        .= (a |^ (2 * 2)) by NEWTON: 9

        .= (a |^ 4);

        

         A21: ((x |^ 2) ^2 ) = ((x |^ 2) |^ 2) by WSIERP_1: 1

        .= (x |^ (2 * 2)) by NEWTON: 9

        .= (x |^ 4);

        

         A22: (f2 . x) = (x #Z 2) by A3, TAYLOR_1:def 1

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

        assume

         A23: x in Z;

        

        then

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

        .= ((a ^2 ) + (x |^ 2)) by A4, A23, A22;

        

         A25: ((f1 - f2) . x) = ((f1 . x) - (f2 . x)) by A7, A23, VALUED_1: 13

        .= ((a ^2 ) - (x |^ 2)) by A4, A23, A22;

        then

         A26: ((a ^2 ) - (x |^ 2)) > 0 by A4, A23;

        

         A27: (((f1 + f2) / (f1 - f2)) . x) = (((f1 + f2) . x) * (((f1 - f2) . x) " )) by A5, A23, RFUNCT_1:def 1

        .= (((a ^2 ) + (x |^ 2)) / ((a ^2 ) - (x |^ 2))) by A24, A25, XCMPLX_0:def 9;

        ((f1 + f2) / (f1 - f2)) is_differentiable_in x & (((f1 + f2) / (f1 - f2)) . x) > 0 by A9, A11, A23, FDIFF_1: 9;

        

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

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

        .= ((((4 * (a ^2 )) * x) / (((a ^2 ) - (x |^ 2)) ^2 )) / (((a ^2 ) + (x |^ 2)) / ((a ^2 ) - (x |^ 2)))) by A3, A5, A8, A23, A27, Th4

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

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

        .= ((((4 * (a ^2 )) * x) / ((a ^2 ) + (x |^ 2))) / ((a ^2 ) - (x |^ 2))) by A26, XCMPLX_1: 55

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

        .= (((4 * (a ^2 )) * x) / ((a |^ 4) - (x |^ 4))) by A20, A21;

        hence thesis by A2, A19, A23, FDIFF_1:def 7;

      end;

      hence thesis by A1, A2, A18, FDIFF_1: 9;

    end;

    theorem :: FDIFF_6:6

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

    proof

      assume that

       A1: Z c= ( dom ((1 / (4 * (a ^2 ))) (#) f)) and

       A2: f = ( ln * ((f1 + f2) / (f1 - f2))) & f2 = ( #Z 2) and

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

      

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

      then

       A5: f is_differentiable_on Z by A2, A3, Th5;

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

      proof

        let x;

        assume

         A6: x in Z;

        then a <> 0 by A3;

        then (a ^2 ) > 0 by SQUARE_1: 12;

        then

         A7: (4 * (a ^2 )) > (4 * 0 ) by XREAL_1: 68;

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

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

        .= ((1 / (4 * (a ^2 ))) * (((4 * (a ^2 )) * x) / ((a |^ 4) - (x |^ 4)))) by A2, A3, A4, A6, Th5

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

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

        .= (x / ((a |^ 4) - (x |^ 4))) by A7, XCMPLX_1: 108;

        hence thesis;

      end;

      hence thesis by A1, A5, FDIFF_1: 20;

    end;

    theorem :: FDIFF_6:7

    

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

    proof

      assume that

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

       A2: f1 = ( #Z 2) and

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

      

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

      then

       A5: Z c= ( dom (f2 + f1)) by XBOOLE_1: 1;

      

       A6: for x st x in Z holds f1 is_differentiable_in x by A2, TAYLOR_1: 2;

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

      then

       A7: f1 is_differentiable_on Z by A6, FDIFF_1: 9;

      

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

      proof

        let x;

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

        then

         A9: ( diff (f1,x)) = (2 * x) by A2, TAYLOR_1: 2;

        assume x in Z;

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

      end;

      

       A10: for x st x in Z holds (f2 . x) = (1 ^2 ) by A3;

      then

       A11: (f2 + f1) is_differentiable_on Z by A2, A5, FDIFF_4: 17;

      

       A12: for x st x in Z holds ((f2 + f1) . x) <> 0

      proof

        let x;

        

         A13: (1 + (x ^2 )) > ( 0 + 0 ) by XREAL_1: 8, XREAL_1: 63;

        assume

         A14: x in Z;

        

        then ((f2 + f1) . x) = ((f2 . x) + (f1 . x)) by A5, VALUED_1:def 1

        .= (1 + (f1 . x)) by A3, A14

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

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

        .= (1 + (x ^2 )) by NEWTON: 81;

        hence thesis by A13;

      end;

      then

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

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

      proof

        let x;

        

         A16: f1 is_differentiable_in x by A2, TAYLOR_1: 2;

        

         A17: (f1 . x) = (x #Z 2) by A2, TAYLOR_1:def 1

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

        .= (x ^2 ) by NEWTON: 81;

        assume

         A18: x in Z;

        

        then

         A19: ((f2 + f1) . x) = ((f2 . x) + (f1 . x)) by A5, VALUED_1:def 1

        .= (1 + (f1 . x)) by A3, A18

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

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

        .= (1 + (x ^2 )) by NEWTON: 81;

        (f2 + f1) is_differentiable_in x & ((f2 + f1) . x) <> 0 by A11, A12, A18, FDIFF_1: 9;

        

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

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

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

        .= ((((2 * x) * ((f2 + f1) . x)) - ((((f2 + f1) `| Z) . x) * (f1 . x))) / (((f2 + f1) . x) ^2 )) by A8, A18

        .= ((((2 * x) * (1 + (x ^2 ))) - ((2 * x) * (x ^2 ))) / ((1 + (x ^2 )) ^2 )) by A2, A10, A5, A18, A17, A19, FDIFF_4: 17

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

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

      end;

      hence thesis by A11, A7, A12, FDIFF_2: 21;

    end;

    theorem :: FDIFF_6:8

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

    proof

      assume that

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

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

       A3: f1 = ( #Z 2) and

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

      

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

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

      then

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

      then

       A7: (f1 / (f2 + f1)) is_differentiable_on Z by A3, A4, Th7;

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

      then

       A8: Z c= ( dom (f2 + f1)) by XBOOLE_1: 1;

      

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

      proof

        let x;

        assume

         A10: x in Z;

        

        then

         A11: ((f1 / (f2 + f1)) . x) = ((f1 . x) * (((f2 + f1) . x) " )) by A6, RFUNCT_1:def 1

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

        

         A12: x <> 0 by A4, A10;

        then

         A13: (1 + (x ^2 )) > ( 0 + 0 ) by SQUARE_1: 12, XREAL_1: 8;

        

         A14: (f1 . x) = (x #Z 2) by A3, TAYLOR_1:def 1

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

        .= (x ^2 ) by NEWTON: 81;

        then

         A15: (f1 . x) > 0 by A12, SQUARE_1: 12;

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

        .= (1 + (x ^2 )) by A4, A10, A14;

        hence thesis by A15, A13, A11, XREAL_1: 139;

      end;

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

      proof

        let x;

        assume x in Z;

        then (f1 / (f2 + f1)) is_differentiable_in x & ((f1 / (f1 + f2)) . x) > 0 by A7, A9, FDIFF_1: 9;

        hence thesis by TAYLOR_1: 20;

      end;

      then

       A16: f is_differentiable_on Z by A2, A5, FDIFF_1: 9;

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

      proof

        let x;

        

         A17: (f1 . x) = (x #Z 2) by A3, TAYLOR_1:def 1

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

        .= (x ^2 ) by NEWTON: 81;

        assume

         A18: x in Z;

        then

         A19: (f1 / (f2 + f1)) is_differentiable_in x & ((f1 / (f1 + f2)) . x) > 0 by A7, A9, FDIFF_1: 9;

        x <> 0 by A4, A18;

        then

         A20: (1 + (x ^2 )) > ( 0 + 0 ) by SQUARE_1: 12, XREAL_1: 8;

        

         A21: ((f2 + f1) . x) = ((f2 . x) + (f1 . x)) by A8, A18, VALUED_1:def 1

        .= (1 + (x ^2 )) by A4, A18, A17;

        

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

        .= ((x ^2 ) / (1 + (x ^2 ))) by A17, A21, XCMPLX_0:def 9;

        ((((1 / 2) (#) f) `| Z) . x) = ((1 / 2) * ( diff (( ln * (f1 / (f2 + f1))),x))) by A1, A2, A16, A18, FDIFF_1: 20

        .= ((1 / 2) * (( diff ((f1 / (f2 + f1)),x)) / ((f1 / (f2 + f1)) . x))) by A19, TAYLOR_1: 20

        .= ((1 / 2) * ((((f1 / (f2 + f1)) `| Z) . x) / ((f1 / (f2 + f1)) . x))) by A7, A18, FDIFF_1:def 7

        .= ((1 / 2) * (((2 * x) / ((1 + (x ^2 )) ^2 )) / ((x ^2 ) / (1 + (x ^2 ))))) by A3, A4, A6, A18, A22, Th7

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

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

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

        .= (((x / (1 + (x ^2 ))) / ((x ^2 ) / (1 + (x ^2 )))) / (1 + (x ^2 ))) by XCMPLX_1: 48

        .= ((x / (x ^2 )) / (1 + (x ^2 ))) by A20, XCMPLX_1: 55

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

        .= ((1 / x) / (1 + (x ^2 ))) by A4, A18, XCMPLX_1: 60

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

        hence thesis;

      end;

      hence thesis by A1, A16, FDIFF_1: 20;

    end;

    theorem :: FDIFF_6:9

    Z c= ( dom ( ln * ( #Z n))) & (for x st x in Z holds x > 0 ) implies ( ln * ( #Z n)) is_differentiable_on Z & for x st x in Z holds ((( ln * ( #Z n)) `| Z) . x) = (n / x)

    proof

      assume that

       A1: Z c= ( dom ( ln * ( #Z n))) and

       A2: for x st x in Z holds x > 0 ;

      

       A3: for x st x in Z holds ( ln * ( #Z n)) is_differentiable_in x

      proof

        let x;

        

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

        assume x in Z;

        then ( #Z n) is_differentiable_in x & (( #Z n) . x) > 0 by A2, A4, PREPOWER: 39, TAYLOR_1: 2;

        hence thesis by TAYLOR_1: 20;

      end;

      then

       A5: ( ln * ( #Z n)) is_differentiable_on Z by A1, FDIFF_1: 9;

      for x st x in Z holds ((( ln * ( #Z n)) `| Z) . x) = (n / x)

      proof

        let x;

        

         A6: ( #Z n) is_differentiable_in x & ( diff (( #Z n),x)) = (n * (x #Z (n - 1))) by TAYLOR_1: 2;

        assume

         A7: x in Z;

        then

         A8: x > 0 by A2;

        

         A9: (x |^ n) > 0 by A2, A7, NEWTON: 83;

        

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

        then (( #Z n) . x) > 0 by A2, A7, PREPOWER: 39;

        

        then ( diff (( ln * ( #Z n)),x)) = ((n * (x #Z (n - 1))) / (x #Z n)) by A6, A10, TAYLOR_1: 20

        .= ((n * (x #Z (n - 1))) / (x |^ n)) by PREPOWER: 36

        .= ((n * ((x |^ n) / (x |^ 1))) / (x |^ n)) by A8, PREPOWER: 43

        .= (n * (((x |^ n) / (x |^ 1)) / (x |^ n))) by XCMPLX_1: 74

        .= (n * (((x |^ n) / (x |^ n)) / (x |^ 1))) by XCMPLX_1: 48

        .= (n * (1 / (x |^ 1))) by A9, XCMPLX_1: 60

        .= (n * (1 / x))

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

        .= (n / x);

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

      end;

      hence thesis by A1, A3, FDIFF_1: 9;

    end;

    theorem :: FDIFF_6:10

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

    proof

      assume that

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

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

      

       A3: Z c= (( dom (f2 ^ )) /\ ( dom ( ln * (f1 / f2)))) by A1, VALUED_1:def 1;

      then

       A4: Z c= ( dom ( ln * (f1 / f2))) by XBOOLE_1: 18;

      

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

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

      then

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

      

       A7: for x st x in Z holds (f1 . x) = (x - 1) & (f1 . x) > 0 & (f2 . x) = (x - 0 ) & (f2 . x) > 0 by A2;

      then

       A8: ( ln * (f1 / f2)) is_differentiable_on Z by A4, FDIFF_4: 24;

      

       A9: for x st x in Z holds (f2 . x) = ( 0 + x) & (f2 . x) <> 0 by A2;

      then

       A10: (f2 ^ ) is_differentiable_on Z by A6, FDIFF_4: 14;

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

      proof

        let x;

        assume

         A11: x in Z;

        then

         A12: (f2 . x) = x & (f2 . x) > 0 by A2;

        

         A13: (f1 . x) = (x - 1) & (f1 . x) > 0 by A2, A11;

        ((((f2 ^ ) + ( ln * (f1 / f2))) `| Z) . x) = (( diff ((f2 ^ ),x)) + ( diff (( ln * (f1 / f2)),x))) by A1, A10, A8, A11, FDIFF_1: 18

        .= ((((f2 ^ ) `| Z) . x) + ( diff (( ln * (f1 / f2)),x))) by A10, A11, FDIFF_1:def 7

        .= ((((f2 ^ ) `| Z) . x) + ((( ln * (f1 / f2)) `| Z) . x)) by A8, A11, FDIFF_1:def 7

        .= (( - (1 / (( 0 + x) ^2 ))) + ((( ln * (f1 / f2)) `| Z) . x)) by A6, A9, A11, FDIFF_4: 14

        .= (( - (1 / (( 0 + x) ^2 ))) + ((1 - 0 ) / ((x - 1) * (x - 0 )))) by A4, A7, A11, FDIFF_4: 24

        .= (( - ((1 * (x - 1)) / ((x ^2 ) * (x - 1)))) + (1 / ((x - 1) * x))) by A13, XCMPLX_1: 91

        .= (( - ((1 * (x - 1)) / ((x ^2 ) * (x - 1)))) + ((1 * x) / (((x - 1) * x) * x))) by A12, XCMPLX_1: 91

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

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

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

        hence thesis;

      end;

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

    end;

    theorem :: FDIFF_6:11

    

     Th11: Z c= ( dom ( exp_R * f)) & (for x st x in Z holds (f . x) = (x * ( log ( number_e ,a)))) & a > 0 implies ( exp_R * f) is_differentiable_on Z & for x st x in Z holds ((( exp_R * f) `| Z) . x) = ((a #R x) * ( log ( number_e ,a)))

    proof

      assume that

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

       A2: for x st x in Z holds (f . x) = (x * ( log ( number_e ,a))) and

       A3: a > 0 ;

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

      then

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

      

       A5: for x st x in Z holds (f . x) = ((( log ( number_e ,a)) * x) + 0 ) by A2;

      then

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

      

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

      proof

        let x;

        assume x in Z;

        then f is_differentiable_in x by A6, FDIFF_1: 9;

        hence thesis by TAYLOR_1: 19;

      end;

      then

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

      for x st x in Z holds ((( exp_R * f) `| Z) . x) = ((a #R x) * ( log ( number_e ,a)))

      proof

        let x;

        assume

         A9: x in Z;

        then f is_differentiable_in x by A6, FDIFF_1: 9;

        

        then ( diff (( exp_R * f),x)) = (( exp_R . (f . x)) * ( diff (f,x))) by TAYLOR_1: 19

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

        .= (( exp_R . (f . x)) * ( log ( number_e ,a))) by A4, A5, A9, FDIFF_1: 23

        .= (( exp_R . (x * ( log ( number_e ,a)))) * ( log ( number_e ,a))) by A2, A9

        .= ((a #R x) * ( log ( number_e ,a))) by A3, Th1;

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

      end;

      hence thesis by A1, A7, FDIFF_1: 9;

    end;

    theorem :: FDIFF_6:12

    Z c= ( dom ((1 / ( log ( number_e ,a))) (#) (( exp_R * f1) (#) f2))) & (for x st x in Z holds (f1 . x) = (x * ( log ( number_e ,a))) & (f2 . x) = (x - (1 / ( log ( number_e ,a))))) & a > 0 & a <> 1 implies ((1 / ( log ( number_e ,a))) (#) (( exp_R * f1) (#) f2)) is_differentiable_on Z & for x st x in Z holds ((((1 / ( log ( number_e ,a))) (#) (( exp_R * f1) (#) f2)) `| Z) . x) = (x * (a #R x))

    proof

      assume that

       A1: Z c= ( dom ((1 / ( log ( number_e ,a))) (#) (( exp_R * f1) (#) f2))) and

       A2: for x st x in Z holds (f1 . x) = (x * ( log ( number_e ,a))) & (f2 . x) = (x - (1 / ( log ( number_e ,a)))) and

       A3: a > 0 and

       A4: a <> 1;

      

       A5: Z c= ( dom (( exp_R * f1) (#) f2)) by A1, VALUED_1:def 5;

      then

       A6: Z c= (( dom ( exp_R * f1)) /\ ( dom f2)) by VALUED_1:def 4;

      then

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

      

       A8: for x st x in Z holds (f2 . x) = ((1 * x) + ( - (1 / ( log ( number_e ,a)))))

      proof

        let x;

        

         A9: ((1 * x) + ( - (1 / ( log ( number_e ,a))))) = ((1 * x) - (1 / ( log ( number_e ,a))));

        assume x in Z;

        hence thesis by A2, A9;

      end;

      

       A10: for x st x in Z holds (f1 . x) = (x * ( log ( number_e ,a))) by A2;

      then

       A11: ( exp_R * f1) is_differentiable_on Z by A3, A7, Th11;

      

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

      then

       A13: f2 is_differentiable_on Z by A8, FDIFF_1: 23;

      then

       A14: (( exp_R * f1) (#) f2) is_differentiable_on Z by A5, A11, FDIFF_1: 21;

      

       A15: ( log ( number_e ,a)) <> 0

      proof

        

         A16: number_e <> 1 by TAYLOR_1: 11;

        assume ( log ( number_e ,a)) = 0 ;

        then ( log ( number_e ,a)) = ( log ( number_e ,1)) by SIN_COS2: 13, TAYLOR_1: 13;

        

        then a = ( number_e to_power ( log ( number_e ,1))) by A3, A16, POWER:def 3, TAYLOR_1: 11

        .= 1 by A16, POWER:def 3, TAYLOR_1: 11;

        hence contradiction by A4;

      end;

      for x st x in Z holds ((((1 / ( log ( number_e ,a))) (#) (( exp_R * f1) (#) f2)) `| Z) . x) = (x * (a #R x))

      proof

        let x;

        assume

         A17: x in Z;

        

        then

         A18: (( exp_R * f1) . x) = ( exp_R . (f1 . x)) by A7, FUNCT_1: 12

        .= ( exp_R . (x * ( log ( number_e ,a)))) by A2, A17

        .= (a #R x) by A3, Th1;

        ((((1 / ( log ( number_e ,a))) (#) (( exp_R * f1) (#) f2)) `| Z) . x) = ((1 / ( log ( number_e ,a))) * ( diff ((( exp_R * f1) (#) f2),x))) by A1, A14, A17, FDIFF_1: 20

        .= ((1 / ( log ( number_e ,a))) * (((( exp_R * f1) (#) f2) `| Z) . x)) by A14, A17, FDIFF_1:def 7

        .= ((1 / ( log ( number_e ,a))) * (((f2 . x) * ( diff (( exp_R * f1),x))) + ((( exp_R * f1) . x) * ( diff (f2,x))))) by A5, A11, A13, A17, FDIFF_1: 21

        .= ((1 / ( log ( number_e ,a))) * (((f2 . x) * ((( exp_R * f1) `| Z) . x)) + ((( exp_R * f1) . x) * ( diff (f2,x))))) by A11, A17, FDIFF_1:def 7

        .= ((1 / ( log ( number_e ,a))) * (((f2 . x) * ((( exp_R * f1) `| Z) . x)) + ((( exp_R * f1) . x) * ((f2 `| Z) . x)))) by A13, A17, FDIFF_1:def 7

        .= ((1 / ( log ( number_e ,a))) * (((f2 . x) * ((a #R x) * ( log ( number_e ,a)))) + ((( exp_R * f1) . x) * ((f2 `| Z) . x)))) by A3, A10, A7, A17, Th11

        .= ((1 / ( log ( number_e ,a))) * (((f2 . x) * ((a #R x) * ( log ( number_e ,a)))) + ((( exp_R * f1) . x) * 1))) by A12, A8, A17, FDIFF_1: 23

        .= ((1 / ( log ( number_e ,a))) * ((((f2 . x) * ( log ( number_e ,a))) + 1) * (a #R x))) by A18

        .= ((1 / ( log ( number_e ,a))) * ((((x - (1 / ( log ( number_e ,a)))) * ( log ( number_e ,a))) + 1) * (a #R x))) by A2, A17

        .= (((1 / ( log ( number_e ,a))) * (((x * ( log ( number_e ,a))) - ((1 / ( log ( number_e ,a))) * ( log ( number_e ,a)))) + 1)) * (a #R x))

        .= (((1 / ( log ( number_e ,a))) * (((x * ( log ( number_e ,a))) - 1) + 1)) * (a #R x)) by A15, XCMPLX_1: 106

        .= ((((1 / ( log ( number_e ,a))) * ( log ( number_e ,a))) * x) * (a #R x))

        .= ((1 * x) * (a #R x)) by A15, XCMPLX_1: 106

        .= (x * (a #R x));

        hence thesis;

      end;

      hence thesis by A1, A14, FDIFF_1: 20;

    end;

    theorem :: FDIFF_6:13

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

    proof

      assume that

       A1: Z c= ( dom ((1 / (1 + ( log ( number_e ,a)))) (#) (( exp_R * f) (#) exp_R ))) and

       A2: for x st x in Z holds (f . x) = (x * ( log ( number_e ,a))) and

       A3: a > 0 and

       A4: a <> (1 / number_e );

      

       A5: Z c= ( dom (( exp_R * f) (#) exp_R )) by A1, VALUED_1:def 5;

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

      then

       A6: Z c= ( dom ( exp_R * f)) by XBOOLE_1: 18;

      then

       A7: ( exp_R * f) is_differentiable_on Z by A2, A3, Th11;

      

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

      then

       A9: (( exp_R * f) (#) exp_R ) is_differentiable_on Z by A5, A7, FDIFF_1: 21;

      

       A10: (1 + ( log ( number_e ,a))) <> 0

      proof

        

         A11: ( number_e * a) > ( 0 * a) by A3, TAYLOR_1: 11, XREAL_1: 68;

        assume

         A12: (1 + ( log ( number_e ,a))) = 0 ;

        

         A13: number_e <> 1 by TAYLOR_1: 11;

        ( log ( number_e ,1)) = 0 by SIN_COS2: 13, TAYLOR_1: 13

        .= (( log ( number_e , number_e )) + ( log ( number_e ,a))) by A12, A13, POWER: 52, TAYLOR_1: 11

        .= ( log ( number_e ,( number_e * a))) by A3, A13, POWER: 53, TAYLOR_1: 11;

        

        then ( number_e * a) = ( number_e to_power ( log ( number_e ,1))) by A13, A11, POWER:def 3, TAYLOR_1: 11

        .= 1 by A13, POWER:def 3, TAYLOR_1: 11;

        hence contradiction by A4, XCMPLX_1: 73;

      end;

      for x st x in Z holds ((((1 / (1 + ( log ( number_e ,a)))) (#) (( exp_R * f) (#) exp_R )) `| Z) . x) = ((a #R x) * ( exp_R . x))

      proof

        let x;

        assume

         A14: x in Z;

        

        then

         A15: (( exp_R * f) . x) = ( exp_R . (f . x)) by A6, FUNCT_1: 12

        .= ( exp_R . (x * ( log ( number_e ,a)))) by A2, A14

        .= (a #R x) by A3, Th1;

        ((((1 / (1 + ( log ( number_e ,a)))) (#) (( exp_R * f) (#) exp_R )) `| Z) . x) = ((1 / (1 + ( log ( number_e ,a)))) * ( diff ((( exp_R * f) (#) exp_R ),x))) by A1, A9, A14, FDIFF_1: 20

        .= ((1 / (1 + ( log ( number_e ,a)))) * (((( exp_R * f) (#) exp_R ) `| Z) . x)) by A9, A14, FDIFF_1:def 7

        .= ((1 / (1 + ( log ( number_e ,a)))) * ((( exp_R . x) * ( diff (( exp_R * f),x))) + ((( exp_R * f) . x) * ( diff ( exp_R ,x))))) by A5, A7, A8, A14, FDIFF_1: 21

        .= ((1 / (1 + ( log ( number_e ,a)))) * ((( exp_R . x) * ((( exp_R * f) `| Z) . x)) + ((( exp_R * f) . x) * ( diff ( exp_R ,x))))) by A7, A14, FDIFF_1:def 7

        .= ((1 / (1 + ( log ( number_e ,a)))) * ((( exp_R . x) * ((( exp_R * f) `| Z) . x)) + ((( exp_R * f) . x) * ( exp_R . x)))) by TAYLOR_1: 16

        .= ((1 / (1 + ( log ( number_e ,a)))) * ((((( exp_R * f) `| Z) . x) + (( exp_R * f) . x)) * ( exp_R . x)))

        .= ((1 / (1 + ( log ( number_e ,a)))) * ((((a #R x) * ( log ( number_e ,a))) + (( exp_R * f) . x)) * ( exp_R . x))) by A2, A3, A6, A14, Th11

        .= ((((1 / (1 + ( log ( number_e ,a)))) * (( log ( number_e ,a)) + 1)) * (a #R x)) * ( exp_R . x)) by A15

        .= ((1 * (a #R x)) * ( exp_R . x)) by A10, XCMPLX_1: 106

        .= ((a #R x) * ( exp_R . x));

        hence thesis;

      end;

      hence thesis by A1, A9, FDIFF_1: 20;

    end;

    theorem :: FDIFF_6:14

    

     Th14: Z c= ( dom ( exp_R * f)) & (for x st x in Z holds (f . x) = ( - x)) implies ( exp_R * f) is_differentiable_on Z & for x st x in Z holds ((( exp_R * f) `| Z) . 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);

      

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

      proof

        let x;

        assume x in Z;

        

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

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

        hence thesis;

      end;

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

      then

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

      then

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

      

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

      proof

        let x;

        assume x in Z;

        then f is_differentiable_in x by A5, FDIFF_1: 9;

        hence thesis by TAYLOR_1: 19;

      end;

      then

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

      for x st x in Z holds ((( exp_R * f) `| Z) . x) = ( - ( exp_R ( - x)))

      proof

        let x;

        assume

         A8: x in Z;

        then f is_differentiable_in x by A5, FDIFF_1: 9;

        

        then ( diff (( exp_R * f),x)) = (( exp_R . (f . x)) * ( diff (f,x))) by TAYLOR_1: 19

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

        .= (( exp_R . (f . x)) * ( - 1)) by A4, A3, A8, FDIFF_1: 23

        .= (( exp_R . ( - x)) * ( - 1)) by A2, A8

        .= ( - ( exp_R . ( - x)))

        .= ( - ( exp_R ( - x))) by SIN_COS:def 23;

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

      end;

      hence thesis by A1, A6, FDIFF_1: 9;

    end;

    theorem :: FDIFF_6:15

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

    proof

      assume that

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

       A2: for x st x in Z holds (f1 . x) = (( - x) - 1) & (f2 . x) = ( - x);

      

       A3: Z c= (( dom f1) /\ ( dom ( exp_R * f2))) by A1, VALUED_1:def 4;

      then

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

      

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

      

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

      proof

        let x;

        assume x in Z;

        

        then (f1 . x) = (( - x) - 1) by A2

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

        hence thesis;

      end;

      then

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

      

       A8: for x st x in Z holds (f2 . x) = ( - x) by A2;

      then

       A9: ( exp_R * f2) is_differentiable_on Z by A5, Th14;

      for x st x in Z holds (((f1 (#) ( exp_R * f2)) `| Z) . x) = (x / ( exp_R x))

      proof

        let x;

        assume

         A10: x in Z;

        

        then

         A11: (( exp_R * f2) . x) = ( exp_R . (f2 . x)) by A5, FUNCT_1: 12

        .= ( exp_R . ( - x)) by A2, A10

        .= ( exp_R ( - x)) by SIN_COS:def 23;

        (((f1 (#) ( exp_R * f2)) `| Z) . x) = (((( exp_R * f2) . x) * ( diff (f1,x))) + ((f1 . x) * ( diff (( exp_R * f2),x)))) by A1, A7, A9, A10, FDIFF_1: 21

        .= ((( exp_R ( - x)) * ( diff (f1,x))) + ((( - x) - 1) * ( diff (( exp_R * f2),x)))) by A2, A10, A11

        .= ((( exp_R ( - x)) * ((f1 `| Z) . x)) + ((( - x) - 1) * ( diff (( exp_R * f2),x)))) by A7, A10, FDIFF_1:def 7

        .= ((( exp_R ( - x)) * ((f1 `| Z) . x)) + ((( - x) - 1) * ((( exp_R * f2) `| Z) . x))) by A9, A10, FDIFF_1:def 7

        .= ((( exp_R ( - x)) * ( - 1)) + ((( - x) - 1) * ((( exp_R * f2) `| Z) . x))) by A4, A6, A10, FDIFF_1: 23

        .= ((( exp_R ( - x)) * ( - 1)) + ((( - x) - 1) * ( - ( exp_R ( - x))))) by A8, A5, A10, Th14

        .= (x * ( exp_R ( - x)))

        .= (x * (1 / ( exp_R x))) by TAYLOR_1: 4

        .= (x / ( exp_R x)) by XCMPLX_1: 99;

        hence thesis;

      end;

      hence thesis by A1, A7, A9, FDIFF_1: 21;

    end;

    theorem :: FDIFF_6:16

    

     Th16: Z c= ( dom ( - ( exp_R * f))) & (for x st x in Z holds (f . x) = ( - (x * ( log ( number_e ,a))))) & a > 0 implies ( - ( exp_R * f)) is_differentiable_on Z & for x st x in Z holds ((( - ( exp_R * f)) `| Z) . x) = ((a #R ( - x)) * ( log ( number_e ,a)))

    proof

      assume that

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

       A2: for x st x in Z holds (f . x) = ( - (x * ( log ( number_e ,a)))) and

       A3: a > 0 ;

      

       A4: Z c= ( dom ( exp_R * 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

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

      

       A6: for x st x in Z holds (f . x) = ((( - ( log ( number_e ,a))) * x) + 0 )

      proof

        let x;

        assume x in Z;

        

        then (f . x) = ( - (( log ( number_e ,a)) * x)) by A2

        .= ((( - ( log ( number_e ,a))) * x) + 0 );

        hence thesis;

      end;

      then

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

      for x st x in Z holds ( exp_R * f) is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then f is_differentiable_in x by A7, FDIFF_1: 9;

        hence thesis by TAYLOR_1: 19;

      end;

      then

       A8: ( exp_R * f) is_differentiable_on Z by A4, FDIFF_1: 9;

      

       A9: for x st x in Z holds ((( - ( exp_R * f)) `| Z) . x) = ((a #R ( - x)) * ( log ( number_e ,a)))

      proof

        let x;

        assume

         A10: x in Z;

        then

         A11: f is_differentiable_in x by A7, FDIFF_1: 9;

        ((( - ( exp_R * f)) `| Z) . x) = (( - 1) * ( diff (( exp_R * f),x))) by A1, A8, A10, FDIFF_1: 20

        .= (( - 1) * (( exp_R . (f . x)) * ( diff (f,x)))) by A11, TAYLOR_1: 19

        .= (( - 1) * (( exp_R . (f . x)) * ((f `| Z) . x))) by A7, A10, FDIFF_1:def 7

        .= (( - 1) * (( exp_R . (f . x)) * ( - ( log ( number_e ,a))))) by A5, A6, A10, FDIFF_1: 23

        .= (( - 1) * (( exp_R . ( - (x * ( log ( number_e ,a))))) * ( - ( log ( number_e ,a))))) by A2, A10

        .= (( - 1) * ((a #R ( - x)) * ( - ( log ( number_e ,a))))) by A3, Th2

        .= ((a #R ( - x)) * ( log ( number_e ,a)));

        hence thesis;

      end;

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

      hence thesis by A8, A9, FDIFF_1: 20;

    end;

    theorem :: FDIFF_6:17

    Z c= ( dom ((1 / ( log ( number_e ,a))) (#) (( - ( exp_R * f1)) (#) f2))) & (for x st x in Z holds (f1 . x) = ( - (x * ( log ( number_e ,a)))) & (f2 . x) = (x + (1 / ( log ( number_e ,a))))) & a > 0 & a <> 1 implies ((1 / ( log ( number_e ,a))) (#) (( - ( exp_R * f1)) (#) f2)) is_differentiable_on Z & for x st x in Z holds ((((1 / ( log ( number_e ,a))) (#) (( - ( exp_R * f1)) (#) f2)) `| Z) . x) = (x / (a #R x))

    proof

      assume that

       A1: Z c= ( dom ((1 / ( log ( number_e ,a))) (#) (( - ( exp_R * f1)) (#) f2))) and

       A2: for x st x in Z holds (f1 . x) = ( - (x * ( log ( number_e ,a)))) & (f2 . x) = (x + (1 / ( log ( number_e ,a)))) and

       A3: a > 0 and

       A4: a <> 1;

      

       A5: for x st x in Z holds (f2 . x) = ((1 * x) + (1 / ( log ( number_e ,a)))) by A2;

      

       A6: Z c= ( dom (( - ( exp_R * f1)) (#) f2)) by A1, VALUED_1:def 5;

      then

       A7: Z c= (( dom ( - ( exp_R * f1))) /\ ( dom f2)) by VALUED_1:def 4;

      then

       A8: Z c= ( dom ( - ( exp_R * f1))) by XBOOLE_1: 18;

      

       A9: for x st x in Z holds (f1 . x) = ( - (x * ( log ( number_e ,a)))) by A2;

      then

       A10: ( - ( exp_R * f1)) is_differentiable_on Z by A3, A8, Th16;

      

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

      then

       A12: f2 is_differentiable_on Z by A5, FDIFF_1: 23;

      then

       A13: (( - ( exp_R * f1)) (#) f2) is_differentiable_on Z by A6, A10, FDIFF_1: 21;

      

       A14: ( log ( number_e ,a)) <> 0

      proof

        

         A15: number_e <> 1 by TAYLOR_1: 11;

        assume ( log ( number_e ,a)) = 0 ;

        then ( log ( number_e ,a)) = ( log ( number_e ,1)) by SIN_COS2: 13, TAYLOR_1: 13;

        

        then a = ( number_e to_power ( log ( number_e ,1))) by A3, A15, POWER:def 3, TAYLOR_1: 11

        .= 1 by A15, POWER:def 3, TAYLOR_1: 11;

        hence contradiction by A4;

      end;

      for x st x in Z holds ((((1 / ( log ( number_e ,a))) (#) (( - ( exp_R * f1)) (#) f2)) `| Z) . x) = (x / (a #R x))

      proof

        let x;

        assume

         A16: x in Z;

        then x in ( dom ( - ( exp_R * f1))) by A8;

        then

         A17: x in ( dom ( exp_R * f1)) by VALUED_1: 8;

        

         A18: (( - ( exp_R * f1)) . x) = ( - (( exp_R * f1) . x)) by VALUED_1: 8

        .= ( - ( exp_R . (f1 . x))) by A17, FUNCT_1: 12

        .= ( - ( exp_R . ( - (x * ( log ( number_e ,a)))))) by A2, A16

        .= ( - (a #R ( - x))) by A3, Th2;

        ((((1 / ( log ( number_e ,a))) (#) (( - ( exp_R * f1)) (#) f2)) `| Z) . x) = ((1 / ( log ( number_e ,a))) * ( diff ((( - ( exp_R * f1)) (#) f2),x))) by A1, A13, A16, FDIFF_1: 20

        .= ((1 / ( log ( number_e ,a))) * (((( - ( exp_R * f1)) (#) f2) `| Z) . x)) by A13, A16, FDIFF_1:def 7

        .= ((1 / ( log ( number_e ,a))) * (((f2 . x) * ( diff (( - ( exp_R * f1)),x))) + ((( - ( exp_R * f1)) . x) * ( diff (f2,x))))) by A6, A10, A12, A16, FDIFF_1: 21

        .= ((1 / ( log ( number_e ,a))) * (((f2 . x) * ((( - ( exp_R * f1)) `| Z) . x)) + ((( - ( exp_R * f1)) . x) * ( diff (f2,x))))) by A10, A16, FDIFF_1:def 7

        .= ((1 / ( log ( number_e ,a))) * (((f2 . x) * ((( - ( exp_R * f1)) `| Z) . x)) + ((( - ( exp_R * f1)) . x) * ((f2 `| Z) . x)))) by A12, A16, FDIFF_1:def 7

        .= ((1 / ( log ( number_e ,a))) * (((f2 . x) * ((a #R ( - x)) * ( log ( number_e ,a)))) + ((( - ( exp_R * f1)) . x) * ((f2 `| Z) . x)))) by A3, A9, A8, A16, Th16

        .= ((1 / ( log ( number_e ,a))) * (((f2 . x) * ((a #R ( - x)) * ( log ( number_e ,a)))) + ((( - ( exp_R * f1)) . x) * 1))) by A11, A5, A16, FDIFF_1: 23

        .= ((1 / ( log ( number_e ,a))) * ((((f2 . x) * ( log ( number_e ,a))) - 1) * (a #R ( - x)))) by A18

        .= ((1 / ( log ( number_e ,a))) * ((((x + (1 / ( log ( number_e ,a)))) * ( log ( number_e ,a))) - 1) * (a #R ( - x)))) by A2, A16

        .= (((1 / ( log ( number_e ,a))) * (((x * ( log ( number_e ,a))) + ((1 / ( log ( number_e ,a))) * ( log ( number_e ,a)))) - 1)) * (a #R ( - x)))

        .= (((1 / ( log ( number_e ,a))) * (((x * ( log ( number_e ,a))) + 1) - 1)) * (a #R ( - x))) by A14, XCMPLX_1: 106

        .= ((((1 / ( log ( number_e ,a))) * ( log ( number_e ,a))) * x) * (a #R ( - x)))

        .= ((1 * x) * (a #R ( - x))) by A14, XCMPLX_1: 106

        .= (x * (1 / (a #R x))) by A3, PREPOWER: 76

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

        hence thesis;

      end;

      hence thesis by A1, A13, FDIFF_1: 20;

    end;

    theorem :: FDIFF_6:18

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

    proof

      assume that

       A1: Z c= ( dom ((1 / (( log ( number_e ,a)) - 1)) (#) (( exp_R * f) / exp_R ))) and

       A2: for x st x in Z holds (f . x) = (x * ( log ( number_e ,a))) and

       A3: a > 0 and

       A4: a <> number_e ;

      Z c= ( dom (( exp_R * f) / exp_R )) by A1, VALUED_1:def 5;

      then Z c= (( dom ( exp_R * f)) /\ (( dom exp_R ) \ ( exp_R " { 0 }))) by RFUNCT_1:def 1;

      then

       A5: Z c= ( dom ( exp_R * f)) by XBOOLE_1: 18;

      then

       A6: ( exp_R * f) is_differentiable_on Z by A2, A3, Th11;

       exp_R is_differentiable_on Z & for x st x in Z holds ( exp_R . x) <> 0 by FDIFF_1: 26, SIN_COS: 54, TAYLOR_1: 16;

      then

       A7: (( exp_R * f) / exp_R ) is_differentiable_on Z by A6, FDIFF_2: 21;

      

       A8: (( log ( number_e ,a)) - 1) <> 0

      proof

        

         A9: number_e <> 1 by TAYLOR_1: 11;

        assume (( log ( number_e ,a)) - 1) = 0 ;

        then ( log ( number_e ,a)) = ( log ( number_e , number_e )) by A9, POWER: 52, TAYLOR_1: 11;

        

        then a = ( number_e to_power ( log ( number_e , number_e ))) by A3, A9, POWER:def 3, TAYLOR_1: 11

        .= number_e by A9, POWER:def 3, TAYLOR_1: 11;

        hence contradiction by A4;

      end;

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

      proof

        let x;

        

         A10: ( exp_R . x) <> 0 by SIN_COS: 54;

        assume

         A11: x in Z;

        

        then

         A12: (( exp_R * f) . x) = ( exp_R . (f . x)) by A5, FUNCT_1: 12

        .= ( exp_R . (x * ( log ( number_e ,a)))) by A2, A11

        .= (a #R x) by A3, Th1;

        

         A13: exp_R is_differentiable_in x & ( exp_R * f) is_differentiable_in x by A6, A11, FDIFF_1: 9, SIN_COS: 65;

        ((((1 / (( log ( number_e ,a)) - 1)) (#) (( exp_R * f) / exp_R )) `| Z) . x) = ((1 / (( log ( number_e ,a)) - 1)) * ( diff ((( exp_R * f) / exp_R ),x))) by A1, A7, A11, FDIFF_1: 20

        .= ((1 / (( log ( number_e ,a)) - 1)) * (((( diff (( exp_R * f),x)) * ( exp_R . x)) - (( diff ( exp_R ,x)) * (( exp_R * f) . x))) / (( exp_R . x) ^2 ))) by A13, A10, FDIFF_2: 14

        .= ((1 / (( log ( number_e ,a)) - 1)) * (((( diff (( exp_R * f),x)) * ( exp_R . x)) - (( exp_R . x) * (a #R x))) / (( exp_R . x) ^2 ))) by A12, SIN_COS: 65

        .= ((1 / (( log ( number_e ,a)) - 1)) * (((( diff (( exp_R * f),x)) - (a #R x)) * ( exp_R . x)) / (( exp_R . x) * ( exp_R . x))))

        .= ((1 / (( log ( number_e ,a)) - 1)) * ((( diff (( exp_R * f),x)) - (a #R x)) / ( exp_R . x))) by A10, XCMPLX_1: 91

        .= (((1 / (( log ( number_e ,a)) - 1)) * (( diff (( exp_R * f),x)) - (a #R x))) / ( exp_R . x)) by XCMPLX_1: 74

        .= (((1 / (( log ( number_e ,a)) - 1)) * (((( exp_R * f) `| Z) . x) - (a #R x))) / ( exp_R . x)) by A6, A11, FDIFF_1:def 7

        .= (((1 / (( log ( number_e ,a)) - 1)) * (((a #R x) * ( log ( number_e ,a))) - (a #R x))) / ( exp_R . x)) by A2, A3, A5, A11, Th11

        .= ((((1 / (( log ( number_e ,a)) - 1)) * (( log ( number_e ,a)) - 1)) * (a #R x)) / ( exp_R . x))

        .= ((1 * (a #R x)) / ( exp_R . x)) by A8, XCMPLX_1: 106

        .= ((a #R x) / ( exp_R . x));

        hence thesis;

      end;

      hence thesis by A1, A7, FDIFF_1: 20;

    end;

    theorem :: FDIFF_6:19

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

    proof

      assume that

       A1: Z c= ( dom ((1 / (1 - ( log ( number_e ,a)))) (#) ( exp_R / ( exp_R * f)))) and

       A2: for x st x in Z holds (f . x) = (x * ( log ( number_e ,a))) and

       A3: a > 0 and

       A4: a <> number_e ;

      Z c= ( dom ( exp_R / ( exp_R * f))) by A1, VALUED_1:def 5;

      then Z c= (( dom exp_R ) /\ (( dom ( exp_R * f)) \ (( exp_R * f) " { 0 }))) by RFUNCT_1:def 1;

      then

       A5: Z c= ( dom ( exp_R * f)) by XBOOLE_1: 1;

      then

       A6: ( exp_R * f) is_differentiable_on Z by A2, A3, Th11;

      

       A7: for x st x in Z holds (( exp_R * f) . x) <> 0

      proof

        let x;

        assume x in Z;

        then (( exp_R * f) . x) = ( exp_R . (f . x)) by A5, FUNCT_1: 12;

        hence thesis by SIN_COS: 54;

      end;

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

      then

       A8: ( exp_R / ( exp_R * f)) is_differentiable_on Z by A6, A7, FDIFF_2: 21;

      

       A9: (1 - ( log ( number_e ,a))) <> 0

      proof

        

         A10: number_e <> 1 by TAYLOR_1: 11;

        assume (1 - ( log ( number_e ,a))) = 0 ;

        then ( log ( number_e ,a)) = ( log ( number_e , number_e )) by A10, POWER: 52, TAYLOR_1: 11;

        

        then a = ( number_e to_power ( log ( number_e , number_e ))) by A3, A10, POWER:def 3, TAYLOR_1: 11

        .= number_e by A10, POWER:def 3, TAYLOR_1: 11;

        hence contradiction by A4;

      end;

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

      proof

        let x;

        

         A11: exp_R is_differentiable_in x by SIN_COS: 65;

        

         A12: (a #R x) > 0 by A3, PREPOWER: 81;

        assume

         A13: x in Z;

        

        then

         A14: (( exp_R * f) . x) = ( exp_R . (f . x)) by A5, FUNCT_1: 12

        .= ( exp_R . (x * ( log ( number_e ,a)))) by A2, A13

        .= (a #R x) by A3, Th1;

        

         A15: ( exp_R * f) is_differentiable_in x & (( exp_R * f) . x) <> 0 by A6, A7, A13, FDIFF_1: 9;

        ((((1 / (1 - ( log ( number_e ,a)))) (#) ( exp_R / ( exp_R * f))) `| Z) . x) = ((1 / (1 - ( log ( number_e ,a)))) * ( diff (( exp_R / ( exp_R * f)),x))) by A1, A8, A13, FDIFF_1: 20

        .= ((1 / (1 - ( log ( number_e ,a)))) * (((( diff ( exp_R ,x)) * (( exp_R * f) . x)) - (( diff (( exp_R * f),x)) * ( exp_R . x))) / ((( exp_R * f) . x) ^2 ))) by A11, A15, FDIFF_2: 14

        .= ((1 / (1 - ( log ( number_e ,a)))) * (((( exp_R . x) * (a #R x)) - (( diff (( exp_R * f),x)) * ( exp_R . x))) / ((a #R x) ^2 ))) by A14, SIN_COS: 65

        .= ((1 / (1 - ( log ( number_e ,a)))) * ((( exp_R . x) * ((a #R x) - ( diff (( exp_R * f),x)))) / ((a #R x) ^2 )))

        .= ((1 / (1 - ( log ( number_e ,a)))) * ((( exp_R . x) * ((a #R x) - ((( exp_R * f) `| Z) . x))) / ((a #R x) ^2 ))) by A6, A13, FDIFF_1:def 7

        .= ((1 / (1 - ( log ( number_e ,a)))) * ((( exp_R . x) * ((a #R x) - ((a #R x) * ( log ( number_e ,a))))) / ((a #R x) ^2 ))) by A2, A3, A5, A13, Th11

        .= (((1 / (1 - ( log ( number_e ,a)))) * (((1 - ( log ( number_e ,a))) * ( exp_R . x)) * (a #R x))) / ((a #R x) ^2 )) by XCMPLX_1: 74

        .= (((((1 / (1 - ( log ( number_e ,a)))) * (1 - ( log ( number_e ,a)))) * ( exp_R . x)) * (a #R x)) / ((a #R x) ^2 ))

        .= (((1 * ( exp_R . x)) * (a #R x)) / ((a #R x) ^2 )) by A9, XCMPLX_1: 106

        .= (( exp_R . x) / (a #R x)) by A12, XCMPLX_1: 91;

        hence thesis;

      end;

      hence thesis by A1, A8, FDIFF_1: 20;

    end;

    theorem :: FDIFF_6:20

    Z c= ( dom ( ln * ( exp_R + f))) & (for x st x in Z holds (f . x) = 1) implies ( ln * ( exp_R + f)) is_differentiable_on Z & for x st x in Z holds ((( ln * ( exp_R + f)) `| Z) . x) = (( exp_R . x) / (( exp_R . x) + 1))

    proof

      assume that

       A1: Z c= ( dom ( ln * ( 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 + f)) by A1, FUNCT_1: 11;

      then

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

      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) `| Z) . x) = ( exp_R . x)

      proof

        let x;

        assume

         A10: 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, A10, FDIFF_1:def 7

        .= (( exp_R . x) + 0 ) by A5, A3, A10, FDIFF_1: 23

        .= ( exp_R . x);

      end;

      

       A11: for x st x in Z holds (( exp_R + f) . x) > 0

      proof

        let x;

        assume

         A12: 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, A12;

        hence thesis by SIN_COS: 54, XREAL_1: 34;

      end;

      

       A13: for x st x in Z holds ( ln * ( exp_R + f)) is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then ( exp_R + f) is_differentiable_in x & (( exp_R + f) . x) > 0 by A8, A11, FDIFF_1: 9;

        hence thesis by TAYLOR_1: 20;

      end;

      then

       A14: ( ln * ( exp_R + f)) is_differentiable_on Z by A1, FDIFF_1: 9;

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

      proof

        let x;

        assume

         A15: x in Z;

        

        then

         A16: (( exp_R + f) . x) = (( exp_R . x) + (f . x)) by A4, VALUED_1:def 1

        .= (( exp_R . x) + 1) by A2, A15;

        ( exp_R + f) is_differentiable_in x & (( exp_R + f) . x) > 0 by A8, A11, A15, FDIFF_1: 9;

        

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

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

        .= (( exp_R . x) / (( exp_R . x) + 1)) by A9, A15, A16;

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

      end;

      hence thesis by A1, A13, FDIFF_1: 9;

    end;

    theorem :: FDIFF_6:21

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

    proof

      assume that

       A1: Z c= ( dom ( ln * ( exp_R - f))) 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)) by A1, FUNCT_1: 11;

      then

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

      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;

      

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

      proof

        let x;

        assume

         A10: 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, A10, FDIFF_1:def 7

        .= (( exp_R . x) - 0 ) by A5, A3, A10, FDIFF_1: 23

        .= ( exp_R . x);

      end;

      

       A11: for x st x in Z holds ( ln * ( exp_R - f)) is_differentiable_in x

      proof

        let x;

        assume x in Z;

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

        hence thesis by TAYLOR_1: 20;

      end;

      then

       A12: ( ln * ( exp_R - f)) is_differentiable_on Z by A1, FDIFF_1: 9;

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

      proof

        let x;

        assume

         A13: x in Z;

        

        then

         A14: (( exp_R - f) . x) = (( exp_R . x) - (f . x)) by A4, VALUED_1: 13

        .= (( exp_R . x) - 1) by A2, A13;

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

        

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

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

        .= (( exp_R . x) / (( exp_R . x) - 1)) by A9, A13, A14;

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

      end;

      hence thesis by A1, A11, FDIFF_1: 9;

    end;

    theorem :: FDIFF_6:22

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

    proof

      assume that

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

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

      

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

      

       A4: Z c= ( dom ( ln * (f - exp_R ))) by A1, VALUED_1: 8;

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

      then

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

      then Z c= (( dom exp_R ) /\ ( dom f)) by VALUED_1: 12;

      then

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

      then

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

      

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

      then

       A9: (f - exp_R ) is_differentiable_on Z by A5, A7, FDIFF_1: 19;

      for x st x in Z holds ( ln * (f - exp_R )) is_differentiable_in x

      proof

        let x;

        assume x in Z;

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

        hence thesis by TAYLOR_1: 20;

      end;

      then

       A10: ( ln * (f - exp_R )) is_differentiable_on Z by A4, FDIFF_1: 9;

      

       A11: for x st x in Z holds (((f - exp_R ) `| Z) . x) = ( - ( exp_R . x))

      proof

        let x;

        assume

         A12: x in Z;

        

        hence (((f - exp_R ) `| Z) . x) = (( diff (f,x)) - ( diff ( exp_R ,x))) by A5, A7, A8, FDIFF_1: 19

        .= (( diff (f,x)) - ( exp_R . x)) by SIN_COS: 65

        .= (((f `| Z) . x) - ( exp_R . x)) by A7, A12, FDIFF_1:def 7

        .= ( 0 - ( exp_R . x)) by A6, A3, A12, FDIFF_1: 23

        .= ( - ( exp_R . x));

      end;

      

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

      proof

        let x;

        assume

         A14: x in Z;

        

        then

         A15: ((f - exp_R ) . x) = ((f . x) - ( exp_R . x)) by A5, VALUED_1: 13

        .= (1 - ( exp_R . x)) by A2, A14;

        

         A16: (f - exp_R ) is_differentiable_in x & ((f - exp_R ) . x) > 0 by A2, A9, A14, FDIFF_1: 9;

        (((( - 1) (#) ( ln * (f - exp_R ))) `| Z) . x) = (( - 1) * ( diff (( ln * (f - exp_R )),x))) by A1, A10, A14, FDIFF_1: 20

        .= (( - 1) * (( diff ((f - exp_R ),x)) / ((f - exp_R ) . x))) by A16, TAYLOR_1: 20

        .= (( - 1) * ((((f - exp_R ) `| Z) . x) / ((f - exp_R ) . x))) by A9, A14, FDIFF_1:def 7

        .= (( - 1) * (( - ( exp_R . x)) / (1 - ( exp_R . x)))) by A11, A14, A15

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

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

        hence thesis;

      end;

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

      hence thesis by A10, A13, FDIFF_1: 20;

    end;

    theorem :: FDIFF_6:23

    

     Th23: Z c= ( dom ((( #Z 2) * exp_R ) + f)) & (for x st x in Z holds (f . x) = 1) implies ((( #Z 2) * exp_R ) + f) is_differentiable_on Z & for x st x in Z holds ((((( #Z 2) * exp_R ) + f) `| Z) . x) = (2 * ( exp_R (2 * x)))

    proof

      assume that

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

       A2: for x st x in Z holds (f . x) = 1;

      

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

      then

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

       A5:

      now

        let x;

        assume x in Z;

         exp_R is_differentiable_in x by SIN_COS: 65;

        hence (( #Z 2) * exp_R ) is_differentiable_in x by TAYLOR_1: 3;

      end;

      

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

      then

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

      Z c= ( dom (( #Z 2) * exp_R )) by A3, XBOOLE_1: 18;

      then

       A8: (( #Z 2) * exp_R ) is_differentiable_on Z by A5, FDIFF_1: 9;

      for x st x in Z holds ((((( #Z 2) * exp_R ) + f) `| Z) . x) = (2 * ( exp_R (2 * x)))

      proof

        let x;

        

         A9: exp_R is_differentiable_in x by SIN_COS: 65;

        assume

         A10: x in Z;

        

        then ((((( #Z 2) * exp_R ) + f) `| Z) . x) = (( diff ((( #Z 2) * exp_R ),x)) + ( diff (f,x))) by A1, A7, A8, FDIFF_1: 18

        .= (((2 * (( exp_R . x) #Z (2 - 1))) * ( diff ( exp_R ,x))) + ( diff (f,x))) by A9, TAYLOR_1: 3

        .= (((2 * (( exp_R . x) #Z (2 - 1))) * ( exp_R . x)) + ( diff (f,x))) by SIN_COS: 65

        .= (((2 * ( exp_R . x)) * ( exp_R . x)) + ( diff (f,x))) by PREPOWER: 35

        .= ((2 * (( exp_R . x) * ( exp_R . x))) + ( diff (f,x)))

        .= ((2 * (( exp_R x) * ( exp_R . x))) + ( diff (f,x))) by SIN_COS:def 23

        .= ((2 * (( exp_R x) * ( exp_R x))) + ( diff (f,x))) by SIN_COS:def 23

        .= ((2 * ( exp_R (x + x))) + ( diff (f,x))) by SIN_COS: 50

        .= ((2 * ( exp_R (2 * x))) + ((f `| Z) . x)) by A7, A10, FDIFF_1:def 7

        .= ((2 * ( exp_R (2 * x))) + 0 ) by A4, A6, A10, FDIFF_1: 23

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

        hence thesis;

      end;

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

    end;

    theorem :: FDIFF_6:24

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

    proof

      assume that

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

       A2: f = ((( #Z 2) * exp_R ) + f1) and

       A3: for x st x in Z holds (f1 . x) = 1;

      

       A4: Z c= ( dom ( ln * 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

       A5: Z c= ( dom ((( #Z 2) * exp_R ) + f1)) by A2, TARSKI:def 3;

      then

       A6: ((( #Z 2) * exp_R ) + f1) is_differentiable_on Z by A3, Th23;

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

      then

       A7: Z c= ( dom (( #Z 2) * exp_R )) by XBOOLE_1: 18;

      

       A8: for x st x in Z holds (f . x) > 0

      proof

        let x;

        

         A9: (( exp_R . x) #Z 2) > 0 by PREPOWER: 39, SIN_COS: 54;

        assume

         A10: x in Z;

        

        then (((( #Z 2) * exp_R ) + f1) . x) = (((( #Z 2) * exp_R ) . x) + (f1 . x)) by A5, VALUED_1:def 1

        .= ((( #Z 2) . ( exp_R . x)) + (f1 . x)) by A7, A10, FUNCT_1: 12

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

        .= ((( exp_R . x) #Z 2) + 1) by A3, A10;

        hence thesis by A2, A9;

      end;

      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, A8, FDIFF_1: 9;

        hence thesis by TAYLOR_1: 20;

      end;

      then

       A11: ( ln * f) is_differentiable_on Z by A4, FDIFF_1: 9;

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

      proof

        let x;

        

         A12: ( exp_R x) > 0 by SIN_COS: 55;

        assume

         A13: x in Z;

        then

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

        

         A15: (((( #Z 2) * exp_R ) + f1) . x) = (((( #Z 2) * exp_R ) . x) + (f1 . x)) by A5, A13, VALUED_1:def 1

        .= ((( #Z 2) . ( exp_R . x)) + (f1 . x)) by A7, A13, FUNCT_1: 12

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

        .= ((( exp_R . x) #Z 2) + 1) by A3, A13

        .= ((( exp_R x) #Z (1 + 1)) + 1) by SIN_COS:def 23

        .= (((( exp_R x) #Z 1) * (( exp_R x) #Z 1)) + 1) by A12, PREPOWER: 44

        .= ((( exp_R x) * (( exp_R x) #Z 1)) + 1) by PREPOWER: 35

        .= ((( exp_R x) * ( exp_R x)) + 1) by PREPOWER: 35;

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

        .= ((1 / 2) * (( diff (f,x)) / (f . x))) by A14, TAYLOR_1: 20

        .= ((1 / 2) * (((((( #Z 2) * exp_R ) + f1) `| Z) . x) / (((( #Z 2) * exp_R ) + f1) . x))) by A2, A6, A13, FDIFF_1:def 7

        .= ((1 / 2) * ((2 * ( exp_R (2 * x))) / ((( exp_R x) * ( exp_R x)) + 1))) by A3, A5, A13, A15, Th23

        .= (((1 / 2) * (2 * ( exp_R (2 * x)))) / ((( exp_R x) * ( exp_R x)) + 1)) by XCMPLX_1: 74

        .= ((( exp_R (x + x)) / ( exp_R x)) / (((( exp_R x) * ( exp_R x)) + 1) / ( exp_R x))) by A12, XCMPLX_1: 55

        .= (((( exp_R x) * ( exp_R x)) / ( exp_R x)) / (((( exp_R x) * ( exp_R x)) + 1) / ( exp_R x))) by SIN_COS: 50

        .= (((( exp_R x) * ( exp_R x)) / ( exp_R x)) / (((( exp_R x) * ( exp_R x)) / ( exp_R x)) + (1 / ( exp_R x)))) by XCMPLX_1: 62

        .= (( exp_R x) / (((( exp_R x) * ( exp_R x)) / ( exp_R x)) + (1 / ( exp_R x)))) by A12, XCMPLX_1: 89

        .= (( exp_R x) / (( exp_R x) + (1 / ( exp_R x)))) by A12, XCMPLX_1: 89

        .= (( exp_R x) / (( exp_R x) + ( exp_R ( - x)))) by TAYLOR_1: 4;

        hence thesis;

      end;

      hence thesis by A1, A11, FDIFF_1: 20;

    end;

    theorem :: FDIFF_6:25

    

     Th25: Z c= ( dom ((( #Z 2) * exp_R ) - f)) & (for x st x in Z holds (f . x) = 1) implies ((( #Z 2) * exp_R ) - f) is_differentiable_on Z & for x st x in Z holds ((((( #Z 2) * exp_R ) - f) `| Z) . x) = (2 * ( exp_R (2 * x)))

    proof

      assume that

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

       A2: for x st x in Z holds (f . x) = 1;

      

       A3: Z c= (( dom (( #Z 2) * exp_R )) /\ ( dom f)) by A1, VALUED_1: 12;

      then

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

       A5:

      now

        let x;

        assume x in Z;

         exp_R is_differentiable_in x by SIN_COS: 65;

        hence (( #Z 2) * exp_R ) is_differentiable_in x by TAYLOR_1: 3;

      end;

      

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

      then

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

      Z c= ( dom (( #Z 2) * exp_R )) by A3, XBOOLE_1: 18;

      then

       A8: (( #Z 2) * exp_R ) is_differentiable_on Z by A5, FDIFF_1: 9;

      for x st x in Z holds ((((( #Z 2) * exp_R ) - f) `| Z) . x) = (2 * ( exp_R (2 * x)))

      proof

        let x;

        

         A9: exp_R is_differentiable_in x by SIN_COS: 65;

        assume

         A10: x in Z;

        

        then ((((( #Z 2) * exp_R ) - f) `| Z) . x) = (( diff ((( #Z 2) * exp_R ),x)) - ( diff (f,x))) by A1, A7, A8, FDIFF_1: 19

        .= (((2 * (( exp_R . x) #Z (2 - 1))) * ( diff ( exp_R ,x))) - ( diff (f,x))) by A9, TAYLOR_1: 3

        .= (((2 * (( exp_R . x) #Z 1)) * ( exp_R . x)) - ( diff (f,x))) by SIN_COS: 65

        .= (((2 * ( exp_R . x)) * ( exp_R . x)) - ( diff (f,x))) by PREPOWER: 35

        .= ((2 * (( exp_R . x) * ( exp_R . x))) - ( diff (f,x)))

        .= ((2 * (( exp_R x) * ( exp_R . x))) - ( diff (f,x))) by SIN_COS:def 23

        .= ((2 * (( exp_R x) * ( exp_R x))) - ( diff (f,x))) by SIN_COS:def 23

        .= ((2 * ( exp_R (x + x))) - ( diff (f,x))) by SIN_COS: 50

        .= ((2 * ( exp_R (2 * x))) - ((f `| Z) . x)) by A7, A10, FDIFF_1:def 7

        .= ((2 * ( exp_R (2 * x))) - 0 ) by A4, A6, A10, FDIFF_1: 23

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

        hence thesis;

      end;

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

    end;

    theorem :: FDIFF_6:26

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

    proof

      assume that

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

       A2: f = ((( #Z 2) * exp_R ) - f1) and

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

      

       A4: Z c= ( dom ( ln * 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

       A5: Z c= ( dom ((( #Z 2) * exp_R ) - f1)) by A2, TARSKI:def 3;

      

       A6: for x st x in Z holds (f1 . x) = 1 by A3;

      then

       A7: ((( #Z 2) * exp_R ) - f1) is_differentiable_on Z by A5, Th25;

      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, A3, A7, FDIFF_1: 9;

        hence thesis by TAYLOR_1: 20;

      end;

      then

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

      Z c= (( dom (( #Z 2) * exp_R )) /\ ( dom f1)) by A5, VALUED_1: 12;

      then

       A9: Z c= ( dom (( #Z 2) * exp_R )) by XBOOLE_1: 18;

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

      proof

        let x;

        

         A10: ( exp_R x) > 0 by SIN_COS: 55;

        assume

         A11: x in Z;

        then

         A12: f is_differentiable_in x & (f . x) > 0 by A2, A3, A7, FDIFF_1: 9;

        

         A13: (((( #Z 2) * exp_R ) - f1) . x) = (((( #Z 2) * exp_R ) . x) - (f1 . x)) by A5, A11, VALUED_1: 13

        .= ((( #Z 2) . ( exp_R . x)) - (f1 . x)) by A9, A11, FUNCT_1: 12

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

        .= ((( exp_R . x) #Z 2) - 1) by A3, A11

        .= ((( exp_R x) #Z (1 + 1)) - 1) by SIN_COS:def 23

        .= (((( exp_R x) #Z 1) * (( exp_R x) #Z 1)) - 1) by A10, PREPOWER: 44

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

        .= ((( exp_R x) * ( exp_R x)) - 1) by PREPOWER: 35;

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

        .= ((1 / 2) * (( diff (f,x)) / (f . x))) by A12, TAYLOR_1: 20

        .= ((1 / 2) * (((((( #Z 2) * exp_R ) - f1) `| Z) . x) / (((( #Z 2) * exp_R ) - f1) . x))) by A2, A7, A11, FDIFF_1:def 7

        .= ((1 / 2) * ((2 * ( exp_R (2 * x))) / ((( exp_R x) * ( exp_R x)) - 1))) by A6, A5, A11, A13, Th25

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

        .= ((( exp_R (x + x)) / ( exp_R x)) / (((( exp_R x) * ( exp_R x)) - 1) / ( exp_R x))) by A10, XCMPLX_1: 55

        .= (((( exp_R x) * ( exp_R x)) / ( exp_R x)) / (((( exp_R x) * ( exp_R x)) - 1) / ( exp_R x))) by SIN_COS: 50

        .= (((( exp_R x) * ( exp_R x)) / ( exp_R x)) / (((( exp_R x) * ( exp_R x)) / ( exp_R x)) - (1 / ( exp_R x)))) by XCMPLX_1: 120

        .= (( exp_R x) / (((( exp_R x) * ( exp_R x)) / ( exp_R x)) - (1 / ( exp_R x)))) by A10, XCMPLX_1: 89

        .= (( exp_R x) / (( exp_R x) - (1 / ( exp_R x)))) by A10, XCMPLX_1: 89

        .= (( exp_R x) / (( exp_R x) - ( exp_R ( - x)))) by TAYLOR_1: 4;

        hence thesis;

      end;

      hence thesis by A1, A8, FDIFF_1: 20;

    end;

    theorem :: FDIFF_6:27

    

     Th27: Z c= ( dom (( #Z 2) * ( exp_R - f))) & (for x st x in Z holds (f . x) = 1) implies (( #Z 2) * ( exp_R - f)) is_differentiable_on Z & for x st x in Z holds (((( #Z 2) * ( exp_R - f)) `| Z) . x) = ((2 * ( exp_R . x)) * (( exp_R . x) - 1))

    proof

      assume that

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

       A2: for x st x in Z holds (f . x) = 1;

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

      then

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

      then Z c= (( dom exp_R ) /\ ( dom f)) by VALUED_1: 12;

      then

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

      

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

      then

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

      

       A7: for x st x in Z holds (( #Z 2) * ( exp_R - f)) is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then

         A8: f is_differentiable_in x by A6, FDIFF_1: 9;

         exp_R is_differentiable_in x by SIN_COS: 65;

        then ( exp_R - f) is_differentiable_in x by A8, FDIFF_1: 14;

        hence thesis by TAYLOR_1: 3;

      end;

      then

       A9: (( #Z 2) * ( exp_R - f)) is_differentiable_on Z by A1, FDIFF_1: 9;

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

      proof

        let x;

        

         A10: exp_R is_differentiable_in x by SIN_COS: 65;

        assume

         A11: x in Z;

        

        then

         A12: (( exp_R - f) . x) = (( exp_R . x) - (f . x)) by A3, VALUED_1: 13

        .= (( exp_R . x) - 1) by A2, A11;

        

         A13: f is_differentiable_in x by A6, A11, FDIFF_1: 9;

        

        then

         A14: ( diff (( exp_R - f),x)) = (( diff ( exp_R ,x)) - ( diff (f,x))) by A10, FDIFF_1: 14

        .= (( diff ( exp_R ,x)) - ((f `| Z) . x)) by A6, A11, FDIFF_1:def 7

        .= (( exp_R . x) - ((f `| Z) . x)) by SIN_COS: 65

        .= (( exp_R . x) - 0 ) by A4, A5, A11, FDIFF_1: 23

        .= ( exp_R . x);

        

         A15: ( exp_R - f) is_differentiable_in x by A13, A10, FDIFF_1: 14;

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

        .= ((2 * ((( exp_R - f) . x) #Z (2 - 1))) * ( diff (( exp_R - f),x))) by A15, TAYLOR_1: 3

        .= ((2 * (( exp_R . x) - 1)) * ( exp_R . x)) by A14, A12, PREPOWER: 35

        .= ((2 * ( exp_R . x)) * (( exp_R . x) - 1));

        hence thesis;

      end;

      hence thesis by A1, A7, FDIFF_1: 9;

    end;

    theorem :: FDIFF_6:28

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

    proof

      assume that

       A1: Z c= ( dom f) and

       A2: f = ( ln * ((( #Z 2) * ( exp_R - f1)) / exp_R )) and

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

      for y be object st y in Z holds y in ( dom ((( #Z 2) * ( exp_R - f1)) / exp_R )) by A1, A2, FUNCT_1: 11;

      then

       A4: Z c= ( dom ((( #Z 2) * ( exp_R - f1)) / exp_R )) by TARSKI:def 3;

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

      then

       A5: Z c= ( dom (( #Z 2) * ( exp_R - f1))) by XBOOLE_1: 18;

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

      then

       A6: Z c= ( dom ( exp_R - f1)) by TARSKI:def 3;

      

       A7: for x st x in Z holds (((( #Z 2) * ( exp_R - f1)) / exp_R ) . x) > 0

      proof

        let x;

        

         A8: ( exp_R . x) > 0 by SIN_COS: 54;

        assume

         A9: x in Z;

        then

         A10: ((( exp_R - f1) . x) #Z 2) > 0 by A3, PREPOWER: 39;

        (((( #Z 2) * ( exp_R - f1)) / exp_R ) . x) = (((( #Z 2) * ( exp_R - f1)) . x) * (( exp_R . x) " )) by A4, A9, RFUNCT_1:def 1

        .= (((( #Z 2) * ( exp_R - f1)) . x) * (1 / ( exp_R . x))) by XCMPLX_1: 215

        .= (((( #Z 2) * ( exp_R - f1)) . x) / ( exp_R . x)) by XCMPLX_1: 99

        .= ((( #Z 2) . (( exp_R - f1) . x)) / ( exp_R . x)) by A5, A9, FUNCT_1: 12

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

        hence thesis by A10, A8, XREAL_1: 139;

      end;

      

       A11: for x st x in Z holds (f1 . x) = 1 by A3;

      then

       A12: (( #Z 2) * ( exp_R - f1)) is_differentiable_on Z by A5, Th27;

       exp_R is_differentiable_on Z & for x st x in Z holds ( exp_R . x) <> 0 by FDIFF_1: 26, SIN_COS: 54, TAYLOR_1: 16;

      then

       A13: ((( #Z 2) * ( exp_R - f1)) / exp_R ) is_differentiable_on Z by A12, FDIFF_2: 21;

      

       A14: for x st x in Z holds ( ln * ((( #Z 2) * ( exp_R - f1)) / exp_R )) is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then ((( #Z 2) * ( exp_R - f1)) / exp_R ) is_differentiable_in x & (((( #Z 2) * ( exp_R - f1)) / exp_R ) . x) > 0 by A13, A7, FDIFF_1: 9;

        hence thesis by TAYLOR_1: 20;

      end;

      then

       A15: f is_differentiable_on Z by A1, A2, FDIFF_1: 9;

      for x st x in Z holds ((f `| Z) . x) = ((( exp_R . x) + 1) / (( exp_R . x) - 1))

      proof

        let x;

        

         A16: ( exp_R . x) > 0 by SIN_COS: 54;

        

         A17: exp_R is_differentiable_in x by SIN_COS: 65;

        assume

         A18: x in Z;

        

        then

         A19: (( exp_R - f1) . x) = (( exp_R . x) - (f1 . x)) by A6, VALUED_1: 13

        .= (( exp_R . x) - 1) by A3, A18;

        then

         A20: (( exp_R . x) - 1) > 0 by A3, A18;

        

         A21: (((( #Z 2) * ( exp_R - f1)) / exp_R ) . x) = (((( #Z 2) * ( exp_R - f1)) . x) * (( exp_R . x) " )) by A4, A18, RFUNCT_1:def 1

        .= (((( #Z 2) * ( exp_R - f1)) . x) * (1 / ( exp_R . x))) by XCMPLX_1: 215

        .= (((( #Z 2) * ( exp_R - f1)) . x) / ( exp_R . x)) by XCMPLX_1: 99

        .= ((( #Z 2) . (( exp_R - f1) . x)) / ( exp_R . x)) by A5, A18, FUNCT_1: 12

        .= (((( exp_R . x) - 1) #Z (1 + 1)) / ( exp_R . x)) by A19, TAYLOR_1:def 1

        .= ((((( exp_R . x) - 1) #Z 1) * ((( exp_R . x) - 1) #Z 1)) / ( exp_R . x)) by A20, PREPOWER: 44

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

        .= (((( exp_R . x) - 1) * (( exp_R . x) - 1)) / ( exp_R . x)) by PREPOWER: 35;

        

         A22: ((( #Z 2) * ( exp_R - f1)) / exp_R ) is_differentiable_in x & (((( #Z 2) * ( exp_R - f1)) / exp_R ) . x) > 0 by A13, A7, A18, FDIFF_1: 9;

        (( #Z 2) * ( exp_R - f1)) is_differentiable_in x by A12, A18, FDIFF_1: 9;

        

        then

         A23: ( diff (((( #Z 2) * ( exp_R - f1)) / exp_R ),x)) = (((( diff ((( #Z 2) * ( exp_R - f1)),x)) * ( exp_R . x)) - (( diff ( exp_R ,x)) * ((( #Z 2) * ( exp_R - f1)) . x))) / (( exp_R . x) ^2 )) by A16, A17, FDIFF_2: 14

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

        .= (((((2 * ( exp_R . x)) * (( exp_R . x) - 1)) * ( exp_R . x)) - (( diff ( exp_R ,x)) * ((( #Z 2) * ( exp_R - f1)) . x))) / (( exp_R . x) ^2 )) by A11, A5, A18, Th27

        .= (((((2 * ( exp_R . x)) * (( exp_R . x) - 1)) * ( exp_R . x)) - (( exp_R . x) * ((( #Z 2) * ( exp_R - f1)) . x))) / (( exp_R . x) ^2 )) by SIN_COS: 65

        .= (((((2 * ( exp_R . x)) * (( exp_R . x) - 1)) - ((( #Z 2) * ( exp_R - f1)) . x)) * ( exp_R . x)) / (( exp_R . x) * ( exp_R . x)))

        .= ((((2 * ( exp_R . x)) * (( exp_R . x) - 1)) - ((( #Z 2) * ( exp_R - f1)) . x)) / ( exp_R . x)) by A16, XCMPLX_1: 91

        .= ((((2 * ( exp_R . x)) * (( exp_R . x) - 1)) - (( #Z 2) . (( exp_R - f1) . x))) / ( exp_R . x)) by A5, A18, FUNCT_1: 12

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

        .= ((((2 * ( exp_R . x)) * (( exp_R . x) - 1)) - ((( exp_R . x) - (f1 . x)) #Z 2)) / ( exp_R . x)) by A6, A18, VALUED_1: 13

        .= ((((2 * ( exp_R . x)) * (( exp_R . x) - 1)) - ((( exp_R . x) - 1) #Z (1 + 1))) / ( exp_R . x)) by A3, A18

        .= ((((2 * ( exp_R . x)) * (( exp_R . x) - 1)) - (((( exp_R . x) - 1) #Z 1) * ((( exp_R . x) - 1) #Z 1))) / ( exp_R . x)) by A20, PREPOWER: 44

        .= ((((2 * ( exp_R . x)) * (( exp_R . x) - 1)) - ((( exp_R . x) - 1) * ((( exp_R . x) - 1) #Z 1))) / ( exp_R . x)) by PREPOWER: 35

        .= ((((2 * ( exp_R . x)) * (( exp_R . x) - 1)) - ((( exp_R . x) - 1) * (( exp_R . x) - 1))) / ( exp_R . x)) by PREPOWER: 35

        .= (((( exp_R . x) + 1) * (( exp_R . x) - 1)) / ( exp_R . x));

        ((f `| Z) . x) = ( diff (( ln * ((( #Z 2) * ( exp_R - f1)) / exp_R )),x)) by A2, A15, A18, FDIFF_1:def 7

        .= ((((( exp_R . x) + 1) * (( exp_R . x) - 1)) / ( exp_R . x)) / (((( exp_R . x) - 1) * (( exp_R . x) - 1)) / ( exp_R . x))) by A22, A23, A21, TAYLOR_1: 20

        .= (((( exp_R . x) + 1) * (( exp_R . x) - 1)) / ((( exp_R . x) - 1) * (( exp_R . x) - 1))) by A16, XCMPLX_1: 55

        .= ((( exp_R . x) + 1) / (( exp_R . x) - 1)) by A20, XCMPLX_1: 91;

        hence thesis;

      end;

      hence thesis by A1, A2, A14, FDIFF_1: 9;

    end;

    theorem :: FDIFF_6:29

    

     Th29: Z c= ( dom (( #Z 2) * ( exp_R + f))) & (for x st x in Z holds (f . x) = 1) implies (( #Z 2) * ( exp_R + f)) is_differentiable_on Z & for x st x in Z holds (((( #Z 2) * ( exp_R + f)) `| Z) . x) = ((2 * ( exp_R . x)) * (( exp_R . x) + 1))

    proof

      assume that

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

       A2: for x st x in Z holds (f . x) = 1;

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

      then

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

      then Z c= (( dom exp_R ) /\ ( dom f)) by VALUED_1:def 1;

      then

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

      

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

      then

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

      

       A7: for x st x in Z holds (( #Z 2) * ( exp_R + f)) is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then

         A8: f is_differentiable_in x by A6, FDIFF_1: 9;

         exp_R is_differentiable_in x by SIN_COS: 65;

        then ( exp_R + f) is_differentiable_in x by A8, FDIFF_1: 13;

        hence thesis by TAYLOR_1: 3;

      end;

      then

       A9: (( #Z 2) * ( exp_R + f)) is_differentiable_on Z by A1, FDIFF_1: 9;

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

      proof

        let x;

        

         A10: exp_R is_differentiable_in x by SIN_COS: 65;

        assume

         A11: x in Z;

        

        then

         A12: (( exp_R + f) . x) = (( exp_R . x) + (f . x)) by A3, VALUED_1:def 1

        .= (( exp_R . x) + 1) by A2, A11;

        

         A13: f is_differentiable_in x by A6, A11, FDIFF_1: 9;

        

        then

         A14: ( diff (( exp_R + f),x)) = (( diff ( exp_R ,x)) + ( diff (f,x))) by A10, FDIFF_1: 13

        .= (( diff ( exp_R ,x)) + ((f `| Z) . x)) by A6, A11, FDIFF_1:def 7

        .= (( exp_R . x) + ((f `| Z) . x)) by SIN_COS: 65

        .= (( exp_R . x) + 0 ) by A4, A5, A11, FDIFF_1: 23

        .= ( exp_R . x);

        

         A15: ( exp_R + f) is_differentiable_in x by A13, A10, FDIFF_1: 13;

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

        .= ((2 * ((( exp_R + f) . x) #Z (2 - 1))) * ( diff (( exp_R + f),x))) by A15, TAYLOR_1: 3

        .= ((2 * (( exp_R . x) + 1)) * ( exp_R . x)) by A14, A12, PREPOWER: 35

        .= ((2 * ( exp_R . x)) * (( exp_R . x) + 1));

        hence thesis;

      end;

      hence thesis by A1, A7, FDIFF_1: 9;

    end;

    theorem :: FDIFF_6:30

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

    proof

      assume that

       A1: Z c= ( dom f) and

       A2: f = ( ln * ((( #Z 2) * ( exp_R + f1)) / exp_R )) and

       A3: for x st x in Z holds (f1 . x) = 1;

      for y be object st y in Z holds y in ( dom ((( #Z 2) * ( exp_R + f1)) / exp_R )) by A1, A2, FUNCT_1: 11;

      then

       A4: Z c= ( dom ((( #Z 2) * ( exp_R + f1)) / exp_R )) by TARSKI:def 3;

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

      then

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

      then

       A6: (( #Z 2) * ( exp_R + f1)) is_differentiable_on Z by A3, Th29;

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

      then

       A7: Z c= ( dom ( exp_R + f1)) by TARSKI:def 3;

      

       A8: for x st x in Z holds (((( #Z 2) * ( exp_R + f1)) / exp_R ) . x) > 0

      proof

        let x;

        

         A9: ( exp_R . x) > 0 by SIN_COS: 54;

        assume

         A10: x in Z;

        

        then (( exp_R + f1) . x) = (( exp_R . x) + (f1 . x)) by A7, VALUED_1:def 1

        .= (( exp_R . x) + 1) by A3, A10;

        then (( exp_R + f1) . x) > 0 by SIN_COS: 54, XREAL_1: 34;

        then

         A11: ((( exp_R + f1) . x) #Z 2) > 0 by PREPOWER: 39;

        (((( #Z 2) * ( exp_R + f1)) / exp_R ) . x) = (((( #Z 2) * ( exp_R + f1)) . x) * (( exp_R . x) " )) by A4, A10, RFUNCT_1:def 1

        .= (((( #Z 2) * ( exp_R + f1)) . x) * (1 / ( exp_R . x))) by XCMPLX_1: 215

        .= (((( #Z 2) * ( exp_R + f1)) . x) / ( exp_R . x)) by XCMPLX_1: 99

        .= ((( #Z 2) . (( exp_R + f1) . x)) / ( exp_R . x)) by A5, A10, FUNCT_1: 12

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

        hence thesis by A11, A9, XREAL_1: 139;

      end;

       exp_R is_differentiable_on Z & for x st x in Z holds ( exp_R . x) <> 0 by FDIFF_1: 26, SIN_COS: 54, TAYLOR_1: 16;

      then

       A12: ((( #Z 2) * ( exp_R + f1)) / exp_R ) is_differentiable_on Z by A6, FDIFF_2: 21;

      

       A13: for x st x in Z holds ( ln * ((( #Z 2) * ( exp_R + f1)) / exp_R )) is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then ((( #Z 2) * ( exp_R + f1)) / exp_R ) is_differentiable_in x & (((( #Z 2) * ( exp_R + f1)) / exp_R ) . x) > 0 by A12, A8, FDIFF_1: 9;

        hence thesis by TAYLOR_1: 20;

      end;

      then

       A14: f is_differentiable_on Z by A1, A2, FDIFF_1: 9;

      for x st x in Z holds ((f `| Z) . x) = ((( exp_R . x) - 1) / (( exp_R . x) + 1))

      proof

        let x;

        

         A15: ( exp_R . x) > 0 by SIN_COS: 54;

        

         A16: exp_R is_differentiable_in x by SIN_COS: 65;

        

         A17: (( exp_R . x) + 1) > 0 by SIN_COS: 54, XREAL_1: 34;

        assume

         A18: x in Z;

        

        then

         A19: (( exp_R + f1) . x) = (( exp_R . x) + (f1 . x)) by A7, VALUED_1:def 1

        .= (( exp_R . x) + 1) by A3, A18;

        

         A20: ((( #Z 2) * ( exp_R + f1)) . x) = (( #Z 2) . (( exp_R + f1) . x)) by A5, A18, FUNCT_1: 12

        .= ((( exp_R . x) + 1) #Z (1 + 1)) by A19, TAYLOR_1:def 1

        .= (((( exp_R . x) + 1) #Z 1) * ((( exp_R . x) + 1) #Z 1)) by A17, PREPOWER: 44

        .= ((( exp_R . x) + 1) * ((( exp_R . x) + 1) #Z 1)) by PREPOWER: 35

        .= ((( exp_R . x) + 1) * (( exp_R . x) + 1)) by PREPOWER: 35;

        

         A21: ((( #Z 2) * ( exp_R + f1)) / exp_R ) is_differentiable_in x & (((( #Z 2) * ( exp_R + f1)) / exp_R ) . x) > 0 by A12, A8, A18, FDIFF_1: 9;

        (( #Z 2) * ( exp_R + f1)) is_differentiable_in x by A6, A18, FDIFF_1: 9;

        

        then

         A22: ( diff (((( #Z 2) * ( exp_R + f1)) / exp_R ),x)) = (((( diff ((( #Z 2) * ( exp_R + f1)),x)) * ( exp_R . x)) - (( diff ( exp_R ,x)) * ((( #Z 2) * ( exp_R + f1)) . x))) / (( exp_R . x) ^2 )) by A15, A16, FDIFF_2: 14

        .= ((((((( #Z 2) * ( exp_R + f1)) `| Z) . x) * ( exp_R . x)) - (( diff ( exp_R ,x)) * ((( #Z 2) * ( exp_R + f1)) . x))) / (( exp_R . x) ^2 )) by A6, A18, FDIFF_1:def 7

        .= (((((2 * ( exp_R . x)) * (( exp_R . x) + 1)) * ( exp_R . x)) - (( diff ( exp_R ,x)) * ((( #Z 2) * ( exp_R + f1)) . x))) / (( exp_R . x) ^2 )) by A3, A5, A18, Th29

        .= (((((2 * ( exp_R . x)) * (( exp_R . x) + 1)) * ( exp_R . x)) - (( exp_R . x) * ((( #Z 2) * ( exp_R + f1)) . x))) / (( exp_R . x) ^2 )) by SIN_COS: 65

        .= (((((2 * ( exp_R . x)) * (( exp_R . x) + 1)) - ((( #Z 2) * ( exp_R + f1)) . x)) * ( exp_R . x)) / (( exp_R . x) * ( exp_R . x)))

        .= (((( exp_R . x) - 1) * (( exp_R . x) + 1)) / ( exp_R . x)) by A15, A20, XCMPLX_1: 91;

        

         A23: (((( #Z 2) * ( exp_R + f1)) / exp_R ) . x) = (((( #Z 2) * ( exp_R + f1)) . x) * (( exp_R . x) " )) by A4, A18, RFUNCT_1:def 1

        .= (((( #Z 2) * ( exp_R + f1)) . x) * (1 / ( exp_R . x))) by XCMPLX_1: 215

        .= (((( exp_R . x) + 1) * (( exp_R . x) + 1)) / ( exp_R . x)) by A20, XCMPLX_1: 99;

        ((f `| Z) . x) = ( diff (( ln * ((( #Z 2) * ( exp_R + f1)) / exp_R )),x)) by A2, A14, A18, FDIFF_1:def 7

        .= ((((( exp_R . x) + 1) * (( exp_R . x) - 1)) / ( exp_R . x)) / (((( exp_R . x) + 1) * (( exp_R . x) + 1)) / ( exp_R . x))) by A21, A22, A23, TAYLOR_1: 20

        .= (((( exp_R . x) + 1) * (( exp_R . x) - 1)) / ((( exp_R . x) + 1) * (( exp_R . x) + 1))) by A15, XCMPLX_1: 55

        .= ((( exp_R . x) - 1) / (( exp_R . x) + 1)) by A17, XCMPLX_1: 91;

        hence thesis;

      end;

      hence thesis by A1, A2, A13, FDIFF_1: 9;

    end;

    theorem :: FDIFF_6:31

    

     Th31: Z c= ( dom (( #Z 2) * (f - exp_R ))) & (for x st x in Z holds (f . x) = 1) implies (( #Z 2) * (f - exp_R )) is_differentiable_on Z & for x st x in Z holds (((( #Z 2) * (f - exp_R )) `| Z) . x) = ( - ((2 * ( exp_R . x)) * (1 - ( exp_R . x))))

    proof

      assume that

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

       A2: for x st x in Z holds (f . x) = 1;

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

      then

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

      then Z c= (( dom exp_R ) /\ ( dom f)) by VALUED_1: 12;

      then

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

      

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

      then

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

      

       A7: for x st x in Z holds (( #Z 2) * (f - exp_R )) is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then

         A8: f is_differentiable_in x by A6, FDIFF_1: 9;

         exp_R is_differentiable_in x by SIN_COS: 65;

        then (f - exp_R ) is_differentiable_in x by A8, FDIFF_1: 14;

        hence thesis by TAYLOR_1: 3;

      end;

      then

       A9: (( #Z 2) * (f - exp_R )) is_differentiable_on Z by A1, FDIFF_1: 9;

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

      proof

        let x;

        

         A10: exp_R is_differentiable_in x by SIN_COS: 65;

        assume

         A11: x in Z;

        

        then

         A12: ((f - exp_R ) . x) = ((f . x) - ( exp_R . x)) by A3, VALUED_1: 13

        .= (1 - ( exp_R . x)) by A2, A11;

        

         A13: f is_differentiable_in x by A6, A11, FDIFF_1: 9;

        

        then

         A14: ( diff ((f - exp_R ),x)) = (( diff (f,x)) - ( diff ( exp_R ,x))) by A10, FDIFF_1: 14

        .= (((f `| Z) . x) - ( diff ( exp_R ,x))) by A6, A11, FDIFF_1:def 7

        .= (((f `| Z) . x) - ( exp_R . x)) by SIN_COS: 65

        .= ( 0 - ( exp_R . x)) by A4, A5, A11, FDIFF_1: 23

        .= ( - ( exp_R . x));

        

         A15: (f - exp_R ) is_differentiable_in x by A13, A10, FDIFF_1: 14;

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

        .= ((2 * (((f - exp_R ) . x) #Z (2 - 1))) * ( diff ((f - exp_R ),x))) by A15, TAYLOR_1: 3

        .= ((2 * (1 - ( exp_R . x))) * ( - ( exp_R . x))) by A14, A12, PREPOWER: 35

        .= ( - ((2 * ( exp_R . x)) * (1 - ( exp_R . x))));

        hence thesis;

      end;

      hence thesis by A1, A7, FDIFF_1: 9;

    end;

    theorem :: FDIFF_6:32

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

    proof

      assume that

       A1: Z c= ( dom f) and

       A2: f = ( ln * ( exp_R / (( #Z 2) * (f1 - exp_R )))) and

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

      for y be object st y in Z holds y in ( dom ( exp_R / (( #Z 2) * (f1 - exp_R )))) by A1, A2, FUNCT_1: 11;

      then

       A4: Z c= ( dom ( exp_R / (( #Z 2) * (f1 - exp_R )))) by TARSKI:def 3;

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

      then

       A5: Z c= ( dom (( #Z 2) * (f1 - exp_R ))) by XBOOLE_1: 1;

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

      then

       A6: Z c= ( dom (f1 - exp_R )) by TARSKI:def 3;

      

       A7: for x st x in Z holds ((( #Z 2) * (f1 - exp_R )) . x) > 0

      proof

        let x;

        assume

         A8: x in Z;

        

        then ((( #Z 2) * (f1 - exp_R )) . x) = (( #Z 2) . ((f1 - exp_R ) . x)) by A5, FUNCT_1: 12

        .= (((f1 - exp_R ) . x) #Z 2) by TAYLOR_1:def 1;

        hence thesis by A3, A8, PREPOWER: 39;

      end;

      

       A9: for x st x in Z holds (( exp_R / (( #Z 2) * (f1 - exp_R ))) . x) > 0

      proof

        let x;

        

         A10: ( exp_R . x) > 0 by SIN_COS: 54;

        assume

         A11: x in Z;

        then

         A12: ((( #Z 2) * (f1 - exp_R )) . x) > 0 by A7;

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

        .= (( exp_R . x) * (1 / ((( #Z 2) * (f1 - exp_R )) . x))) by XCMPLX_1: 215

        .= (( exp_R . x) / ((( #Z 2) * (f1 - exp_R )) . x)) by XCMPLX_1: 99;

        hence thesis by A12, A10, XREAL_1: 139;

      end;

      

       A13: for x st x in Z holds (f1 . x) = 1 by A3;

      then

       A14: (( #Z 2) * (f1 - exp_R )) is_differentiable_on Z by A5, Th31;

       exp_R is_differentiable_on Z & for x st x in Z holds ((( #Z 2) * (f1 - exp_R )) . x) <> 0 by A7, FDIFF_1: 26, TAYLOR_1: 16;

      then

       A15: ( exp_R / (( #Z 2) * (f1 - exp_R ))) is_differentiable_on Z by A14, FDIFF_2: 21;

      

       A16: for x st x in Z holds ( ln * ( exp_R / (( #Z 2) * (f1 - exp_R )))) is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then ( exp_R / (( #Z 2) * (f1 - exp_R ))) is_differentiable_in x & (( exp_R / (( #Z 2) * (f1 - exp_R ))) . x) > 0 by A15, A9, FDIFF_1: 9;

        hence thesis by TAYLOR_1: 20;

      end;

      then

       A17: f is_differentiable_on Z by A1, A2, FDIFF_1: 9;

      for x st x in Z holds ((f `| Z) . x) = ((1 + ( exp_R . x)) / (1 - ( exp_R . x)))

      proof

        let x;

        

         A18: exp_R is_differentiable_in x by SIN_COS: 65;

        assume

         A19: x in Z;

        

        then

         A20: ((( #Z 2) * (f1 - exp_R )) . x) = (( #Z 2) . ((f1 - exp_R ) . x)) by A5, FUNCT_1: 12

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

        .= (((f1 . x) - ( exp_R . x)) #Z 2) by A6, A19, VALUED_1: 13

        .= ((1 - ( exp_R . x)) #Z 2) by A3, A19;

        

         A21: (( exp_R / (( #Z 2) * (f1 - exp_R ))) . x) = (( exp_R . x) * (((( #Z 2) * (f1 - exp_R )) . x) " )) by A4, A19, RFUNCT_1:def 1

        .= (( exp_R . x) * (1 / ((( #Z 2) * (f1 - exp_R )) . x))) by XCMPLX_1: 215

        .= (( exp_R . x) / ((1 - ( exp_R . x)) #Z 2)) by A20, XCMPLX_1: 99;

        

         A22: ( exp_R / (( #Z 2) * (f1 - exp_R ))) is_differentiable_in x & (( exp_R / (( #Z 2) * (f1 - exp_R ))) . x) > 0 by A15, A9, A19, FDIFF_1: 9;

        

         A23: ((f1 - exp_R ) . x) > 0 by A3, A19;

        ((( #Z 2) * (f1 - exp_R )) . x) <> 0 & (( #Z 2) * (f1 - exp_R )) is_differentiable_in x by A14, A7, A19, FDIFF_1: 9;

        

        then

         A24: ( diff (( exp_R / (( #Z 2) * (f1 - exp_R ))),x)) = (((( diff ( exp_R ,x)) * ((( #Z 2) * (f1 - exp_R )) . x)) - (( diff ((( #Z 2) * (f1 - exp_R )),x)) * ( exp_R . x))) / (((( #Z 2) * (f1 - exp_R )) . x) ^2 )) by A18, FDIFF_2: 14

        .= (((( exp_R . x) * ((( #Z 2) * (f1 - exp_R )) . x)) - (( diff ((( #Z 2) * (f1 - exp_R )),x)) * ( exp_R . x))) / (((( #Z 2) * (f1 - exp_R )) . x) ^2 )) by SIN_COS: 65

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

        .= (((( exp_R . x) * ((1 - ( exp_R . x)) #Z 2)) - (( - ((2 * ( exp_R . x)) * (1 - ( exp_R . x)))) * ( exp_R . x))) / (((1 - ( exp_R . x)) #Z 2) ^2 )) by A13, A5, A19, A20, Th31

        .= ((( exp_R . x) * (((1 - ( exp_R . x)) #Z 2) + ((2 * (1 - ( exp_R . x))) * ( exp_R . x)))) / (((1 - ( exp_R . x)) #Z 2) * ((1 - ( exp_R . x)) #Z 2)))

        .= (((( exp_R . x) / ((1 - ( exp_R . x)) #Z 2)) * (((1 - ( exp_R . x)) #Z 2) + ((2 * (1 - ( exp_R . x))) * ( exp_R . x)))) / ((1 - ( exp_R . x)) #Z 2)) by XCMPLX_1: 83;

        

         A25: ( exp_R . x) > 0 by SIN_COS: 54;

        

         A26: ((f1 - exp_R ) . x) = ((f1 . x) - ( exp_R . x)) by A6, A19, VALUED_1: 13

        .= (1 - ( exp_R . x)) by A3, A19;

        then ((1 - ( exp_R . x)) #Z 2) > 0 by A3, A19, PREPOWER: 39;

        then

         A27: (( exp_R . x) / ((1 - ( exp_R . x)) #Z 2)) <> 0 by A25, XREAL_1: 139;

        

         A28: ((1 - ( exp_R . x)) #Z 2) = ((1 - ( exp_R . x)) #Z (1 + 1))

        .= (((1 - ( exp_R . x)) #Z 1) * ((1 - ( exp_R . x)) #Z 1)) by A23, A26, PREPOWER: 44

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

        .= ((1 - ( exp_R . x)) * (1 - ( exp_R . x))) by PREPOWER: 35;

        ((f `| Z) . x) = ( diff (( ln * ( exp_R / (( #Z 2) * (f1 - exp_R )))),x)) by A2, A17, A19, FDIFF_1:def 7

        .= ((((( exp_R . x) / ((1 - ( exp_R . x)) #Z 2)) * (((1 - ( exp_R . x)) #Z 2) + ((2 * (1 - ( exp_R . x))) * ( exp_R . x)))) / ((1 - ( exp_R . x)) #Z 2)) / (( exp_R . x) / ((1 - ( exp_R . x)) #Z 2))) by A22, A24, A21, TAYLOR_1: 20

        .= (((( exp_R . x) / ((1 - ( exp_R . x)) #Z 2)) * (((1 - ( exp_R . x)) #Z 2) + ((2 * (1 - ( exp_R . x))) * ( exp_R . x)))) / ((( exp_R . x) / ((1 - ( exp_R . x)) #Z 2)) * ((1 - ( exp_R . x)) #Z 2))) by XCMPLX_1: 78

        .= (((1 - ( exp_R . x)) * (1 + ( exp_R . x))) / ((1 - ( exp_R . x)) * (1 - ( exp_R . x)))) by A27, A28, XCMPLX_1: 91

        .= ((1 + ( exp_R . x)) / (1 - ( exp_R . x))) by A23, A26, XCMPLX_1: 91;

        hence thesis;

      end;

      hence thesis by A1, A2, A16, FDIFF_1: 9;

    end;

    theorem :: FDIFF_6:33

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

    proof

      assume that

       A1: Z c= ( dom f) and

       A2: f = ( ln * ( exp_R / (( #Z 2) * (f1 + exp_R )))) and

       A3: for x st x in Z holds (f1 . x) = 1;

      for y be object st y in Z holds y in ( dom ( exp_R / (( #Z 2) * (f1 + exp_R )))) by A1, A2, FUNCT_1: 11;

      then

       A4: Z c= ( dom ( exp_R / (( #Z 2) * (f1 + exp_R )))) by TARSKI:def 3;

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

      then

       A5: Z c= ( dom (( #Z 2) * (f1 + exp_R ))) by XBOOLE_1: 1;

      then

       A6: (( #Z 2) * (f1 + exp_R )) is_differentiable_on Z by A3, Th29;

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

      then

       A7: Z c= ( dom (f1 + exp_R )) by TARSKI:def 3;

      

       A8: for x st x in Z holds ((( #Z 2) * (f1 + exp_R )) . x) > 0

      proof

        let x;

        assume

         A9: x in Z;

        

        then ((f1 + exp_R ) . x) = ((f1 . x) + ( exp_R . x)) by A7, VALUED_1:def 1

        .= (1 + ( exp_R . x)) by A3, A9;

        then

         A10: ((f1 + exp_R ) . x) > 0 by SIN_COS: 54, XREAL_1: 34;

        ((( #Z 2) * (f1 + exp_R )) . x) = (( #Z 2) . ((f1 + exp_R ) . x)) by A5, A9, FUNCT_1: 12

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

        hence thesis by A10, PREPOWER: 39;

      end;

      

       A11: for x st x in Z holds (( exp_R / (( #Z 2) * (f1 + exp_R ))) . x) > 0

      proof

        let x;

        

         A12: ( exp_R . x) > 0 by SIN_COS: 54;

        assume

         A13: x in Z;

        then

         A14: ((( #Z 2) * (f1 + exp_R )) . x) > 0 by A8;

        (( exp_R / (( #Z 2) * (f1 + exp_R ))) . x) = (( exp_R . x) * (((( #Z 2) * (f1 + exp_R )) . x) " )) by A4, A13, RFUNCT_1:def 1

        .= (( exp_R . x) * (1 / ((( #Z 2) * (f1 + exp_R )) . x))) by XCMPLX_1: 215

        .= (( exp_R . x) / ((( #Z 2) * (f1 + exp_R )) . x)) by XCMPLX_1: 99;

        hence thesis by A14, A12, XREAL_1: 139;

      end;

       exp_R is_differentiable_on Z & for x st x in Z holds ((( #Z 2) * (f1 + exp_R )) . x) <> 0 by A8, FDIFF_1: 26, TAYLOR_1: 16;

      then

       A15: ( exp_R / (( #Z 2) * (f1 + exp_R ))) is_differentiable_on Z by A6, FDIFF_2: 21;

      

       A16: for x st x in Z holds ( ln * ( exp_R / (( #Z 2) * (f1 + exp_R )))) is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then ( exp_R / (( #Z 2) * (f1 + exp_R ))) is_differentiable_in x & (( exp_R / (( #Z 2) * (f1 + exp_R ))) . x) > 0 by A15, A11, FDIFF_1: 9;

        hence thesis by TAYLOR_1: 20;

      end;

      then

       A17: f is_differentiable_on Z by A1, A2, FDIFF_1: 9;

      for x st x in Z holds ((f `| Z) . x) = ((1 - ( exp_R . x)) / (1 + ( exp_R . x)))

      proof

        let x;

        

         A18: exp_R is_differentiable_in x by SIN_COS: 65;

        assume

         A19: x in Z;

        

        then

         A20: ((( #Z 2) * (f1 + exp_R )) . x) = (( #Z 2) . ((f1 + exp_R ) . x)) by A5, FUNCT_1: 12

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

        .= (((f1 . x) + ( exp_R . x)) #Z 2) by A7, A19, VALUED_1:def 1

        .= ((1 + ( exp_R . x)) #Z 2) by A3, A19;

        ((( #Z 2) * (f1 + exp_R )) . x) <> 0 & (( #Z 2) * (f1 + exp_R )) is_differentiable_in x by A6, A8, A19, FDIFF_1: 9;

        

        then

         A21: ( diff (( exp_R / (( #Z 2) * (f1 + exp_R ))),x)) = (((( diff ( exp_R ,x)) * ((( #Z 2) * (f1 + exp_R )) . x)) - (( diff ((( #Z 2) * (f1 + exp_R )),x)) * ( exp_R . x))) / (((( #Z 2) * (f1 + exp_R )) . x) ^2 )) by A18, FDIFF_2: 14

        .= (((( exp_R . x) * ((( #Z 2) * (f1 + exp_R )) . x)) - (( diff ((( #Z 2) * (f1 + exp_R )),x)) * ( exp_R . x))) / (((( #Z 2) * (f1 + exp_R )) . x) ^2 )) by SIN_COS: 65

        .= (((( exp_R . x) * ((( #Z 2) * (f1 + exp_R )) . x)) - ((((( #Z 2) * (f1 + exp_R )) `| Z) . x) * ( exp_R . x))) / (((( #Z 2) * (f1 + exp_R )) . x) ^2 )) by A6, A19, FDIFF_1:def 7

        .= (((( exp_R . x) * ((1 + ( exp_R . x)) #Z 2)) - (((2 * ( exp_R . x)) * (1 + ( exp_R . x))) * ( exp_R . x))) / (((1 + ( exp_R . x)) #Z 2) ^2 )) by A3, A5, A19, A20, Th29

        .= ((( exp_R . x) * (((1 + ( exp_R . x)) #Z 2) - ((2 * (1 + ( exp_R . x))) * ( exp_R . x)))) / (((1 + ( exp_R . x)) #Z 2) * ((1 + ( exp_R . x)) #Z 2)))

        .= (((( exp_R . x) / ((1 + ( exp_R . x)) #Z 2)) * (((1 + ( exp_R . x)) #Z 2) - ((2 * (1 + ( exp_R . x))) * ( exp_R . x)))) / ((1 + ( exp_R . x)) #Z 2)) by XCMPLX_1: 83;

        

         A22: (1 + ( exp_R . x)) > 0 by SIN_COS: 54, XREAL_1: 34;

        then ( exp_R . x) > 0 & ((1 + ( exp_R . x)) #Z 2) > 0 by PREPOWER: 39, SIN_COS: 54;

        then

         A23: (( exp_R . x) / ((1 + ( exp_R . x)) #Z 2)) <> 0 by XREAL_1: 139;

        

         A24: (( exp_R / (( #Z 2) * (f1 + exp_R ))) . x) = (( exp_R . x) * (((( #Z 2) * (f1 + exp_R )) . x) " )) by A4, A19, RFUNCT_1:def 1

        .= (( exp_R . x) * (1 / ((( #Z 2) * (f1 + exp_R )) . x))) by XCMPLX_1: 215

        .= (( exp_R . x) / ((1 + ( exp_R . x)) #Z 2)) by A20, XCMPLX_1: 99;

        

         A25: ( exp_R / (( #Z 2) * (f1 + exp_R ))) is_differentiable_in x & (( exp_R / (( #Z 2) * (f1 + exp_R ))) . x) > 0 by A15, A11, A19, FDIFF_1: 9;

        

         A26: ((1 + ( exp_R . x)) #Z 2) = ((1 + ( exp_R . x)) #Z (1 + 1))

        .= (((1 + ( exp_R . x)) #Z 1) * ((1 + ( exp_R . x)) #Z 1)) by A22, PREPOWER: 44

        .= ((1 + ( exp_R . x)) * ((1 + ( exp_R . x)) #Z 1)) by PREPOWER: 35

        .= ((1 + ( exp_R . x)) * (1 + ( exp_R . x))) by PREPOWER: 35;

        ((f `| Z) . x) = ( diff (( ln * ( exp_R / (( #Z 2) * (f1 + exp_R )))),x)) by A2, A17, A19, FDIFF_1:def 7

        .= ((((( exp_R . x) / ((1 + ( exp_R . x)) #Z 2)) * (((1 + ( exp_R . x)) #Z 2) - ((2 * (1 + ( exp_R . x))) * ( exp_R . x)))) / ((1 + ( exp_R . x)) #Z 2)) / (( exp_R . x) / ((1 + ( exp_R . x)) #Z 2))) by A25, A21, A24, TAYLOR_1: 20

        .= (((( exp_R . x) / ((1 + ( exp_R . x)) #Z 2)) * (((1 + ( exp_R . x)) #Z 2) - ((2 * (1 + ( exp_R . x))) * ( exp_R . x)))) / ((( exp_R . x) / ((1 + ( exp_R . x)) #Z 2)) * ((1 + ( exp_R . x)) #Z 2))) by XCMPLX_1: 78

        .= (((1 + ( exp_R . x)) * (1 - ( exp_R . x))) / ((1 + ( exp_R . x)) * (1 + ( exp_R . x)))) by A23, A26, XCMPLX_1: 91

        .= ((1 - ( exp_R . x)) / (1 + ( exp_R . x))) by A22, XCMPLX_1: 91;

        hence thesis;

      end;

      hence thesis by A1, A2, A16, FDIFF_1: 9;

    end;

    theorem :: FDIFF_6:34

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

    proof

      assume that

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

       A2: f = ( exp_R + ( exp_R * f1)) and

       A3: for x st x in Z holds (f1 . x) = ( - x);

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

      then

       A4: Z c= ( dom ( exp_R + ( exp_R * f1))) by A2, TARSKI:def 3;

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

      then

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

      then

       A6: ( exp_R * f1) is_differentiable_on Z by A3, Th14;

      

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

      then

       A8: f is_differentiable_on Z by A2, A4, A6, FDIFF_1: 18;

      

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

      proof

        let x;

        assume

         A10: x in Z;

        

        hence ((( exp_R + ( exp_R * f1)) `| Z) . x) = (( diff ( exp_R ,x)) + ( diff (( exp_R * f1),x))) by A4, A6, A7, FDIFF_1: 18

        .= (( exp_R . x) + ( diff (( exp_R * f1),x))) by SIN_COS: 65

        .= (( exp_R . x) + ((( exp_R * f1) `| Z) . x)) by A6, A10, FDIFF_1:def 7

        .= (( exp_R . x) + ( - ( exp_R ( - x)))) by A3, A5, A10, Th14

        .= (( exp_R x) + ( - ( exp_R ( - x)))) by SIN_COS:def 23

        .= (( exp_R x) - ( exp_R ( - x)));

      end;

      

       A11: for x st x in Z holds (( exp_R + ( exp_R * f1)) . x) > 0

      proof

        let x;

        

         A12: ( exp_R x) > 0 by SIN_COS: 55;

        assume

         A13: x in Z;

        

        then (( exp_R + ( exp_R * f1)) . x) = (( exp_R . x) + (( exp_R * f1) . x)) by A4, VALUED_1:def 1

        .= (( exp_R . x) + ( exp_R . (f1 . x))) by A5, A13, FUNCT_1: 12

        .= (( exp_R . x) + ( exp_R . ( - x))) by A3, A13

        .= (( exp_R x) + ( exp_R . ( - x))) by SIN_COS:def 23

        .= (( exp_R x) + ( exp_R ( - x))) by SIN_COS:def 23;

        hence thesis by A12, SIN_COS: 55, XREAL_1: 34;

      end;

      

       A14: 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, A8, A11, FDIFF_1: 9;

        hence thesis by TAYLOR_1: 20;

      end;

      then

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

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

      proof

        let x;

        assume

         A16: x in Z;

        

        then

         A17: (f . x) = (( exp_R . x) + (( exp_R * f1) . x)) by A2, A4, VALUED_1:def 1

        .= (( exp_R . x) + ( exp_R . (f1 . x))) by A5, A16, FUNCT_1: 12

        .= (( exp_R . x) + ( exp_R . ( - x))) by A3, A16

        .= (( exp_R x) + ( exp_R . ( - x))) by SIN_COS:def 23

        .= (( exp_R x) + ( exp_R ( - x))) by SIN_COS:def 23;

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

        

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

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

        .= ((( exp_R x) - ( exp_R ( - x))) / (( exp_R x) + ( exp_R ( - x)))) by A2, A9, A16, A17;

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

      end;

      hence thesis by A1, A14, FDIFF_1: 9;

    end;

    theorem :: FDIFF_6:35

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

    proof

      assume that

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

       A2: f = ( exp_R - ( exp_R * f1)) and

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

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

      then

       A4: Z c= ( dom ( exp_R - ( exp_R * f1))) by A2, TARSKI:def 3;

      then Z c= (( dom exp_R ) /\ ( dom ( exp_R * f1))) by VALUED_1: 12;

      then

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

      

       A6: for x st x in Z holds (f1 . x) = ( - x) by A3;

      then

       A7: ( exp_R * f1) is_differentiable_on Z by A5, Th14;

      

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

      then

       A9: f is_differentiable_on Z by A2, A4, A7, FDIFF_1: 19;

      

       A10: for x st x in Z holds ((( exp_R - ( exp_R * f1)) `| Z) . x) = (( exp_R x) + ( exp_R ( - x)))

      proof

        let x;

        assume

         A11: x in Z;

        

        hence ((( exp_R - ( exp_R * f1)) `| Z) . x) = (( diff ( exp_R ,x)) - ( diff (( exp_R * f1),x))) by A4, A7, A8, FDIFF_1: 19

        .= (( exp_R . x) - ( diff (( exp_R * f1),x))) by SIN_COS: 65

        .= (( exp_R . x) - ((( exp_R * f1) `| Z) . x)) by A7, A11, FDIFF_1:def 7

        .= (( exp_R . x) - ( - ( exp_R ( - x)))) by A6, A5, A11, Th14

        .= (( exp_R . x) + ( exp_R ( - x)))

        .= (( exp_R x) + ( exp_R ( - x))) by SIN_COS:def 23;

      end;

      

       A12: 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 A3, A9, FDIFF_1: 9;

        hence thesis by TAYLOR_1: 20;

      end;

      then

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

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

      proof

        let x;

        assume

         A14: x in Z;

        

        then

         A15: (f . x) = (( exp_R . x) - (( exp_R * f1) . x)) by A2, A4, VALUED_1: 13

        .= (( exp_R . x) - ( exp_R . (f1 . x))) by A5, A14, FUNCT_1: 12

        .= (( exp_R . x) - ( exp_R . ( - x))) by A3, A14

        .= (( exp_R x) - ( exp_R . ( - x))) by SIN_COS:def 23

        .= (( exp_R x) - ( exp_R ( - x))) by SIN_COS:def 23;

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

        

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

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

        .= ((( exp_R x) + ( exp_R ( - x))) / (( exp_R x) - ( exp_R ( - x)))) by A2, A10, A14, A15;

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

      end;

      hence thesis by A1, A12, FDIFF_1: 9;

    end;

    theorem :: FDIFF_6:36

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

    proof

      assume that

       A1: Z c= ( dom ((2 / 3) (#) (( #R (3 / 2)) * (f + exp_R )))) 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;

      

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

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

      then

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

      then Z c= (( dom exp_R ) /\ ( dom f)) by VALUED_1:def 1;

      then

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

      then

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

      

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

      then

       A9: (f + exp_R ) is_differentiable_on Z by A5, A7, FDIFF_1: 18;

      

       A10: for x st x in Z holds ((f + exp_R ) . x) > 0

      proof

        let x;

        assume

         A11: x in Z;

        

        then ((f + exp_R ) . x) = ((f . x) + ( exp_R . x)) by A5, VALUED_1:def 1

        .= (1 + ( exp_R . x)) by A2, A11;

        hence thesis by SIN_COS: 54, XREAL_1: 34;

      end;

      now

        let x;

        assume x in Z;

        then (f + exp_R ) is_differentiable_in x & ((f + exp_R ) . x) > 0 by A9, A10, FDIFF_1: 9;

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

      end;

      then

       A12: (( #R (3 / 2)) * (f + exp_R )) is_differentiable_on Z by A4, FDIFF_1: 9;

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

      proof

        let x;

        assume

         A13: x in Z;

        

        then

         A14: (((f + exp_R ) `| Z) . x) = (( diff (f,x)) + ( diff ( exp_R ,x))) by A5, A7, A8, FDIFF_1: 18

        .= (( diff (f,x)) + ( exp_R . x)) by SIN_COS: 65

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

        .= ( 0 + ( exp_R . x)) by A6, A3, A13, FDIFF_1: 23

        .= ( exp_R . x);

        

         A15: (f + exp_R ) is_differentiable_in x & ((f + exp_R ) . x) > 0 by A9, A10, A13, FDIFF_1: 9;

        

         A16: ((f + exp_R ) . x) = ((f . x) + ( exp_R . x)) by A5, A13, VALUED_1:def 1

        .= (1 + ( exp_R . x)) by A2, A13;

        ((((2 / 3) (#) (( #R (3 / 2)) * (f + exp_R ))) `| Z) . x) = ((2 / 3) * ( diff ((( #R (3 / 2)) * (f + exp_R )),x))) by A1, A12, A13, FDIFF_1: 20

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

        .= ((2 / 3) * (((3 / 2) * (((f + exp_R ) . x) #R ((3 / 2) - 1))) * (((f + exp_R ) `| Z) . x))) by A9, A13, FDIFF_1:def 7

        .= (( exp_R . x) * ((1 + ( exp_R . x)) #R (1 / 2))) by A16, A14;

        hence thesis;

      end;

      hence thesis by A1, A12, FDIFF_1: 20;

    end;

    theorem :: FDIFF_6:37

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

    proof

      assume that

       A1: Z c= ( dom ((2 / (3 * ( log ( number_e ,a)))) (#) (( #R (3 / 2)) * (f + ( exp_R * f1))))) and

       A2: for x st x in Z holds (f . x) = 1 & (f1 . x) = (x * ( log ( number_e ,a))) and

       A3: a > 0 and

       A4: a <> 1;

      

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

      

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

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

      then

       A7: Z c= ( dom (f + ( exp_R * f1))) by TARSKI:def 3;

      then

       A8: Z c= (( dom ( exp_R * f1)) /\ ( dom f)) by VALUED_1:def 1;

      then

       A9: Z c= ( dom ( exp_R * f1)) by XBOOLE_1: 18;

      

       A10: for x st x in Z holds (f1 . x) = (x * ( log ( number_e ,a))) by A2;

      then

       A11: ( exp_R * f1) is_differentiable_on Z by A3, A9, Th11;

      

       A12: Z c= ( dom f) by A8, XBOOLE_1: 18;

      then

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

      then

       A14: (f + ( exp_R * f1)) is_differentiable_on Z by A7, A11, FDIFF_1: 18;

      

       A15: for x st x in Z holds ((f + ( exp_R * f1)) . x) > 0

      proof

        let x;

        assume

         A16: x in Z;

        

        then ((f + ( exp_R * f1)) . x) = ((f . x) + (( exp_R * f1) . x)) by A7, VALUED_1:def 1

        .= ((f . x) + ( exp_R . (f1 . x))) by A9, A16, FUNCT_1: 12

        .= (1 + ( exp_R . (f1 . x))) by A2, A16

        .= (1 + ( exp_R . (x * ( log ( number_e ,a))))) by A2, A16;

        hence thesis by SIN_COS: 54, XREAL_1: 34;

      end;

      now

        let x;

        assume x in Z;

        then (f + ( exp_R * f1)) is_differentiable_in x & ((f + ( exp_R * f1)) . x) > 0 by A14, A15, FDIFF_1: 9;

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

      end;

      then

       A17: (( #R (3 / 2)) * (f + ( exp_R * f1))) is_differentiable_on Z by A6, FDIFF_1: 9;

      

       A18: ( log ( number_e ,a)) <> 0

      proof

        

         A19: number_e <> 1 by TAYLOR_1: 11;

        assume ( log ( number_e ,a)) = 0 ;

        then ( log ( number_e ,a)) = ( log ( number_e ,1)) by SIN_COS2: 13, TAYLOR_1: 13;

        

        then a = ( number_e to_power ( log ( number_e ,1))) by A3, A19, POWER:def 3, TAYLOR_1: 11

        .= 1 by A19, POWER:def 3, TAYLOR_1: 11;

        hence contradiction by A4;

      end;

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

      proof

        let x;

        

         A20: (3 * ( log ( number_e ,a))) <> 0 by A18;

        assume

         A21: x in Z;

        

        then

         A22: (((f + ( exp_R * f1)) `| Z) . x) = (( diff (f,x)) + ( diff (( exp_R * f1),x))) by A7, A13, A11, FDIFF_1: 18

        .= (( diff (f,x)) + ((( exp_R * f1) `| Z) . x)) by A11, A21, FDIFF_1:def 7

        .= (((f `| Z) . x) + ((( exp_R * f1) `| Z) . x)) by A13, A21, FDIFF_1:def 7

        .= ( 0 + ((( exp_R * f1) `| Z) . x)) by A12, A5, A21, FDIFF_1: 23

        .= ((a #R x) * ( log ( number_e ,a))) by A3, A10, A9, A21, Th11;

        

         A23: ((f + ( exp_R * f1)) . x) = ((f . x) + (( exp_R * f1) . x)) by A7, A21, VALUED_1:def 1

        .= ((f . x) + ( exp_R . (f1 . x))) by A9, A21, FUNCT_1: 12

        .= (1 + ( exp_R . (f1 . x))) by A2, A21

        .= (1 + ( exp_R . (x * ( log ( number_e ,a))))) by A2, A21

        .= (1 + (a #R x)) by A3, Th1;

        (f + ( exp_R * f1)) is_differentiable_in x & ((f + ( exp_R * f1)) . x) > 0 by A14, A15, A21, FDIFF_1: 9;

        

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

        .= (((3 / 2) * ((1 + (a #R x)) #R (1 / 2))) * ((a #R x) * ( log ( number_e ,a)))) by A14, A21, A23, A22, FDIFF_1:def 7

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

        

        then ((((2 / (3 * ( log ( number_e ,a)))) (#) (( #R (3 / 2)) * (f + ( exp_R * f1)))) `| Z) . x) = ((2 / (3 * ( log ( number_e ,a)))) * ((((3 * ( log ( number_e ,a))) / 2) * (a #R x)) * ((1 + (a #R x)) #R (1 / 2)))) by A1, A17, A21, FDIFF_1: 20

        .= ((((2 / (3 * ( log ( number_e ,a)))) * ((3 * ( log ( number_e ,a))) / 2)) * (a #R x)) * ((1 + (a #R x)) #R (1 / 2)))

        .= ((1 * (a #R x)) * ((1 + (a #R x)) #R (1 / 2))) by A20, XCMPLX_1: 112

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

        hence thesis;

      end;

      hence thesis by A1, A17, FDIFF_1: 20;

    end;

    theorem :: FDIFF_6:38

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

    proof

      assume that

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

       A2: for x st x in Z holds (f . x) = (2 * x);

      

       A3: Z c= ( dom ( cos * f)) & for x st x in Z holds (f . x) = ((2 * x) + 0 ) by A1, A2, VALUED_1:def 5;

      then

       A4: ( cos * f) is_differentiable_on Z by FDIFF_4: 38;

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

      proof

        let x;

        assume

         A5: x in Z;

        

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

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

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

        .= ( sin (2 * x)) by SIN_COS:def 17;

        hence thesis;

      end;

      hence thesis by A1, A4, FDIFF_1: 20;

    end;

    theorem :: FDIFF_6:39

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

    proof

      assume that

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

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

      

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

      

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

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

      then

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

      then Z c= (( dom cos ) /\ ( dom f)) by VALUED_1: 12;

      then

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

      then

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

      

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

      then

       A9: (f - cos ) is_differentiable_on Z by A5, A7, FDIFF_1: 19;

      

       A10: for x st x in Z holds ((f - cos ) . x) > 0

      proof

        let x;

        assume

         A11: x in Z;

        then ( cos . x) < 1 by A2;

        then

         A12: (1 - ( cos . x)) > (1 - 1) by XREAL_1: 15;

        ((f - cos ) . x) = ((f . x) - ( cos . x)) by A5, A11, VALUED_1: 13

        .= (1 - ( cos . x)) by A2, A11;

        hence thesis by A12;

      end;

      now

        let x;

        assume x in Z;

        then (f - cos ) is_differentiable_in x & ((f - cos ) . x) > 0 by A9, A10, FDIFF_1: 9;

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

      end;

      then

       A13: (( #R (1 / 2)) * (f - cos )) is_differentiable_on Z by A4, FDIFF_1: 9;

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

      proof

        let x;

        assume

         A14: x in Z;

        

        then

         A15: ( diff ((f - cos ),x)) = (((f - cos ) `| Z) . x) by A9, FDIFF_1:def 7

        .= (( diff (f,x)) - ( diff ( cos ,x))) by A5, A7, A8, A14, FDIFF_1: 19

        .= (((f `| Z) . x) - ( diff ( cos ,x))) by A7, A14, FDIFF_1:def 7

        .= ( 0 - ( diff ( cos ,x))) by A6, A3, A14, FDIFF_1: 23

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

        .= ( sin . x);

        

         A16: ( cos . x) > ( - 1) by A2, A14;

        

         A17: ((f - cos ) . x) = ((f . x) - ( cos . x)) by A5, A14, VALUED_1: 13

        .= (1 - ( cos . x)) by A2, A14;

        

         A18: (f - cos ) is_differentiable_in x & ((f - cos ) . x) > 0 by A9, A10, A14, FDIFF_1: 9;

        

         A19: ( sin . x) > 0 & ( cos . x) < 1 by A2, A14;

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

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

        .= (( sin . x) * ((1 - ( cos . x)) #R ( - (1 / 2)))) by A17, A15

        .= (( sin . x) * (1 / ((1 - ( cos . x)) #R (1 / 2)))) by A10, A14, A17, PREPOWER: 76

        .= (( sin . x) / ((1 - ( cos . x)) #R (1 / 2))) by XCMPLX_1: 99

        .= ((1 + ( cos . x)) #R (1 / 2)) by A19, A16, Lm4;

        hence thesis;

      end;

      hence thesis by A1, A13, FDIFF_1: 20;

    end;

    theorem :: FDIFF_6:40

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

    proof

      assume that

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

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

      

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

      

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

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

      then

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

      then Z c= (( dom cos ) /\ ( dom f)) by VALUED_1:def 1;

      then

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

      then

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

      

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

      then

       A9: (f + cos ) is_differentiable_on Z by A5, A7, FDIFF_1: 18;

      

       A10: for x st x in Z holds ((f + cos ) . x) > 0

      proof

        let x;

        assume

         A11: x in Z;

        then ( cos . x) > ( - 1) by A2;

        then

         A12: (1 + ( cos . x)) > (1 + ( - 1)) by XREAL_1: 8;

        ((f + cos ) . x) = ((f . x) + ( cos . x)) by A5, A11, VALUED_1:def 1

        .= (1 + ( cos . x)) by A2, A11;

        hence thesis by A12;

      end;

      now

        let x;

        assume x in Z;

        then (f + cos ) is_differentiable_in x & ((f + cos ) . x) > 0 by A9, A10, FDIFF_1: 9;

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

      end;

      then

       A13: (( #R (1 / 2)) * (f + cos )) is_differentiable_on Z by A4, FDIFF_1: 9;

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

      proof

        let x;

        assume

         A14: x in Z;

        

        then

         A15: ( diff ((f + cos ),x)) = (((f + cos ) `| Z) . x) by A9, FDIFF_1:def 7

        .= (( diff (f,x)) + ( diff ( cos ,x))) by A5, A7, A8, A14, FDIFF_1: 18

        .= (((f `| Z) . x) + ( diff ( cos ,x))) by A7, A14, FDIFF_1:def 7

        .= ( 0 + ( diff ( cos ,x))) by A6, A3, A14, FDIFF_1: 23

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

        

         A16: ( cos . x) > ( - 1) by A2, A14;

        

         A17: ((f + cos ) . x) = ((f . x) + ( cos . x)) by A5, A14, VALUED_1:def 1

        .= (1 + ( cos . x)) by A2, A14;

        

         A18: (f + cos ) is_differentiable_in x & ((f + cos ) . x) > 0 by A9, A10, A14, FDIFF_1: 9;

        

         A19: ( sin . x) > 0 & ( cos . x) < 1 by A2, A14;

        (((( - 2) (#) (( #R (1 / 2)) * (f + cos ))) `| Z) . x) = (( - 2) * ( diff ((( #R (1 / 2)) * (f + cos )),x))) by A1, A13, A14, FDIFF_1: 20

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

        .= ( - ( - (( sin . x) * ((1 + ( cos . x)) #R ( - (1 / 2)))))) by A17, A15

        .= (( sin . x) * (1 / ((1 + ( cos . x)) #R (1 / 2)))) by A10, A14, A17, PREPOWER: 76

        .= (( sin . x) / ((1 + ( cos . x)) #R (1 / 2))) by XCMPLX_1: 99

        .= ((1 - ( cos . x)) #R (1 / 2)) by A19, A16, Lm5;

        hence thesis;

      end;

      hence thesis by A1, A13, FDIFF_1: 20;

    end;

    

     Lm6: Z c= ( dom (f1 + (2 (#) sin ))) & (for x st x in Z holds (f1 . x) = 1) implies (f1 + (2 (#) sin )) is_differentiable_on Z & for x st x in Z holds (((f1 + (2 (#) sin )) `| Z) . x) = (2 * ( cos . x))

    proof

      assume that

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

       A2: for x st x in Z holds (f1 . x) = 1;

      

       A3: Z c= (( dom f1) /\ ( dom (2 (#) sin ))) by A1, VALUED_1:def 1;

      then

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

      

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

      

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

      then

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

      Z c= ( dom (2 (#) sin )) by A3, XBOOLE_1: 18;

      then

       A8: (2 (#) sin ) is_differentiable_on Z by A5, FDIFF_1: 20;

      for x st x in Z holds (((f1 + (2 (#) sin )) `| Z) . x) = (2 * ( cos . x))

      proof

        let x;

        

         A9: sin is_differentiable_in x by SIN_COS: 64;

        assume

         A10: x in Z;

        

        then (((f1 + (2 (#) sin )) `| Z) . x) = (( diff (f1,x)) + ( diff ((2 (#) sin ),x))) by A1, A7, A8, FDIFF_1: 18

        .= (((f1 `| Z) . x) + ( diff ((2 (#) sin ),x))) by A7, A10, FDIFF_1:def 7

        .= (((f1 `| Z) . x) + (2 * ( diff ( sin ,x)))) by A9, FDIFF_1: 15

        .= ( 0 + (2 * ( diff ( sin ,x)))) by A4, A6, A10, FDIFF_1: 23

        .= (2 * ( cos . x)) by SIN_COS: 64;

        hence thesis;

      end;

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

    end;

    theorem :: FDIFF_6:41

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

    proof

      assume that

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

       A2: f = (f1 + (2 (#) sin )) and

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

      

       A4: Z c= ( dom ( ln * 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

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

      

       A6: for x st x in Z holds (f1 . x) = 1 by A3;

      then

       A7: f is_differentiable_on Z by A2, A5, Lm6;

      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 A3, A7, FDIFF_1: 9;

        hence thesis by TAYLOR_1: 20;

      end;

      then

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

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

      then

       A9: Z c= ( dom (2 (#) sin )) by XBOOLE_1: 18;

      for x st x in Z holds ((((1 / 2) (#) ( ln * f)) `| Z) . x) = (( cos . x) / (1 + (2 * ( sin . x))))

      proof

        let x;

        assume

         A10: x in Z;

        

        then

         A11: (f . x) = ((f1 . x) + ((2 (#) sin ) . x)) by A2, A5, VALUED_1:def 1

        .= (1 + ((2 (#) sin ) . x)) by A3, A10

        .= (1 + (2 * ( sin . x))) by A9, A10, VALUED_1:def 5;

        

         A12: f is_differentiable_in x & (f . x) > 0 by A3, A7, A10, FDIFF_1: 9;

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

        .= ((1 / 2) * (( diff (f,x)) / (f . x))) by A12, TAYLOR_1: 20

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

        .= ((1 / 2) * ((2 * ( cos . x)) / (f . x))) by A2, A6, A5, A10, Lm6

        .= (((1 / 2) * (2 * ( cos . x))) / (f . x)) by XCMPLX_1: 74

        .= (( cos . x) / (1 + (2 * ( sin . x)))) by A11;

        hence thesis;

      end;

      hence thesis by A1, A8, FDIFF_1: 20;

    end;

    

     Lm7: Z c= ( dom (f1 + (2 (#) cos ))) & (for x st x in Z holds (f1 . x) = 1) implies (f1 + (2 (#) cos )) is_differentiable_on Z & for x st x in Z holds (((f1 + (2 (#) cos )) `| Z) . x) = ( - (2 * ( sin . x)))

    proof

      assume that

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

       A2: for x st x in Z holds (f1 . x) = 1;

      

       A3: Z c= (( dom f1) /\ ( dom (2 (#) cos ))) by A1, VALUED_1:def 1;

      then

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

      

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

      

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

      then

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

      Z c= ( dom (2 (#) cos )) by A3, XBOOLE_1: 18;

      then

       A8: (2 (#) cos ) is_differentiable_on Z by A5, FDIFF_1: 20;

      for x st x in Z holds (((f1 + (2 (#) cos )) `| Z) . x) = ( - (2 * ( sin . x)))

      proof

        let x;

        

         A9: cos is_differentiable_in x by SIN_COS: 63;

        assume

         A10: x in Z;

        

        then (((f1 + (2 (#) cos )) `| Z) . x) = (( diff (f1,x)) + ( diff ((2 (#) cos ),x))) by A1, A7, A8, FDIFF_1: 18

        .= (((f1 `| Z) . x) + ( diff ((2 (#) cos ),x))) by A7, A10, FDIFF_1:def 7

        .= (((f1 `| Z) . x) + (2 * ( diff ( cos ,x)))) by A9, FDIFF_1: 15

        .= ( 0 + (2 * ( diff ( cos ,x)))) by A4, A6, A10, FDIFF_1: 23

        .= ( 0 + (2 * ( - ( sin . x)))) by SIN_COS: 63

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

        hence thesis;

      end;

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

    end;

    theorem :: FDIFF_6:42

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

    proof

      assume that

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

       A2: f = (f1 + (2 (#) cos )) and

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

      

       A4: Z c= ( dom ( ln * 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

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

      

       A6: for x st x in Z holds (f1 . x) = 1 by A3;

      then

       A7: f is_differentiable_on Z by A2, A5, Lm7;

      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 A3, A7, FDIFF_1: 9;

        hence thesis by TAYLOR_1: 20;

      end;

      then

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

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

      then

       A9: Z c= ( dom (2 (#) cos )) by XBOOLE_1: 18;

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

      proof

        let x;

        assume

         A10: x in Z;

        

        then

         A11: (f . x) = ((f1 . x) + ((2 (#) cos ) . x)) by A2, A5, VALUED_1:def 1

        .= (1 + ((2 (#) cos ) . x)) by A3, A10

        .= (1 + (2 * ( cos . x))) by A9, A10, VALUED_1:def 5;

        

         A12: f is_differentiable_in x & (f . x) > 0 by A3, A7, A10, FDIFF_1: 9;

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

        .= (( - (1 / 2)) * (( diff (f,x)) / (f . x))) by A12, TAYLOR_1: 20

        .= (( - (1 / 2)) * (((f `| Z) . x) / (f . x))) by A7, A10, FDIFF_1:def 7

        .= (( - (1 / 2)) * (( - (2 * ( sin . x))) / (f . x))) by A2, A6, A5, A10, Lm7

        .= ((( - (1 / 2)) * ( - (2 * ( sin . x)))) / (f . x)) by XCMPLX_1: 74

        .= (( sin . x) / (1 + (2 * ( cos . x)))) by A11;

        hence thesis;

      end;

      hence thesis by A1, A8, FDIFF_1: 20;

    end;

    theorem :: FDIFF_6:43

    

     Th43: Z c= ( dom ((1 / (4 * a)) (#) ( sin * f))) & (for x st x in Z holds (f . x) = ((2 * a) * x)) & a <> 0 implies ((1 / (4 * a)) (#) ( sin * f)) is_differentiable_on Z & for x st x in Z holds ((((1 / (4 * a)) (#) ( sin * f)) `| Z) . x) = ((1 / 2) * ( cos ((2 * a) * x)))

    proof

      assume that

       A1: Z c= ( dom ((1 / (4 * a)) (#) ( sin * f))) and

       A2: for x st x in Z holds (f . x) = ((2 * a) * x) and

       A3: a <> 0 ;

      

       A4: Z c= ( dom ( sin * f)) & for x st x in Z holds (f . x) = (((2 * a) * x) + 0 ) by A1, A2, VALUED_1:def 5;

      then

       A5: ( sin * f) is_differentiable_on Z by FDIFF_4: 37;

      for x st x in Z holds ((((1 / (4 * a)) (#) ( sin * f)) `| Z) . x) = ((1 / 2) * ( cos ((2 * a) * x)))

      proof

        let x;

        assume

         A6: x in Z;

        

        then ((((1 / (4 * a)) (#) ( sin * f)) `| Z) . x) = ((1 / (4 * a)) * ( diff (( sin * f),x))) by A1, A5, FDIFF_1: 20

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

        .= ((1 / (4 * a)) * ((2 * a) * ( cos . (((2 * a) * x) + 0 )))) by A4, A6, FDIFF_4: 37

        .= (((1 / (4 * a)) * (2 * a)) * ( cos . (((2 * a) * x) + 0 )))

        .= ((((1 / 4) * (1 / a)) * (2 * a)) * ( cos . ((2 * a) * x))) by XCMPLX_1: 102

        .= ((((1 / 4) * 2) * ((1 / a) * a)) * ( cos . ((2 * a) * x)))

        .= (((1 / 2) * 1) * ( cos . ((2 * a) * x))) by A3, XCMPLX_1: 106

        .= ((1 / 2) * ( cos ((2 * a) * x))) by SIN_COS:def 19;

        hence thesis;

      end;

      hence thesis by A1, A5, FDIFF_1: 20;

    end;

    theorem :: FDIFF_6:44

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

    proof

      assume that

       A1: Z c= ( dom (f1 - ((1 / (4 * a)) (#) ( sin * f)))) and

       A2: for x st x in Z holds (f1 . x) = (x / 2) & (f . x) = ((2 * a) * x) and

       A3: a <> 0 ;

      

       A4: Z c= (( dom f1) /\ ( dom ((1 / (4 * a)) (#) ( sin * f)))) by A1, VALUED_1: 12;

      then

       A5: Z c= ( dom ((1 / (4 * a)) (#) ( sin * f))) by XBOOLE_1: 18;

      

       A6: for x st x in Z holds (f1 . x) = (((1 / 2) * x) + 0 )

      proof

        let x;

        assume x in Z;

        

        then (f1 . x) = (x / 2) by A2

        .= (((1 / 2) * x) + 0 );

        hence thesis;

      end;

      

       A7: for x st x in Z holds (f . x) = ((2 * a) * x) by A2;

      then

       A8: ((1 / (4 * a)) (#) ( sin * f)) is_differentiable_on Z by A3, A5, Th43;

      

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

      then

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

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

      proof

        let x;

        assume

         A11: x in Z;

        

        then (((f1 - ((1 / (4 * a)) (#) ( sin * f))) `| Z) . x) = (( diff (f1,x)) - ( diff (((1 / (4 * a)) (#) ( sin * f)),x))) by A1, A8, A10, FDIFF_1: 19

        .= (((f1 `| Z) . x) - ( diff (((1 / (4 * a)) (#) ( sin * f)),x))) by A10, A11, FDIFF_1:def 7

        .= (((f1 `| Z) . x) - ((((1 / (4 * a)) (#) ( sin * f)) `| Z) . x)) by A8, A11, FDIFF_1:def 7

        .= (((f1 `| Z) . x) - ((1 / 2) * ( cos ((2 * a) * x)))) by A3, A7, A5, A11, Th43

        .= ((1 / 2) - ((1 / 2) * ( cos ((2 * a) * x)))) by A9, A6, A11, FDIFF_1: 23

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

        .= ((1 / 2) * (2 * (( sin (a * x)) ^2 ))) by Lm1

        .= (( sin (a * x)) ^2 );

        hence thesis;

      end;

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

    end;

    theorem :: FDIFF_6:45

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

    proof

      assume that

       A1: Z c= ( dom (f1 + ((1 / (4 * a)) (#) ( sin * f)))) and

       A2: for x st x in Z holds (f1 . x) = (x / 2) & (f . x) = ((2 * a) * x) and

       A3: a <> 0 ;

      

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

      then

       A5: Z c= ( dom ((1 / (4 * a)) (#) ( sin * f))) by XBOOLE_1: 18;

      

       A6: for x st x in Z holds (f1 . x) = (((1 / 2) * x) + 0 )

      proof

        let x;

        assume x in Z;

        

        then (f1 . x) = (x / 2) by A2

        .= (((1 / 2) * x) + 0 );

        hence thesis;

      end;

      

       A7: for x st x in Z holds (f . x) = ((2 * a) * x) by A2;

      then

       A8: ((1 / (4 * a)) (#) ( sin * f)) is_differentiable_on Z by A3, A5, Th43;

      

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

      then

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

      for x st x in Z holds (((f1 + ((1 / (4 * a)) (#) ( sin * f))) `| Z) . x) = (( cos (a * x)) ^2 )

      proof

        let x;

        assume

         A11: x in Z;

        

        then (((f1 + ((1 / (4 * a)) (#) ( sin * f))) `| Z) . x) = (( diff (f1,x)) + ( diff (((1 / (4 * a)) (#) ( sin * f)),x))) by A1, A8, A10, FDIFF_1: 18

        .= (((f1 `| Z) . x) + ( diff (((1 / (4 * a)) (#) ( sin * f)),x))) by A10, A11, FDIFF_1:def 7

        .= (((f1 `| Z) . x) + ((((1 / (4 * a)) (#) ( sin * f)) `| Z) . x)) by A8, A11, FDIFF_1:def 7

        .= (((f1 `| Z) . x) + ((1 / 2) * ( cos ((2 * a) * x)))) by A3, A7, A5, A11, Th43

        .= ((1 / 2) + ((1 / 2) * ( cos ((2 * a) * x)))) by A9, A6, A11, FDIFF_1: 23

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

        .= ((1 / 2) * (2 * (( cos (a * x)) ^2 ))) by Lm2

        .= (( cos (a * x)) ^2 );

        hence thesis;

      end;

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

    end;

    theorem :: FDIFF_6:46

    

     Th46: Z c= ( dom ((1 / n) (#) (( #Z n) * cos ))) & n > 0 implies ((1 / n) (#) (( #Z n) * cos )) is_differentiable_on Z & for x st x in Z holds ((((1 / n) (#) (( #Z n) * cos )) `| Z) . x) = ( - ((( cos . x) #Z (n - 1)) * ( sin . x)))

    proof

      assume that

       A1: Z c= ( dom ((1 / n) (#) (( #Z n) * cos ))) and

       A2: n > 0 ;

       A3:

      now

        let x;

        assume x in Z;

         cos is_differentiable_in x by SIN_COS: 63;

        hence (( #Z n) * cos ) is_differentiable_in x by TAYLOR_1: 3;

      end;

      Z c= ( dom (( #Z n) * cos )) by A1, VALUED_1:def 5;

      then

       A4: (( #Z n) * cos ) is_differentiable_on Z by A3, FDIFF_1: 9;

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

      proof

        let x;

        

         A5: cos is_differentiable_in x by SIN_COS: 63;

        assume x in Z;

        

        then ((((1 / n) (#) (( #Z n) * cos )) `| Z) . x) = ((1 / n) * ( diff ((( #Z n) * cos ),x))) by A1, A4, FDIFF_1: 20

        .= ((1 / n) * ((n * (( cos . x) #Z (n - 1))) * ( diff ( cos ,x)))) by A5, TAYLOR_1: 3

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

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

        .= ((((n " ) * n) * (( cos . x) #Z (n - 1))) * ( - ( sin . x))) by XCMPLX_1: 215

        .= ((1 * (( cos . x) #Z (n - 1))) * ( - ( sin . x))) by A2, XCMPLX_0:def 7

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

        hence thesis;

      end;

      hence thesis by A1, A4, FDIFF_1: 20;

    end;

    theorem :: FDIFF_6:47

    Z c= ( dom (((1 / 3) (#) (( #Z 3) * cos )) - cos )) implies (((1 / 3) (#) (( #Z 3) * cos )) - cos ) is_differentiable_on Z & for x st x in Z holds (((((1 / 3) (#) (( #Z 3) * cos )) - cos ) `| Z) . x) = (( sin . x) |^ 3)

    proof

      assume

       A1: Z c= ( dom (((1 / 3) (#) (( #Z 3) * cos )) - cos ));

      then Z c= (( dom ((1 / 3) (#) (( #Z 3) * cos ))) /\ ( dom cos )) by VALUED_1: 12;

      then

       A2: Z c= ( dom ((1 / 3) (#) (( #Z 3) * cos ))) by XBOOLE_1: 18;

      then

       A3: ((1 / 3) (#) (( #Z 3) * cos )) is_differentiable_on Z by Th46;

      

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

      now

        let x;

        assume

         A5: x in Z;

        

        then (((((1 / 3) (#) (( #Z 3) * cos )) - cos ) `| Z) . x) = (( diff (((1 / 3) (#) (( #Z 3) * cos )),x)) - ( diff ( cos ,x))) by A1, A3, A4, FDIFF_1: 19

        .= (( diff (((1 / 3) (#) (( #Z 3) * cos )),x)) - ( - ( sin . x))) by SIN_COS: 63

        .= (((((1 / 3) (#) (( #Z 3) * cos )) `| Z) . x) - ( - ( sin . x))) by A3, A5, FDIFF_1:def 7

        .= (( - ((( cos . x) #Z (3 - 1)) * ( sin . x))) - ( - ( sin . x))) by A2, A5, Th46

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

        .= (( sin . x) * (1 - (( cos . x) |^ |.2.|))) by PREPOWER:def 3

        .= (( sin . x) * (1 - (( cos . x) |^ 2))) by ABSVALUE:def 1

        .= (( sin . x) * (1 - (( cos . x) * ( cos . x)))) by WSIERP_1: 1

        .= (( sin . x) * (((( cos . x) * ( cos . x)) + (( sin . x) * ( sin . x))) - (( cos . x) * ( cos . x)))) by SIN_COS: 28

        .= (( sin . x) * (( sin . x) |^ 2)) by WSIERP_1: 1

        .= (( sin . x) |^ (2 + 1)) by NEWTON: 6

        .= (( sin . x) |^ 3);

        hence (((((1 / 3) (#) (( #Z 3) * cos )) - cos ) `| Z) . x) = (( sin . x) |^ 3);

      end;

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

    end;

    theorem :: FDIFF_6:48

    Z c= ( dom ( sin - ((1 / 3) (#) (( #Z 3) * sin )))) implies ( sin - ((1 / 3) (#) (( #Z 3) * sin ))) is_differentiable_on Z & for x st x in Z holds ((( sin - ((1 / 3) (#) (( #Z 3) * sin ))) `| Z) . x) = (( cos . x) |^ 3)

    proof

      assume

       A1: Z c= ( dom ( sin - ((1 / 3) (#) (( #Z 3) * sin ))));

      then Z c= (( dom ((1 / 3) (#) (( #Z 3) * sin ))) /\ ( dom sin )) by VALUED_1: 12;

      then

       A2: Z c= ( dom ((1 / 3) (#) (( #Z 3) * sin ))) by XBOOLE_1: 18;

      then

       A3: ((1 / 3) (#) (( #Z 3) * sin )) is_differentiable_on Z by FDIFF_4: 54;

      

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

      now

        let x;

        assume

         A5: x in Z;

        

        then ((( sin - ((1 / 3) (#) (( #Z 3) * sin ))) `| Z) . x) = (( diff ( sin ,x)) - ( diff (((1 / 3) (#) (( #Z 3) * sin )),x))) by A1, A3, A4, FDIFF_1: 19

        .= (( cos . x) - ( diff (((1 / 3) (#) (( #Z 3) * sin )),x))) by SIN_COS: 64

        .= (( cos . x) - ((((1 / 3) (#) (( #Z 3) * sin )) `| Z) . x)) by A3, A5, FDIFF_1:def 7

        .= (( cos . x) - ((( sin . x) #Z (3 - 1)) * ( cos . x))) by A2, A5, FDIFF_4: 54

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

        .= (( cos . x) * (1 - (( sin . x) |^ |.2.|))) by PREPOWER:def 3

        .= (( cos . x) * (1 - (( sin . x) |^ 2))) by ABSVALUE:def 1

        .= (( cos . x) * (1 - (( sin . x) * ( sin . x)))) by WSIERP_1: 1

        .= (( cos . x) * (((( cos . x) * ( cos . x)) + (( sin . x) * ( sin . x))) - (( sin . x) * ( sin . x)))) by SIN_COS: 28

        .= (( cos . x) * (( cos . x) |^ 2)) by WSIERP_1: 1

        .= (( cos . x) |^ (2 + 1)) by NEWTON: 6

        .= (( cos . x) |^ 3);

        hence ((( sin - ((1 / 3) (#) (( #Z 3) * sin ))) `| Z) . x) = (( cos . x) |^ 3);

      end;

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

    end;

    theorem :: FDIFF_6:49

    Z c= ( dom ( sin * ln )) implies ( sin * ln ) is_differentiable_on Z & for x st x in Z holds ((( sin * ln ) `| Z) . x) = (( cos . ( log ( number_e ,x))) / x)

    proof

      assume

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

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

      then

       A2: Z c= ( dom ln ) by TARSKI:def 3;

      then

       A3: ln is_differentiable_on Z by FDIFF_1: 26, TAYLOR_1: 18;

      

       A4: for x st x in Z holds ( sin * ln ) is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then

         A5: ln is_differentiable_in x by A3, FDIFF_1: 9;

         sin is_differentiable_in ( ln . x) by SIN_COS: 64;

        hence thesis by A5, FDIFF_2: 13;

      end;

      then

       A6: ( sin * ln ) is_differentiable_on Z by A1, FDIFF_1: 9;

      for x st x in Z holds ((( sin * ln ) `| Z) . x) = (( cos . ( log ( number_e ,x))) / x)

      proof

        let x;

        

         A7: sin is_differentiable_in ( ln . x) by SIN_COS: 64;

        assume

         A8: x in Z;

        then

         A9: x in ( right_open_halfline 0 ) by A1, FUNCT_1: 11, TAYLOR_1: 18;

         ln is_differentiable_in x by A3, A8, FDIFF_1: 9;

        

        then ( diff (( sin * ln ),x)) = (( diff ( sin ,( ln . x))) * ( diff ( ln ,x))) by A7, FDIFF_2: 13

        .= (( cos . ( ln . x)) * ( diff ( ln ,x))) by SIN_COS: 64

        .= (( cos . ( log ( number_e ,x))) * ( diff ( ln ,x))) by A9, TAYLOR_1:def 2

        .= (( cos . ( log ( number_e ,x))) * (1 / x)) by A2, A8, TAYLOR_1: 18

        .= (( cos . ( log ( number_e ,x))) / x) by XCMPLX_1: 99;

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

      end;

      hence thesis by A1, A4, FDIFF_1: 9;

    end;

    theorem :: FDIFF_6:50

    Z c= ( dom ( - ( cos * ln ))) implies ( - ( cos * ln )) is_differentiable_on Z & for x st x in Z holds ((( - ( cos * ln )) `| Z) . x) = (( sin . ( log ( number_e ,x))) / x)

    proof

      assume

       A1: Z c= ( dom ( - ( cos * ln )));

      then

       A2: Z c= ( dom ( cos * ln )) by VALUED_1: 8;

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

      then

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

      then

       A4: ln is_differentiable_on Z by FDIFF_1: 26, TAYLOR_1: 18;

      for x st x in Z holds ( cos * ln ) is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then

         A5: ln is_differentiable_in x by A4, FDIFF_1: 9;

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

        hence thesis by A5, FDIFF_2: 13;

      end;

      then

       A6: ( cos * ln ) is_differentiable_on Z by A2, FDIFF_1: 9;

      

       A7: for x st x in Z holds ((( - ( cos * ln )) `| Z) . x) = (( sin . ( log ( number_e ,x))) / x)

      proof

        let x;

        

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

        assume

         A9: x in Z;

        then

         A10: x in ( right_open_halfline 0 ) by A2, FUNCT_1: 11, TAYLOR_1: 18;

        

         A11: ln is_differentiable_in x by A4, A9, FDIFF_1: 9;

        ((( - ( cos * ln )) `| Z) . x) = (( - 1) * ( diff (( cos * ln ),x))) by A1, A6, A9, FDIFF_1: 20

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

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

        .= ((( - 1) * ( - ( sin . ( ln . x)))) * ( diff ( ln ,x)))

        .= ((( - 1) * ( - ( sin . ( log ( number_e ,x))))) * ( diff ( ln ,x))) by A10, TAYLOR_1:def 2

        .= ((( - 1) * ( - ( sin . ( log ( number_e ,x))))) * (1 / x)) by A3, A9, TAYLOR_1: 18

        .= (( sin . ( log ( number_e ,x))) / x) by XCMPLX_1: 99;

        hence thesis;

      end;

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

      hence thesis by A6, A7, FDIFF_1: 20;

    end;