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