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:22 ;
hence (cD cos ,h) . x = - (2 * ((sin x) * (sin (h / 2)))) ; :: thesis: verum