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

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

proof

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

end;

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

proof

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

end;

end;

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