let r be Real; :: thesis: ( 0 < r & r <= PI / 2 implies arccosec2 (cosec . r) = r )
A1: dom (cosec | ].0 ,(PI / 2).]) = ].0 ,(PI / 2).] by Th4, RELAT_1:91;
assume ( 0 < r & r <= PI / 2 ) ; :: thesis: arccosec2 (cosec . r) = r
then A2: r in ].0 ,(PI / 2).] ;
then arccosec2 (cosec . r) = arccosec2 . ((cosec | ].0 ,(PI / 2).]) . r) by FUNCT_1:72
.= (id ].0 ,(PI / 2).]) . r by A2, A1, Th68, FUNCT_1:23
.= r by A2, FUNCT_1:35 ;
hence arccosec2 (cosec . r) = r ; :: thesis: verum