theorem :: DIFF_4:22

for x0, x1 being Real st x0 in dom tan & x1 in dom tan holds
[!((tan (#) tan) (#) cos),x0,x1!] = [!(tan (#) sin),x0,x1!]