theorem :: DIFF_2:44

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