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

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (sec | [.0,(PI / 4).]) or y in rng (sec | [.0,(PI / 2).[) )
assume y in rng (sec | [.0,(PI / 4).]) ; :: thesis: y in rng (sec | [.0,(PI / 2).[)
then y in sec .: [.0,(PI / 4).] by RELAT_1:115;
then ex x being object st
( x in dom sec & x in [.0,(PI / 4).] & y = sec . x ) by FUNCT_1:def 6;
then y in sec .: [.0,(PI / 2).[ by A1, FUNCT_1:def 6;
hence y in rng (sec | [.0,(PI / 2).[) by RELAT_1:115; :: thesis: verum

end;

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