theorem :: DIFF_4:60

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