now

let y be set ; :: thesis: ( ( y in [.(- (sqrt 2)),(- 1).] implies ex x being set st
( x in dom (cosec | [.(- (PI / 2)),(- (PI / 4)).]) & y = (cosec | [.(- (PI / 2)),(- (PI / 4)).]) . x ) ) & ( ex x being set 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 set st
( x in dom (cosec | [.(- (PI / 2)),(- (PI / 4)).]) & y = (cosec | [.(- (PI / 2)),(- (PI / 4)).]) . x ) ) :: thesis: ( ex x being set st
( x in dom (cosec | [.(- (PI / 2)),(- (PI / 4)).]) & y = (cosec | [.(- (PI / 2)),(- (PI / 4)).]) . x ) implies y in [.(- (sqrt 2)),(- 1).] )

proof

assume A1: y in [.(- (sqrt 2)),(- 1).] ; :: thesis: ex x being set st
( x in dom (cosec | [.(- (PI / 2)),(- (PI / 4)).]) & y = (cosec | [.(- (PI / 2)),(- (PI / 4)).]) . x )
then reconsider y1 = y as Real ;
A2: - (PI / 2) <= - (PI / 4) by Lm11, XXREAL_1:3;
[.(- (PI / 2)),(- (PI / 4)).] c= [.(- (PI / 2)),0 .[ by Lm11, XXREAL_2:def 12;
then A4: cosec | [.(- (PI / 2)),(- (PI / 4)).] is continuous by Th39, FCONT_1:17;
y1 in [.(cosec . (- (PI / 4))),(cosec . (- (PI / 2))).] \/ [.(cosec . (- (PI / 2))),(cosec . (- (PI / 4))).] by A1, Th32, XBOOLE_0:def 3;
then consider x being Real such that
A5: x in [.(- (PI / 2)),(- (PI / 4)).] and
A6: y1 = cosec . x by A2, A4, X7, FCONT_2:16;
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 A5, A6, Lm15, FUNCT_1:72; :: thesis: verum

end;

thus ( ex x being set 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 set such that A7: x in dom (cosec | [.(- (PI / 2)),(- (PI / 4)).]) and
A8: y = (cosec | [.(- (PI / 2)),(- (PI / 4)).]) . x ; :: thesis: y in [.(- (sqrt 2)),(- 1).]
reconsider x1 = x as Real by A7;
y = cosec . x1 by A7, A8, Lm15, FUNCT_1:72;
hence y in [.(- (sqrt 2)),(- 1).] by A7, Lm15, Th35; :: thesis: verum

end;

end;

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