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