diff_4.miz



    begin

    reserve n,m,i,p for Nat,

h,k,r,r1,r2,x,x0,x1,x2,x3 for Real;

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

    theorem :: DIFF_4:1

    

     Th1: x0 > 0 & x1 > 0 implies (( log ( number_e ,x0)) - ( log ( number_e ,x1))) = ( log ( number_e ,(x0 / x1)))

    proof

      assume

       A1: x0 > 0 & x1 > 0 ;

       number_e > 1 by TAYLOR_1: 11, XXREAL_0: 2;

      hence thesis by A1, POWER: 54;

    end;

    theorem :: DIFF_4:2

    x0 > 0 & x1 > 0 implies (( log ( number_e ,x0)) + ( log ( number_e ,x1))) = ( log ( number_e ,(x0 * x1)))

    proof

      assume

       A1: x0 > 0 & x1 > 0 ;

       number_e > 1 by TAYLOR_1: 11, XXREAL_0: 2;

      hence thesis by A1, POWER: 53;

    end;

    theorem :: DIFF_4:3

    

     Th3: x > 0 implies ( log ( number_e ,x)) = ( ln . x)

    proof

      assume

       A1: x > 0 ;

      x in ( right_open_halfline 0 )

      proof

        x in { g where g be Real : 0 < g } by A1;

        hence thesis by XXREAL_1: 230;

      end;

      hence thesis by TAYLOR_1:def 2;

    end;

    theorem :: DIFF_4:4

    

     Th4: x0 > 0 & x1 > 0 implies (( ln . x0) - ( ln . x1)) = ( ln . (x0 / x1))

    proof

      assume

       A1: x0 > 0 & x1 > 0 ;

      

       A2: ( log ( number_e ,(x0 / x1))) = ( ln . (x0 / x1))

      proof

        (x0 / x1) in ( right_open_halfline 0 )

        proof

          (x0 / x1) in { g where g be Real : 0 < g } by A1;

          hence thesis by XXREAL_1: 230;

        end;

        hence thesis by TAYLOR_1:def 2;

      end;

      (( ln . x0) - ( ln . x1)) = (( log ( number_e ,x0)) - ( ln . x1)) by A1, Th3

      .= (( log ( number_e ,x0)) - ( log ( number_e ,x1))) by A1, Th3

      .= ( log ( number_e ,(x0 / x1))) by A1, Th1;

      hence thesis by A2;

    end;

    theorem :: DIFF_4:5

    (for x holds (f . x) = (k / (x ^2 ))) & x0 <> 0 & x1 <> 0 & x2 <> 0 & x3 <> 0 & (x0,x1,x2,x3) are_mutually_distinct implies [!f, x0, x1, x2, x3!] = ((k * (((1 / ((x1 * x2) * x0)) * (((1 / x0) + (1 / x2)) + (1 / x1))) - ((1 / ((x2 * x1) * x3)) * (((1 / x3) + (1 / x1)) + (1 / x2))))) / (x0 - x3))

    proof

      assume that

       A1: for x holds (f . x) = (k / (x ^2 )) and

       A2: x0 <> 0 & x1 <> 0 & x2 <> 0 & x3 <> 0 and

       A3: (x0,x1,x2,x3) are_mutually_distinct ;

      x0 <> x1 & x0 <> x2 & x1 <> x2 by A3, ZFMISC_1:def 6;

      then (x0,x1,x2) are_mutually_distinct by ZFMISC_1:def 5;

      

      then

       A4: [!f, x0, x1, x2!] = ((k / ((x0 * x1) * x2)) * (((1 / x0) + (1 / x1)) + (1 / x2))) by A1, A2, DIFF_3: 49

      .= ((k * (1 / ((x1 * x2) * x0))) * (((1 / x0) + (1 / x2)) + (1 / x1)));

      x1 <> x2 & x1 <> x3 & x2 <> x3 by A3, ZFMISC_1:def 6;

      then (x1,x2,x3) are_mutually_distinct by ZFMISC_1:def 5;

      then [!f, x1, x2, x3!] = ((k / ((x1 * x2) * x3)) * (((1 / x1) + (1 / x2)) + (1 / x3))) by A1, A2, DIFF_3: 49;

      hence thesis by A4;

    end;

    theorem :: DIFF_4:6

    x0 in ( dom cot ) & x1 in ( dom cot ) implies [!( cot (#) cot ), x0, x1!] = ( - (((( cos x1) ^2 ) - (( cos x0) ^2 )) / (((( sin x0) * ( sin x1)) ^2 ) * (x0 - x1))))

    proof

      assume that

       A1: x0 in ( dom cot ) & x1 in ( dom cot );

      

       A2: ( sin x0) <> 0 & ( sin x1) <> 0 by A1, FDIFF_8: 2;

       [!( cot (#) cot ), x0, x1!] = (((( cot . x0) * ( cot . x0)) - (( cot (#) cot ) . x1)) / (x0 - x1)) by VALUED_1: 5

      .= (((( cot . x0) * ( cot . x0)) - (( cot . x1) * ( cot . x1))) / (x0 - x1)) by VALUED_1: 5

      .= ((((( cos . x0) * (( sin . x0) " )) * ( cot . x0)) - (( cot . x1) * ( cot . x1))) / (x0 - x1)) by A1, RFUNCT_1:def 1

      .= ((((( cos . x0) * (( sin . x0) " )) * (( cos . x0) * (( sin . x0) " ))) - (( cot . x1) * ( cot . x1))) / (x0 - x1)) by A1, RFUNCT_1:def 1

      .= ((((( cos . x0) * (( sin . x0) " )) * (( cos . x0) * (( sin . x0) " ))) - ((( cos . x1) * (( sin . x1) " )) * ( cot . x1))) / (x0 - x1)) by A1, RFUNCT_1:def 1

      .= (((( cot x0) ^2 ) - (( cot x1) ^2 )) / (x0 - x1)) by A1, RFUNCT_1:def 1

      .= (((( cot x0) - ( cot x1)) * (( cot x0) + ( cot x1))) / (x0 - x1))

      .= ((( - (( sin (x0 - x1)) / (( sin x0) * ( sin x1)))) * (( cot x0) + ( cot x1))) / (x0 - x1)) by A2, SIN_COS4: 24

      .= (( - ((( sin (x0 - x1)) / (( sin x0) * ( sin x1))) * (( cot x0) + ( cot x1)))) / (x0 - x1))

      .= (( - ((( sin (x0 - x1)) / (( sin x0) * ( sin x1))) * (( sin (x0 + x1)) / (( sin x0) * ( sin x1))))) / (x0 - x1)) by A2, SIN_COS4: 23

      .= (( - ((( sin (x0 + x1)) * ( sin (x0 - x1))) / ((( sin x0) * ( sin x1)) ^2 ))) / (x0 - x1)) by XCMPLX_1: 76

      .= (( - (((( cos x1) ^2 ) - (( cos x0) ^2 )) / ((( sin x0) * ( sin x1)) ^2 ))) / (x0 - x1)) by SIN_COS4: 38

      .= ( - ((((( cos x1) ^2 ) - (( cos x0) ^2 )) / ((( sin x0) * ( sin x1)) ^2 )) / (x0 - x1)))

      .= ( - (((( cos x1) ^2 ) - (( cos x0) ^2 )) / (((( sin x0) * ( sin x1)) ^2 ) * (x0 - x1)))) by XCMPLX_1: 78;

      hence thesis;

    end;

    theorem :: DIFF_4:7

    x in ( dom cot ) & (x + h) in ( dom cot ) implies (( fD (( cot (#) cot ),h)) . x) = (((1 / 2) * (( cos (2 * (x + h))) - ( cos (2 * x)))) / ((( sin (x + h)) * ( sin x)) ^2 ))

    proof

      set f = ( cot (#) cot );

      assume

       A1: x in ( dom cot ) & (x + h) in ( dom cot );

      

       A2: ( sin x) <> 0 & ( sin (x + h)) <> 0 by A1, FDIFF_8: 2;

      x in ( dom f) & (x + h) in ( dom f)

      proof

        x in (( dom cot ) /\ ( dom cot )) & (x + h) in (( dom cot ) /\ ( dom cot )) by A1;

        hence thesis by VALUED_1:def 4;

      end;

      

      then (( fD (f,h)) . x) = ((( cot (#) cot ) . (x + h)) - (( cot (#) cot ) . x)) by DIFF_1: 1

      .= ((( cot . (x + h)) * ( cot . (x + h))) - (( cot (#) cot ) . x)) by VALUED_1: 5

      .= ((( cot . (x + h)) * ( cot . (x + h))) - (( cot . x) * ( cot . x))) by VALUED_1: 5

      .= (((( cos . (x + h)) * (( sin . (x + h)) " )) * ( cot . (x + h))) - (( cot . x) * ( cot . x))) by A1, RFUNCT_1:def 1

      .= (((( cos . (x + h)) * (( sin . (x + h)) " )) * (( cos . (x + h)) * (( sin . (x + h)) " ))) - (( cot . x) * ( cot . x))) by A1, RFUNCT_1:def 1

      .= (((( cos . (x + h)) * (( sin . (x + h)) " )) * (( cos . (x + h)) * (( sin . (x + h)) " ))) - ((( cos . x) * (( sin . x) " )) * ( cot . x))) by A1, RFUNCT_1:def 1

      .= ((( cot (x + h)) ^2 ) - (( cot x) ^2 )) by A1, RFUNCT_1:def 1

      .= ((( cot (x + h)) - ( cot x)) * (( cot (x + h)) + ( cot x)))

      .= (( - (( sin ((x + h) - x)) / (( sin (x + h)) * ( sin x)))) * (( cot (x + h)) + ( cot x))) by A2, SIN_COS4: 24

      .= (( - (( sin ((x + h) - x)) / (( sin (x + h)) * ( sin x)))) * (( sin ((x + h) + x)) / (( sin (x + h)) * ( sin x)))) by A2, SIN_COS4: 23

      .= ( - ((( sin ((x + h) - x)) / (( sin (x + h)) * ( sin x))) * (( sin ((x + h) + x)) / (( sin (x + h)) * ( sin x)))))

      .= ( - ((( sin ((2 * x) + h)) * ( sin h)) / ((( sin (x + h)) * ( sin x)) ^2 ))) by XCMPLX_1: 76

      .= ( - (( - ((1 / 2) * (( cos (((2 * x) + h) + h)) - ( cos (((2 * x) + h) - h))))) / ((( sin (x + h)) * ( sin x)) ^2 ))) by SIN_COS4: 29

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

      hence thesis;

    end;

    theorem :: DIFF_4:8

    x in ( dom cot ) & (x - h) in ( dom cot ) implies (( bD (( cot (#) cot ),h)) . x) = (((1 / 2) * (( cos (2 * x)) - ( cos (2 * (h - x))))) / ((( sin x) * ( sin (x - h))) ^2 ))

    proof

      set f = ( cot (#) cot );

      assume

       A1: x in ( dom cot ) & (x - h) in ( dom cot );

      

       A2: ( sin x) <> 0 & ( sin (x - h)) <> 0 by A1, FDIFF_8: 2;

      x in ( dom f) & (x - h) in ( dom f)

      proof

        x in (( dom cot ) /\ ( dom cot )) & (x - h) in (( dom cot ) /\ ( dom cot )) by A1;

        hence thesis by VALUED_1:def 4;

      end;

      

      then (( bD (f,h)) . x) = ((( cot (#) cot ) . x) - (( cot (#) cot ) . (x - h))) by DIFF_1: 38

      .= ((( cot . x) * ( cot . x)) - (( cot (#) cot ) . (x - h))) by VALUED_1: 5

      .= ((( cot . x) * ( cot . x)) - (( cot . (x - h)) * ( cot . (x - h)))) by VALUED_1: 5

      .= (((( cos . x) * (( sin . x) " )) * ( cot . x)) - (( cot . (x - h)) * ( cot . (x - h)))) by A1, RFUNCT_1:def 1

      .= (((( cos . x) * (( sin . x) " )) * (( cos . x) * (( sin . x) " ))) - (( cot . (x - h)) * ( cot . (x - h)))) by A1, RFUNCT_1:def 1

      .= (((( cos . x) * (( sin . x) " )) * (( cos . x) * (( sin . x) " ))) - ((( cos . (x - h)) * (( sin . (x - h)) " )) * ( cot . (x - h)))) by A1, RFUNCT_1:def 1

      .= ((( cot x) ^2 ) - (( cot (x - h)) ^2 )) by A1, RFUNCT_1:def 1

      .= ((( cot x) - ( cot (x - h))) * (( cot x) + ( cot (x - h))))

      .= (( - (( sin (x - (x - h))) / (( sin x) * ( sin (x - h))))) * (( cot x) + ( cot (x - h)))) by A2, SIN_COS4: 24

      .= ( - ((( sin (x - (x - h))) / (( sin x) * ( sin (x - h)))) * (( cot x) + ( cot (x - h)))))

      .= ( - ((( sin h) / (( sin x) * ( sin (x - h)))) * (( sin (x + (x - h))) / (( sin x) * ( sin (x - h)))))) by A2, SIN_COS4: 23

      .= ( - ((( sin h) * ( sin ((2 * x) - h))) / ((( sin x) * ( sin (x - h))) ^2 ))) by XCMPLX_1: 76

      .= ( - (( - ((1 / 2) * (( cos (h + ((2 * x) - h))) - ( cos (h - ((2 * x) - h)))))) / ((( sin x) * ( sin (x - h))) ^2 ))) by SIN_COS4: 29

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

      hence thesis;

    end;

    theorem :: DIFF_4:9

    (x + (h / 2)) in ( dom cot ) & (x - (h / 2)) in ( dom cot ) implies (( cD (( cot (#) cot ),h)) . x) = (((1 / 2) * (( cos (h + (2 * x))) - ( cos (h - (2 * x))))) / ((( sin (x + (h / 2))) * ( sin (x - (h / 2)))) ^2 ))

    proof

      set f = ( cot (#) cot );

      assume

       A1: (x + (h / 2)) in ( dom cot ) & (x - (h / 2)) in ( dom cot );

      

       A2: ( sin (x + (h / 2))) <> 0 & ( sin (x - (h / 2))) <> 0 by A1, FDIFF_8: 2;

      (x + (h / 2)) in ( dom f) & (x - (h / 2)) in ( dom f)

      proof

        (x + (h / 2)) in (( dom cot ) /\ ( dom cot )) & (x - (h / 2)) in (( dom cot ) /\ ( dom cot )) by A1;

        hence thesis by VALUED_1:def 4;

      end;

      

      then (( cD (f,h)) . x) = ((( cot (#) cot ) . (x + (h / 2))) - (( cot (#) cot ) . (x - (h / 2)))) by DIFF_1: 39

      .= ((( cot . (x + (h / 2))) * ( cot . (x + (h / 2)))) - (( cot (#) cot ) . (x - (h / 2)))) by VALUED_1: 5

      .= ((( cot . (x + (h / 2))) * ( cot . (x + (h / 2)))) - (( cot . (x - (h / 2))) * ( cot . (x - (h / 2))))) by VALUED_1: 5

      .= (((( cos . (x + (h / 2))) * (( sin . (x + (h / 2))) " )) * ( cot . (x + (h / 2)))) - (( cot . (x - (h / 2))) * ( cot . (x - (h / 2))))) by A1, RFUNCT_1:def 1

      .= (((( cos . (x + (h / 2))) * (( sin . (x + (h / 2))) " )) * (( cos . (x + (h / 2))) * (( sin . (x + (h / 2))) " ))) - (( cot . (x - (h / 2))) * ( cot . (x - (h / 2))))) by A1, RFUNCT_1:def 1

      .= (((( cos . (x + (h / 2))) * (( sin . (x + (h / 2))) " )) * (( cos . (x + (h / 2))) * (( sin . (x + (h / 2))) " ))) - ((( cos . (x - (h / 2))) * (( sin . (x - (h / 2))) " )) * ( cot . (x - (h / 2))))) by A1, RFUNCT_1:def 1

      .= ((( cot (x + (h / 2))) ^2 ) - (( cot (x - (h / 2))) ^2 )) by A1, RFUNCT_1:def 1

      .= ((( cot (x + (h / 2))) - ( cot (x - (h / 2)))) * (( cot (x + (h / 2))) + ( cot (x - (h / 2)))))

      .= (( - (( sin ((x + (h / 2)) - (x - (h / 2)))) / (( sin (x + (h / 2))) * ( sin (x - (h / 2)))))) * (( cot (x + (h / 2))) + ( cot (x - (h / 2))))) by A2, SIN_COS4: 24

      .= (( - (( sin h) / (( sin (x + (h / 2))) * ( sin (x - (h / 2)))))) * (( sin ((x + (h / 2)) + (x - (h / 2)))) / (( sin (x + (h / 2))) * ( sin (x - (h / 2)))))) by A2, SIN_COS4: 23

      .= ( - ((( sin h) / (( sin (x + (h / 2))) * ( sin (x - (h / 2))))) * (( sin ((x + (h / 2)) + (x - (h / 2)))) / (( sin (x + (h / 2))) * ( sin (x - (h / 2)))))))

      .= ( - ((( sin h) * ( sin (2 * x))) / ((( sin (x + (h / 2))) * ( sin (x - (h / 2)))) ^2 ))) by XCMPLX_1: 76

      .= ( - (( - ((1 / 2) * (( cos (h + (2 * x))) - ( cos (h - (2 * x)))))) / ((( sin (x + (h / 2))) * ( sin (x - (h / 2)))) ^2 ))) by SIN_COS4: 29

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

      hence thesis;

    end;

    theorem :: DIFF_4:10

    x0 in ( dom cosec ) & x1 in ( dom cosec ) implies [!( cosec (#) cosec ), x0, x1!] = ((4 * (( sin (x1 + x0)) * ( sin (x1 - x0)))) / (((( cos (x0 + x1)) - ( cos (x0 - x1))) ^2 ) * (x0 - x1)))

    proof

      assume

       A1: x0 in ( dom cosec ) & x1 in ( dom cosec );

      

       A2: ( sin . x0) <> 0 & ( sin . x1) <> 0 by A1, RFUNCT_1: 3;

       [!( cosec (#) cosec ), x0, x1!] = (((( cosec . x0) * ( cosec . x0)) - (( cosec (#) cosec ) . x1)) / (x0 - x1)) by VALUED_1: 5

      .= (((( cosec . x0) * ( cosec . x0)) - (( cosec . x1) * ( cosec . x1))) / (x0 - x1)) by VALUED_1: 5

      .= ((((( sin . x0) " ) * ( cosec . x0)) - (( cosec . x1) * ( cosec . x1))) / (x0 - x1)) by A1, RFUNCT_1:def 2

      .= ((((( sin . x0) " ) * (( sin . x0) " )) - (( cosec . x1) * ( cosec . x1))) / (x0 - x1)) by A1, RFUNCT_1:def 2

      .= ((((( sin . x0) " ) * (( sin . x0) " )) - ((( sin . x1) " ) * ( cosec . x1))) / (x0 - x1)) by A1, RFUNCT_1:def 2

      .= ((((( sin . x0) " ) ^2 ) - ((( sin . x1) " ) ^2 )) / (x0 - x1)) by A1, RFUNCT_1:def 2

      .= ((((1 / ( sin . x0)) - (1 / ( sin . x1))) * ((1 / ( sin . x0)) + (1 / ( sin . x1)))) / (x0 - x1))

      .= (((((1 * ( sin . x1)) - (1 * ( sin . x0))) / (( sin . x0) * ( sin . x1))) * ((1 / ( sin . x0)) + (1 / ( sin . x1)))) / (x0 - x1)) by A2, XCMPLX_1: 130

      .= ((((( sin . x1) - ( sin . x0)) / (( sin . x0) * ( sin . x1))) * ((( sin . x1) + ( sin . x0)) / (( sin . x0) * ( sin . x1)))) / (x0 - x1)) by A2, XCMPLX_1: 116

      .= ((((( sin . x1) - ( sin . x0)) * (( sin . x1) + ( sin . x0))) / ((( sin . x0) * ( sin . x1)) * (( sin . x0) * ( sin . x1)))) / (x0 - x1)) by XCMPLX_1: 76

      .= ((((( sin x1) * ( sin x1)) - (( sin x0) * ( sin x0))) / ((( sin x0) * ( sin x1)) ^2 )) / (x0 - x1))

      .= (((( sin (x1 + x0)) * ( sin (x1 - x0))) / ((( sin x0) * ( sin x1)) ^2 )) / (x0 - x1)) by SIN_COS4: 37

      .= (((( sin (x1 + x0)) * ( sin (x1 - x0))) / (( - ((1 / 2) * (( cos (x0 + x1)) - ( cos (x0 - x1))))) ^2 )) / (x0 - x1)) by SIN_COS4: 29

      .= (((1 * (( sin (x1 + x0)) * ( sin (x1 - x0)))) / ((1 / 4) * ((( cos (x0 + x1)) - ( cos (x0 - x1))) ^2 ))) / (x0 - x1))

      .= (((1 / (1 / 4)) * ((( sin (x1 + x0)) * ( sin (x1 - x0))) / ((( cos (x0 + x1)) - ( cos (x0 - x1))) ^2 ))) / (x0 - x1)) by XCMPLX_1: 76

      .= (((4 * (( sin (x1 + x0)) * ( sin (x1 - x0)))) / ((( cos (x0 + x1)) - ( cos (x0 - x1))) ^2 )) / (x0 - x1))

      .= ((4 * (( sin (x1 + x0)) * ( sin (x1 - x0)))) / (((( cos (x0 + x1)) - ( cos (x0 - x1))) ^2 ) * (x0 - x1))) by XCMPLX_1: 78;

      hence thesis;

    end;

    theorem :: DIFF_4:11

    x in ( dom cosec ) & (x + h) in ( dom cosec ) implies (( fD (( cosec (#) cosec ),h)) . x) = ( - (((4 * ( sin ((2 * x) + h))) * ( sin h)) / ((( cos ((2 * x) + h)) - ( cos h)) ^2 )))

    proof

      set f = ( cosec (#) cosec );

      assume

       A1: x in ( dom cosec ) & (x + h) in ( dom cosec );

      

       A2: ( sin . x) <> 0 & ( sin . (x + h)) <> 0 by A1, RFUNCT_1: 3;

      x in ( dom f) & (x + h) in ( dom f)

      proof

        x in (( dom cosec ) /\ ( dom cosec )) & (x + h) in (( dom cosec ) /\ ( dom cosec )) by A1;

        hence thesis by VALUED_1:def 4;

      end;

      

      then (( fD (f,h)) . x) = ((( cosec (#) cosec ) . (x + h)) - (( cosec (#) cosec ) . x)) by DIFF_1: 1

      .= ((( cosec . (x + h)) * ( cosec . (x + h))) - (( cosec (#) cosec ) . x)) by VALUED_1: 5

      .= ((( cosec . (x + h)) * ( cosec . (x + h))) - (( cosec . x) * ( cosec . x))) by VALUED_1: 5

      .= (((( sin . (x + h)) " ) * ( cosec . (x + h))) - (( cosec . x) * ( cosec . x))) by A1, RFUNCT_1:def 2

      .= (((( sin . (x + h)) " ) * (( sin . (x + h)) " )) - (( cosec . x) * ( cosec . x))) by A1, RFUNCT_1:def 2

      .= (((( sin . (x + h)) " ) * (( sin . (x + h)) " )) - ((( sin . x) " ) * ( cosec . x))) by A1, RFUNCT_1:def 2

      .= (((( sin . (x + h)) " ) ^2 ) - ((( sin . x) " ) ^2 )) by A1, RFUNCT_1:def 2

      .= (((1 / ( sin . (x + h))) - (1 / ( sin . x))) * ((1 / ( sin . (x + h))) + (1 / ( sin . x))))

      .= ((((1 * ( sin . x)) - (1 * ( sin . (x + h)))) / (( sin . (x + h)) * ( sin . x))) * ((1 / ( sin . (x + h))) + (1 / ( sin . x)))) by A2, XCMPLX_1: 130

      .= (((( sin . x) - ( sin . (x + h))) / (( sin . (x + h)) * ( sin . x))) * ((( sin . x) + ( sin . (x + h))) / (( sin . (x + h)) * ( sin . x)))) by A2, XCMPLX_1: 116

      .= (((( sin . x) - ( sin . (x + h))) * (( sin . x) + ( sin . (x + h)))) / ((( sin . (x + h)) * ( sin . x)) * (( sin . (x + h)) * ( sin . x)))) by XCMPLX_1: 76

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

      .= ((( sin (x + (x + h))) * ( sin (x - (x + h)))) / ((( sin (x + h)) * ( sin x)) ^2 )) by SIN_COS4: 37

      .= ((( sin ((2 * x) + h)) * ( sin ( - h))) / (( - ((1 / 2) * (( cos ((x + h) + x)) - ( cos ((x + h) - x))))) ^2 )) by SIN_COS4: 29

      .= ((( sin ((2 * x) + h)) * ( - ( sin h))) / ((1 / 4) * ((( cos ((2 * x) + h)) - ( cos h)) ^2 ))) by SIN_COS: 31

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

      .= ( - ((1 / (1 / 4)) * ((( sin ((2 * x) + h)) * ( sin h)) / ((( cos ((2 * x) + h)) - ( cos h)) ^2 )))) by XCMPLX_1: 76

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

      hence thesis;

    end;

    theorem :: DIFF_4:12

    x in ( dom cosec ) & (x - h) in ( dom cosec ) implies (( bD (( cosec (#) cosec ),h)) . x) = ( - (((4 * ( sin ((2 * x) - h))) * ( sin h)) / ((( cos ((2 * x) - h)) - ( cos h)) ^2 )))

    proof

      set f = ( cosec (#) cosec );

      assume

       A1: x in ( dom cosec ) & (x - h) in ( dom cosec );

      

       A2: ( sin . x) <> 0 & ( sin . (x - h)) <> 0 by A1, RFUNCT_1: 3;

      x in ( dom f) & (x - h) in ( dom f)

      proof

        x in (( dom cosec ) /\ ( dom cosec )) & (x - h) in (( dom cosec ) /\ ( dom cosec )) by A1;

        hence thesis by VALUED_1:def 4;

      end;

      

      then (( bD (f,h)) . x) = ((( cosec (#) cosec ) . x) - (( cosec (#) cosec ) . (x - h))) by DIFF_1: 38

      .= ((( cosec . x) * ( cosec . x)) - (( cosec (#) cosec ) . (x - h))) by VALUED_1: 5

      .= ((( cosec . x) * ( cosec . x)) - (( cosec . (x - h)) * ( cosec . (x - h)))) by VALUED_1: 5

      .= (((( sin . x) " ) * ( cosec . x)) - (( cosec . (x - h)) * ( cosec . (x - h)))) by A1, RFUNCT_1:def 2

      .= (((( sin . x) " ) * (( sin . x) " )) - (( cosec . (x - h)) * ( cosec . (x - h)))) by A1, RFUNCT_1:def 2

      .= (((( sin . x) " ) * (( sin . x) " )) - ((( sin . (x - h)) " ) * ( cosec . (x - h)))) by A1, RFUNCT_1:def 2

      .= (((( sin . x) " ) ^2 ) - ((( sin . (x - h)) " ) ^2 )) by A1, RFUNCT_1:def 2

      .= (((1 / ( sin . x)) - (1 / ( sin . (x - h)))) * ((1 / ( sin . x)) + (1 / ( sin . (x - h)))))

      .= ((((1 * ( sin . (x - h))) - (1 * ( sin . x))) / (( sin . x) * ( sin . (x - h)))) * ((1 / ( sin . x)) + (1 / ( sin . (x - h))))) by A2, XCMPLX_1: 130

      .= (((( sin . (x - h)) - ( sin . x)) / (( sin . x) * ( sin . (x - h)))) * ((( sin . (x - h)) + ( sin . x)) / (( sin . x) * ( sin . (x - h))))) by A2, XCMPLX_1: 116

      .= (((( sin . (x - h)) - ( sin . x)) * (( sin . (x - h)) + ( sin . x))) / ((( sin . x) * ( sin . (x - h))) * (( sin . x) * ( sin . (x - h))))) by XCMPLX_1: 76

      .= (((( sin (x - h)) * ( sin (x - h))) - (( sin x) * ( sin x))) / ((( sin x) * ( sin (x - h))) ^2 ))

      .= ((( sin ((x - h) + x)) * ( sin ((x - h) - x))) / ((( sin x) * ( sin (x - h))) ^2 )) by SIN_COS4: 37

      .= ((( sin ((2 * x) - h)) * ( sin ( - h))) / (( - ((1 / 2) * (( cos (x + (x - h))) - ( cos (x - (x - h)))))) ^2 )) by SIN_COS4: 29

      .= ((( sin ((2 * x) - h)) * ( - ( sin h))) / ((1 / 4) * ((( cos ((2 * x) - h)) - ( cos h)) ^2 ))) by SIN_COS: 31

      .= ( - ((1 * (( sin ((2 * x) - h)) * ( sin h))) / ((1 / 4) * ((( cos ((2 * x) - h)) - ( cos h)) ^2 ))))

      .= ( - ((1 / (1 / 4)) * ((( sin ((2 * x) - h)) * ( sin h)) / ((( cos ((2 * x) - h)) - ( cos h)) ^2 )))) by XCMPLX_1: 76

      .= ( - (((4 * ( sin ((2 * x) - h))) * ( sin h)) / ((( cos ((2 * x) - h)) - ( cos h)) ^2 )));

      hence thesis;

    end;

    theorem :: DIFF_4:13

    (x + (h / 2)) in ( dom cosec ) & (x - (h / 2)) in ( dom cosec ) implies (( cD (( cosec (#) cosec ),h)) . x) = ( - (((4 * ( sin (2 * x))) * ( sin h)) / ((( cos (2 * x)) - ( cos h)) ^2 )))

    proof

      set f = ( cosec (#) cosec );

      assume

       A1: (x + (h / 2)) in ( dom cosec ) & (x - (h / 2)) in ( dom cosec );

      

       A2: ( sin . (x + (h / 2))) <> 0 & ( sin . (x - (h / 2))) <> 0 by A1, RFUNCT_1: 3;

      (x + (h / 2)) in ( dom f) & (x - (h / 2)) in ( dom f)

      proof

        (x + (h / 2)) in (( dom cosec ) /\ ( dom cosec )) & (x - (h / 2)) in (( dom cosec ) /\ ( dom cosec )) by A1;

        hence thesis by VALUED_1:def 4;

      end;

      

      then (( cD (f,h)) . x) = ((( cosec (#) cosec ) . (x + (h / 2))) - (( cosec (#) cosec ) . (x - (h / 2)))) by DIFF_1: 39

      .= ((( cosec . (x + (h / 2))) * ( cosec . (x + (h / 2)))) - (( cosec (#) cosec ) . (x - (h / 2)))) by VALUED_1: 5

      .= ((( cosec . (x + (h / 2))) * ( cosec . (x + (h / 2)))) - (( cosec . (x - (h / 2))) * ( cosec . (x - (h / 2))))) by VALUED_1: 5

      .= (((( sin . (x + (h / 2))) " ) * ( cosec . (x + (h / 2)))) - (( cosec . (x - (h / 2))) * ( cosec . (x - (h / 2))))) by A1, RFUNCT_1:def 2

      .= (((( sin . (x + (h / 2))) " ) * (( sin . (x + (h / 2))) " )) - (( cosec . (x - (h / 2))) * ( cosec . (x - (h / 2))))) by A1, RFUNCT_1:def 2

      .= (((( sin . (x + (h / 2))) " ) * (( sin . (x + (h / 2))) " )) - ((( sin . (x - (h / 2))) " ) * ( cosec . (x - (h / 2))))) by A1, RFUNCT_1:def 2

      .= (((( sin . (x + (h / 2))) " ) ^2 ) - ((( sin . (x - (h / 2))) " ) ^2 )) by A1, RFUNCT_1:def 2

      .= (((1 / ( sin . (x + (h / 2)))) - (1 / ( sin . (x - (h / 2))))) * ((1 / ( sin . (x + (h / 2)))) + (1 / ( sin . (x - (h / 2))))))

      .= ((((1 * ( sin . (x - (h / 2)))) - (1 * ( sin . (x + (h / 2))))) / (( sin . (x + (h / 2))) * ( sin . (x - (h / 2))))) * ((1 / ( sin . (x + (h / 2)))) + (1 / ( sin . (x - (h / 2)))))) by A2, XCMPLX_1: 130

      .= (((( sin . (x - (h / 2))) - ( sin . (x + (h / 2)))) / (( sin . (x + (h / 2))) * ( sin . (x - (h / 2))))) * ((( sin . (x - (h / 2))) + ( sin . (x + (h / 2)))) / (( sin . (x + (h / 2))) * ( sin . (x - (h / 2)))))) by A2, XCMPLX_1: 116

      .= (((( sin . (x - (h / 2))) - ( sin . (x + (h / 2)))) * (( sin . (x - (h / 2))) + ( sin . (x + (h / 2))))) / ((( sin . (x + (h / 2))) * ( sin . (x - (h / 2)))) * (( sin . (x + (h / 2))) * ( sin . (x - (h / 2)))))) by XCMPLX_1: 76

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

      .= ((( sin ((x - (h / 2)) + (x + (h / 2)))) * ( sin ((x - (h / 2)) - (x + (h / 2))))) / ((( sin (x + (h / 2))) * ( sin (x - (h / 2)))) ^2 )) by SIN_COS4: 37

      .= ((( sin (2 * x)) * ( sin ( - h))) / (( - ((1 / 2) * (( cos ((x + (h / 2)) + (x - (h / 2)))) - ( cos ((x + (h / 2)) - (x - (h / 2))))))) ^2 )) by SIN_COS4: 29

      .= ((( sin (2 * x)) * ( - ( sin h))) / ((1 / 4) * ((( cos (2 * x)) - ( cos h)) ^2 ))) by SIN_COS: 31

      .= ( - ((1 * (( sin (2 * x)) * ( sin h))) / ((1 / 4) * ((( cos (2 * x)) - ( cos h)) ^2 ))))

      .= ( - ((1 / (1 / 4)) * ((( sin (2 * x)) * ( sin h)) / ((( cos (2 * x)) - ( cos h)) ^2 )))) by XCMPLX_1: 76

      .= ( - (((4 * ( sin (2 * x))) * ( sin h)) / ((( cos (2 * x)) - ( cos h)) ^2 )));

      hence thesis;

    end;

    theorem :: DIFF_4:14

    x0 in ( dom sec ) & x1 in ( dom sec ) implies [!( sec (#) sec ), x0, x1!] = ((4 * (( sin (x0 + x1)) * ( sin (x0 - x1)))) / (((( cos (x0 + x1)) + ( cos (x0 - x1))) ^2 ) * (x0 - x1)))

    proof

      assume

       A1: x0 in ( dom sec ) & x1 in ( dom sec );

      

       A2: ( cos . x0) <> 0 & ( cos . x1) <> 0 by A1, RFUNCT_1: 3;

       [!( sec (#) sec ), x0, x1!] = (((( sec . x0) * ( sec . x0)) - (( sec (#) sec ) . x1)) / (x0 - x1)) by VALUED_1: 5

      .= (((( sec . x0) * ( sec . x0)) - (( sec . x1) * ( sec . x1))) / (x0 - x1)) by VALUED_1: 5

      .= ((((( cos . x0) " ) * ( sec . x0)) - (( sec . x1) * ( sec . x1))) / (x0 - x1)) by A1, RFUNCT_1:def 2

      .= ((((( cos . x0) " ) * (( cos . x0) " )) - (( sec . x1) * ( sec . x1))) / (x0 - x1)) by A1, RFUNCT_1:def 2

      .= ((((( cos . x0) " ) * (( cos . x0) " )) - ((( cos . x1) " ) * ( sec . x1))) / (x0 - x1)) by A1, RFUNCT_1:def 2

      .= ((((( cos . x0) " ) ^2 ) - ((( cos . x1) " ) ^2 )) / (x0 - x1)) by A1, RFUNCT_1:def 2

      .= ((((1 / ( cos . x0)) - (1 / ( cos . x1))) * ((1 / ( cos . x0)) + (1 / ( cos . x1)))) / (x0 - x1))

      .= (((((1 * ( cos . x1)) - (1 * ( cos . x0))) / (( cos . x0) * ( cos . x1))) * ((1 / ( cos . x0)) + (1 / ( cos . x1)))) / (x0 - x1)) by A2, XCMPLX_1: 130

      .= ((((( cos . x1) - ( cos . x0)) / (( cos . x0) * ( cos . x1))) * ((( cos . x1) + ( cos . x0)) / (( cos . x0) * ( cos . x1)))) / (x0 - x1)) by A2, XCMPLX_1: 116

      .= ((((( cos . x1) - ( cos . x0)) * (( cos . x1) + ( cos . x0))) / ((( cos . x0) * ( cos . x1)) * (( cos . x0) * ( cos . x1)))) / (x0 - x1)) by XCMPLX_1: 76

      .= ((((( cos x1) * ( cos x1)) - (( cos x0) * ( cos x0))) / ((( cos x0) * ( cos x1)) ^2 )) / (x0 - x1))

      .= (((( sin (x0 + x1)) * ( sin (x0 - x1))) / ((( cos x0) * ( cos x1)) ^2 )) / (x0 - x1)) by SIN_COS4: 38

      .= (((( sin (x0 + x1)) * ( sin (x0 - x1))) / (((1 / 2) * (( cos (x0 + x1)) + ( cos (x0 - x1)))) ^2 )) / (x0 - x1)) by SIN_COS4: 32

      .= (((1 * (( sin (x0 + x1)) * ( sin (x0 - x1)))) / ((1 / 4) * ((( cos (x0 + x1)) + ( cos (x0 - x1))) ^2 ))) / (x0 - x1))

      .= (((1 / (1 / 4)) * ((( sin (x0 + x1)) * ( sin (x0 - x1))) / ((( cos (x0 + x1)) + ( cos (x0 - x1))) ^2 ))) / (x0 - x1)) by XCMPLX_1: 76

      .= (((4 * (( sin (x0 + x1)) * ( sin (x0 - x1)))) / ((( cos (x0 + x1)) + ( cos (x0 - x1))) ^2 )) / (x0 - x1))

      .= ((4 * (( sin (x0 + x1)) * ( sin (x0 - x1)))) / (((( cos (x0 + x1)) + ( cos (x0 - x1))) ^2 ) * (x0 - x1))) by XCMPLX_1: 78;

      hence thesis;

    end;

    theorem :: DIFF_4:15

    x in ( dom sec ) & (x + h) in ( dom sec ) implies (( fD (( sec (#) sec ),h)) . x) = (((4 * ( sin ((2 * x) + h))) * ( sin h)) / ((( cos ((2 * x) + h)) + ( cos h)) ^2 ))

    proof

      set f = ( sec (#) sec );

      assume

       A1: x in ( dom sec ) & (x + h) in ( dom sec );

      

       A2: ( cos . x) <> 0 & ( cos . (x + h)) <> 0 by A1, RFUNCT_1: 3;

      x in ( dom f) & (x + h) in ( dom f)

      proof

        x in (( dom sec ) /\ ( dom sec )) & (x + h) in (( dom sec ) /\ ( dom sec )) by A1;

        hence thesis by VALUED_1:def 4;

      end;

      

      then (( fD (f,h)) . x) = ((( sec (#) sec ) . (x + h)) - (( sec (#) sec ) . x)) by DIFF_1: 1

      .= ((( sec . (x + h)) * ( sec . (x + h))) - (( sec (#) sec ) . x)) by VALUED_1: 5

      .= ((( sec . (x + h)) * ( sec . (x + h))) - (( sec . x) * ( sec . x))) by VALUED_1: 5

      .= (((( cos . (x + h)) " ) * ( sec . (x + h))) - (( sec . x) * ( sec . x))) by A1, RFUNCT_1:def 2

      .= (((( cos . (x + h)) " ) * (( cos . (x + h)) " )) - (( sec . x) * ( sec . x))) by A1, RFUNCT_1:def 2

      .= (((( cos . (x + h)) " ) * (( cos . (x + h)) " )) - ((( cos . x) " ) * ( sec . x))) by A1, RFUNCT_1:def 2

      .= (((( cos . (x + h)) " ) ^2 ) - ((( cos . x) " ) ^2 )) by A1, RFUNCT_1:def 2

      .= (((1 / ( cos . (x + h))) - (1 / ( cos . x))) * ((1 / ( cos . (x + h))) + (1 / ( cos . x))))

      .= ((((1 * ( cos . x)) - (1 * ( cos . (x + h)))) / (( cos . (x + h)) * ( cos . x))) * ((1 / ( cos . (x + h))) + (1 / ( cos . x)))) by A2, XCMPLX_1: 130

      .= (((( cos . x) - ( cos . (x + h))) / (( cos . (x + h)) * ( cos . x))) * ((( cos . x) + ( cos . (x + h))) / (( cos . (x + h)) * ( cos . x)))) by A2, XCMPLX_1: 116

      .= (((( cos . x) - ( cos . (x + h))) * (( cos . x) + ( cos . (x + h)))) / ((( cos . (x + h)) * ( cos . x)) * (( cos . (x + h)) * ( cos . x)))) by XCMPLX_1: 76

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

      .= ((( sin ((x + h) + x)) * ( sin ((x + h) - x))) / ((( cos (x + h)) * ( cos x)) ^2 )) by SIN_COS4: 38

      .= ((( sin ((2 * x) + h)) * ( sin h)) / (((1 / 2) * (( cos ((x + h) + x)) + ( cos ((x + h) - x)))) ^2 )) by SIN_COS4: 32

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

      .= ((1 / (1 / 4)) * ((( sin ((2 * x) + h)) * ( sin h)) / ((( cos ((2 * x) + h)) + ( cos h)) ^2 ))) by XCMPLX_1: 76

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

      hence thesis;

    end;

    theorem :: DIFF_4:16

    x in ( dom sec ) & (x - h) in ( dom sec ) implies (( bD (( sec (#) sec ),h)) . x) = (((4 * ( sin ((2 * x) - h))) * ( sin h)) / ((( cos ((2 * x) - h)) + ( cos h)) ^2 ))

    proof

      set f = ( sec (#) sec );

      assume

       A1: x in ( dom sec ) & (x - h) in ( dom sec );

      

       A2: ( cos . x) <> 0 & ( cos . (x - h)) <> 0 by A1, RFUNCT_1: 3;

      x in ( dom f) & (x - h) in ( dom f)

      proof

        x in (( dom sec ) /\ ( dom sec )) & (x - h) in (( dom sec ) /\ ( dom sec )) by A1;

        hence thesis by VALUED_1:def 4;

      end;

      

      then (( bD (f,h)) . x) = ((( sec (#) sec ) . x) - (( sec (#) sec ) . (x - h))) by DIFF_1: 38

      .= ((( sec . x) * ( sec . x)) - (( sec (#) sec ) . (x - h))) by VALUED_1: 5

      .= ((( sec . x) * ( sec . x)) - (( sec . (x - h)) * ( sec . (x - h)))) by VALUED_1: 5

      .= (((( cos . x) " ) * ( sec . x)) - (( sec . (x - h)) * ( sec . (x - h)))) by A1, RFUNCT_1:def 2

      .= (((( cos . x) " ) * (( cos . x) " )) - (( sec . (x - h)) * ( sec . (x - h)))) by A1, RFUNCT_1:def 2

      .= (((( cos . x) " ) * (( cos . x) " )) - ((( cos . (x - h)) " ) * ( sec . (x - h)))) by A1, RFUNCT_1:def 2

      .= (((( cos . x) " ) ^2 ) - ((( cos . (x - h)) " ) ^2 )) by A1, RFUNCT_1:def 2

      .= (((1 / ( cos . x)) - (1 / ( cos . (x - h)))) * ((1 / ( cos . x)) + (1 / ( cos . (x - h)))))

      .= ((((1 * ( cos . (x - h))) - (1 * ( cos . x))) / (( cos . x) * ( cos . (x - h)))) * ((1 / ( cos . x)) + (1 / ( cos . (x - h))))) by A2, XCMPLX_1: 130

      .= (((( cos . (x - h)) - ( cos . x)) / (( cos . x) * ( cos . (x - h)))) * ((( cos . (x - h)) + ( cos . x)) / (( cos . x) * ( cos . (x - h))))) by A2, XCMPLX_1: 116

      .= (((( cos . (x - h)) - ( cos . x)) * (( cos . (x - h)) + ( cos . x))) / ((( cos . x) * ( cos . (x - h))) * (( cos . x) * ( cos . (x - h))))) by XCMPLX_1: 76

      .= (((( cos (x - h)) * ( cos (x - h))) - (( cos x) * ( cos x))) / ((( cos x) * ( cos (x - h))) ^2 ))

      .= ((( sin (x + (x - h))) * ( sin (x - (x - h)))) / ((( cos x) * ( cos (x - h))) ^2 )) by SIN_COS4: 38

      .= ((( sin ((2 * x) - h)) * ( sin h)) / (((1 / 2) * (( cos (x + (x - h))) + ( cos (x - (x - h))))) ^2 )) by SIN_COS4: 32

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

      .= ((1 / (1 / 4)) * ((( sin ((2 * x) - h)) * ( sin h)) / ((( cos ((2 * x) - h)) + ( cos h)) ^2 ))) by XCMPLX_1: 76

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

      hence thesis;

    end;

    theorem :: DIFF_4:17

    (x + (h / 2)) in ( dom sec ) & (x - (h / 2)) in ( dom sec ) implies (( cD (( sec (#) sec ),h)) . x) = (((4 * ( sin (2 * x))) * ( sin h)) / ((( cos (2 * x)) + ( cos h)) ^2 ))

    proof

      set f = ( sec (#) sec );

      assume

       A1: (x + (h / 2)) in ( dom sec ) & (x - (h / 2)) in ( dom sec );

      

       A2: ( cos . (x + (h / 2))) <> 0 & ( cos . (x - (h / 2))) <> 0 by A1, RFUNCT_1: 3;

      (x + (h / 2)) in ( dom f) & (x - (h / 2)) in ( dom f)

      proof

        (x + (h / 2)) in (( dom sec ) /\ ( dom sec )) & (x - (h / 2)) in (( dom sec ) /\ ( dom sec )) by A1;

        hence thesis by VALUED_1:def 4;

      end;

      

      then (( cD (f,h)) . x) = ((( sec (#) sec ) . (x + (h / 2))) - (( sec (#) sec ) . (x - (h / 2)))) by DIFF_1: 39

      .= ((( sec . (x + (h / 2))) * ( sec . (x + (h / 2)))) - (( sec (#) sec ) . (x - (h / 2)))) by VALUED_1: 5

      .= ((( sec . (x + (h / 2))) * ( sec . (x + (h / 2)))) - (( sec . (x - (h / 2))) * ( sec . (x - (h / 2))))) by VALUED_1: 5

      .= (((( cos . (x + (h / 2))) " ) * ( sec . (x + (h / 2)))) - (( sec . (x - (h / 2))) * ( sec . (x - (h / 2))))) by A1, RFUNCT_1:def 2

      .= (((( cos . (x + (h / 2))) " ) * (( cos . (x + (h / 2))) " )) - (( sec . (x - (h / 2))) * ( sec . (x - (h / 2))))) by A1, RFUNCT_1:def 2

      .= (((( cos . (x + (h / 2))) " ) * (( cos . (x + (h / 2))) " )) - ((( cos . (x - (h / 2))) " ) * ( sec . (x - (h / 2))))) by A1, RFUNCT_1:def 2

      .= (((( cos . (x + (h / 2))) " ) ^2 ) - ((( cos . (x - (h / 2))) " ) ^2 )) by A1, RFUNCT_1:def 2

      .= (((1 / ( cos . (x + (h / 2)))) - (1 / ( cos . (x - (h / 2))))) * ((1 / ( cos . (x + (h / 2)))) + (1 / ( cos . (x - (h / 2))))))

      .= ((((1 * ( cos . (x - (h / 2)))) - (1 * ( cos . (x + (h / 2))))) / (( cos . (x + (h / 2))) * ( cos . (x - (h / 2))))) * ((1 / ( cos . (x + (h / 2)))) + (1 / ( cos . (x - (h / 2)))))) by A2, XCMPLX_1: 130

      .= (((( cos . (x - (h / 2))) - ( cos . (x + (h / 2)))) / (( cos . (x + (h / 2))) * ( cos . (x - (h / 2))))) * ((( cos . (x - (h / 2))) + ( cos . (x + (h / 2)))) / (( cos . (x + (h / 2))) * ( cos . (x - (h / 2)))))) by A2, XCMPLX_1: 116

      .= (((( cos . (x - (h / 2))) - ( cos . (x + (h / 2)))) * (( cos . (x - (h / 2))) + ( cos . (x + (h / 2))))) / ((( cos . (x + (h / 2))) * ( cos . (x - (h / 2)))) * (( cos . (x + (h / 2))) * ( cos . (x - (h / 2)))))) by XCMPLX_1: 76

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

      .= ((( sin ((x + (h / 2)) + (x - (h / 2)))) * ( sin ((x + (h / 2)) - (x - (h / 2))))) / ((( cos (x + (h / 2))) * ( cos (x - (h / 2)))) ^2 )) by SIN_COS4: 38

      .= ((( sin (2 * x)) * ( sin h)) / (((1 / 2) * (( cos ((x + (h / 2)) + (x - (h / 2)))) + ( cos ((x + (h / 2)) - (x - (h / 2)))))) ^2 )) by SIN_COS4: 32

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

      .= ((1 / (1 / 4)) * ((( sin (2 * x)) * ( sin h)) / ((( cos (2 * x)) + ( cos h)) ^2 ))) by XCMPLX_1: 76

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

      hence thesis;

    end;

    theorem :: DIFF_4:18

    x0 in (( dom cosec ) /\ ( dom sec )) & x1 in (( dom cosec ) /\ ( dom sec )) implies [!( cosec (#) sec ), x0, x1!] = (((4 * (( cos (x1 + x0)) * ( sin (x1 - x0)))) / (( sin (2 * x0)) * ( sin (2 * x1)))) / (x0 - x1))

    proof

      assume

       A1: x0 in (( dom cosec ) /\ ( dom sec )) & x1 in (( dom cosec ) /\ ( dom sec ));

      

       A2: x0 in ( dom cosec ) & x0 in ( dom sec ) by A1, XBOOLE_0:def 4;

      

       A3: x1 in ( dom cosec ) & x1 in ( dom sec ) by A1, XBOOLE_0:def 4;

      

       A4: ( sin . x0) <> 0 & ( cos . x0) <> 0 by A2, RFUNCT_1: 3;

      

       A5: ( sin . x1) <> 0 & ( cos . x1) <> 0 by A3, RFUNCT_1: 3;

       [!( cosec (#) sec ), x0, x1!] = (((( cosec . x0) * ( sec . x0)) - (( cosec (#) sec ) . x1)) / (x0 - x1)) by VALUED_1: 5

      .= (((( cosec . x0) * ( sec . x0)) - (( cosec . x1) * ( sec . x1))) / (x0 - x1)) by VALUED_1: 5

      .= ((((( sin . x0) " ) * ( sec . x0)) - (( cosec . x1) * ( sec . x1))) / (x0 - x1)) by A2, RFUNCT_1:def 2

      .= ((((( sin . x0) " ) * (( cos . x0) " )) - (( cosec . x1) * ( sec . x1))) / (x0 - x1)) by A2, RFUNCT_1:def 2

      .= ((((( sin . x0) " ) * (( cos . x0) " )) - ((( sin . x1) " ) * ( sec . x1))) / (x0 - x1)) by A3, RFUNCT_1:def 2

      .= ((((( sin . x0) " ) * (( cos . x0) " )) - ((( sin . x1) " ) * (( cos . x1) " ))) / (x0 - x1)) by A3, RFUNCT_1:def 2

      .= ((((( sin . x0) * ( cos . x0)) " ) - ((( sin . x1) " ) * (( cos . x1) " ))) / (x0 - x1)) by XCMPLX_1: 204

      .= (((1 / (( sin . x0) * ( cos . x0))) - (1 / (( sin . x1) * ( cos . x1)))) / (x0 - x1)) by XCMPLX_1: 204

      .= ((((1 * (( sin . x1) * ( cos . x1))) - (1 * (( sin . x0) * ( cos . x0)))) / ((( sin . x0) * ( cos . x0)) * (( sin . x1) * ( cos . x1)))) / (x0 - x1)) by A4, A5, XCMPLX_1: 130

      .= (((( cos (x1 + x0)) * ( sin (x1 - x0))) / (((1 / 2) * ((2 * ( sin x0)) * ( cos x0))) * ((1 / 2) * ((2 * ( sin x1)) * ( cos x1))))) / (x0 - x1)) by SIN_COS4: 40

      .= (((( cos (x1 + x0)) * ( sin (x1 - x0))) / (((1 / 2) * ( sin (2 * x0))) * ((1 / 2) * ((2 * ( sin x1)) * ( cos x1))))) / (x0 - x1)) by SIN_COS5: 5

      .= (((( cos (x1 + x0)) * ( sin (x1 - x0))) / (((1 / 2) * ( sin (2 * x0))) * ((1 / 2) * ( sin (2 * x1))))) / (x0 - x1)) by SIN_COS5: 5

      .= (((( cos (x1 + x0)) * ( sin (x1 - x0))) / (((( sin (2 * x0)) * ( sin (2 * x1))) * 1) / 4)) / (x0 - x1))

      .= (((1 / (1 / 4)) * ((( cos (x1 + x0)) * ( sin (x1 - x0))) / (( sin (2 * x0)) * ( sin (2 * x1))))) / (x0 - x1)) by XCMPLX_1: 103

      .= (((4 * (( cos (x1 + x0)) * ( sin (x1 - x0)))) / (( sin (2 * x0)) * ( sin (2 * x1)))) / (x0 - x1));

      hence thesis;

    end;

    theorem :: DIFF_4:19

    (x + h) in (( dom cosec ) /\ ( dom sec )) & x in (( dom cosec ) /\ ( dom sec )) implies (( fD (( cosec (#) sec ),h)) . x) = ( - (4 * ((( cos ((2 * x) + h)) * ( sin h)) / (( sin (2 * (x + h))) * ( sin (2 * x))))))

    proof

      set f = ( cosec (#) sec );

      assume

       A1: (x + h) in (( dom cosec ) /\ ( dom sec )) & x in (( dom cosec ) /\ ( dom sec ));

      

       A2: (x + h) in ( dom cosec ) & (x + h) in ( dom sec ) by A1, XBOOLE_0:def 4;

      

       A3: x in ( dom cosec ) & x in ( dom sec ) by A1, XBOOLE_0:def 4;

      

       A4: ( sin . (x + h)) <> 0 & ( cos . (x + h)) <> 0 by A2, RFUNCT_1: 3;

      

       A5: ( sin . x) <> 0 & ( cos . x) <> 0 by A3, RFUNCT_1: 3;

      x in ( dom f) & (x + h) in ( dom f) by A1, VALUED_1:def 4;

      

      then (( fD (f,h)) . x) = ((( cosec (#) sec ) . (x + h)) - (( cosec (#) sec ) . x)) by DIFF_1: 1

      .= ((( cosec . (x + h)) * ( sec . (x + h))) - (( cosec (#) sec ) . x)) by VALUED_1: 5

      .= ((( cosec . (x + h)) * ( sec . (x + h))) - (( cosec . x) * ( sec . x))) by VALUED_1: 5

      .= (((( sin . (x + h)) " ) * ( sec . (x + h))) - (( cosec . x) * ( sec . x))) by A2, RFUNCT_1:def 2

      .= (((( sin . (x + h)) " ) * (( cos . (x + h)) " )) - (( cosec . x) * ( sec . x))) by A2, RFUNCT_1:def 2

      .= (((( sin . (x + h)) " ) * (( cos . (x + h)) " )) - ((( sin . x) " ) * ( sec . x))) by A3, RFUNCT_1:def 2

      .= (((( sin . (x + h)) " ) * (( cos . (x + h)) " )) - ((( sin . x) " ) * (( cos . x) " ))) by A3, RFUNCT_1:def 2

      .= (((( sin . (x + h)) * ( cos . (x + h))) " ) - ((( sin . x) " ) * (( cos . x) " ))) by XCMPLX_1: 204

      .= ((1 / (( sin . (x + h)) * ( cos . (x + h)))) - (1 / (( sin . x) * ( cos . x)))) by XCMPLX_1: 204

      .= (((1 * (( sin . x) * ( cos . x))) - (1 * (( sin . (x + h)) * ( cos . (x + h))))) / ((( sin . (x + h)) * ( cos . (x + h))) * (( sin . x) * ( cos . x)))) by A4, A5, XCMPLX_1: 130

      .= ((( cos (x + (x + h))) * ( sin (x - (x + h)))) / ((( sin (x + h)) * ( cos (x + h))) * (( sin x) * ( cos x)))) by SIN_COS4: 40

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

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

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

      .= (( - (( cos ((2 * x) + h)) * ( sin h))) / (((1 / 2) * ( sin (2 * (x + h)))) * ((1 / 2) * ((2 * ( sin x)) * ( cos x))))) by SIN_COS5: 5

      .= (( - (( cos ((2 * x) + h)) * ( sin h))) / (((1 / 2) * ( sin (2 * (x + h)))) * ((1 / 2) * ( sin (2 * x))))) by SIN_COS5: 5

      .= ( - ((( cos ((2 * x) + h)) * ( sin h)) / ((( sin (2 * (x + h))) * ( sin (2 * x))) * (1 / 4))))

      .= ( - ((1 / (1 / 4)) * ((( cos ((2 * x) + h)) * ( sin h)) / (( sin (2 * (x + h))) * ( sin (2 * x)))))) by XCMPLX_1: 103

      .= ( - (4 * ((( cos ((2 * x) + h)) * ( sin h)) / (( sin (2 * (x + h))) * ( sin (2 * x))))));

      hence thesis;

    end;

    theorem :: DIFF_4:20

    (x - h) in (( dom cosec ) /\ ( dom sec )) & x in (( dom cosec ) /\ ( dom sec )) implies (( bD (( cosec (#) sec ),h)) . x) = ( - (4 * ((( cos ((2 * x) - h)) * ( sin h)) / (( sin (2 * x)) * ( sin (2 * (x - h)))))))

    proof

      set f = ( cosec (#) sec );

      assume

       A1: (x - h) in (( dom cosec ) /\ ( dom sec )) & x in (( dom cosec ) /\ ( dom sec ));

      

       A2: (x - h) in ( dom cosec ) & (x - h) in ( dom sec ) by A1, XBOOLE_0:def 4;

      

       A3: x in ( dom cosec ) & x in ( dom sec ) by A1, XBOOLE_0:def 4;

      

       A4: ( sin . (x - h)) <> 0 & ( cos . (x - h)) <> 0 by A2, RFUNCT_1: 3;

      

       A5: ( sin . x) <> 0 & ( cos . x) <> 0 by A3, RFUNCT_1: 3;

      x in ( dom f) & (x - h) in ( dom f) by A1, VALUED_1:def 4;

      

      then (( bD (f,h)) . x) = ((( cosec (#) sec ) . x) - (( cosec (#) sec ) . (x - h))) by DIFF_1: 38

      .= ((( cosec . x) * ( sec . x)) - (( cosec (#) sec ) . (x - h))) by VALUED_1: 5

      .= ((( cosec . x) * ( sec . x)) - (( cosec . (x - h)) * ( sec . (x - h)))) by VALUED_1: 5

      .= (((( sin . x) " ) * ( sec . x)) - (( cosec . (x - h)) * ( sec . (x - h)))) by A3, RFUNCT_1:def 2

      .= (((( sin . x) " ) * (( cos . x) " )) - (( cosec . (x - h)) * ( sec . (x - h)))) by A3, RFUNCT_1:def 2

      .= (((( sin . x) " ) * (( cos . x) " )) - ((( sin . (x - h)) " ) * ( sec . (x - h)))) by A2, RFUNCT_1:def 2

      .= (((( sin . x) " ) * (( cos . x) " )) - ((( sin . (x - h)) " ) * (( cos . (x - h)) " ))) by A2, RFUNCT_1:def 2

      .= (((( sin . x) * ( cos . x)) " ) - ((( sin . (x - h)) " ) * (( cos . (x - h)) " ))) by XCMPLX_1: 204

      .= ((1 / (( sin . x) * ( cos . x))) - (1 / (( sin . (x - h)) * ( cos . (x - h))))) by XCMPLX_1: 204

      .= (((1 * (( sin . (x - h)) * ( cos . (x - h)))) - (1 * (( sin . x) * ( cos . x)))) / ((( sin . x) * ( cos . x)) * (( sin . (x - h)) * ( cos . (x - h))))) by A4, A5, XCMPLX_1: 130

      .= ((( cos ((x - h) + x)) * ( sin ((x - h) - x))) / ((( sin x) * ( cos x)) * (( sin (x - h)) * ( cos (x - h))))) by SIN_COS4: 40

      .= ((( cos ((2 * x) - h)) * ( - ( sin h))) / (((((1 / 2) * 2) * ( sin x)) * ( cos x)) * ((((1 / 2) * 2) * ( sin (x - h))) * ( cos (x - h))))) by SIN_COS: 31

      .= (( - (( cos ((2 * x) - h)) * ( sin h))) / (((1 / 2) * ((2 * ( sin x)) * ( cos x))) * ((1 / 2) * ((2 * ( sin (x - h))) * ( cos (x - h))))))

      .= (( - (( cos ((2 * x) - h)) * ( sin h))) / (((1 / 2) * ( sin (2 * x))) * ((1 / 2) * ((2 * ( sin (x - h))) * ( cos (x - h)))))) by SIN_COS5: 5

      .= (( - (( cos ((2 * x) - h)) * ( sin h))) / (((1 / 2) * ( sin (2 * x))) * ((1 / 2) * ( sin (2 * (x - h)))))) by SIN_COS5: 5

      .= ( - ((( cos ((2 * x) - h)) * ( sin h)) / ((( sin (2 * x)) * ( sin (2 * (x - h)))) * (1 / 4))))

      .= ( - ((1 / (1 / 4)) * ((( cos ((2 * x) - h)) * ( sin h)) / (( sin (2 * x)) * ( sin (2 * (x - h))))))) by XCMPLX_1: 103

      .= ( - (4 * ((( cos ((2 * x) - h)) * ( sin h)) / (( sin (2 * x)) * ( sin (2 * (x - h)))))));

      hence thesis;

    end;

    theorem :: DIFF_4:21

    (x + (h / 2)) in (( dom cosec ) /\ ( dom sec )) & (x - (h / 2)) in (( dom cosec ) /\ ( dom sec )) implies (( cD (( cosec (#) sec ),h)) . x) = ( - (4 * ((( cos (2 * x)) * ( sin h)) / (( sin ((2 * x) + h)) * ( sin ((2 * x) - h))))))

    proof

      set f = ( cosec (#) sec );

      assume

       A1: (x + (h / 2)) in (( dom cosec ) /\ ( dom sec )) & (x - (h / 2)) in (( dom cosec ) /\ ( dom sec ));

      

       A2: (x + (h / 2)) in ( dom cosec ) & (x + (h / 2)) in ( dom sec ) by A1, XBOOLE_0:def 4;

      

       A3: (x - (h / 2)) in ( dom cosec ) & (x - (h / 2)) in ( dom sec ) by A1, XBOOLE_0:def 4;

      

       A4: ( sin . (x + (h / 2))) <> 0 & ( cos . (x + (h / 2))) <> 0 by A2, RFUNCT_1: 3;

      

       A5: ( sin . (x - (h / 2))) <> 0 & ( cos . (x - (h / 2))) <> 0 by A3, RFUNCT_1: 3;

      (x + (h / 2)) in ( dom f) & (x - (h / 2)) in ( dom f) by A1, VALUED_1:def 4;

      

      then (( cD (f,h)) . x) = ((( cosec (#) sec ) . (x + (h / 2))) - (( cosec (#) sec ) . (x - (h / 2)))) by DIFF_1: 39

      .= ((( cosec . (x + (h / 2))) * ( sec . (x + (h / 2)))) - (( cosec (#) sec ) . (x - (h / 2)))) by VALUED_1: 5

      .= ((( cosec . (x + (h / 2))) * ( sec . (x + (h / 2)))) - (( cosec . (x - (h / 2))) * ( sec . (x - (h / 2))))) by VALUED_1: 5

      .= (((( sin . (x + (h / 2))) " ) * ( sec . (x + (h / 2)))) - (( cosec . (x - (h / 2))) * ( sec . (x - (h / 2))))) by A2, RFUNCT_1:def 2

      .= (((( sin . (x + (h / 2))) " ) * (( cos . (x + (h / 2))) " )) - (( cosec . (x - (h / 2))) * ( sec . (x - (h / 2))))) by A2, RFUNCT_1:def 2

      .= (((( sin . (x + (h / 2))) " ) * (( cos . (x + (h / 2))) " )) - ((( sin . (x - (h / 2))) " ) * ( sec . (x - (h / 2))))) by A3, RFUNCT_1:def 2

      .= (((( sin . (x + (h / 2))) " ) * (( cos . (x + (h / 2))) " )) - ((( sin . (x - (h / 2))) " ) * (( cos . (x - (h / 2))) " ))) by A3, RFUNCT_1:def 2

      .= (((( sin . (x + (h / 2))) * ( cos . (x + (h / 2)))) " ) - ((( sin . (x - (h / 2))) " ) * (( cos . (x - (h / 2))) " ))) by XCMPLX_1: 204

      .= ((1 / (( sin . (x + (h / 2))) * ( cos . (x + (h / 2))))) - (1 / (( sin . (x - (h / 2))) * ( cos . (x - (h / 2)))))) by XCMPLX_1: 204

      .= (((1 * (( sin . (x - (h / 2))) * ( cos . (x - (h / 2))))) - (1 * (( sin . (x + (h / 2))) * ( cos . (x + (h / 2)))))) / ((( sin . (x + (h / 2))) * ( cos . (x + (h / 2)))) * (( sin . (x - (h / 2))) * ( cos . (x - (h / 2)))))) by A4, A5, XCMPLX_1: 130

      .= ((( cos ((x - (h / 2)) + (x + (h / 2)))) * ( sin ((x - (h / 2)) - (x + (h / 2))))) / ((( sin (x + (h / 2))) * ( cos (x + (h / 2)))) * (( sin (x - (h / 2))) * ( cos (x - (h / 2)))))) by SIN_COS4: 40

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

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

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

      .= (( - (( cos (2 * x)) * ( sin h))) / (((1 / 2) * ( sin (2 * (x + (h / 2))))) * ((1 / 2) * ((2 * ( sin (x - (h / 2)))) * ( cos (x - (h / 2))))))) by SIN_COS5: 5

      .= (( - (( cos (2 * x)) * ( sin h))) / (((1 / 2) * ( sin (2 * (x + (h / 2))))) * ((1 / 2) * ( sin (2 * (x - (h / 2))))))) by SIN_COS5: 5

      .= ( - ((( cos (2 * x)) * ( sin h)) / ((( sin ((2 * x) + h)) * ( sin ((2 * x) - h))) * (1 / 4))))

      .= ( - ((1 / (1 / 4)) * ((( cos (2 * x)) * ( sin h)) / (( sin ((2 * x) + h)) * ( sin ((2 * x) - h)))))) by XCMPLX_1: 103

      .= ( - (4 * ((( cos (2 * x)) * ( sin h)) / (( sin ((2 * x) + h)) * ( sin ((2 * x) - h))))));

      hence thesis;

    end;

    theorem :: DIFF_4:22

    x0 in ( dom tan ) & x1 in ( dom tan ) implies [!(( tan (#) tan ) (#) cos ), x0, x1!] = [!( tan (#) sin ), x0, x1!]

    proof

      assume

       A1: x0 in ( dom tan ) & x1 in ( dom tan );

       [!(( tan (#) tan ) (#) cos ), x0, x1!] = ((((( tan (#) tan ) . x0) * ( cos . x0)) - ((( tan (#) tan ) (#) cos ) . x1)) / (x0 - x1)) by VALUED_1: 5

      .= ((((( tan . x0) * ( tan . x0)) * ( cos . x0)) - ((( tan (#) tan ) (#) cos ) . x1)) / (x0 - x1)) by VALUED_1: 5

      .= ((((( tan . x0) * ( tan . x0)) * ( cos . x0)) - ((( tan (#) tan ) . x1) * ( cos . x1))) / (x0 - x1)) by VALUED_1: 5

      .= ((((( tan . x0) * ( tan . x0)) * ( cos . x0)) - ((( tan . x1) * ( tan . x1)) * ( cos . x1))) / (x0 - x1)) by VALUED_1: 5

      .= (((((( sin . x0) * (( cos . x0) " )) * ( tan . x0)) * ( cos . x0)) - ((( tan . x1) * ( tan . x1)) * ( cos . x1))) / (x0 - x1)) by A1, RFUNCT_1:def 1

      .= (((((( sin . x0) * (( cos . x0) " )) * ( tan . x0)) * ( cos . x0)) - (((( sin . x1) * (( cos . x1) " )) * ( tan . x1)) * ( cos . x1))) / (x0 - x1)) by A1, RFUNCT_1:def 1

      .= ((((( sin . x0) * (( cos . x0) * (1 / ( cos . x0)))) * ( tan . x0)) - ((( sin . x1) * (( cos . x1) * (1 / ( cos . x1)))) * ( tan . x1))) / (x0 - x1))

      .= ((((( sin . x0) * 1) * ( tan . x0)) - ((( sin . x1) * (( cos . x1) * (1 / ( cos . x1)))) * ( tan . x1))) / (x0 - x1)) by A1, FDIFF_8: 1, XCMPLX_1: 106

      .= ((((( sin . x0) * 1) * ( tan . x0)) - ((( sin . x1) * 1) * ( tan . x1))) / (x0 - x1)) by A1, FDIFF_8: 1, XCMPLX_1: 106

      .= (((( tan (#) sin ) . x0) - (( tan . x1) * ( sin . x1))) / (x0 - x1)) by VALUED_1: 5

      .= [!( tan (#) sin ), x0, x1!] by VALUED_1: 5;

      hence thesis;

    end;

    theorem :: DIFF_4:23

    x in ( dom tan ) & (x + h) in ( dom tan ) implies (( fD ((( tan (#) tan ) (#) cos ),h)) . x) = ((( tan (#) sin ) . (x + h)) - (( tan (#) sin ) . x))

    proof

      set f = (( tan (#) tan ) (#) cos );

      assume

       A1: x in ( dom tan ) & (x + h) in ( dom tan );

      x in ( dom f) & (x + h) in ( dom f)

      proof

        set f1 = ( tan (#) tan );

        set f2 = cos ;

        

         A2: x in ( dom f1) & (x + h) in ( dom f1)

        proof

          x in (( dom tan ) /\ ( dom tan )) & (x + h) in (( dom tan ) /\ ( dom tan )) by A1;

          hence thesis by VALUED_1:def 4;

        end;

        x in (( dom f1) /\ ( dom f2)) & (x + h) in (( dom f1) /\ ( dom f2)) by A2, SIN_COS: 24, XBOOLE_0:def 4;

        hence thesis by VALUED_1:def 4;

      end;

      

      then (( fD (f,h)) . x) = (((( tan (#) tan ) (#) cos ) . (x + h)) - ((( tan (#) tan ) (#) cos ) . x)) by DIFF_1: 1

      .= (((( tan (#) tan ) . (x + h)) * ( cos . (x + h))) - ((( tan (#) tan ) (#) cos ) . x)) by VALUED_1: 5

      .= (((( tan . (x + h)) * ( tan . (x + h))) * ( cos . (x + h))) - ((( tan (#) tan ) (#) cos ) . x)) by VALUED_1: 5

      .= (((( tan . (x + h)) * ( tan . (x + h))) * ( cos . (x + h))) - ((( tan (#) tan ) . x) * ( cos . x))) by VALUED_1: 5

      .= (((( tan . (x + h)) * ( tan . (x + h))) * ( cos . (x + h))) - ((( tan . x) * ( tan . x)) * ( cos . x))) by VALUED_1: 5

      .= ((((( sin . (x + h)) * (( cos . (x + h)) " )) * ( tan . (x + h))) * ( cos . (x + h))) - ((( tan . x) * ( tan . x)) * ( cos . x))) by A1, RFUNCT_1:def 1

      .= ((((( sin . (x + h)) * (( cos . (x + h)) " )) * ( tan . (x + h))) * ( cos . (x + h))) - (((( sin . x) * (( cos . x) " )) * ( tan . x)) * ( cos . x))) by A1, RFUNCT_1:def 1

      .= (((( sin . (x + h)) * ( tan . (x + h))) * (( cos . (x + h)) * (1 / ( cos . (x + h))))) - ((( sin . x) * ( tan . x)) * (( cos . x) * (1 / ( cos . x)))))

      .= (((( sin . (x + h)) * ( tan . (x + h))) * 1) - ((( sin . x) * ( tan . x)) * (( cos . x) * (1 / ( cos . x))))) by A1, FDIFF_8: 1, XCMPLX_1: 106

      .= (((( sin . (x + h)) * ( tan . (x + h))) * 1) - ((( sin . x) * ( tan . x)) * 1)) by A1, FDIFF_8: 1, XCMPLX_1: 106

      .= ((( tan (#) sin ) . (x + h)) - (( tan . x) * ( sin . x))) by VALUED_1: 5

      .= ((( tan (#) sin ) . (x + h)) - (( tan (#) sin ) . x)) by VALUED_1: 5;

      hence thesis;

    end;

    theorem :: DIFF_4:24

    x in ( dom tan ) & (x - h) in ( dom tan ) implies (( bD ((( tan (#) tan ) (#) cos ),h)) . x) = ((( tan (#) sin ) . x) - (( tan (#) sin ) . (x - h)))

    proof

      set f = (( tan (#) tan ) (#) cos );

      assume

       A1: x in ( dom tan ) & (x - h) in ( dom tan );

      x in ( dom f) & (x - h) in ( dom f)

      proof

        set f1 = ( tan (#) tan );

        set f2 = cos ;

        

         A2: x in ( dom f1) & (x - h) in ( dom f1)

        proof

          x in (( dom tan ) /\ ( dom tan )) & (x - h) in (( dom tan ) /\ ( dom tan )) by A1;

          hence thesis by VALUED_1:def 4;

        end;

        x in (( dom f1) /\ ( dom f2)) & (x - h) in (( dom f1) /\ ( dom f2)) by A2, SIN_COS: 24, XBOOLE_0:def 4;

        hence thesis by VALUED_1:def 4;

      end;

      

      then (( bD (f,h)) . x) = (((( tan (#) tan ) (#) cos ) . x) - ((( tan (#) tan ) (#) cos ) . (x - h))) by DIFF_1: 38

      .= (((( tan (#) tan ) . x) * ( cos . x)) - ((( tan (#) tan ) (#) cos ) . (x - h))) by VALUED_1: 5

      .= (((( tan . x) * ( tan . x)) * ( cos . x)) - ((( tan (#) tan ) (#) cos ) . (x - h))) by VALUED_1: 5

      .= (((( tan . x) * ( tan . x)) * ( cos . x)) - ((( tan (#) tan ) . (x - h)) * ( cos . (x - h)))) by VALUED_1: 5

      .= (((( tan . x) * ( tan . x)) * ( cos . x)) - ((( tan . (x - h)) * ( tan . (x - h))) * ( cos . (x - h)))) by VALUED_1: 5

      .= ((((( sin . x) * (( cos . x) " )) * ( tan . x)) * ( cos . x)) - ((( tan . (x - h)) * ( tan . (x - h))) * ( cos . (x - h)))) by A1, RFUNCT_1:def 1

      .= ((((( sin . x) * (( cos . x) " )) * ( tan . x)) * ( cos . x)) - (((( sin . (x - h)) * (( cos . (x - h)) " )) * ( tan . (x - h))) * ( cos . (x - h)))) by A1, RFUNCT_1:def 1

      .= (((( sin . x) * ( tan . x)) * (( cos . x) * (1 / ( cos . x)))) - ((( sin . (x - h)) * ( tan . (x - h))) * (( cos . (x - h)) * (1 / ( cos . (x - h))))))

      .= (((( sin . x) * ( tan . x)) * 1) - ((( sin . (x - h)) * ( tan . (x - h))) * (( cos . (x - h)) * (1 / ( cos . (x - h)))))) by A1, FDIFF_8: 1, XCMPLX_1: 106

      .= (((( sin . x) * ( tan . x)) * 1) - ((( sin . (x - h)) * ( tan . (x - h))) * 1)) by A1, FDIFF_8: 1, XCMPLX_1: 106

      .= ((( tan (#) sin ) . x) - (( tan . (x - h)) * ( sin . (x - h)))) by VALUED_1: 5

      .= ((( tan (#) sin ) . x) - (( tan (#) sin ) . (x - h))) by VALUED_1: 5;

      hence thesis;

    end;

    theorem :: DIFF_4:25

    (x + (h / 2)) in ( dom tan ) & (x - (h / 2)) in ( dom tan ) implies (( cD ((( tan (#) tan ) (#) cos ),h)) . x) = ((( tan (#) sin ) . (x + (h / 2))) - (( tan (#) sin ) . (x - (h / 2))))

    proof

      set f = (( tan (#) tan ) (#) cos );

      assume

       A1: (x + (h / 2)) in ( dom tan ) & (x - (h / 2)) in ( dom tan );

      (x + (h / 2)) in ( dom f) & (x - (h / 2)) in ( dom f)

      proof

        set f1 = ( tan (#) tan );

        set f2 = cos ;

        

         A2: (x + (h / 2)) in ( dom f1) & (x - (h / 2)) in ( dom f1)

        proof

          (x + (h / 2)) in (( dom tan ) /\ ( dom tan )) & (x - (h / 2)) in (( dom tan ) /\ ( dom tan )) by A1;

          hence thesis by VALUED_1:def 4;

        end;

        (x + (h / 2)) in (( dom f1) /\ ( dom f2)) & (x - (h / 2)) in (( dom f1) /\ ( dom f2)) by A2, SIN_COS: 24, XBOOLE_0:def 4;

        hence thesis by VALUED_1:def 4;

      end;

      

      then (( cD (f,h)) . x) = (((( tan (#) tan ) (#) cos ) . (x + (h / 2))) - ((( tan (#) tan ) (#) cos ) . (x - (h / 2)))) by DIFF_1: 39

      .= (((( tan (#) tan ) . (x + (h / 2))) * ( cos . (x + (h / 2)))) - ((( tan (#) tan ) (#) cos ) . (x - (h / 2)))) by VALUED_1: 5

      .= (((( tan . (x + (h / 2))) * ( tan . (x + (h / 2)))) * ( cos . (x + (h / 2)))) - ((( tan (#) tan ) (#) cos ) . (x - (h / 2)))) by VALUED_1: 5

      .= (((( tan . (x + (h / 2))) * ( tan . (x + (h / 2)))) * ( cos . (x + (h / 2)))) - ((( tan (#) tan ) . (x - (h / 2))) * ( cos . (x - (h / 2))))) by VALUED_1: 5

      .= (((( tan . (x + (h / 2))) * ( tan . (x + (h / 2)))) * ( cos . (x + (h / 2)))) - ((( tan . (x - (h / 2))) * ( tan . (x - (h / 2)))) * ( cos . (x - (h / 2))))) by VALUED_1: 5

      .= ((((( sin . (x + (h / 2))) * (( cos . (x + (h / 2))) " )) * ( tan . (x + (h / 2)))) * ( cos . (x + (h / 2)))) - ((( tan . (x - (h / 2))) * ( tan . (x - (h / 2)))) * ( cos . (x - (h / 2))))) by A1, RFUNCT_1:def 1

      .= ((((( sin . (x + (h / 2))) * (( cos . (x + (h / 2))) " )) * ( tan . (x + (h / 2)))) * ( cos . (x + (h / 2)))) - (((( sin . (x - (h / 2))) * (( cos . (x - (h / 2))) " )) * ( tan . (x - (h / 2)))) * ( cos . (x - (h / 2))))) by A1, RFUNCT_1:def 1

      .= (((( sin . (x + (h / 2))) * ( tan . (x + (h / 2)))) * (( cos . (x + (h / 2))) * (1 / ( cos . (x + (h / 2)))))) - ((( sin . (x - (h / 2))) * ( tan . (x - (h / 2)))) * (( cos . (x - (h / 2))) * (1 / ( cos . (x - (h / 2)))))))

      .= (((( sin . (x + (h / 2))) * ( tan . (x + (h / 2)))) * 1) - ((( sin . (x - (h / 2))) * ( tan . (x - (h / 2)))) * (( cos . (x - (h / 2))) * (1 / ( cos . (x - (h / 2))))))) by A1, FDIFF_8: 1, XCMPLX_1: 106

      .= (((( sin . (x + (h / 2))) * ( tan . (x + (h / 2)))) * 1) - ((( sin . (x - (h / 2))) * ( tan . (x - (h / 2)))) * 1)) by A1, FDIFF_8: 1, XCMPLX_1: 106

      .= ((( tan (#) sin ) . (x + (h / 2))) - (( tan . (x - (h / 2))) * ( sin . (x - (h / 2))))) by VALUED_1: 5

      .= ((( tan (#) sin ) . (x + (h / 2))) - (( tan (#) sin ) . (x - (h / 2)))) by VALUED_1: 5;

      hence thesis;

    end;

    theorem :: DIFF_4:26

    x0 in ( dom cot ) & x1 in ( dom cot ) implies [!(( cot (#) cot ) (#) sin ), x0, x1!] = [!( cot (#) cos ), x0, x1!]

    proof

      assume

       A1: x0 in ( dom cot ) & x1 in ( dom cot );

       [!(( cot (#) cot ) (#) sin ), x0, x1!] = ((((( cot (#) cot ) . x0) * ( sin . x0)) - ((( cot (#) cot ) (#) sin ) . x1)) / (x0 - x1)) by VALUED_1: 5

      .= ((((( cot . x0) * ( cot . x0)) * ( sin . x0)) - ((( cot (#) cot ) (#) sin ) . x1)) / (x0 - x1)) by VALUED_1: 5

      .= ((((( cot . x0) * ( cot . x0)) * ( sin . x0)) - ((( cot (#) cot ) . x1) * ( sin . x1))) / (x0 - x1)) by VALUED_1: 5

      .= ((((( cot . x0) * ( cot . x0)) * ( sin . x0)) - ((( cot . x1) * ( cot . x1)) * ( sin . x1))) / (x0 - x1)) by VALUED_1: 5

      .= (((((( cos . x0) * (( sin . x0) " )) * ( cot . x0)) * ( sin . x0)) - ((( cot . x1) * ( cot . x1)) * ( sin . x1))) / (x0 - x1)) by A1, RFUNCT_1:def 1

      .= (((((( cos . x0) * (( sin . x0) " )) * ( cot . x0)) * ( sin . x0)) - (((( cos . x1) * (( sin . x1) " )) * ( cot . x1)) * ( sin . x1))) / (x0 - x1)) by A1, RFUNCT_1:def 1

      .= ((((( cot . x0) * ( cos . x0)) * (( sin . x0) * (1 / ( sin . x0)))) - ((( cot . x1) * ( cos . x1)) * (( sin . x1) * (1 / ( sin . x1))))) / (x0 - x1))

      .= ((((( cot . x0) * ( cos . x0)) * 1) - ((( cot . x1) * ( cos . x1)) * (( sin . x1) * (1 / ( sin . x1))))) / (x0 - x1)) by A1, FDIFF_8: 2, XCMPLX_1: 106

      .= ((((( cot . x0) * ( cos . x0)) * 1) - ((( cot . x1) * ( cos . x1)) * 1)) / (x0 - x1)) by A1, FDIFF_8: 2, XCMPLX_1: 106

      .= (((( cot (#) cos ) . x0) - (( cot . x1) * ( cos . x1))) / (x0 - x1)) by VALUED_1: 5

      .= [!( cot (#) cos ), x0, x1!] by VALUED_1: 5;

      hence thesis;

    end;

    theorem :: DIFF_4:27

    x in ( dom cot ) & (x + h) in ( dom cot ) implies (( fD ((( cot (#) cot ) (#) sin ),h)) . x) = ((( cot (#) cos ) . (x + h)) - (( cot (#) cos ) . x))

    proof

      set f = (( cot (#) cot ) (#) sin );

      assume

       A1: x in ( dom cot ) & (x + h) in ( dom cot );

      x in ( dom f) & (x + h) in ( dom f)

      proof

        set f1 = ( cot (#) cot );

        set f2 = sin ;

        

         A2: x in ( dom f1) & (x + h) in ( dom f1)

        proof

          x in (( dom cot ) /\ ( dom cot )) & (x + h) in (( dom cot ) /\ ( dom cot )) by A1;

          hence thesis by VALUED_1:def 4;

        end;

        x in (( dom f1) /\ ( dom f2)) & (x + h) in (( dom f1) /\ ( dom f2)) by A2, SIN_COS: 24, XBOOLE_0:def 4;

        hence thesis by VALUED_1:def 4;

      end;

      

      then (( fD (f,h)) . x) = (((( cot (#) cot ) (#) sin ) . (x + h)) - ((( cot (#) cot ) (#) sin ) . x)) by DIFF_1: 1

      .= (((( cot (#) cot ) . (x + h)) * ( sin . (x + h))) - ((( cot (#) cot ) (#) sin ) . x)) by VALUED_1: 5

      .= (((( cot . (x + h)) * ( cot . (x + h))) * ( sin . (x + h))) - ((( cot (#) cot ) (#) sin ) . x)) by VALUED_1: 5

      .= (((( cot . (x + h)) * ( cot . (x + h))) * ( sin . (x + h))) - ((( cot (#) cot ) . x) * ( sin . x))) by VALUED_1: 5

      .= (((( cot . (x + h)) * ( cot . (x + h))) * ( sin . (x + h))) - ((( cot . x) * ( cot . x)) * ( sin . x))) by VALUED_1: 5

      .= ((((( cos . (x + h)) * (( sin . (x + h)) " )) * ( cot . (x + h))) * ( sin . (x + h))) - ((( cot . x) * ( cot . x)) * ( sin . x))) by A1, RFUNCT_1:def 1

      .= ((((( cos . (x + h)) * (( sin . (x + h)) " )) * ( cot . (x + h))) * ( sin . (x + h))) - (((( cos . x) * (( sin . x) " )) * ( cot . x)) * ( sin . x))) by A1, RFUNCT_1:def 1

      .= (((( cot . (x + h)) * ( cos . (x + h))) * (( sin . (x + h)) * (1 / ( sin . (x + h))))) - ((( cot . x) * ( cos . x)) * (( sin . x) * (1 / ( sin . x)))))

      .= (((( cot . (x + h)) * ( cos . (x + h))) * 1) - ((( cot . x) * ( cos . x)) * (( sin . x) * (1 / ( sin . x))))) by A1, FDIFF_8: 2, XCMPLX_1: 106

      .= (((( cot . (x + h)) * ( cos . (x + h))) * 1) - ((( cot . x) * ( cos . x)) * 1)) by A1, FDIFF_8: 2, XCMPLX_1: 106

      .= ((( cot (#) cos ) . (x + h)) - (( cot . x) * ( cos . x))) by VALUED_1: 5

      .= ((( cot (#) cos ) . (x + h)) - (( cot (#) cos ) . x)) by VALUED_1: 5;

      hence thesis;

    end;

    theorem :: DIFF_4:28

    x in ( dom cot ) & (x - h) in ( dom cot ) implies (( bD ((( cot (#) cot ) (#) sin ),h)) . x) = ((( cot (#) cos ) . x) - (( cot (#) cos ) . (x - h)))

    proof

      set f = (( cot (#) cot ) (#) sin );

      assume

       A1: x in ( dom cot ) & (x - h) in ( dom cot );

      x in ( dom f) & (x - h) in ( dom f)

      proof

        set f1 = ( cot (#) cot );

        set f2 = sin ;

        

         A2: x in ( dom f1) & (x - h) in ( dom f1)

        proof

          x in (( dom cot ) /\ ( dom cot )) & (x - h) in (( dom cot ) /\ ( dom cot )) by A1;

          hence thesis by VALUED_1:def 4;

        end;

        x in (( dom f1) /\ ( dom f2)) & (x - h) in (( dom f1) /\ ( dom f2)) by A2, SIN_COS: 24, XBOOLE_0:def 4;

        hence thesis by VALUED_1:def 4;

      end;

      

      then (( bD (f,h)) . x) = (((( cot (#) cot ) (#) sin ) . x) - ((( cot (#) cot ) (#) sin ) . (x - h))) by DIFF_1: 38

      .= (((( cot (#) cot ) . x) * ( sin . x)) - ((( cot (#) cot ) (#) sin ) . (x - h))) by VALUED_1: 5

      .= (((( cot . x) * ( cot . x)) * ( sin . x)) - ((( cot (#) cot ) (#) sin ) . (x - h))) by VALUED_1: 5

      .= (((( cot . x) * ( cot . x)) * ( sin . x)) - ((( cot (#) cot ) . (x - h)) * ( sin . (x - h)))) by VALUED_1: 5

      .= (((( cot . x) * ( cot . x)) * ( sin . x)) - ((( cot . (x - h)) * ( cot . (x - h))) * ( sin . (x - h)))) by VALUED_1: 5

      .= ((((( cos . x) * (( sin . x) " )) * ( cot . x)) * ( sin . x)) - ((( cot . (x - h)) * ( cot . (x - h))) * ( sin . (x - h)))) by A1, RFUNCT_1:def 1

      .= ((((( cos . x) * (( sin . x) " )) * ( cot . x)) * ( sin . x)) - (((( cos . (x - h)) * (( sin . (x - h)) " )) * ( cot . (x - h))) * ( sin . (x - h)))) by A1, RFUNCT_1:def 1

      .= (((( cot . x) * ( cos . x)) * (( sin . x) * (1 / ( sin . x)))) - ((( cot . (x - h)) * ( cos . (x - h))) * (( sin . (x - h)) * (1 / ( sin . (x - h))))))

      .= (((( cot . x) * ( cos . x)) * 1) - ((( cot . (x - h)) * ( cos . (x - h))) * (( sin . (x - h)) * (1 / ( sin . (x - h)))))) by A1, FDIFF_8: 2, XCMPLX_1: 106

      .= (((( cot . x) * ( cos . x)) * 1) - ((( cot . (x - h)) * ( cos . (x - h))) * 1)) by A1, FDIFF_8: 2, XCMPLX_1: 106

      .= ((( cot (#) cos ) . x) - (( cot . (x - h)) * ( cos . (x - h)))) by VALUED_1: 5

      .= ((( cot (#) cos ) . x) - (( cot (#) cos ) . (x - h))) by VALUED_1: 5;

      hence thesis;

    end;

    theorem :: DIFF_4:29

    (x + (h / 2)) in ( dom cot ) & (x - (h / 2)) in ( dom cot ) implies (( cD ((( cot (#) cot ) (#) sin ),h)) . x) = ((( cot (#) cos ) . (x + (h / 2))) - (( cot (#) cos ) . (x - (h / 2))))

    proof

      set f = (( cot (#) cot ) (#) sin );

      assume

       A1: (x + (h / 2)) in ( dom cot ) & (x - (h / 2)) in ( dom cot );

      (x + (h / 2)) in ( dom f) & (x - (h / 2)) in ( dom f)

      proof

        set f1 = ( cot (#) cot );

        set f2 = sin ;

        

         A2: (x + (h / 2)) in ( dom f1) & (x - (h / 2)) in ( dom f1)

        proof

          (x + (h / 2)) in (( dom cot ) /\ ( dom cot )) & (x - (h / 2)) in (( dom cot ) /\ ( dom cot )) by A1;

          hence thesis by VALUED_1:def 4;

        end;

        (x + (h / 2)) in (( dom f1) /\ ( dom f2)) & (x - (h / 2)) in (( dom f1) /\ ( dom f2)) by A2, SIN_COS: 24, XBOOLE_0:def 4;

        hence thesis by VALUED_1:def 4;

      end;

      

      then (( cD (f,h)) . x) = (((( cot (#) cot ) (#) sin ) . (x + (h / 2))) - ((( cot (#) cot ) (#) sin ) . (x - (h / 2)))) by DIFF_1: 39

      .= (((( cot (#) cot ) . (x + (h / 2))) * ( sin . (x + (h / 2)))) - ((( cot (#) cot ) (#) sin ) . (x - (h / 2)))) by VALUED_1: 5

      .= (((( cot . (x + (h / 2))) * ( cot . (x + (h / 2)))) * ( sin . (x + (h / 2)))) - ((( cot (#) cot ) (#) sin ) . (x - (h / 2)))) by VALUED_1: 5

      .= (((( cot . (x + (h / 2))) * ( cot . (x + (h / 2)))) * ( sin . (x + (h / 2)))) - ((( cot (#) cot ) . (x - (h / 2))) * ( sin . (x - (h / 2))))) by VALUED_1: 5

      .= (((( cot . (x + (h / 2))) * ( cot . (x + (h / 2)))) * ( sin . (x + (h / 2)))) - ((( cot . (x - (h / 2))) * ( cot . (x - (h / 2)))) * ( sin . (x - (h / 2))))) by VALUED_1: 5

      .= ((((( cos . (x + (h / 2))) * (( sin . (x + (h / 2))) " )) * ( cot . (x + (h / 2)))) * ( sin . (x + (h / 2)))) - ((( cot . (x - (h / 2))) * ( cot . (x - (h / 2)))) * ( sin . (x - (h / 2))))) by A1, RFUNCT_1:def 1

      .= ((((( cos . (x + (h / 2))) * (( sin . (x + (h / 2))) " )) * ( cot . (x + (h / 2)))) * ( sin . (x + (h / 2)))) - (((( cos . (x - (h / 2))) * (( sin . (x - (h / 2))) " )) * ( cot . (x - (h / 2)))) * ( sin . (x - (h / 2))))) by A1, RFUNCT_1:def 1

      .= (((( cot . (x + (h / 2))) * ( cos . (x + (h / 2)))) * (( sin . (x + (h / 2))) * (1 / ( sin . (x + (h / 2)))))) - ((( cot . (x - (h / 2))) * ( cos . (x - (h / 2)))) * (( sin . (x - (h / 2))) * (1 / ( sin . (x - (h / 2)))))))

      .= (((( cot . (x + (h / 2))) * ( cos . (x + (h / 2)))) * 1) - ((( cot . (x - (h / 2))) * ( cos . (x - (h / 2)))) * (( sin . (x - (h / 2))) * (1 / ( sin . (x - (h / 2))))))) by A1, FDIFF_8: 2, XCMPLX_1: 106

      .= (((( cot . (x + (h / 2))) * ( cos . (x + (h / 2)))) * 1) - ((( cot . (x - (h / 2))) * ( cos . (x - (h / 2)))) * 1)) by A1, FDIFF_8: 2, XCMPLX_1: 106

      .= ((( cot (#) cos ) . (x + (h / 2))) - (( cot . (x - (h / 2))) * ( cos . (x - (h / 2))))) by VALUED_1: 5

      .= ((( cot (#) cos ) . (x + (h / 2))) - (( cot (#) cos ) . (x - (h / 2)))) by VALUED_1: 5;

      hence thesis;

    end;

    theorem :: DIFF_4:30

    x0 > 0 & x1 > 0 implies [! ln , x0, x1!] = (( ln . (x0 / x1)) / (x0 - x1)) by Th4;

    theorem :: DIFF_4:31

    x > 0 & (x + h) > 0 implies (( fD ( ln ,h)) . x) = ( ln . (1 + (h / x)))

    proof

      set f = ln ;

      assume

       A1: x > 0 & (x + h) > 0 ;

      

       A2: x in ( right_open_halfline 0 )

      proof

        x in { g where g be Real : 0 < g } by A1;

        hence thesis by XXREAL_1: 230;

      end;

      

       A3: (x + h) in ( right_open_halfline 0 )

      proof

        (x + h) in { g where g be Real : 0 < g } by A1;

        hence thesis by XXREAL_1: 230;

      end;

      (( fD (f,h)) . x) = (( ln . (x + h)) - ( ln . x)) by A2, A3, DIFF_1: 1, TAYLOR_1: 18

      .= ( ln . ((x + h) / x)) by A1, Th4

      .= ( ln . ((x / x) + (h / x)))

      .= ( ln . (1 + (h / x))) by A1, XCMPLX_1: 60;

      hence thesis;

    end;

    theorem :: DIFF_4:32

    x > 0 & (x - h) > 0 implies (( bD ( ln ,h)) . x) = ( ln . (1 + (h / (x - h))))

    proof

      set f = ln ;

      assume

       A1: x > 0 & (x - h) > 0 ;

      

       A2: x in ( right_open_halfline 0 )

      proof

        x in { g where g be Real : 0 < g } by A1;

        hence thesis by XXREAL_1: 230;

      end;

      

       A3: (x - h) in ( right_open_halfline 0 )

      proof

        (x - h) in { g where g be Real : 0 < g } by A1;

        hence thesis by XXREAL_1: 230;

      end;

      (( bD (f,h)) . x) = (( ln . x) - ( ln . (x - h))) by A2, A3, DIFF_1: 38, TAYLOR_1: 18

      .= ( ln . (x / (x - h))) by A1, Th4

      .= ( ln . (((x - h) / (x - h)) + (h / (x - h))))

      .= ( ln . (1 + (h / (x - h)))) by A1, XCMPLX_1: 60;

      hence thesis;

    end;

    theorem :: DIFF_4:33

    (x + (h / 2)) > 0 & (x - (h / 2)) > 0 implies (( cD ( ln ,h)) . x) = ( ln . (1 + (h / (x - (h / 2)))))

    proof

      set f = ln ;

      assume

       A1: (x + (h / 2)) > 0 & (x - (h / 2)) > 0 ;

      

       A2: (x + (h / 2)) in ( right_open_halfline 0 )

      proof

        (x + (h / 2)) in { g where g be Real : 0 < g } by A1;

        hence thesis by XXREAL_1: 230;

      end;

      

       A3: (x - (h / 2)) in ( right_open_halfline 0 )

      proof

        (x - (h / 2)) in { g where g be Real : 0 < g } by A1;

        hence thesis by XXREAL_1: 230;

      end;

      (( cD (f,h)) . x) = (( ln . (x + (h / 2))) - ( ln . (x - (h / 2)))) by A2, A3, DIFF_1: 39, TAYLOR_1: 18

      .= ( ln . (((x - (h / 2)) + h) / (x - (h / 2)))) by A1, Th4

      .= ( ln . (((x - (h / 2)) / (x - (h / 2))) + (h / (x - (h / 2)))))

      .= ( ln . (1 + (h / (x - (h / 2))))) by A1, XCMPLX_1: 60;

      hence thesis;

    end;

    theorem :: DIFF_4:34

    for h,k be Real holds ( exp_R (h - k)) = (( exp_R h) / ( exp_R k))

    proof

      let h,k be Real;

      ( exp_R (h - k)) = (( exp_R h) * ( exp_R ( - k))) by SIN_COS: 50

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

      .= (( exp_R h) / ( exp_R k));

      hence thesis;

    end;

    theorem :: DIFF_4:35

    (( fD (f,h)) . x) = ((( Shift (f,h)) . x) - (f . x))

    proof

      (( fD (f,h)) . x) = ((( fdif (f,h)) . 1) . x) by DIFF_3: 7

      .= ((( Shift (f,h)) . x) - (f . x)) by DIFF_1: 11;

      hence thesis;

    end;

    theorem :: DIFF_4:36

    (for x holds (f . x) = (( fD (g,h)) . x)) implies [!f, x0, x1!] = ( [!g, (x0 + h), (x1 + h)!] - [!g, x0, x1!])

    proof

      assume

       A1: for x holds (f . x) = (( fD (g,h)) . x);

       [!f, x0, x1!] = (((( fD (g,h)) . x0) - (f . x1)) / (x0 - x1)) by A1

      .= (((( fD (g,h)) . x0) - (( fD (g,h)) . x1)) / (x0 - x1)) by A1

      .= ((((g . (x0 + h)) - (g . x0)) - (( fD (g,h)) . x1)) / (x0 - x1)) by DIFF_1: 3

      .= ((((g . (x0 + h)) - (g . x0)) - ((g . (x1 + h)) - (g . x1))) / (x0 - x1)) by DIFF_1: 3

      .= ( [!g, (x0 + h), (x1 + h)!] - [!g, x0, x1!]);

      hence thesis;

    end;

    theorem :: DIFF_4:37

    (( fD (( fD (f,h)),h)) . x) = ((( fD (f,(2 * h))) . x) - (2 * (( fD (f,h)) . x)))

    proof

      (( fD (( fD (f,h)),h)) . x) = ((( fD (f,h)) . (x + h)) - (( fD (f,h)) . x)) by DIFF_1: 3

      .= (((f . ((x + h) + h)) - (f . (x + h))) - (( fD (f,h)) . x)) by DIFF_1: 3

      .= (((f . ((x + h) + h)) - (f . (x + h))) - ((f . (x + h)) - (f . x))) by DIFF_1: 3

      .= (((f . (x + (2 * h))) - (f . x)) - ((2 * (f . (x + h))) - (2 * (f . x))))

      .= ((( fD (f,(2 * h))) . x) - (2 * ((f . (x + h)) - (f . x)))) by DIFF_1: 3

      .= ((( fD (f,(2 * h))) . x) - (2 * (( fD (f,h)) . x))) by DIFF_1: 3;

      hence thesis;

    end;

    theorem :: DIFF_4:38

    (( bD (( fD (f,h)),h)) . x) = ((( fD (f,h)) . x) - (( bD (f,h)) . x))

    proof

      (( bD (( fD (f,h)),h)) . x) = ((( fD (f,h)) . x) - (( fD (f,h)) . (x - h))) by DIFF_1: 4

      .= ((( fD (f,h)) . x) - ((f . ((x - h) + h)) - (f . (x - h)))) by DIFF_1: 3

      .= ((( fD (f,h)) . x) - (( bD (f,h)) . x)) by DIFF_1: 4;

      hence thesis;

    end;

    theorem :: DIFF_4:39

    (( cD (( fD (f,h)),h)) . x) = ((( fD (f,h)) . (x + (h / 2))) - (( cD (f,h)) . x))

    proof

      (( cD (( fD (f,h)),h)) . x) = ((( fD (f,h)) . (x + (h / 2))) - (( fD (f,h)) . (x - (h / 2)))) by DIFF_1: 5

      .= ((( fD (f,h)) . (x + (h / 2))) - ((f . ((x - (h / 2)) + h)) - (f . (x - (h / 2))))) by DIFF_1: 3

      .= ((( fD (f,h)) . (x + (h / 2))) - (( cD (f,h)) . x)) by DIFF_1: 5;

      hence thesis;

    end;

    theorem :: DIFF_4:40

    

     Th40: ((( fdif (f,h)) . 1) . x) = (((( fdif (f,h)) . 0 ) . (x + h)) - ((( fdif (f,h)) . 0 ) . x))

    proof

      ((( fdif (f,h)) . 1) . x) = (( fD (f,h)) . x) by DIFF_3: 7

      .= ((f . (x + h)) - (f . x)) by DIFF_1: 3

      .= (((( fdif (f,h)) . 0 ) . (x + h)) - (f . x)) by DIFF_1:def 6

      .= (((( fdif (f,h)) . 0 ) . (x + h)) - ((( fdif (f,h)) . 0 ) . x)) by DIFF_1:def 6;

      hence thesis;

    end;

    theorem :: DIFF_4:41

    ((( fdif (f,h)) . (n + 1)) . x) = (((( fdif (f,h)) . n) . (x + h)) - ((( fdif (f,h)) . n) . x))

    proof

      defpred X[ Nat] means ((( fdif (f,h)) . ($1 + 1)) . x) = (((( fdif (f,h)) . $1) . (x + h)) - ((( fdif (f,h)) . $1) . x));

      

       A1: for i st X[i] holds X[(i + 1)]

      proof

        let i;

        assume ((( fdif (f,h)) . (i + 1)) . x) = (((( fdif (f,h)) . i) . (x + h)) - ((( fdif (f,h)) . i) . x));

        

         A2: (( fdif (f,h)) . (i + 1)) is Function of REAL , REAL by DIFF_1: 2;

        ((( fdif (f,h)) . (i + 2)) . x) = ((( fdif (f,h)) . ((i + 1) + 1)) . x)

        .= (( fD ((( fdif (f,h)) . (i + 1)),h)) . x) by DIFF_1:def 6

        .= (((( fdif (f,h)) . (i + 1)) . (x + h)) - ((( fdif (f,h)) . (i + 1)) . x)) by A2, DIFF_1: 3;

        hence thesis;

      end;

      

       A3: X[ 0 ] by Th40;

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

      hence thesis;

    end;

    theorem :: DIFF_4:42

    (( bD (f,h)) . x) = ((f . x) - (( Shift (f,( - h))) . x))

    proof

      (( bD (f,h)) . x) = ((( bdif (f,h)) . 1) . x) by DIFF_3: 11

      .= ((f . x) - (( Shift (f,( - h))) . x)) by DIFF_1: 18;

      hence thesis;

    end;

    theorem :: DIFF_4:43

    (for x holds (f . x) = (( bD (g,h)) . x)) implies [!f, x0, x1!] = ( [!g, x0, x1!] - [!g, (x0 - h), (x1 - h)!])

    proof

      assume

       A1: for x holds (f . x) = (( bD (g,h)) . x);

       [!f, x0, x1!] = (((( bD (g,h)) . x0) - (f . x1)) / (x0 - x1)) by A1

      .= (((( bD (g,h)) . x0) - (( bD (g,h)) . x1)) / (x0 - x1)) by A1

      .= ((((g . x0) - (g . (x0 - h))) - (( bD (g,h)) . x1)) / (x0 - x1)) by DIFF_1: 4

      .= ((((g . x0) - (g . (x0 - h))) - ((g . x1) - (g . (x1 - h)))) / (x0 - x1)) by DIFF_1: 4

      .= ( [!g, x0, x1!] - [!g, (x0 - h), (x1 - h)!]);

      hence thesis;

    end;

    theorem :: DIFF_4:44

    (( fD (( bD (f,h)),h)) . x) = ((( fD (f,h)) . x) - (( bD (f,h)) . x))

    proof

      (( fD (( bD (f,h)),h)) . x) = ((( bD (f,h)) . (x + h)) - (( bD (f,h)) . x)) by DIFF_1: 3

      .= (((f . (x + h)) - (f . ((x + h) - h))) - (( bD (f,h)) . x)) by DIFF_1: 4

      .= ((( fD (f,h)) . x) - (( bD (f,h)) . x)) by DIFF_1: 3;

      hence thesis;

    end;

    theorem :: DIFF_4:45

    (( bD (( bD (f,h)),h)) . x) = ((2 * (( bD (f,h)) . x)) - (( bD (f,(2 * h))) . x))

    proof

      (( bD (( bD (f,h)),h)) . x) = ((( bD (f,h)) . x) - (( bD (f,h)) . (x - h))) by DIFF_1: 4

      .= (((f . x) - (f . (x - h))) - (( bD (f,h)) . (x - h))) by DIFF_1: 4

      .= (((f . x) - (f . (x - h))) - ((f . (x - h)) - (f . ((x - h) - h)))) by DIFF_1: 4

      .= ((2 * ((f . x) - (f . (x - h)))) - ((f . x) - (f . (x - (2 * h)))))

      .= ((2 * (( bD (f,h)) . x)) - ((f . x) - (f . (x - (2 * h))))) by DIFF_1: 4

      .= ((2 * (( bD (f,h)) . x)) - (( bD (f,(2 * h))) . x)) by DIFF_1: 4;

      hence thesis;

    end;

    theorem :: DIFF_4:46

    (( cD (( bD (f,h)),h)) . x) = ((( cD (f,h)) . x) - (( bD (f,h)) . (x - (h / 2))))

    proof

      (( cD (( bD (f,h)),h)) . x) = ((( bD (f,h)) . (x + (h / 2))) - (( bD (f,h)) . (x - (h / 2)))) by DIFF_1: 5

      .= (((f . (x + (h / 2))) - (f . ((x + (h / 2)) - h))) - (( bD (f,h)) . (x - (h / 2)))) by DIFF_1: 4

      .= ((( cD (f,h)) . x) - (( bD (f,h)) . (x - (h / 2)))) by DIFF_1: 5;

      hence thesis;

    end;

    theorem :: DIFF_4:47

    

     Th47: ((( bdif (f,h)) . 1) . x) = (((( bdif (f,h)) . 0 ) . x) - ((( bdif (f,h)) . 0 ) . (x - h)))

    proof

      ((( bdif (f,h)) . 1) . x) = (( bD (f,h)) . x) by DIFF_3: 11

      .= ((f . x) - (f . (x - h))) by DIFF_1: 4

      .= (((( bdif (f,h)) . 0 ) . x) - (f . (x - h))) by DIFF_1:def 7

      .= (((( bdif (f,h)) . 0 ) . x) - ((( bdif (f,h)) . 0 ) . (x - h))) by DIFF_1:def 7;

      hence thesis;

    end;

    theorem :: DIFF_4:48

    ((( bdif (f,h)) . (n + 1)) . x) = (((( bdif (f,h)) . n) . x) - ((( bdif (f,h)) . n) . (x - h)))

    proof

      defpred X[ Nat] means ((( bdif (f,h)) . ($1 + 1)) . x) = (((( bdif (f,h)) . $1) . x) - ((( bdif (f,h)) . $1) . (x - h)));

      

       A1: for i st X[i] holds X[(i + 1)]

      proof

        let i;

        assume ((( bdif (f,h)) . (i + 1)) . x) = (((( bdif (f,h)) . i) . x) - ((( bdif (f,h)) . i) . (x - h)));

        

         A2: (( bdif (f,h)) . (i + 1)) is Function of REAL , REAL by DIFF_1: 12;

        ((( bdif (f,h)) . (i + 2)) . x) = ((( bdif (f,h)) . ((i + 1) + 1)) . x)

        .= (( bD ((( bdif (f,h)) . (i + 1)),h)) . x) by DIFF_1:def 7

        .= (((( bdif (f,h)) . (i + 1)) . x) - ((( bdif (f,h)) . (i + 1)) . (x - h))) by A2, DIFF_1: 4;

        hence thesis;

      end;

      

       A3: X[ 0 ] by Th47;

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

      hence thesis;

    end;

    theorem :: DIFF_4:49

    (( cD (f,h)) . x) = ((( Shift (f,(h / 2))) . x) - (( Shift (f,( - (h / 2)))) . x))

    proof

      (( cD (f,h)) . x) = ((( cdif (f,h)) . 1) . x) by DIFF_3: 16

      .= ((( Shift (f,(h / 2))) . x) - (( Shift (f,( - (h / 2)))) . x)) by DIFF_1: 25;

      hence thesis;

    end;

    theorem :: DIFF_4:50

    (for x holds (f . x) = (( cD (g,h)) . x)) implies [!f, x0, x1!] = ( [!g, (x0 + (h / 2)), (x1 + (h / 2))!] - [!g, (x0 - (h / 2)), (x1 - (h / 2))!])

    proof

      assume

       A1: for x holds (f . x) = (( cD (g,h)) . x);

       [!f, x0, x1!] = (((( cD (g,h)) . x0) - (f . x1)) / (x0 - x1)) by A1

      .= (((( cD (g,h)) . x0) - (( cD (g,h)) . x1)) / (x0 - x1)) by A1

      .= ((((g . (x0 + (h / 2))) - (g . (x0 - (h / 2)))) - (( cD (g,h)) . x1)) / (x0 - x1)) by DIFF_1: 5

      .= ((((g . (x0 + (h / 2))) - (g . (x0 - (h / 2)))) - ((g . (x1 + (h / 2))) - (g . (x1 - (h / 2))))) / (x0 - x1)) by DIFF_1: 5

      .= ( [!g, (x0 + (h / 2)), (x1 + (h / 2))!] - [!g, (x0 - (h / 2)), (x1 - (h / 2))!]);

      hence thesis;

    end;

    theorem :: DIFF_4:51

    (( fD (( cD (f,h)),h)) . x) = ((( fD (f,h)) . (x + (h / 2))) - (( cD (f,h)) . x))

    proof

      (( fD (( cD (f,h)),h)) . x) = ((( cD (f,h)) . (x + h)) - (( cD (f,h)) . x)) by DIFF_1: 3

      .= (((f . ((x + h) + (h / 2))) - (f . ((x + h) - (h / 2)))) - (( cD (f,h)) . x)) by DIFF_1: 5

      .= (((f . ((x + (h / 2)) + h)) - (f . (x + (h / 2)))) - (( cD (f,h)) . x))

      .= ((( fD (f,h)) . (x + (h / 2))) - (( cD (f,h)) . x)) by DIFF_1: 3;

      hence thesis;

    end;

    theorem :: DIFF_4:52

    (( bD (( cD (f,h)),h)) . x) = ((( cD (f,h)) . x) - (( bD (f,h)) . (x - (h / 2))))

    proof

      (( bD (( cD (f,h)),h)) . x) = ((( cD (f,h)) . x) - (( cD (f,h)) . (x - h))) by DIFF_1: 4

      .= ((( cD (f,h)) . x) - ((f . ((x - h) + (h / 2))) - (f . ((x - h) - (h / 2))))) by DIFF_1: 5

      .= ((( cD (f,h)) . x) - ((f . (x - (h / 2))) - (f . ((x - (h / 2)) - h))))

      .= ((( cD (f,h)) . x) - (( bD (f,h)) . (x - (h / 2)))) by DIFF_1: 4;

      hence thesis;

    end;

    theorem :: DIFF_4:53

    (( cD (( cD (f,h)),h)) . x) = ((( fD (f,h)) . x) - (( bD (f,h)) . x))

    proof

      (( cD (( cD (f,h)),h)) . x) = ((( cD (f,h)) . (x + (h / 2))) - (( cD (f,h)) . (x - (h / 2)))) by DIFF_1: 5

      .= (((f . ((x + (h / 2)) + (h / 2))) - (f . ((x + (h / 2)) - (h / 2)))) - (( cD (f,h)) . (x - (h / 2)))) by DIFF_1: 5

      .= (((f . ((x + (h / 2)) + (h / 2))) - (f . ((x + (h / 2)) - (h / 2)))) - ((f . ((x - (h / 2)) + (h / 2))) - (f . ((x - (h / 2)) - (h / 2))))) by DIFF_1: 5

      .= (((f . (x + h)) - (f . x)) - ((f . x) - (f . (x - h))))

      .= ((( fD (f,h)) . x) - ((f . x) - (f . (x - h)))) by DIFF_1: 3

      .= ((( fD (f,h)) . x) - (( bD (f,h)) . x)) by DIFF_1: 4;

      hence thesis;

    end;

    theorem :: DIFF_4:54

    

     Th54: ((( cdif (f,h)) . 1) . x) = (((( cdif (f,h)) . 0 ) . (x + (h / 2))) - ((( cdif (f,h)) . 0 ) . (x - (h / 2))))

    proof

      ((( cdif (f,h)) . 1) . x) = (( cD (f,h)) . x) by DIFF_3: 16

      .= ((f . (x + (h / 2))) - (f . (x - (h / 2)))) by DIFF_1: 5

      .= (((( cdif (f,h)) . 0 ) . (x + (h / 2))) - (f . (x - (h / 2)))) by DIFF_1:def 8

      .= (((( cdif (f,h)) . 0 ) . (x + (h / 2))) - ((( cdif (f,h)) . 0 ) . (x - (h / 2)))) by DIFF_1:def 8;

      hence thesis;

    end;

    theorem :: DIFF_4:55

    ((( cdif (f,h)) . (n + 1)) . x) = (((( cdif (f,h)) . n) . (x + (h / 2))) - ((( cdif (f,h)) . n) . (x - (h / 2))))

    proof

      defpred X[ Nat] means ((( cdif (f,h)) . ($1 + 1)) . x) = (((( cdif (f,h)) . $1) . (x + (h / 2))) - ((( cdif (f,h)) . $1) . (x - (h / 2))));

      

       A1: for i st X[i] holds X[(i + 1)]

      proof

        let i;

        assume ((( cdif (f,h)) . (i + 1)) . x) = (((( cdif (f,h)) . i) . (x + (h / 2))) - ((( cdif (f,h)) . i) . (x - (h / 2))));

        

         A2: (( cdif (f,h)) . (i + 1)) is Function of REAL , REAL by DIFF_1: 19;

        ((( cdif (f,h)) . (i + 2)) . x) = ((( cdif (f,h)) . ((i + 1) + 1)) . x)

        .= (( cD ((( cdif (f,h)) . (i + 1)),h)) . x) by DIFF_1:def 8

        .= (((( cdif (f,h)) . (i + 1)) . (x + (h / 2))) - ((( cdif (f,h)) . (i + 1)) . (x - (h / 2)))) by A2, DIFF_1: 5;

        hence thesis;

      end;

      

       A3: X[ 0 ] by Th54;

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

      hence thesis;

    end;

    theorem :: DIFF_4:56

    x0 in ( dom tan ) & x1 in ( dom tan ) implies [!(( tan (#) tan ) (#) sin ), x0, x1!] = ((((( sin x0) |^ 3) * (( cos x1) ^2 )) - ((( sin x1) |^ 3) * (( cos x0) ^2 ))) / (((( cos x0) ^2 ) * (( cos x1) ^2 )) * (x0 - x1)))

    proof

      assume

       A1: x0 in ( dom tan ) & x1 in ( dom tan );

      

       A2: ( cos x0) <> 0 & ( cos x1) <> 0 by A1, FDIFF_8: 1;

       [!(( tan (#) tan ) (#) sin ), x0, x1!] = ((((( tan (#) tan ) . x0) * ( sin . x0)) - ((( tan (#) tan ) (#) sin ) . x1)) / (x0 - x1)) by VALUED_1: 5

      .= ((((( tan . x0) * ( tan . x0)) * ( sin . x0)) - ((( tan (#) tan ) (#) sin ) . x1)) / (x0 - x1)) by VALUED_1: 5

      .= ((((( tan . x0) * ( tan . x0)) * ( sin . x0)) - ((( tan (#) tan ) . x1) * ( sin . x1))) / (x0 - x1)) by VALUED_1: 5

      .= ((((( tan . x0) * ( tan . x0)) * ( sin . x0)) - ((( tan . x1) * ( tan . x1)) * ( sin . x1))) / (x0 - x1)) by VALUED_1: 5

      .= (((((( sin . x0) * (( cos . x0) " )) * ( tan . x0)) * ( sin . x0)) - ((( tan . x1) * ( tan . x1)) * ( sin . x1))) / (x0 - x1)) by A1, RFUNCT_1:def 1

      .= (((((( sin . x0) * (( cos . x0) " )) * (( sin . x0) * (( cos . x0) " ))) * ( sin . x0)) - ((( tan . x1) * ( tan . x1)) * ( sin . x1))) / (x0 - x1)) by A1, RFUNCT_1:def 1

      .= (((((( sin . x0) * (( cos . x0) " )) * (( sin . x0) * (( cos . x0) " ))) * ( sin . x0)) - (((( sin . x1) * (( cos . x1) " )) * ( tan . x1)) * ( sin . x1))) / (x0 - x1)) by A1, RFUNCT_1:def 1

      .= (((((( sin . x0) * (( cos . x0) " )) * (( sin . x0) * (( cos . x0) " ))) * ( sin . x0)) - (((( sin . x1) * (( cos . x1) " )) * (( sin . x1) * (( cos . x1) " ))) * ( sin . x1))) / (x0 - x1)) by A1, RFUNCT_1:def 1

      .= ((((((( sin . x0) * ( sin . x0)) * ( sin . x0)) * (( cos . x0) " )) * (( cos . x0) " )) - ((((( sin . x1) * ( sin . x1)) * ( sin . x1)) * (( cos . x1) " )) * (( cos . x1) " ))) / (x0 - x1))

      .= (((((((( sin . x0) |^ 1) * ( sin . x0)) * ( sin . x0)) * (( cos . x0) " )) * (( cos . x0) " )) - ((((( sin . x1) * ( sin . x1)) * ( sin . x1)) * (( cos . x1) " )) * (( cos . x1) " ))) / (x0 - x1))

      .= ((((((( sin . x0) |^ (1 + 1)) * ( sin . x0)) * (( cos . x0) " )) * (( cos . x0) " )) - ((((( sin . x1) * ( sin . x1)) * ( sin . x1)) * (( cos . x1) " )) * (( cos . x1) " ))) / (x0 - x1)) by NEWTON: 6

      .= (((((( sin . x0) |^ (2 + 1)) * (( cos . x0) " )) * (( cos . x0) " )) - ((((( sin . x1) * ( sin . x1)) * ( sin . x1)) * (( cos . x1) " )) * (( cos . x1) " ))) / (x0 - x1)) by NEWTON: 6

      .= (((((( sin . x0) |^ 3) * (( cos . x0) " )) * (( cos . x0) " )) - (((((( sin . x1) |^ 1) * ( sin . x1)) * ( sin . x1)) * (( cos . x1) " )) * (( cos . x1) " ))) / (x0 - x1))

      .= (((((( sin . x0) |^ 3) * (( cos . x0) " )) * (( cos . x0) " )) - ((((( sin . x1) |^ (1 + 1)) * ( sin . x1)) * (( cos . x1) " )) * (( cos . x1) " ))) / (x0 - x1)) by NEWTON: 6

      .= (((((( sin . x0) |^ 3) * (( cos . x0) " )) * (( cos . x0) " )) - (((( sin . x1) |^ (2 + 1)) * (( cos . x1) " )) * (( cos . x1) " ))) / (x0 - x1)) by NEWTON: 6

      .= ((((( sin . x0) |^ 3) * ((( cos . x0) " ) * (( cos . x0) " ))) - (((( sin . x1) |^ 3) * (( cos . x1) " )) * (( cos . x1) " ))) / (x0 - x1))

      .= ((((( sin . x0) |^ 3) * ((( cos . x0) * ( cos . x0)) " )) - ((( sin . x1) |^ 3) * ((( cos . x1) " ) * (( cos . x1) " )))) / (x0 - x1)) by XCMPLX_1: 204

      .= ((((( sin . x0) |^ 3) / (( cos . x0) ^2 )) - ((( sin . x1) |^ 3) / (( cos . x1) ^2 ))) / (x0 - x1)) by XCMPLX_1: 204

      .= (((((( sin x0) |^ 3) * (( cos x1) ^2 )) - ((( sin x1) |^ 3) * (( cos x0) ^2 ))) / ((( cos x0) ^2 ) * (( cos x1) ^2 ))) / (x0 - x1)) by A2, XCMPLX_1: 130

      .= ((((( sin x0) |^ 3) * (( cos x1) ^2 )) - ((( sin x1) |^ 3) * (( cos x0) ^2 ))) / (((( cos x0) ^2 ) * (( cos x1) ^2 )) * (x0 - x1))) by XCMPLX_1: 78;

      hence thesis;

    end;

    theorem :: DIFF_4:57

    x in ( dom tan ) & (x + h) in ( dom tan ) implies (( fD ((( tan (#) tan ) (#) sin ),h)) . x) = (((( sin . (x + h)) |^ 3) * ((( cos . (x + h)) " ) |^ 2)) - ((( sin . x) |^ 3) * ((( cos . x) " ) |^ 2)))

    proof

      set f = (( tan (#) tan ) (#) sin );

      assume

       A1: x in ( dom tan ) & (x + h) in ( dom tan );

      x in ( dom f) & (x + h) in ( dom f)

      proof

        set f1 = ( tan (#) tan );

        set f2 = sin ;

        

         A2: x in ( dom f1) & (x + h) in ( dom f1)

        proof

          x in (( dom tan ) /\ ( dom tan )) & (x + h) in (( dom tan ) /\ ( dom tan )) by A1;

          hence thesis by VALUED_1:def 4;

        end;

        x in (( dom f1) /\ ( dom f2)) & (x + h) in (( dom f1) /\ ( dom f2)) by A2, SIN_COS: 24, XBOOLE_0:def 4;

        hence thesis by VALUED_1:def 4;

      end;

      

      then (( fD (f,h)) . x) = (((( tan (#) tan ) (#) sin ) . (x + h)) - ((( tan (#) tan ) (#) sin ) . x)) by DIFF_1: 1

      .= (((( tan (#) tan ) . (x + h)) * ( sin . (x + h))) - ((( tan (#) tan ) (#) sin ) . x)) by VALUED_1: 5

      .= (((( tan (#) tan ) . (x + h)) * ( sin . (x + h))) - ((( tan (#) tan ) . x) * ( sin . x))) by VALUED_1: 5

      .= (((( tan . (x + h)) * ( tan . (x + h))) * ( sin . (x + h))) - ((( tan (#) tan ) . x) * ( sin . x))) by VALUED_1: 5

      .= (((( tan . (x + h)) * ( tan . (x + h))) * ( sin . (x + h))) - ((( tan . x) * ( tan . x)) * ( sin . x))) by VALUED_1: 5

      .= ((((( sin . (x + h)) * (( cos . (x + h)) " )) * ( tan . (x + h))) * ( sin . (x + h))) - ((( tan . x) * ( tan . x)) * ( sin . x))) by A1, RFUNCT_1:def 1

      .= ((((( sin . (x + h)) * (( cos . (x + h)) " )) * (( sin . (x + h)) * (( cos . (x + h)) " ))) * ( sin . (x + h))) - ((( tan . x) * ( tan . x)) * ( sin . x))) by A1, RFUNCT_1:def 1

      .= ((((( sin . (x + h)) * (( cos . (x + h)) " )) * (( sin . (x + h)) * (( cos . (x + h)) " ))) * ( sin . (x + h))) - (((( sin . x) * (( cos . x) " )) * ( tan . x)) * ( sin . x))) by A1, RFUNCT_1:def 1

      .= ((((( sin . (x + h)) * (( cos . (x + h)) " )) * (( sin . (x + h)) * (( cos . (x + h)) " ))) * ( sin . (x + h))) - (((( sin . x) * (( cos . x) " )) * (( sin . x) * (( cos . x) " ))) * ( sin . x))) by A1, RFUNCT_1:def 1

      .= ((((( sin . (x + h)) * ( sin . (x + h))) * ( sin . (x + h))) * ((( cos . (x + h)) " ) * (( cos . (x + h)) " ))) - (((( sin . x) * ( sin . x)) * ( sin . x)) * ((( cos . x) " ) * (( cos . x) " ))))

      .= (((((( sin . (x + h)) |^ 1) * ( sin . (x + h))) * ( sin . (x + h))) * ((( cos . (x + h)) " ) * (( cos . (x + h)) " ))) - (((( sin . x) * ( sin . x)) * ( sin . x)) * ((( cos . x) " ) * (( cos . x) " ))))

      .= ((((( sin . (x + h)) |^ (1 + 1)) * ( sin . (x + h))) * ((( cos . (x + h)) " ) * (( cos . (x + h)) " ))) - (((( sin . x) * ( sin . x)) * ( sin . x)) * ((( cos . x) " ) * (( cos . x) " )))) by NEWTON: 6

      .= (((( sin . (x + h)) |^ (2 + 1)) * ((( cos . (x + h)) " ) * (( cos . (x + h)) " ))) - (((( sin . x) * ( sin . x)) * ( sin . x)) * ((( cos . x) " ) * (( cos . x) " )))) by NEWTON: 6

      .= (((( sin . (x + h)) |^ 3) * (((( cos . (x + h)) " ) |^ 1) * (( cos . (x + h)) " ))) - (((( sin . x) * ( sin . x)) * ( sin . x)) * ((( cos . x) " ) * (( cos . x) " ))))

      .= (((( sin . (x + h)) |^ 3) * ((( cos . (x + h)) " ) |^ (1 + 1))) - (((( sin . x) * ( sin . x)) * ( sin . x)) * ((( cos . x) " ) * (( cos . x) " )))) by NEWTON: 6

      .= (((( sin . (x + h)) |^ 3) * ((( cos . (x + h)) " ) |^ 2)) - ((((( sin . x) |^ 1) * ( sin . x)) * ( sin . x)) * ((( cos . x) " ) * (( cos . x) " ))))

      .= (((( sin . (x + h)) |^ 3) * ((( cos . (x + h)) " ) |^ 2)) - (((( sin . x) |^ (1 + 1)) * ( sin . x)) * ((( cos . x) " ) * (( cos . x) " )))) by NEWTON: 6

      .= (((( sin . (x + h)) |^ 3) * ((( cos . (x + h)) " ) |^ 2)) - ((( sin . x) |^ (2 + 1)) * ((( cos . x) " ) * (( cos . x) " )))) by NEWTON: 6

      .= (((( sin . (x + h)) |^ 3) * ((( cos . (x + h)) " ) |^ 2)) - ((( sin . x) |^ 3) * (((( cos . x) " ) |^ 1) * (( cos . x) " ))))

      .= (((( sin . (x + h)) |^ 3) * ((( cos . (x + h)) " ) |^ 2)) - ((( sin . x) |^ 3) * ((( cos . x) " ) |^ (1 + 1)))) by NEWTON: 6

      .= (((( sin . (x + h)) |^ 3) * ((( cos . (x + h)) " ) |^ 2)) - ((( sin . x) |^ 3) * ((( cos . x) " ) |^ 2)));

      hence thesis;

    end;

    theorem :: DIFF_4:58

    x in ( dom tan ) & (x - h) in ( dom tan ) implies (( bD ((( tan (#) tan ) (#) sin ),h)) . x) = (((( sin . x) |^ 3) * ((( cos . x) " ) |^ 2)) - ((( sin . (x - h)) |^ 3) * ((( cos . (x - h)) " ) |^ 2)))

    proof

      set f = (( tan (#) tan ) (#) sin );

      assume

       A1: x in ( dom tan ) & (x - h) in ( dom tan );

      x in ( dom f) & (x - h) in ( dom f)

      proof

        set f1 = ( tan (#) tan );

        set f2 = sin ;

        

         A2: x in ( dom f1) & (x - h) in ( dom f1)

        proof

          x in (( dom tan ) /\ ( dom tan )) & (x - h) in (( dom tan ) /\ ( dom tan )) by A1;

          hence thesis by VALUED_1:def 4;

        end;

        x in (( dom f1) /\ ( dom f2)) & (x - h) in (( dom f1) /\ ( dom f2)) by A2, SIN_COS: 24, XBOOLE_0:def 4;

        hence thesis by VALUED_1:def 4;

      end;

      

      then (( bD (f,h)) . x) = (((( tan (#) tan ) (#) sin ) . x) - ((( tan (#) tan ) (#) sin ) . (x - h))) by DIFF_1: 38

      .= (((( tan (#) tan ) . x) * ( sin . x)) - ((( tan (#) tan ) (#) sin ) . (x - h))) by VALUED_1: 5

      .= (((( tan (#) tan ) . x) * ( sin . x)) - ((( tan (#) tan ) . (x - h)) * ( sin . (x - h)))) by VALUED_1: 5

      .= (((( tan . x) * ( tan . x)) * ( sin . x)) - ((( tan (#) tan ) . (x - h)) * ( sin . (x - h)))) by VALUED_1: 5

      .= (((( tan . x) * ( tan . x)) * ( sin . x)) - ((( tan . (x - h)) * ( tan . (x - h))) * ( sin . (x - h)))) by VALUED_1: 5

      .= ((((( sin . x) * (( cos . x) " )) * ( tan . x)) * ( sin . x)) - ((( tan . (x - h)) * ( tan . (x - h))) * ( sin . (x - h)))) by A1, RFUNCT_1:def 1

      .= ((((( sin . x) * (( cos . x) " )) * (( sin . x) * (( cos . x) " ))) * ( sin . x)) - ((( tan . (x - h)) * ( tan . (x - h))) * ( sin . (x - h)))) by A1, RFUNCT_1:def 1

      .= ((((( sin . x) * (( cos . x) " )) * (( sin . x) * (( cos . x) " ))) * ( sin . x)) - (((( sin . (x - h)) * (( cos . (x - h)) " )) * ( tan . (x - h))) * ( sin . (x - h)))) by A1, RFUNCT_1:def 1

      .= ((((( sin . x) * (( cos . x) " )) * (( sin . x) * (( cos . x) " ))) * ( sin . x)) - (((( sin . (x - h)) * (( cos . (x - h)) " )) * (( sin . (x - h)) * (( cos . (x - h)) " ))) * ( sin . (x - h)))) by A1, RFUNCT_1:def 1

      .= ((((( sin . x) * ( sin . x)) * ( sin . x)) * ((( cos . x) " ) * (( cos . x) " ))) - (((( sin . (x - h)) * ( sin . (x - h))) * ( sin . (x - h))) * ((( cos . (x - h)) " ) * (( cos . (x - h)) " ))))

      .= (((((( sin . x) |^ 1) * ( sin . x)) * ( sin . x)) * ((( cos . x) " ) * (( cos . x) " ))) - (((( sin . (x - h)) * ( sin . (x - h))) * ( sin . (x - h))) * ((( cos . (x - h)) " ) * (( cos . (x - h)) " ))))

      .= ((((( sin . x) |^ (1 + 1)) * ( sin . x)) * ((( cos . x) " ) * (( cos . x) " ))) - (((( sin . (x - h)) * ( sin . (x - h))) * ( sin . (x - h))) * ((( cos . (x - h)) " ) * (( cos . (x - h)) " )))) by NEWTON: 6

      .= (((( sin . x) |^ (2 + 1)) * ((( cos . x) " ) * (( cos . x) " ))) - (((( sin . (x - h)) * ( sin . (x - h))) * ( sin . (x - h))) * ((( cos . (x - h)) " ) * (( cos . (x - h)) " )))) by NEWTON: 6

      .= (((( sin . x) |^ 3) * (((( cos . x) " ) |^ 1) * (( cos . x) " ))) - (((( sin . (x - h)) * ( sin . (x - h))) * ( sin . (x - h))) * ((( cos . (x - h)) " ) * (( cos . (x - h)) " ))))

      .= (((( sin . x) |^ 3) * ((( cos . x) " ) |^ (1 + 1))) - (((( sin . (x - h)) * ( sin . (x - h))) * ( sin . (x - h))) * ((( cos . (x - h)) " ) * (( cos . (x - h)) " )))) by NEWTON: 6

      .= (((( sin . x) |^ 3) * ((( cos . x) " ) |^ 2)) - ((((( sin . (x - h)) |^ 1) * ( sin . (x - h))) * ( sin . (x - h))) * ((( cos . (x - h)) " ) * (( cos . (x - h)) " ))))

      .= (((( sin . x) |^ 3) * ((( cos . x) " ) |^ 2)) - (((( sin . (x - h)) |^ (1 + 1)) * ( sin . (x - h))) * ((( cos . (x - h)) " ) * (( cos . (x - h)) " )))) by NEWTON: 6

      .= (((( sin . x) |^ 3) * ((( cos . x) " ) |^ 2)) - ((( sin . (x - h)) |^ (2 + 1)) * ((( cos . (x - h)) " ) * (( cos . (x - h)) " )))) by NEWTON: 6

      .= (((( sin . x) |^ 3) * ((( cos . x) " ) |^ 2)) - ((( sin . (x - h)) |^ 3) * (((( cos . (x - h)) " ) |^ 1) * (( cos . (x - h)) " ))))

      .= (((( sin . x) |^ 3) * ((( cos . x) " ) |^ 2)) - ((( sin . (x - h)) |^ 3) * ((( cos . (x - h)) " ) |^ (1 + 1)))) by NEWTON: 6

      .= (((( sin . x) |^ 3) * ((( cos . x) " ) |^ 2)) - ((( sin . (x - h)) |^ 3) * ((( cos . (x - h)) " ) |^ 2)));

      hence thesis;

    end;

    theorem :: DIFF_4:59

    (x + (h / 2)) in ( dom tan ) & (x - (h / 2)) in ( dom tan ) implies (( cD ((( tan (#) tan ) (#) sin ),h)) . x) = (((( sin . (x + (h / 2))) |^ 3) * ((( cos . (x + (h / 2))) " ) |^ 2)) - ((( sin . (x - (h / 2))) |^ 3) * ((( cos . (x - (h / 2))) " ) |^ 2)))

    proof

      set f = (( tan (#) tan ) (#) sin );

      assume

       A1: (x + (h / 2)) in ( dom tan ) & (x - (h / 2)) in ( dom tan );

      (x + (h / 2)) in ( dom f) & (x - (h / 2)) in ( dom f)

      proof

        set f1 = ( tan (#) tan );

        set f2 = sin ;

        

         A2: (x + (h / 2)) in ( dom f1) & (x - (h / 2)) in ( dom f1)

        proof

          (x + (h / 2)) in (( dom tan ) /\ ( dom tan )) & (x - (h / 2)) in (( dom tan ) /\ ( dom tan )) by A1;

          hence thesis by VALUED_1:def 4;

        end;

        (x + (h / 2)) in (( dom f1) /\ ( dom f2)) & (x - (h / 2)) in (( dom f1) /\ ( dom f2)) by A2, SIN_COS: 24, XBOOLE_0:def 4;

        hence thesis by VALUED_1:def 4;

      end;

      

      then (( cD (f,h)) . x) = (((( tan (#) tan ) (#) sin ) . (x + (h / 2))) - ((( tan (#) tan ) (#) sin ) . (x - (h / 2)))) by DIFF_1: 39

      .= (((( tan (#) tan ) . (x + (h / 2))) * ( sin . (x + (h / 2)))) - ((( tan (#) tan ) (#) sin ) . (x - (h / 2)))) by VALUED_1: 5

      .= (((( tan (#) tan ) . (x + (h / 2))) * ( sin . (x + (h / 2)))) - ((( tan (#) tan ) . (x - (h / 2))) * ( sin . (x - (h / 2))))) by VALUED_1: 5

      .= (((( tan . (x + (h / 2))) * ( tan . (x + (h / 2)))) * ( sin . (x + (h / 2)))) - ((( tan (#) tan ) . (x - (h / 2))) * ( sin . (x - (h / 2))))) by VALUED_1: 5

      .= (((( tan . (x + (h / 2))) * ( tan . (x + (h / 2)))) * ( sin . (x + (h / 2)))) - ((( tan . (x - (h / 2))) * ( tan . (x - (h / 2)))) * ( sin . (x - (h / 2))))) by VALUED_1: 5

      .= ((((( sin . (x + (h / 2))) * (( cos . (x + (h / 2))) " )) * ( tan . (x + (h / 2)))) * ( sin . (x + (h / 2)))) - ((( tan . (x - (h / 2))) * ( tan . (x - (h / 2)))) * ( sin . (x - (h / 2))))) by A1, RFUNCT_1:def 1

      .= ((((( sin . (x + (h / 2))) * (( cos . (x + (h / 2))) " )) * (( sin . (x + (h / 2))) * (( cos . (x + (h / 2))) " ))) * ( sin . (x + (h / 2)))) - ((( tan . (x - (h / 2))) * ( tan . (x - (h / 2)))) * ( sin . (x - (h / 2))))) by A1, RFUNCT_1:def 1

      .= ((((( sin . (x + (h / 2))) * (( cos . (x + (h / 2))) " )) * (( sin . (x + (h / 2))) * (( cos . (x + (h / 2))) " ))) * ( sin . (x + (h / 2)))) - (((( sin . (x - (h / 2))) * (( cos . (x - (h / 2))) " )) * ( tan . (x - (h / 2)))) * ( sin . (x - (h / 2))))) by A1, RFUNCT_1:def 1

      .= ((((( sin . (x + (h / 2))) * (( cos . (x + (h / 2))) " )) * (( sin . (x + (h / 2))) * (( cos . (x + (h / 2))) " ))) * ( sin . (x + (h / 2)))) - (((( sin . (x - (h / 2))) * (( cos . (x - (h / 2))) " )) * (( sin . (x - (h / 2))) * (( cos . (x - (h / 2))) " ))) * ( sin . (x - (h / 2))))) by A1, RFUNCT_1:def 1

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

      .= (((((( sin . (x + (h / 2))) |^ 1) * ( sin . (x + (h / 2)))) * ( sin . (x + (h / 2)))) * ((( cos . (x + (h / 2))) " ) * (( cos . (x + (h / 2))) " ))) - (((( sin . (x - (h / 2))) * ( sin . (x - (h / 2)))) * ( sin . (x - (h / 2)))) * ((( cos . (x - (h / 2))) " ) * (( cos . (x - (h / 2))) " ))))

      .= ((((( sin . (x + (h / 2))) |^ (1 + 1)) * ( sin . (x + (h / 2)))) * ((( cos . (x + (h / 2))) " ) * (( cos . (x + (h / 2))) " ))) - (((( sin . (x - (h / 2))) * ( sin . (x - (h / 2)))) * ( sin . (x - (h / 2)))) * ((( cos . (x - (h / 2))) " ) * (( cos . (x - (h / 2))) " )))) by NEWTON: 6

      .= (((( sin . (x + (h / 2))) |^ (2 + 1)) * ((( cos . (x + (h / 2))) " ) * (( cos . (x + (h / 2))) " ))) - (((( sin . (x - (h / 2))) * ( sin . (x - (h / 2)))) * ( sin . (x - (h / 2)))) * ((( cos . (x - (h / 2))) " ) * (( cos . (x - (h / 2))) " )))) by NEWTON: 6

      .= (((( sin . (x + (h / 2))) |^ 3) * (((( cos . (x + (h / 2))) " ) |^ 1) * (( cos . (x + (h / 2))) " ))) - (((( sin . (x - (h / 2))) * ( sin . (x - (h / 2)))) * ( sin . (x - (h / 2)))) * ((( cos . (x - (h / 2))) " ) * (( cos . (x - (h / 2))) " ))))

      .= (((( sin . (x + (h / 2))) |^ 3) * ((( cos . (x + (h / 2))) " ) |^ (1 + 1))) - (((( sin . (x - (h / 2))) * ( sin . (x - (h / 2)))) * ( sin . (x - (h / 2)))) * ((( cos . (x - (h / 2))) " ) * (( cos . (x - (h / 2))) " )))) by NEWTON: 6

      .= (((( sin . (x + (h / 2))) |^ 3) * ((( cos . (x + (h / 2))) " ) |^ 2)) - ((((( sin . (x - (h / 2))) |^ 1) * ( sin . (x - (h / 2)))) * ( sin . (x - (h / 2)))) * ((( cos . (x - (h / 2))) " ) * (( cos . (x - (h / 2))) " ))))

      .= (((( sin . (x + (h / 2))) |^ 3) * ((( cos . (x + (h / 2))) " ) |^ 2)) - (((( sin . (x - (h / 2))) |^ (1 + 1)) * ( sin . (x - (h / 2)))) * ((( cos . (x - (h / 2))) " ) * (( cos . (x - (h / 2))) " )))) by NEWTON: 6

      .= (((( sin . (x + (h / 2))) |^ 3) * ((( cos . (x + (h / 2))) " ) |^ 2)) - ((( sin . (x - (h / 2))) |^ (2 + 1)) * ((( cos . (x - (h / 2))) " ) * (( cos . (x - (h / 2))) " )))) by NEWTON: 6

      .= (((( sin . (x + (h / 2))) |^ 3) * ((( cos . (x + (h / 2))) " ) |^ 2)) - ((( sin . (x - (h / 2))) |^ 3) * (((( cos . (x - (h / 2))) " ) |^ 1) * (( cos . (x - (h / 2))) " ))))

      .= (((( sin . (x + (h / 2))) |^ 3) * ((( cos . (x + (h / 2))) " ) |^ 2)) - ((( sin . (x - (h / 2))) |^ 3) * ((( cos . (x - (h / 2))) " ) |^ (1 + 1)))) by NEWTON: 6

      .= (((( sin . (x + (h / 2))) |^ 3) * ((( cos . (x + (h / 2))) " ) |^ 2)) - ((( sin . (x - (h / 2))) |^ 3) * ((( cos . (x - (h / 2))) " ) |^ 2)));

      hence thesis;

    end;

    theorem :: DIFF_4:60

    x0 in ( dom cot ) & x1 in ( dom cot ) implies [!(( cot (#) cot ) (#) cos ), x0, x1!] = ((((( cos x0) |^ 3) * (( sin x1) ^2 )) - ((( cos x1) |^ 3) * (( sin x0) ^2 ))) / (((( sin x0) ^2 ) * (( sin x1) ^2 )) * (x0 - x1)))

    proof

      assume

       A1: x0 in ( dom cot ) & x1 in ( dom cot );

      

       A2: ( sin x0) <> 0 & ( sin x1) <> 0 by A1, FDIFF_8: 2;

       [!(( cot (#) cot ) (#) cos ), x0, x1!] = ((((( cot (#) cot ) . x0) * ( cos . x0)) - ((( cot (#) cot ) (#) cos ) . x1)) / (x0 - x1)) by VALUED_1: 5

      .= ((((( cot . x0) * ( cot . x0)) * ( cos . x0)) - ((( cot (#) cot ) (#) cos ) . x1)) / (x0 - x1)) by VALUED_1: 5

      .= ((((( cot . x0) * ( cot . x0)) * ( cos . x0)) - ((( cot (#) cot ) . x1) * ( cos . x1))) / (x0 - x1)) by VALUED_1: 5

      .= ((((( cot . x0) * ( cot . x0)) * ( cos . x0)) - ((( cot . x1) * ( cot . x1)) * ( cos . x1))) / (x0 - x1)) by VALUED_1: 5

      .= (((((( cos . x0) * (( sin . x0) " )) * ( cot . x0)) * ( cos . x0)) - ((( cot . x1) * ( cot . x1)) * ( cos . x1))) / (x0 - x1)) by A1, RFUNCT_1:def 1

      .= (((((( cos . x0) * (( sin . x0) " )) * (( cos . x0) * (( sin . x0) " ))) * ( cos . x0)) - ((( cot . x1) * ( cot . x1)) * ( cos . x1))) / (x0 - x1)) by A1, RFUNCT_1:def 1

      .= (((((( cos . x0) * (( sin . x0) " )) * (( cos . x0) * (( sin . x0) " ))) * ( cos . x0)) - (((( cos . x1) * (( sin . x1) " )) * ( cot . x1)) * ( cos . x1))) / (x0 - x1)) by A1, RFUNCT_1:def 1

      .= (((((( cos . x0) * (( sin . x0) " )) * (( cos . x0) * (( sin . x0) " ))) * ( cos . x0)) - (((( cos . x1) * (( sin . x1) " )) * (( cos . x1) * (( sin . x1) " ))) * ( cos . x1))) / (x0 - x1)) by A1, RFUNCT_1:def 1

      .= ((((((( cos . x0) * ( cos . x0)) * ( cos . x0)) * (( sin . x0) " )) * (( sin . x0) " )) - ((((( cos . x1) * ( cos . x1)) * ( cos . x1)) * (( sin . x1) " )) * (( sin . x1) " ))) / (x0 - x1))

      .= (((((((( cos . x0) |^ 1) * ( cos . x0)) * ( cos . x0)) * (( sin . x0) " )) * (( sin . x0) " )) - ((((( cos . x1) * ( cos . x1)) * ( cos . x1)) * (( sin . x1) " )) * (( sin . x1) " ))) / (x0 - x1))

      .= ((((((( cos . x0) |^ (1 + 1)) * ( cos . x0)) * (( sin . x0) " )) * (( sin . x0) " )) - ((((( cos . x1) * ( cos . x1)) * ( cos . x1)) * (( sin . x1) " )) * (( sin . x1) " ))) / (x0 - x1)) by NEWTON: 6

      .= (((((( cos . x0) |^ (2 + 1)) * (( sin . x0) " )) * (( sin . x0) " )) - ((((( cos . x1) * ( cos . x1)) * ( cos . x1)) * (( sin . x1) " )) * (( sin . x1) " ))) / (x0 - x1)) by NEWTON: 6

      .= (((((( cos . x0) |^ 3) * (( sin . x0) " )) * (( sin . x0) " )) - (((((( cos . x1) |^ 1) * ( cos . x1)) * ( cos . x1)) * (( sin . x1) " )) * (( sin . x1) " ))) / (x0 - x1))

      .= (((((( cos . x0) |^ 3) * (( sin . x0) " )) * (( sin . x0) " )) - ((((( cos . x1) |^ (1 + 1)) * ( cos . x1)) * (( sin . x1) " )) * (( sin . x1) " ))) / (x0 - x1)) by NEWTON: 6

      .= (((((( cos . x0) |^ 3) * (( sin . x0) " )) * (( sin . x0) " )) - (((( cos . x1) |^ (2 + 1)) * (( sin . x1) " )) * (( sin . x1) " ))) / (x0 - x1)) by NEWTON: 6

      .= ((((( cos . x0) |^ 3) * ((( sin . x0) " ) * (( sin . x0) " ))) - (((( cos . x1) |^ 3) * (( sin . x1) " )) * (( sin . x1) " ))) / (x0 - x1))

      .= ((((( cos . x0) |^ 3) * ((( sin . x0) * ( sin . x0)) " )) - ((( cos . x1) |^ 3) * ((( sin . x1) " ) * (( sin . x1) " )))) / (x0 - x1)) by XCMPLX_1: 204

      .= ((((( cos . x0) |^ 3) / (( sin . x0) ^2 )) - ((( cos . x1) |^ 3) / (( sin . x1) ^2 ))) / (x0 - x1)) by XCMPLX_1: 204

      .= (((((( cos x0) |^ 3) * (( sin x1) ^2 )) - ((( cos x1) |^ 3) * (( sin x0) ^2 ))) / ((( sin x0) ^2 ) * (( sin x1) ^2 ))) / (x0 - x1)) by A2, XCMPLX_1: 130

      .= ((((( cos x0) |^ 3) * (( sin x1) ^2 )) - ((( cos x1) |^ 3) * (( sin x0) ^2 ))) / (((( sin x0) ^2 ) * (( sin x1) ^2 )) * (x0 - x1))) by XCMPLX_1: 78;

      hence thesis;

    end;

    theorem :: DIFF_4:61

    x in ( dom cot ) & (x + h) in ( dom cot ) implies (( fD ((( cot (#) cot ) (#) cos ),h)) . x) = (((( cos . (x + h)) |^ 3) * ((( sin . (x + h)) " ) |^ 2)) - ((( cos . x) |^ 3) * ((( sin . x) " ) |^ 2)))

    proof

      set f = (( cot (#) cot ) (#) cos );

      assume

       A1: x in ( dom cot ) & (x + h) in ( dom cot );

      x in ( dom f) & (x + h) in ( dom f)

      proof

        set f1 = ( cot (#) cot );

        set f2 = cos ;

        

         A2: x in ( dom f1) & (x + h) in ( dom f1)

        proof

          x in (( dom cot ) /\ ( dom cot )) & (x + h) in (( dom cot ) /\ ( dom cot )) by A1;

          hence thesis by VALUED_1:def 4;

        end;

        x in (( dom f1) /\ ( dom f2)) & (x + h) in (( dom f1) /\ ( dom f2)) by A2, SIN_COS: 24, XBOOLE_0:def 4;

        hence thesis by VALUED_1:def 4;

      end;

      

      then (( fD (f,h)) . x) = (((( cot (#) cot ) (#) cos ) . (x + h)) - ((( cot (#) cot ) (#) cos ) . x)) by DIFF_1: 1

      .= (((( cot (#) cot ) . (x + h)) * ( cos . (x + h))) - ((( cot (#) cot ) (#) cos ) . x)) by VALUED_1: 5

      .= (((( cot (#) cot ) . (x + h)) * ( cos . (x + h))) - ((( cot (#) cot ) . x) * ( cos . x))) by VALUED_1: 5

      .= (((( cot . (x + h)) * ( cot . (x + h))) * ( cos . (x + h))) - ((( cot (#) cot ) . x) * ( cos . x))) by VALUED_1: 5

      .= (((( cot . (x + h)) * ( cot . (x + h))) * ( cos . (x + h))) - ((( cot . x) * ( cot . x)) * ( cos . x))) by VALUED_1: 5

      .= ((((( cos . (x + h)) * (( sin . (x + h)) " )) * ( cot . (x + h))) * ( cos . (x + h))) - ((( cot . x) * ( cot . x)) * ( cos . x))) by A1, RFUNCT_1:def 1

      .= ((((( cos . (x + h)) * (( sin . (x + h)) " )) * (( cos . (x + h)) * (( sin . (x + h)) " ))) * ( cos . (x + h))) - ((( cot . x) * ( cot . x)) * ( cos . x))) by A1, RFUNCT_1:def 1

      .= ((((( cos . (x + h)) * (( sin . (x + h)) " )) * (( cos . (x + h)) * (( sin . (x + h)) " ))) * ( cos . (x + h))) - (((( cos . x) * (( sin . x) " )) * ( cot . x)) * ( cos . x))) by A1, RFUNCT_1:def 1

      .= ((((( cos . (x + h)) * (( sin . (x + h)) " )) * (( cos . (x + h)) * (( sin . (x + h)) " ))) * ( cos . (x + h))) - (((( cos . x) * (( sin . x) " )) * (( cos . x) * (( sin . x) " ))) * ( cos . x))) by A1, RFUNCT_1:def 1

      .= ((((( cos . (x + h)) * ( cos . (x + h))) * ( cos . (x + h))) * ((( sin . (x + h)) " ) * (( sin . (x + h)) " ))) - (((( cos . x) * ( cos . x)) * ( cos . x)) * ((( sin . x) " ) * (( sin . x) " ))))

      .= (((((( cos . (x + h)) |^ 1) * ( cos . (x + h))) * ( cos . (x + h))) * ((( sin . (x + h)) " ) * (( sin . (x + h)) " ))) - (((( cos . x) * ( cos . x)) * ( cos . x)) * ((( sin . x) " ) * (( sin . x) " ))))

      .= ((((( cos . (x + h)) |^ (1 + 1)) * ( cos . (x + h))) * ((( sin . (x + h)) " ) * (( sin . (x + h)) " ))) - (((( cos . x) * ( cos . x)) * ( cos . x)) * ((( sin . x) " ) * (( sin . x) " )))) by NEWTON: 6

      .= (((( cos . (x + h)) |^ (2 + 1)) * ((( sin . (x + h)) " ) * (( sin . (x + h)) " ))) - (((( cos . x) * ( cos . x)) * ( cos . x)) * ((( sin . x) " ) * (( sin . x) " )))) by NEWTON: 6

      .= (((( cos . (x + h)) |^ 3) * (((( sin . (x + h)) " ) |^ 1) * (( sin . (x + h)) " ))) - (((( cos . x) * ( cos . x)) * ( cos . x)) * ((( sin . x) " ) * (( sin . x) " ))))

      .= (((( cos . (x + h)) |^ 3) * ((( sin . (x + h)) " ) |^ (1 + 1))) - (((( cos . x) * ( cos . x)) * ( cos . x)) * ((( sin . x) " ) * (( sin . x) " )))) by NEWTON: 6

      .= (((( cos . (x + h)) |^ 3) * ((( sin . (x + h)) " ) |^ 2)) - ((((( cos . x) |^ 1) * ( cos . x)) * ( cos . x)) * ((( sin . x) " ) * (( sin . x) " ))))

      .= (((( cos . (x + h)) |^ 3) * ((( sin . (x + h)) " ) |^ 2)) - (((( cos . x) |^ (1 + 1)) * ( cos . x)) * ((( sin . x) " ) * (( sin . x) " )))) by NEWTON: 6

      .= (((( cos . (x + h)) |^ 3) * ((( sin . (x + h)) " ) |^ 2)) - ((( cos . x) |^ (2 + 1)) * ((( sin . x) " ) * (( sin . x) " )))) by NEWTON: 6

      .= (((( cos . (x + h)) |^ 3) * ((( sin . (x + h)) " ) |^ 2)) - ((( cos . x) |^ 3) * (((( sin . x) " ) |^ 1) * (( sin . x) " ))))

      .= (((( cos . (x + h)) |^ 3) * ((( sin . (x + h)) " ) |^ 2)) - ((( cos . x) |^ 3) * ((( sin . x) " ) |^ (1 + 1)))) by NEWTON: 6

      .= (((( cos . (x + h)) |^ 3) * ((( sin . (x + h)) " ) |^ 2)) - ((( cos . x) |^ 3) * ((( sin . x) " ) |^ 2)));

      hence thesis;

    end;

    theorem :: DIFF_4:62

    x in ( dom cot ) & (x - h) in ( dom cot ) implies (( bD ((( cot (#) cot ) (#) cos ),h)) . x) = (((( cos . x) |^ 3) * ((( sin . x) " ) |^ 2)) - ((( cos . (x - h)) |^ 3) * ((( sin . (x - h)) " ) |^ 2)))

    proof

      set f = (( cot (#) cot ) (#) cos );

      assume

       A1: x in ( dom cot ) & (x - h) in ( dom cot );

      x in ( dom f) & (x - h) in ( dom f)

      proof

        set f1 = ( cot (#) cot );

        set f2 = cos ;

        

         A2: x in ( dom f1) & (x - h) in ( dom f1)

        proof

          x in (( dom cot ) /\ ( dom cot )) & (x - h) in (( dom cot ) /\ ( dom cot )) by A1;

          hence thesis by VALUED_1:def 4;

        end;

        x in (( dom f1) /\ ( dom f2)) & (x - h) in (( dom f1) /\ ( dom f2)) by A2, SIN_COS: 24, XBOOLE_0:def 4;

        hence thesis by VALUED_1:def 4;

      end;

      

      then (( bD (f,h)) . x) = (((( cot (#) cot ) (#) cos ) . x) - ((( cot (#) cot ) (#) cos ) . (x - h))) by DIFF_1: 38

      .= (((( cot (#) cot ) . x) * ( cos . x)) - ((( cot (#) cot ) (#) cos ) . (x - h))) by VALUED_1: 5

      .= (((( cot (#) cot ) . x) * ( cos . x)) - ((( cot (#) cot ) . (x - h)) * ( cos . (x - h)))) by VALUED_1: 5

      .= (((( cot . x) * ( cot . x)) * ( cos . x)) - ((( cot (#) cot ) . (x - h)) * ( cos . (x - h)))) by VALUED_1: 5

      .= (((( cot . x) * ( cot . x)) * ( cos . x)) - ((( cot . (x - h)) * ( cot . (x - h))) * ( cos . (x - h)))) by VALUED_1: 5

      .= ((((( cos . x) * (( sin . x) " )) * ( cot . x)) * ( cos . x)) - ((( cot . (x - h)) * ( cot . (x - h))) * ( cos . (x - h)))) by A1, RFUNCT_1:def 1

      .= ((((( cos . x) * (( sin . x) " )) * (( cos . x) * (( sin . x) " ))) * ( cos . x)) - ((( cot . (x - h)) * ( cot . (x - h))) * ( cos . (x - h)))) by A1, RFUNCT_1:def 1

      .= ((((( cos . x) * (( sin . x) " )) * (( cos . x) * (( sin . x) " ))) * ( cos . x)) - (((( cos . (x - h)) * (( sin . (x - h)) " )) * ( cot . (x - h))) * ( cos . (x - h)))) by A1, RFUNCT_1:def 1

      .= ((((( cos . x) * (( sin . x) " )) * (( cos . x) * (( sin . x) " ))) * ( cos . x)) - (((( cos . (x - h)) * (( sin . (x - h)) " )) * (( cos . (x - h)) * (( sin . (x - h)) " ))) * ( cos . (x - h)))) by A1, RFUNCT_1:def 1

      .= ((((( cos . x) * ( cos . x)) * ( cos . x)) * ((( sin . x) " ) * (( sin . x) " ))) - (((( cos . (x - h)) * ( cos . (x - h))) * ( cos . (x - h))) * ((( sin . (x - h)) " ) * (( sin . (x - h)) " ))))

      .= (((((( cos . x) |^ 1) * ( cos . x)) * ( cos . x)) * ((( sin . x) " ) * (( sin . x) " ))) - (((( cos . (x - h)) * ( cos . (x - h))) * ( cos . (x - h))) * ((( sin . (x - h)) " ) * (( sin . (x - h)) " ))))

      .= ((((( cos . x) |^ (1 + 1)) * ( cos . x)) * ((( sin . x) " ) * (( sin . x) " ))) - (((( cos . (x - h)) * ( cos . (x - h))) * ( cos . (x - h))) * ((( sin . (x - h)) " ) * (( sin . (x - h)) " )))) by NEWTON: 6

      .= (((( cos . x) |^ (2 + 1)) * ((( sin . x) " ) * (( sin . x) " ))) - (((( cos . (x - h)) * ( cos . (x - h))) * ( cos . (x - h))) * ((( sin . (x - h)) " ) * (( sin . (x - h)) " )))) by NEWTON: 6

      .= (((( cos . x) |^ 3) * (((( sin . x) " ) |^ 1) * (( sin . x) " ))) - (((( cos . (x - h)) * ( cos . (x - h))) * ( cos . (x - h))) * ((( sin . (x - h)) " ) * (( sin . (x - h)) " ))))

      .= (((( cos . x) |^ 3) * ((( sin . x) " ) |^ (1 + 1))) - (((( cos . (x - h)) * ( cos . (x - h))) * ( cos . (x - h))) * ((( sin . (x - h)) " ) * (( sin . (x - h)) " )))) by NEWTON: 6

      .= (((( cos . x) |^ 3) * ((( sin . x) " ) |^ 2)) - ((((( cos . (x - h)) |^ 1) * ( cos . (x - h))) * ( cos . (x - h))) * ((( sin . (x - h)) " ) * (( sin . (x - h)) " ))))

      .= (((( cos . x) |^ 3) * ((( sin . x) " ) |^ 2)) - (((( cos . (x - h)) |^ (1 + 1)) * ( cos . (x - h))) * ((( sin . (x - h)) " ) * (( sin . (x - h)) " )))) by NEWTON: 6

      .= (((( cos . x) |^ 3) * ((( sin . x) " ) |^ 2)) - ((( cos . (x - h)) |^ (2 + 1)) * ((( sin . (x - h)) " ) * (( sin . (x - h)) " )))) by NEWTON: 6

      .= (((( cos . x) |^ 3) * ((( sin . x) " ) |^ 2)) - ((( cos . (x - h)) |^ 3) * (((( sin . (x - h)) " ) |^ 1) * (( sin . (x - h)) " ))))

      .= (((( cos . x) |^ 3) * ((( sin . x) " ) |^ 2)) - ((( cos . (x - h)) |^ 3) * ((( sin . (x - h)) " ) |^ (1 + 1)))) by NEWTON: 6

      .= (((( cos . x) |^ 3) * ((( sin . x) " ) |^ 2)) - ((( cos . (x - h)) |^ 3) * ((( sin . (x - h)) " ) |^ 2)));

      hence thesis;

    end;

    theorem :: DIFF_4:63

    (x + (h / 2)) in ( dom cot ) & (x - (h / 2)) in ( dom cot ) implies (( cD ((( cot (#) cot ) (#) cos ),h)) . x) = (((( cos . (x + (h / 2))) |^ 3) * ((( sin . (x + (h / 2))) " ) |^ 2)) - ((( cos . (x - (h / 2))) |^ 3) * ((( sin . (x - (h / 2))) " ) |^ 2)))

    proof

      set f = (( cot (#) cot ) (#) cos );

      assume

       A1: (x + (h / 2)) in ( dom cot ) & (x - (h / 2)) in ( dom cot );

      (x + (h / 2)) in ( dom f) & (x - (h / 2)) in ( dom f)

      proof

        set f1 = ( cot (#) cot );

        set f2 = cos ;

        

         A2: (x + (h / 2)) in ( dom f1) & (x - (h / 2)) in ( dom f1)

        proof

          (x + (h / 2)) in (( dom cot ) /\ ( dom cot )) & (x - (h / 2)) in (( dom cot ) /\ ( dom cot )) by A1;

          hence thesis by VALUED_1:def 4;

        end;

        (x + (h / 2)) in (( dom f1) /\ ( dom f2)) & (x - (h / 2)) in (( dom f1) /\ ( dom f2)) by A2, SIN_COS: 24, XBOOLE_0:def 4;

        hence thesis by VALUED_1:def 4;

      end;

      

      then (( cD (f,h)) . x) = (((( cot (#) cot ) (#) cos ) . (x + (h / 2))) - ((( cot (#) cot ) (#) cos ) . (x - (h / 2)))) by DIFF_1: 39

      .= (((( cot (#) cot ) . (x + (h / 2))) * ( cos . (x + (h / 2)))) - ((( cot (#) cot ) (#) cos ) . (x - (h / 2)))) by VALUED_1: 5

      .= (((( cot (#) cot ) . (x + (h / 2))) * ( cos . (x + (h / 2)))) - ((( cot (#) cot ) . (x - (h / 2))) * ( cos . (x - (h / 2))))) by VALUED_1: 5

      .= (((( cot . (x + (h / 2))) * ( cot . (x + (h / 2)))) * ( cos . (x + (h / 2)))) - ((( cot (#) cot ) . (x - (h / 2))) * ( cos . (x - (h / 2))))) by VALUED_1: 5

      .= (((( cot . (x + (h / 2))) * ( cot . (x + (h / 2)))) * ( cos . (x + (h / 2)))) - ((( cot . (x - (h / 2))) * ( cot . (x - (h / 2)))) * ( cos . (x - (h / 2))))) by VALUED_1: 5

      .= ((((( cos . (x + (h / 2))) * (( sin . (x + (h / 2))) " )) * ( cot . (x + (h / 2)))) * ( cos . (x + (h / 2)))) - ((( cot . (x - (h / 2))) * ( cot . (x - (h / 2)))) * ( cos . (x - (h / 2))))) by A1, RFUNCT_1:def 1

      .= ((((( cos . (x + (h / 2))) * (( sin . (x + (h / 2))) " )) * (( cos . (x + (h / 2))) * (( sin . (x + (h / 2))) " ))) * ( cos . (x + (h / 2)))) - ((( cot . (x - (h / 2))) * ( cot . (x - (h / 2)))) * ( cos . (x - (h / 2))))) by A1, RFUNCT_1:def 1

      .= ((((( cos . (x + (h / 2))) * (( sin . (x + (h / 2))) " )) * (( cos . (x + (h / 2))) * (( sin . (x + (h / 2))) " ))) * ( cos . (x + (h / 2)))) - (((( cos . (x - (h / 2))) * (( sin . (x - (h / 2))) " )) * ( cot . (x - (h / 2)))) * ( cos . (x - (h / 2))))) by A1, RFUNCT_1:def 1

      .= ((((( cos . (x + (h / 2))) * (( sin . (x + (h / 2))) " )) * (( cos . (x + (h / 2))) * (( sin . (x + (h / 2))) " ))) * ( cos . (x + (h / 2)))) - (((( cos . (x - (h / 2))) * (( sin . (x - (h / 2))) " )) * (( cos . (x - (h / 2))) * (( sin . (x - (h / 2))) " ))) * ( cos . (x - (h / 2))))) by A1, RFUNCT_1:def 1

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

      .= (((((( cos . (x + (h / 2))) |^ 1) * ( cos . (x + (h / 2)))) * ( cos . (x + (h / 2)))) * ((( sin . (x + (h / 2))) " ) * (( sin . (x + (h / 2))) " ))) - (((( cos . (x - (h / 2))) * ( cos . (x - (h / 2)))) * ( cos . (x - (h / 2)))) * ((( sin . (x - (h / 2))) " ) * (( sin . (x - (h / 2))) " ))))

      .= ((((( cos . (x + (h / 2))) |^ (1 + 1)) * ( cos . (x + (h / 2)))) * ((( sin . (x + (h / 2))) " ) * (( sin . (x + (h / 2))) " ))) - (((( cos . (x - (h / 2))) * ( cos . (x - (h / 2)))) * ( cos . (x - (h / 2)))) * ((( sin . (x - (h / 2))) " ) * (( sin . (x - (h / 2))) " )))) by NEWTON: 6

      .= (((( cos . (x + (h / 2))) |^ (2 + 1)) * ((( sin . (x + (h / 2))) " ) * (( sin . (x + (h / 2))) " ))) - (((( cos . (x - (h / 2))) * ( cos . (x - (h / 2)))) * ( cos . (x - (h / 2)))) * ((( sin . (x - (h / 2))) " ) * (( sin . (x - (h / 2))) " )))) by NEWTON: 6

      .= (((( cos . (x + (h / 2))) |^ 3) * (((( sin . (x + (h / 2))) " ) |^ 1) * (( sin . (x + (h / 2))) " ))) - (((( cos . (x - (h / 2))) * ( cos . (x - (h / 2)))) * ( cos . (x - (h / 2)))) * ((( sin . (x - (h / 2))) " ) * (( sin . (x - (h / 2))) " ))))

      .= (((( cos . (x + (h / 2))) |^ 3) * ((( sin . (x + (h / 2))) " ) |^ (1 + 1))) - (((( cos . (x - (h / 2))) * ( cos . (x - (h / 2)))) * ( cos . (x - (h / 2)))) * ((( sin . (x - (h / 2))) " ) * (( sin . (x - (h / 2))) " )))) by NEWTON: 6

      .= (((( cos . (x + (h / 2))) |^ 3) * ((( sin . (x + (h / 2))) " ) |^ 2)) - ((((( cos . (x - (h / 2))) |^ 1) * ( cos . (x - (h / 2)))) * ( cos . (x - (h / 2)))) * ((( sin . (x - (h / 2))) " ) * (( sin . (x - (h / 2))) " ))))

      .= (((( cos . (x + (h / 2))) |^ 3) * ((( sin . (x + (h / 2))) " ) |^ 2)) - (((( cos . (x - (h / 2))) |^ (1 + 1)) * ( cos . (x - (h / 2)))) * ((( sin . (x - (h / 2))) " ) * (( sin . (x - (h / 2))) " )))) by NEWTON: 6

      .= (((( cos . (x + (h / 2))) |^ 3) * ((( sin . (x + (h / 2))) " ) |^ 2)) - ((( cos . (x - (h / 2))) |^ (2 + 1)) * ((( sin . (x - (h / 2))) " ) * (( sin . (x - (h / 2))) " )))) by NEWTON: 6

      .= (((( cos . (x + (h / 2))) |^ 3) * ((( sin . (x + (h / 2))) " ) |^ 2)) - ((( cos . (x - (h / 2))) |^ 3) * (((( sin . (x - (h / 2))) " ) |^ 1) * (( sin . (x - (h / 2))) " ))))

      .= (((( cos . (x + (h / 2))) |^ 3) * ((( sin . (x + (h / 2))) " ) |^ 2)) - ((( cos . (x - (h / 2))) |^ 3) * ((( sin . (x - (h / 2))) " ) |^ (1 + 1)))) by NEWTON: 6

      .= (((( cos . (x + (h / 2))) |^ 3) * ((( sin . (x + (h / 2))) " ) |^ 2)) - ((( cos . (x - (h / 2))) |^ 3) * ((( sin . (x - (h / 2))) " ) |^ 2)));

      hence thesis;

    end;