let x be Real; :: thesis: ( x in ].0,PI.[ implies cot . x = cot x )
assume x in ].0,PI.[ ; :: thesis: cot . x = cot x
then cot . x = (cos x) / (sin x) by Th2, RFUNCT_1:def 1
.= cot x by SIN_COS4:def 2 ;
hence cot . x = cot x ; :: thesis: verum