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