let x, h be Real; :: thesis: for f being Function of REAL ,REAL st ( for x being Real holds f . x = (tan (#) tan ) . x ) & x + (h / 2) in dom tan & x - (h / 2) in dom tan holds
(cD f,h) . x = - (((1 / 2) * ((cos (h + (2 * x))) - (cos (h - (2 * x))))) / (((cos (x + (h / 2))) * (cos (x - (h / 2)))) ^2 ))
let f be Function of REAL ,REAL ; :: thesis: ( ( for x being Real holds f . x = (tan (#) tan ) . x ) & x + (h / 2) in dom tan & x - (h / 2) in dom tan implies (cD f,h) . x = - (((1 / 2) * ((cos (h + (2 * x))) - (cos (h - (2 * x))))) / (((cos (x + (h / 2))) * (cos (x - (h / 2)))) ^2 )) )
assume that
A1: for x being Real holds f . x = (tan (#) tan ) . x and
A2: ( x + (h / 2) in dom tan & x - (h / 2) in dom tan ) ; :: thesis: (cD f,h) . x = - (((1 / 2) * ((cos (h + (2 * x))) - (cos (h - (2 * x))))) / (((cos (x + (h / 2))) * (cos (x - (h / 2)))) ^2 ))
A3: ( cos (x + (h / 2)) <> 0 & cos (x - (h / 2)) <> 0 ) by A2, FDIFF_8:1;
(cD f,h) . x = (f . (x + (h / 2))) - (f . (x - (h / 2))) by DIFF_1:5
.= ((tan (#) tan ) . (x + (h / 2))) - (f . (x - (h / 2))) by A1
.= ((tan (#) tan ) . (x + (h / 2))) - ((tan (#) tan ) . (x - (h / 2))) by A1
.= ((tan . (x + (h / 2))) * (tan . (x + (h / 2)))) - ((tan (#) tan ) . (x - (h / 2))) by VALUED_1:5
.= ((tan . (x + (h / 2))) * (tan . (x + (h / 2)))) - ((tan . (x - (h / 2))) * (tan . (x - (h / 2)))) by VALUED_1:5
.= (((sin . (x + (h / 2))) * ((cos . (x + (h / 2))) " )) * (tan . (x + (h / 2)))) - ((tan . (x - (h / 2))) * (tan . (x - (h / 2)))) by A2, RFUNCT_1:def 4
.= (((sin . (x + (h / 2))) * ((cos . (x + (h / 2))) " )) * ((sin . (x + (h / 2))) * ((cos . (x + (h / 2))) " ))) - ((tan . (x - (h / 2))) * (tan . (x - (h / 2)))) by A2, RFUNCT_1:def 4
.= (((sin . (x + (h / 2))) * ((cos . (x + (h / 2))) " )) * ((sin . (x + (h / 2))) * ((cos . (x + (h / 2))) " ))) - (((sin . (x - (h / 2))) * ((cos . (x - (h / 2))) " )) * (tan . (x - (h / 2)))) by A2, RFUNCT_1:def 4
.= ((tan (x + (h / 2))) ^2 ) - ((tan (x - (h / 2))) ^2 ) by A2, RFUNCT_1:def 4
.= ((tan (x + (h / 2))) - (tan (x - (h / 2)))) * ((tan (x + (h / 2))) + (tan (x - (h / 2))))
.= ((sin ((x + (h / 2)) - (x - (h / 2)))) / ((cos (x + (h / 2))) * (cos (x - (h / 2))))) * ((tan (x + (h / 2))) + (tan (x - (h / 2)))) by A3, SIN_COS4:24
.= ((sin h) / ((cos (x + (h / 2))) * (cos (x - (h / 2))))) * ((sin ((x + (h / 2)) + (x - (h / 2)))) / ((cos (x + (h / 2))) * (cos (x - (h / 2))))) by A3, SIN_COS4:23
.= ((sin h) * (sin (2 * x))) / (((cos (x + (h / 2))) * (cos (x - (h / 2)))) ^2 ) by XCMPLX_1:77
.= (- ((1 / 2) * ((cos (h + (2 * x))) - (cos (h - (2 * x)))))) / (((cos (x + (h / 2))) * (cos (x - (h / 2)))) ^2 ) by SIN_COS4:33
.= - (((1 / 2) * ((cos (h + (2 * x))) - (cos (h - (2 * x))))) / (((cos (x + (h / 2))) * (cos (x - (h / 2)))) ^2 )) ;
hence (cD f,h) . x = - (((1 / 2) * ((cos (h + (2 * x))) - (cos (h - (2 * x))))) / (((cos (x + (h / 2))) * (cos (x - (h / 2)))) ^2 )) ; :: thesis: verum