for x being Real st x in ].0,PI.[ holds
cot is_differentiable_in x

proof

let x be Real; :: thesis: ( x in ].0,PI.[ implies cot is_differentiable_in x )
assume x in ].0,PI.[ ; :: thesis: cot is_differentiable_in x
then sin . x <> 0 by COMPTRIG:7;
hence cot is_differentiable_in x by FDIFF_7:47; :: thesis: verum

end;

hence cot is_differentiable_on ].0,PI.[ by Th2, FDIFF_1:9; :: thesis: verum