theorem :: DIFF_4:28

for h, x being Real st x in dom cot & x - h in dom cot holds
(bD (((cot (#) cot) (#) sin),h)) . x = ((cot (#) cos) . x) - ((cot (#) cos) . (x - h))