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