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