now for y being object holds
( ( y in [.1,(sqrt 2).] implies ex x being object st
( x in dom (cosec | [.(PI / 4),(PI / 2).]) & y = (cosec | [.(PI / 4),(PI / 2).]) . x ) ) & ( ex x being object st
( x in dom (cosec | [.(PI / 4),(PI / 2).]) & y = (cosec | [.(PI / 4),(PI / 2).]) . x ) implies y in [.1,(sqrt 2).] ) )let y be
object ;
( ( y in [.1,(sqrt 2).] implies ex x being object st
( x in dom (cosec | [.(PI / 4),(PI / 2).]) & y = (cosec | [.(PI / 4),(PI / 2).]) . x ) ) & ( ex x being object st
( x in dom (cosec | [.(PI / 4),(PI / 2).]) & y = (cosec | [.(PI / 4),(PI / 2).]) . x ) implies y in [.1,(sqrt 2).] ) )thus
(
y in [.1,(sqrt 2).] implies ex
x being
object st
(
x in dom (cosec | [.(PI / 4),(PI / 2).]) &
y = (cosec | [.(PI / 4),(PI / 2).]) . x ) )
( ex x being object st
( x in dom (cosec | [.(PI / 4),(PI / 2).]) & y = (cosec | [.(PI / 4),(PI / 2).]) . x ) implies y in [.1,(sqrt 2).] )proof
[.(PI / 4),(PI / 2).] c= ].0,(PI / 2).]
by Lm8, XXREAL_2:def 12;
then A1:
cosec | [.(PI / 4),(PI / 2).] is
continuous
by Th40, FCONT_1:16;
assume A2:
y in [.1,(sqrt 2).]
;
ex x being object st
( x in dom (cosec | [.(PI / 4),(PI / 2).]) & y = (cosec | [.(PI / 4),(PI / 2).]) . x )
then reconsider y1 =
y as
Real ;
A3:
PI / 4
<= PI / 2
by Lm8, XXREAL_1:2;
y1 in [.(cosec . (PI / 2)),(cosec . (PI / 4)).] \/ [.(cosec . (PI / 4)),(cosec . (PI / 2)).]
by A2, Th32, XBOOLE_0:def 3;
then consider x being
Real such that A4:
(
x in [.(PI / 4),(PI / 2).] &
y1 = cosec . x )
by A3, A1, Lm20, Th4, FCONT_2:15, XBOOLE_1:1;
take
x
;
( x in dom (cosec | [.(PI / 4),(PI / 2).]) & y = (cosec | [.(PI / 4),(PI / 2).]) . x )
thus
(
x in dom (cosec | [.(PI / 4),(PI / 2).]) &
y = (cosec | [.(PI / 4),(PI / 2).]) . x )
by A4, Lm32, FUNCT_1:49;
verum
end; thus
( ex
x being
object st
(
x in dom (cosec | [.(PI / 4),(PI / 2).]) &
y = (cosec | [.(PI / 4),(PI / 2).]) . x ) implies
y in [.1,(sqrt 2).] )
verum end;
hence
rng (cosec | [.(PI / 4),(PI / 2).]) = [.1,(sqrt 2).]
by FUNCT_1:def 3; verum