dom (cos | [.0,PI.]) = [.0,PI.] by RELAT_1:62, SIN_COS:24;
hence rng arccos = [.0,PI.] by FUNCT_1:33; :: thesis: verum