let r be Real; ( - 1 <= r & r <= 1 implies cos (arccos r) = r )
assume
( - 1 <= r & r <= 1 )
; 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
; verum