let r be Real; ( - (sqrt 2) <= r & r <= - 1 implies cosec . (arccosec1 r) = r )
assume
( - (sqrt 2) <= r & r <= - 1 )
; 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
; verum