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:62;
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:49
.= (id ].0,(PI / 2).]) . r by A2, A1, Th68, FUNCT_1:13
.= r by A2, FUNCT_1:18 ;
hence arccosec2 (cosec . r) = r ; :: thesis: verum