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

proof

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

end;

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