let x, h be Real; :: thesis: for f being Function of REAL ,REAL st ( for x being Real holds f . x = (cot (#) cos ) . x ) & x + (h / 2) in dom cot & x - (h / 2) in dom cot holds
(cD f,h) . x = (((1 / (sin (x + (h / 2)))) - (sin (x + (h / 2)))) - (1 / (sin (x - (h / 2))))) + (sin (x - (h / 2)))
let f be Function of REAL ,REAL ; :: thesis: ( ( for x being Real holds f . x = (cot (#) cos ) . x ) & x + (h / 2) in dom cot & x - (h / 2) in dom cot implies (cD f,h) . x = (((1 / (sin (x + (h / 2)))) - (sin (x + (h / 2)))) - (1 / (sin (x - (h / 2))))) + (sin (x - (h / 2))) )
assume that
A1: for x being Real holds f . x = (cot (#) cos ) . x and
A2: ( x + (h / 2) in dom cot & x - (h / 2) in dom cot ) ; :: thesis: (cD f,h) . x = (((1 / (sin (x + (h / 2)))) - (sin (x + (h / 2)))) - (1 / (sin (x - (h / 2))))) + (sin (x - (h / 2)))
(cD f,h) . x = (f . (x + (h / 2))) - (f . (x - (h / 2))) by DIFF_1:5
.= ((cot (#) cos ) . (x + (h / 2))) - (f . (x - (h / 2))) by A1
.= ((cot (#) cos ) . (x + (h / 2))) - ((cot (#) cos ) . (x - (h / 2))) by A1
.= ((cot . (x + (h / 2))) * (cos . (x + (h / 2)))) - ((cot (#) cos ) . (x - (h / 2))) by VALUED_1:5
.= ((cot . (x + (h / 2))) * (cos . (x + (h / 2)))) - ((cot . (x - (h / 2))) * (cos . (x - (h / 2)))) by VALUED_1:5
.= (((cos . (x + (h / 2))) * ((sin . (x + (h / 2))) " )) * (cos . (x + (h / 2)))) - ((cot . (x - (h / 2))) * (cos . (x - (h / 2)))) by A2, RFUNCT_1:def 4
.= (((cos (x + (h / 2))) / (sin (x + (h / 2)))) * (cos (x + (h / 2)))) - (((cos (x - (h / 2))) / (sin (x - (h / 2)))) * (cos (x - (h / 2)))) by A2, RFUNCT_1:def 4
.= ((cos (x + (h / 2))) / ((sin (x + (h / 2))) / (cos (x + (h / 2))))) - (((cos (x - (h / 2))) / (sin (x - (h / 2)))) * (cos (x - (h / 2)))) by XCMPLX_1:83
.= ((cos (x + (h / 2))) / ((sin (x + (h / 2))) / (cos (x + (h / 2))))) - ((cos (x - (h / 2))) / ((sin (x - (h / 2))) / (cos (x - (h / 2))))) by XCMPLX_1:83
.= (((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 XCMPLX_1:78
.= (((cos (x + (h / 2))) * (cos (x + (h / 2)))) / (sin (x + (h / 2)))) - (((cos (x - (h / 2))) * (cos (x - (h / 2)))) / (sin (x - (h / 2)))) by XCMPLX_1:78
.= ((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)))) by SIN_COS4:7
.= ((1 / (sin (x + (h / 2)))) - (((sin (x + (h / 2))) * (sin (x + (h / 2)))) / (sin (x + (h / 2))))) - ((1 - ((sin (x - (h / 2))) * (sin (x - (h / 2))))) / (sin (x - (h / 2)))) by SIN_COS4:7
.= ((1 / (sin (x + (h / 2)))) - (sin (x + (h / 2)))) - ((1 / (sin (x - (h / 2)))) - (((sin (x - (h / 2))) * (sin (x - (h / 2)))) / (sin (x - (h / 2))))) by A2, FDIFF_8:2, XCMPLX_1:90
.= ((1 / (sin (x + (h / 2)))) - (sin (x + (h / 2)))) - ((1 / (sin (x - (h / 2)))) - (sin (x - (h / 2)))) by A2, FDIFF_8:2, XCMPLX_1:90
.= (((1 / (sin (x + (h / 2)))) - (sin (x + (h / 2)))) - (1 / (sin (x - (h / 2))))) + (sin (x - (h / 2))) ;
hence (cD f,h) . x = (((1 / (sin (x + (h / 2)))) - (sin (x + (h / 2)))) - (1 / (sin (x - (h / 2))))) + (sin (x - (h / 2))) ; :: thesis: verum