theorem :: DIFF_2:48

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