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

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

proof

[.(- (PI / 2)),(- (PI / 4)).] c= [.(- (PI / 2)),0.[ by Lm7, XXREAL_2:def 12;
then A1: cosec | [.(- (PI / 2)),(- (PI / 4)).] is continuous by Th39, FCONT_1:16;
assume A2: y in [.(- (sqrt 2)),(- 1).] ; :: thesis: ex x being object st
( x in dom (cosec | [.(- (PI / 2)),(- (PI / 4)).]) & y = (cosec | [.(- (PI / 2)),(- (PI / 4)).]) . x )
then reconsider y1 = y as Real ;
A3: - (PI / 2) <= - (PI / 4) by Lm7, XXREAL_1:3;
y1 in [.(cosec . (- (PI / 4))),(cosec . (- (PI / 2))).] \/ [.(cosec . (- (PI / 2))),(cosec . (- (PI / 4))).] by A2, Th32, XBOOLE_0:def 3;
then consider x being Real such that
A4: ( x in [.(- (PI / 2)),(- (PI / 4)).] & y1 = cosec . x ) by A3, A1, Lm19, Th3, FCONT_2:15, XBOOLE_1:1;
take x ; :: thesis: ( x in dom (cosec | [.(- (PI / 2)),(- (PI / 4)).]) & y = (cosec | [.(- (PI / 2)),(- (PI / 4)).]) . x )
thus ( x in dom (cosec | [.(- (PI / 2)),(- (PI / 4)).]) & y = (cosec | [.(- (PI / 2)),(- (PI / 4)).]) . x ) by A4, Lm31, FUNCT_1:49; :: thesis: verum

end;

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

proof

given x being object such that A5: x in dom (cosec | [.(- (PI / 2)),(- (PI / 4)).]) and
A6: y = (cosec | [.(- (PI / 2)),(- (PI / 4)).]) . x ; :: thesis: y in [.(- (sqrt 2)),(- 1).]
reconsider x1 = x as Real by A5;
y = cosec . x1 by A5, A6, Lm31, FUNCT_1:49;
hence y in [.(- (sqrt 2)),(- 1).] by A5, Lm31, Th35; :: thesis: verum

end;

end;

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