theorem :: DIFF_4:63

for h, x being Real st x + (h / 2) in dom cot & x - (h / 2) in dom cot holds
(cD (((cot (#) cot) (#) cos),h)) . x = (((cos . (x + (h / 2))) |^ 3) * (((sin . (x + (h / 2))) ") |^ 2)) - (((cos . (x - (h / 2))) |^ 3) * (((sin . (x - (h / 2))) ") |^ 2))