theorem :: DIFF_4:24

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