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

proof

let y be object ; :: 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:115;
then ex x being object st
( x in dom cosec & x in [.(- (PI / 2)),(- (PI / 4)).] & y = cosec . x ) by FUNCT_1:def 6;
then y in cosec .: [.(- (PI / 2)),0.[ by A1, FUNCT_1:def 6;
hence y in rng (cosec | [.(- (PI / 2)),0.[) by RELAT_1:115; :: thesis: verum

end;

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