now

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

proof

assume A1: y in [.(PI / 4),(PI / 2).] ; :: thesis: ex x being set st
( x in dom (arccosec2 | [.1,(sqrt 2).]) & y = (arccosec2 | [.1,(sqrt 2).]) . x )
then reconsider y1 = y as Real ;
y1 in [.(arccosec2 . (sqrt 2)),(arccosec2 . 1).] \/ [.(arccosec2 . 1),(arccosec2 . (sqrt 2)).] by A1, Th76, XBOOLE_0:def 3;
then consider x being Real such that
A2: ( x in [.1,(sqrt 2).] & y1 = arccosec2 . x ) by Th48, Th96, FCONT_2:16, SQUARE_1:84;
take x ; :: thesis: ( x in dom (arccosec2 | [.1,(sqrt 2).]) & y = (arccosec2 | [.1,(sqrt 2).]) . x )
thus ( x in dom (arccosec2 | [.1,(sqrt 2).]) & y = (arccosec2 | [.1,(sqrt 2).]) . x ) by A2, Th48, FUNCT_1:72, RELAT_1:91; :: thesis: verum

end;

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

proof

given x being set such that A3: x in dom (arccosec2 | [.1,(sqrt 2).]) and
A4: y = (arccosec2 | [.1,(sqrt 2).]) . x ; :: thesis: y in [.(PI / 4),(PI / 2).]
A5: dom (arccosec2 | [.1,(sqrt 2).]) = [.1,(sqrt 2).] by Th48, RELAT_1:91;
then y = arccosec2 . x by A3, A4, FUNCT_1:72;
hence y in [.(PI / 4),(PI / 2).] by A3, A5, Th88; :: thesis: verum

end;

end;

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