theorem :: DIFF_4:23

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