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