let r be real number ; :: 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 Th87, Th88, FUNCT_1:def 5;
thus cos (arccos r) = cos . (arccos . r) by SIN_COS:def 23
.= (cos | [.0 ,PI .]) . (arccos . r) by A2, FUNCT_1:72
.= (id [.(- 1),1.]) . r by A1, Th88, Th89, FUNCT_1:23
.= r by A1, FUNCT_1:35 ; :: thesis: verum