now :: thesis: for y being object holds
( ( y in [.0,(PI / 4).] implies ex x being object st
( x in dom (arcsec1 | [.1,(sqrt 2).]) & y = (arcsec1 | [.1,(sqrt 2).]) . x ) ) & ( ex x being object st
( x in dom (arcsec1 | [.1,(sqrt 2).]) & y = (arcsec1 | [.1,(sqrt 2).]) . x ) implies y in [.0,(PI / 4).] ) )

let y be object ; :: thesis: ( ( y in [.0,(PI / 4).] implies ex x being object st
( x in dom (arcsec1 | [.1,(sqrt 2).]) & y = (arcsec1 | [.1,(sqrt 2).]) . x ) ) & ( ex x being object st
( x in dom (arcsec1 | [.1,(sqrt 2).]) & y = (arcsec1 | [.1,(sqrt 2).]) . x ) implies y in [.0,(PI / 4).] ) )
thus ( y in [.0,(PI / 4).] implies ex x being object st
( x in dom (arcsec1 | [.1,(sqrt 2).]) & y = (arcsec1 | [.1,(sqrt 2).]) . x ) ) :: thesis: ( ex x being object st
( x in dom (arcsec1 | [.1,(sqrt 2).]) & y = (arcsec1 | [.1,(sqrt 2).]) . x ) implies y in [.0,(PI / 4).] )

proof

assume A1: y in [.0,(PI / 4).] ; :: thesis: ex x being object st
( x in dom (arcsec1 | [.1,(sqrt 2).]) & y = (arcsec1 | [.1,(sqrt 2).]) . x )
then reconsider y1 = y as Real ;
y1 in [.(arcsec1 . 1),(arcsec1 . (sqrt 2)).] \/ [.(arcsec1 . (sqrt 2)),(arcsec1 . 1).] by A1, Th73, XBOOLE_0:def 3;
then consider x being Real such that
A2: ( x in [.1,(sqrt 2).] & y1 = arcsec1 . x ) by Th45, Th93, FCONT_2:15, SQUARE_1:19;
take x ; :: thesis: ( x in dom (arcsec1 | [.1,(sqrt 2).]) & y = (arcsec1 | [.1,(sqrt 2).]) . x )
thus ( x in dom (arcsec1 | [.1,(sqrt 2).]) & y = (arcsec1 | [.1,(sqrt 2).]) . x ) by A2, Th45, FUNCT_1:49, RELAT_1:62; :: thesis: verum

end;

thus ( ex x being object st
( x in dom (arcsec1 | [.1,(sqrt 2).]) & y = (arcsec1 | [.1,(sqrt 2).]) . x ) implies y in [.0,(PI / 4).] ) :: thesis: verum

proof

given x being object such that A3: x in dom (arcsec1 | [.1,(sqrt 2).]) and
A4: y = (arcsec1 | [.1,(sqrt 2).]) . x ; :: thesis: y in [.0,(PI / 4).]
A5: dom (arcsec1 | [.1,(sqrt 2).]) = [.1,(sqrt 2).] by Th45, RELAT_1:62;
then y = arcsec1 . x by A3, A4, FUNCT_1:49;
hence y in [.0,(PI / 4).] by A3, A5, Th85; :: thesis: verum

end;

end;

hence rng (arcsec1 | [.1,(sqrt 2).]) = [.0,(PI / 4).] by FUNCT_1:def 3; :: thesis: verum