dom (cot | ].0,PI.[) = ].0,PI.[ by Th2, RELAT_1:91;
hence rng arccot = ].0,PI.[ by FUNCT_1:55; :: thesis: verum