let r be Real; :: thesis: ( - (PI / 2) <= r & r < 0 implies arccosec1 (cosec . r) = r )
assume ( - (PI / 2) <= r & r < 0 ) ; :: thesis: arccosec1 (cosec . r) = r
then A1: r in [.(- (PI / 2)),0 .[ ;
A2: dom (cosec | [.(- (PI / 2)),0 .[) = [.(- (PI / 2)),0 .[ by Th3, RELAT_1:91;
arccosec1 (cosec . r) = arccosec1 . ((cosec | [.(- (PI / 2)),0 .[) . r) by A1, FUNCT_1:72
.= (id [.(- (PI / 2)),0 .[) . r by A1, A2, Th67, FUNCT_1:23
.= r by A1, FUNCT_1:35 ;
hence arccosec1 (cosec . r) = r ; :: thesis: verum