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:23;
hence cot is_differentiable_in x by FDIFF_7:47; :: thesis: verum

end;

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