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