let r be Real; :: thesis: ( - 1 <= r & r <= 1 implies cos (arccos r) = r )
assume ( - 1 <= r & r <= 1 ) ; :: thesis: cos (arccos r) = r
then A1: r in [.(- 1),1.] by XXREAL_1:1;
then A2: arccos . r in [.0,PI.] by Th85, Th86, FUNCT_1:def 3;
thus cos (arccos r) = cos . (arccos . r) by SIN_COS:def 19
.= (cos | [.0,PI.]) . (arccos . r) by A2, FUNCT_1:49
.= (id [.(- 1),1.]) . r by A1, Th86, Th87, FUNCT_1:13
.= r by A1, FUNCT_1:18 ; :: thesis: verum