let r be Real; :: thesis: ( 1 <= r & r <= sqrt 2 implies cosec . (arccosec2 r) = r )
assume ( 1 <= r & r <= sqrt 2 ) ; :: thesis: cosec . (arccosec2 r) = r
then A1: r in [.1,(sqrt 2).] ;
then A2: r in dom (arccosec2 | [.1,(sqrt 2).]) by Th48, RELAT_1:91;
cosec . (arccosec2 r) = (cosec | [.(PI / 4),(PI / 2).]) . (arccosec2 . r) by A1, Th88, FUNCT_1:72
.= (cosec | [.(PI / 4),(PI / 2).]) . ((arccosec2 | [.1,(sqrt 2).]) . r) by A1, FUNCT_1:72
.= ((cosec | [.(PI / 4),(PI / 2).]) * (arccosec2 | [.1,(sqrt 2).])) . r by A2, FUNCT_1:23
.= (id [.1,(sqrt 2).]) . r by Th44, Th52, FUNCT_1:61
.= r by A1, FUNCT_1:35 ;
hence cosec . (arccosec2 r) = r ; :: thesis: verum