now 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 ;
( ( 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 ) )
( 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).]
;
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
;
( 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;
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).] )
verum end;
hence
rng (cosec | [.(- (PI / 2)),(- (PI / 4)).]) = [.(- (sqrt 2)),(- 1).]
by FUNCT_1:def 3; verum