let h, x be Real; :: thesis: (cD (cos,h)) . x = - (2 * ((sin x) * (sin (h / 2))))
(cD (cos,h)) . x = (cos (x + (h / 2))) - (cos (x - (h / 2))) by DIFF_1:5
.= - (2 * ((sin (((x + (h / 2)) + (x - (h / 2))) / 2)) * (sin (((x + (h / 2)) - (x - (h / 2))) / 2)))) by SIN_COS4:18 ;
hence (cD (cos,h)) . x = - (2 * ((sin x) * (sin (h / 2)))) ; :: thesis: verum