now for y being object holds
( ( y in [.(PI / 4),(PI / 2).] implies ex x being object st
( x in dom (arccosec2 | [.1,(sqrt 2).]) & y = (arccosec2 | [.1,(sqrt 2).]) . x ) ) & ( ex x being object st
( x in dom (arccosec2 | [.1,(sqrt 2).]) & y = (arccosec2 | [.1,(sqrt 2).]) . x ) implies y in [.(PI / 4),(PI / 2).] ) )let y be
object ;
( ( y in [.(PI / 4),(PI / 2).] implies ex x being object st
( x in dom (arccosec2 | [.1,(sqrt 2).]) & y = (arccosec2 | [.1,(sqrt 2).]) . x ) ) & ( ex x being object st
( x in dom (arccosec2 | [.1,(sqrt 2).]) & y = (arccosec2 | [.1,(sqrt 2).]) . x ) implies y in [.(PI / 4),(PI / 2).] ) )thus
(
y in [.(PI / 4),(PI / 2).] implies ex
x being
object st
(
x in dom (arccosec2 | [.1,(sqrt 2).]) &
y = (arccosec2 | [.1,(sqrt 2).]) . x ) )
( ex x being object st
( x in dom (arccosec2 | [.1,(sqrt 2).]) & y = (arccosec2 | [.1,(sqrt 2).]) . x ) implies y in [.(PI / 4),(PI / 2).] )proof
assume A1:
y in [.(PI / 4),(PI / 2).]
;
ex x being object st
( x in dom (arccosec2 | [.1,(sqrt 2).]) & y = (arccosec2 | [.1,(sqrt 2).]) . x )
then reconsider y1 =
y as
Real ;
y1 in [.(arccosec2 . (sqrt 2)),(arccosec2 . 1).] \/ [.(arccosec2 . 1),(arccosec2 . (sqrt 2)).]
by A1, Th76, XBOOLE_0:def 3;
then consider x being
Real such that A2:
(
x in [.1,(sqrt 2).] &
y1 = arccosec2 . x )
by Th48, Th96, FCONT_2:15, SQUARE_1:19;
take
x
;
( x in dom (arccosec2 | [.1,(sqrt 2).]) & y = (arccosec2 | [.1,(sqrt 2).]) . x )
thus
(
x in dom (arccosec2 | [.1,(sqrt 2).]) &
y = (arccosec2 | [.1,(sqrt 2).]) . x )
by A2, Th48, FUNCT_1:49, RELAT_1:62;
verum
end; thus
( ex
x being
object st
(
x in dom (arccosec2 | [.1,(sqrt 2).]) &
y = (arccosec2 | [.1,(sqrt 2).]) . x ) implies
y in [.(PI / 4),(PI / 2).] )
verumproof
given x being
object such that A3:
x in dom (arccosec2 | [.1,(sqrt 2).])
and A4:
y = (arccosec2 | [.1,(sqrt 2).]) . x
;
y in [.(PI / 4),(PI / 2).]
A5:
dom (arccosec2 | [.1,(sqrt 2).]) = [.1,(sqrt 2).]
by Th48, RELAT_1:62;
then
y = arccosec2 . x
by A3, A4, FUNCT_1:49;
hence
y in [.(PI / 4),(PI / 2).]
by A3, A5, Th88;
verum
end; end;
hence
rng (arccosec2 | [.1,(sqrt 2).]) = [.(PI / 4),(PI / 2).]
by FUNCT_1:def 3; verum