theorem :: SIN_COS9:10

cot | ].0,PI.[ is one-to-one by Th8, FCONT_3:8;