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