set f = cos | [.0,PI.];
dom (cos | [.0,PI.]) = [.0,PI.] by RELAT_1:62, SIN_COS:24;
then ( (cos | [.0,PI.]) | [.0,PI.] = cos | [.0,PI.] & (((cos | [.0,PI.]) | [.0,PI.]) ") | ((cos | [.0,PI.]) .: [.0,PI.]) is continuous ) by COMPTRIG:25, FCONT_1:47, RELAT_1:73;
hence arccos | [.(- 1),1.] is continuous by COMPTRIG:32, RELAT_1:115; :: thesis: verum