let r be real number ; :: thesis: ( 0 <= r & r <= PI implies arccos (cos r) = r )
assume ( 0 <= r & r <= PI ) ; :: thesis: arccos (cos r) = r
then A1: r in [.0 ,PI .] by XXREAL_1:1;
A2: dom (cos | [.0 ,PI .]) = [.0 ,PI .] by Lm2, RELAT_1:91;
thus arccos (cos r) = arccos . (cos . r) by SIN_COS:def 23
.= arccos . ((cos | [.0 ,PI .]) . r) by A1, FUNCT_1:72
.= (id [.0 ,PI .]) . r by A1, A2, Th91, FUNCT_1:23
.= r by A1, FUNCT_1:35 ; :: thesis: verum