let r be Real; :: thesis: ( - (sqrt 2) <= r & r <= - 1 implies cosec . (arccosec1 r) = r )
assume ( - (sqrt 2) <= r & r <= - 1 ) ; :: thesis: cosec . (arccosec1 r) = r
then A1: r in [.(- (sqrt 2)),(- 1).] ;
then A2: r in dom (arccosec1 | [.(- (sqrt 2)),(- 1).]) by Th47, RELAT_1:91;
cosec . (arccosec1 r) = (cosec | [.(- (PI / 2)),(- (PI / 4)).]) . (arccosec1 . r) by A1, Th87, FUNCT_1:72
.= (cosec | [.(- (PI / 2)),(- (PI / 4)).]) . ((arccosec1 | [.(- (sqrt 2)),(- 1).]) . r) by A1, FUNCT_1:72
.= ((cosec | [.(- (PI / 2)),(- (PI / 4)).]) * (arccosec1 | [.(- (sqrt 2)),(- 1).])) . r by A2, FUNCT_1:23
.= (id [.(- (sqrt 2)),(- 1).]) . r by Th43, Th51, FUNCT_1:61
.= r by A1, FUNCT_1:35 ;
hence cosec . (arccosec1 r) = r ; :: thesis: verum