theorem :: DIFF_4:61

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