theorem Th87: :: SIN_COS6:87

(cos | [.0,PI.]) * arccos = id [.(- 1),1.] by COMPTRIG:32, FUNCT_1:39;