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

proof

let y be set ; :: 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:148;
then consider x being set such that
A3: x in dom sec and
A4: x in [.0 ,(PI / 4).] and
A5: y = sec . x by FUNCT_1:def 12;
y in sec .: [.0 ,(PI / 2).[ by A1, A3, A4, A5, FUNCT_1:def 12;
hence y in rng (sec | [.0 ,(PI / 2).[) by RELAT_1:148; :: thesis: verum

end;

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