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