now let y be
set ;
:: thesis: ( ( y in [.(PI / 4),(PI / 2).] implies ex x being set st
( x in dom (arccosec2 | [.1,(sqrt 2).]) & y = (arccosec2 | [.1,(sqrt 2).]) . x ) ) & ( ex x being set 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
set st
(
x in dom (arccosec2 | [.1,(sqrt 2).]) &
y = (arccosec2 | [.1,(sqrt 2).]) . x ) )
:: thesis: ( ex x being set 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).]
;
:: thesis: ex x being set 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).]
and A3:
y1 = arccosec2 . x
by Th96, Th48, FCONT_2:16, SQUARE_1:84;
take
x
;
:: thesis: ( 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, A3, Th48, FUNCT_1:72, RELAT_1:91;
:: thesis: verum
end; thus
( ex
x being
set st
(
x in dom (arccosec2 | [.1,(sqrt 2).]) &
y = (arccosec2 | [.1,(sqrt 2).]) . x ) implies
y in [.(PI / 4),(PI / 2).] )
:: thesis: verumproof
given x being
set such that A4:
x in dom (arccosec2 | [.1,(sqrt 2).])
and A5:
y = (arccosec2 | [.1,(sqrt 2).]) . x
;
:: thesis: y in [.(PI / 4),(PI / 2).]
A6:
dom (arccosec2 | [.1,(sqrt 2).]) = [.1,(sqrt 2).]
by Th48, RELAT_1:91;
reconsider x1 =
x as
Real by A4;
y = arccosec2 . x
by A4, A5, A6, FUNCT_1:72;
hence
y in [.(PI / 4),(PI / 2).]
by A4, A6, Th88;
:: thesis: verum
end; end;
hence
rng (arccosec2 | [.1,(sqrt 2).]) = [.(PI / 4),(PI / 2).]
by FUNCT_1:def 5; :: thesis: verum