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