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:103
.=
((cosec | [.(- (PI / 2)),0 .[) " ) | ((cosec | [.(- (PI / 2)),0 .[) .: [.(- (PI / 2)),(- (PI / 4)).])
by RFUNCT_2:40
.=
((cosec | [.(- (PI / 2)),0 .[) " ) | (rng ((cosec | [.(- (PI / 2)),0 .[) | [.(- (PI / 2)),(- (PI / 4)).]))
by RELAT_1:148
.=
((cosec | [.(- (PI / 2)),0 .[) " ) | [.(- (sqrt 2)),(- 1).]
by A1, Th43, RELAT_1:103
;
hence
arccosec1 | [.(- (sqrt 2)),(- 1).] = (cosec | [.(- (PI / 2)),(- (PI / 4)).]) "
; verum