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