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