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