set h = cosec | [.(- (PI / 2)),0 .[;
X: [.(- (PI / 2)),(- (PI / 4)).] c= [.(- (PI / 2)),0 .[ by Lm11, 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 Th43, X, RELAT_1:103 ;
hence arccosec1 | [.(- (sqrt 2)),(- 1).] = (cosec | [.(- (PI / 2)),(- (PI / 4)).]) " ; :: thesis: verum