theorem :: DIFF_4:56

for x0, x1 being Real st x0 in dom tan & x1 in dom tan holds
[!((tan (#) tan) (#) sin),x0,x1!] = ((((sin x0) |^ 3) * ((cos x1) ^2)) - (((sin x1) |^ 3) * ((cos x0) ^2))) / ((((cos x0) ^2) * ((cos x1) ^2)) * (x0 - x1))