set f = cos | [.0 ,PI .];
dom (cos | [.0 ,PI .]) = [.0 ,PI .] by RELAT_1:91, SIN_COS:27;
then ( (cos | [.0 ,PI .]) | [.0 ,PI .] = cos | [.0 ,PI .] & (((cos | [.0 ,PI .]) | [.0 ,PI .]) " ) | ((cos | [.0 ,PI .]) .: [.0 ,PI .]) is continuous ) by COMPTRIG:41, FCONT_1:54, RELAT_1:102;
hence arccos | [.(- 1),1.] is continuous by COMPTRIG:50, RELAT_1:148; :: thesis: verum