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