let x, h be Real; :: thesis: for f being Function of REAL ,REAL st ( for x being Real holds f . x = 1 / (cos x) ) & cos (x + (h / 2)) <> 0 & cos (x - (h / 2)) <> 0 holds
(cD f,h) . x = (2 * ((cos (x - (h / 2))) - (cos (x + (h / 2))))) / ((cos (2 * x)) + (cos h))
let f be Function of REAL ,REAL ; :: thesis: ( ( for x being Real holds f . x = 1 / (cos x) ) & cos (x + (h / 2)) <> 0 & cos (x - (h / 2)) <> 0 implies (cD f,h) . x = (2 * ((cos (x - (h / 2))) - (cos (x + (h / 2))))) / ((cos (2 * x)) + (cos h)) )
assume that
A1: for x being Real holds f . x = 1 / (cos x) and
A2: ( cos (x + (h / 2)) <> 0 & cos (x - (h / 2)) <> 0 ) ; :: thesis: (cD f,h) . x = (2 * ((cos (x - (h / 2))) - (cos (x + (h / 2))))) / ((cos (2 * x)) + (cos h))
(cD f,h) . x = (f . (x + (h / 2))) - (f . (x - (h / 2))) by DIFF_1:5
.= (1 / (cos (x + (h / 2)))) - (f . (x - (h / 2))) by A1
.= (1 / (cos (x + (h / 2)))) - (1 / (cos (x - (h / 2)))) by A1
.= ((1 * (cos (x - (h / 2)))) - (1 * (cos (x + (h / 2))))) / ((cos (x + (h / 2))) * (cos (x - (h / 2)))) by A2, XCMPLX_1:131
.= ((cos (x - (h / 2))) - (cos (x + (h / 2)))) / ((1 / 2) * ((cos ((x + (h / 2)) + (x - (h / 2)))) + (cos ((x + (h / 2)) - (x - (h / 2)))))) by SIN_COS4:36
.= (((cos (x - (h / 2))) - (cos (x + (h / 2)))) / (1 / 2)) / ((cos (2 * x)) + (cos h)) by XCMPLX_1:79
.= 2 * (((cos (x - (h / 2))) - (cos (x + (h / 2)))) / ((cos (2 * x)) + (cos h))) ;
hence (cD f,h) . x = (2 * ((cos (x - (h / 2))) - (cos (x + (h / 2))))) / ((cos (2 * x)) + (cos h)) ; :: thesis: verum