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:62;
A4: r in ].0,PI.[ by A1, A2, XXREAL_1:4;
then arccot (cot . r) = arccot . ((cot | ].0,PI.[) . r) by FUNCT_1:49
.= (id ].0,PI.[) . r by A4, A3, Th32, FUNCT_1:13
.= r by A4, FUNCT_1:18 ;
hence ( arccot (cot . r) = r & arccot (cot r) = r ) by A4, Th14; :: thesis: verum