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

proof

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

end;

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