let r be real number ; :: thesis: ( 0 <= r & r <= PI implies arccos (cos r) = r )
A1: dom (cos | [.0,PI.]) = [.0,PI.] by RELAT_1:91, SIN_COS:27;
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 23
.= arccos . ((cos | [.0,PI.]) . r) by A2, FUNCT_1:72
.= (id [.0,PI.]) . r by A2, A1, Th91, FUNCT_1:23
.= r by A2, FUNCT_1:35 ; :: thesis: verum