theorem :: DIFF_4:7

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