dom (cos | [.0,PI.]) = [.0,PI.] by RELAT_1:91, SIN_COS:27;
hence rng arccos = [.0,PI.] by FUNCT_1:55; :: thesis: verum