let r be Real; :: thesis: ( 0 < r & r < PI implies ( arccot (cot . r) = r & arccot (cot r) = r ) )
assume ( 0 < r & r < PI ) ; :: thesis: ( arccot (cot . r) = r & arccot (cot r) = r )
then A1: r in ].0 ,PI .[ by XXREAL_1:4;
A2: dom (cot | ].0 ,PI .[) = ].0 ,PI .[ by Th2, RELAT_1:91;
A3: arccot (cot . r) = arccot . ((cot | ].0 ,PI .[) . r) by A1, FUNCT_1:72
.= (id ].0 ,PI .[) . r by A1, A2, Th30, FUNCT_1:23
.= r by A1, FUNCT_1:35 ;
thus ( arccot (cot . r) = r & arccot (cot r) = r ) by A1, A3, Th14; :: thesis: verum