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