theorem :: DIFF_4:57

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