theorem :: DIFF_2:47

for h, x being Real holds (bD (cos,h)) . x = - (2 * ((sin (((2 * x) - h) / 2)) * (sin (h / 2))))