let x be real number ; :: 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 4
.= cot x by SIN_COS4:def 2 ;
hence cot . x = cot x ; :: thesis: verum