theorem :: DIFF_4:62

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