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