theorem :: DIFF_4:26

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