A1: [.(- (PI / 2)),(- (PI / 4)).] c= [.(- (PI / 2)),0 .[ by Lm11, XXREAL_2:def 12;
A2: rng (cosec | [.(- (PI / 2)),(- (PI / 4)).]) c= rng (cosec | [.(- (PI / 2)),0 .[)

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (cosec | [.(- (PI / 2)),(- (PI / 4)).]) or y in rng (cosec | [.(- (PI / 2)),0 .[) )
assume y in rng (cosec | [.(- (PI / 2)),(- (PI / 4)).]) ; :: thesis: y in rng (cosec | [.(- (PI / 2)),0 .[)
then y in cosec .: [.(- (PI / 2)),(- (PI / 4)).] by RELAT_1:148;
then consider x being set such that
A3: x in dom cosec and
A4: x in [.(- (PI / 2)),(- (PI / 4)).] and
A5: y = cosec . x by FUNCT_1:def 12;
y in cosec .: [.(- (PI / 2)),0 .[ by A1, A3, A4, A5, FUNCT_1:def 12;
hence y in rng (cosec | [.(- (PI / 2)),0 .[) by RELAT_1:148; :: thesis: verum

end;

thus [.(- (sqrt 2)),(- 1).] c= dom arccosec1 by A2, Th43, FUNCT_1:55; :: thesis: verum