now let y be
set ;
:: thesis: ( ( y in [.((3 / 4) * PI ),PI .] implies ex x being set st
( x in dom (arcsec2 | [.(- (sqrt 2)),(- 1).]) & y = (arcsec2 | [.(- (sqrt 2)),(- 1).]) . x ) ) & ( ex x being set st
( x in dom (arcsec2 | [.(- (sqrt 2)),(- 1).]) & y = (arcsec2 | [.(- (sqrt 2)),(- 1).]) . x ) implies y in [.((3 / 4) * PI ),PI .] ) )thus
(
y in [.((3 / 4) * PI ),PI .] implies ex
x being
set st
(
x in dom (arcsec2 | [.(- (sqrt 2)),(- 1).]) &
y = (arcsec2 | [.(- (sqrt 2)),(- 1).]) . x ) )
:: thesis: ( ex x being set st
( x in dom (arcsec2 | [.(- (sqrt 2)),(- 1).]) & y = (arcsec2 | [.(- (sqrt 2)),(- 1).]) . x ) implies y in [.((3 / 4) * PI ),PI .] )proof
assume A1:
y in [.((3 / 4) * PI ),PI .]
;
:: thesis: ex x being set st
( x in dom (arcsec2 | [.(- (sqrt 2)),(- 1).]) & y = (arcsec2 | [.(- (sqrt 2)),(- 1).]) . x )
then reconsider y1 =
y as
Real ;
A2:
- (sqrt 2) < - 1
by SQUARE_1:84, XREAL_1:26;
y1 in [.(arcsec2 . (- (sqrt 2))),(arcsec2 . (- 1)).] \/ [.(arcsec2 . (- 1)),(arcsec2 . (- (sqrt 2))).]
by A1, Th74, XBOOLE_0:def 3;
then consider x being
Real such that A3:
x in [.(- (sqrt 2)),(- 1).]
and A4:
y1 = arcsec2 . x
by A2, Th94, Th46, FCONT_2:16;
take
x
;
:: thesis: ( x in dom (arcsec2 | [.(- (sqrt 2)),(- 1).]) & y = (arcsec2 | [.(- (sqrt 2)),(- 1).]) . x )
thus
(
x in dom (arcsec2 | [.(- (sqrt 2)),(- 1).]) &
y = (arcsec2 | [.(- (sqrt 2)),(- 1).]) . x )
by A3, A4, Th46, FUNCT_1:72, RELAT_1:91;
:: thesis: verum
end; thus
( ex
x being
set st
(
x in dom (arcsec2 | [.(- (sqrt 2)),(- 1).]) &
y = (arcsec2 | [.(- (sqrt 2)),(- 1).]) . x ) implies
y in [.((3 / 4) * PI ),PI .] )
:: thesis: verumproof
given x being
set such that A5:
x in dom (arcsec2 | [.(- (sqrt 2)),(- 1).])
and A6:
y = (arcsec2 | [.(- (sqrt 2)),(- 1).]) . x
;
:: thesis: y in [.((3 / 4) * PI ),PI .]
A7:
dom (arcsec2 | [.(- (sqrt 2)),(- 1).]) = [.(- (sqrt 2)),(- 1).]
by Th46, RELAT_1:91;
reconsider x1 =
x as
Real by A5;
y = arcsec2 . x
by A5, A6, A7, FUNCT_1:72;
hence
y in [.((3 / 4) * PI ),PI .]
by A5, A7, Th86;
:: thesis: verum
end; end;
hence
rng (arcsec2 | [.(- (sqrt 2)),(- 1).]) = [.((3 / 4) * PI ),PI .]
by FUNCT_1:def 5; :: thesis: verum