theorem :: DIFF_2:43

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