A2: arccosec1 . (- 1) = arccosec1 (- 1)
.= - (PI / 2) by Th32, Th71 ;
A3: ( - (PI / 2) <= - (PI / 4) & - (PI / 4) < 0 ) by Lm11, XXREAL_1:3;
arccosec1 . (- (sqrt 2)) = arccosec1 (- (sqrt 2))
.= - (PI / 4) by A3, Th32, Th71 ;
hence ( arccosec1 . (- 1) = - (PI / 2) & arccosec1 . (- (sqrt 2)) = - (PI / 4) ) by A2; :: thesis: verum