theorem :: DIFF_4:59

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