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:62;
cosec . (arccosec1 r) = (cosec | [.(- (PI / 2)),(- (PI / 4)).]) . (arccosec1 . r) by A1, Th87, FUNCT_1:49
.= (cosec | [.(- (PI / 2)),(- (PI / 4)).]) . ((arccosec1 | [.(- (sqrt 2)),(- 1).]) . r) by A1, FUNCT_1:49
.= ((cosec | [.(- (PI / 2)),(- (PI / 4)).]) * (arccosec1 | [.(- (sqrt 2)),(- 1).])) . r by A2, FUNCT_1:13
.= (id [.(- (sqrt 2)),(- 1).]) . r by Th43, Th51, FUNCT_1:39
.= r by A1, FUNCT_1:18 ;
hence cosec . (arccosec1 r) = r ; :: thesis: verum