theorem :: DIFF_4:58

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