set h = cosec | [.(- (PI / 2)),0.[;
A1:
[.(- (PI / 2)),(- (PI / 4)).] c= [.(- (PI / 2)),0.[
by Lm7, XXREAL_2:def 12;
then (cosec | [.(- (PI / 2)),(- (PI / 4)).]) " =
((cosec | [.(- (PI / 2)),0.[) | [.(- (PI / 2)),(- (PI / 4)).]) "
by RELAT_1:74
.=
((cosec | [.(- (PI / 2)),0.[) ") | ((cosec | [.(- (PI / 2)),0.[) .: [.(- (PI / 2)),(- (PI / 4)).])
by RFUNCT_2:17
.=
((cosec | [.(- (PI / 2)),0.[) ") | (rng ((cosec | [.(- (PI / 2)),0.[) | [.(- (PI / 2)),(- (PI / 4)).]))
by RELAT_1:115
.=
((cosec | [.(- (PI / 2)),0.[) ") | [.(- (sqrt 2)),(- 1).]
by A1, Th43, RELAT_1:74
;
hence
arccosec1 | [.(- (sqrt 2)),(- 1).] = (cosec | [.(- (PI / 2)),(- (PI / 4)).]) "
; verum