now for y being object holds
( ( y in [.1,(sqrt 2).] implies ex x being object st
( x in dom (sec | [.0,(PI / 4).]) & y = (sec | [.0,(PI / 4).]) . x ) ) & ( ex x being object st
( x in dom (sec | [.0,(PI / 4).]) & y = (sec | [.0,(PI / 4).]) . 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 (sec | [.0,(PI / 4).]) & y = (sec | [.0,(PI / 4).]) . x ) ) & ( ex x being object st
( x in dom (sec | [.0,(PI / 4).]) & y = (sec | [.0,(PI / 4).]) . x ) implies y in [.1,(sqrt 2).] ) )thus
(
y in [.1,(sqrt 2).] implies ex
x being
object st
(
x in dom (sec | [.0,(PI / 4).]) &
y = (sec | [.0,(PI / 4).]) . x ) )
( ex x being object st
( x in dom (sec | [.0,(PI / 4).]) & y = (sec | [.0,(PI / 4).]) . x ) implies y in [.1,(sqrt 2).] )proof
assume A1:
y in [.1,(sqrt 2).]
;
ex x being object st
( x in dom (sec | [.0,(PI / 4).]) & y = (sec | [.0,(PI / 4).]) . x )
then reconsider y1 =
y as
Real ;
[.0,(PI / 4).] c= [.0,(PI / 2).[
by Lm5, XXREAL_2:def 12;
then A2:
sec | [.0,(PI / 4).] is
continuous
by Th37, FCONT_1:16;
y1 in [.(sec . 0),(sec . (PI / 4)).] \/ [.(sec . (PI / 4)),(sec . 0).]
by A1, Th31, XBOOLE_0:def 3;
then consider x being
Real such that A3:
(
x in [.0,(PI / 4).] &
y1 = sec . x )
by A2, Lm13, Th1, FCONT_2:15, XBOOLE_1:1;
take
x
;
( x in dom (sec | [.0,(PI / 4).]) & y = (sec | [.0,(PI / 4).]) . x )
thus
(
x in dom (sec | [.0,(PI / 4).]) &
y = (sec | [.0,(PI / 4).]) . x )
by A3, Lm29, FUNCT_1:49;
verum
end; thus
( ex
x being
object st
(
x in dom (sec | [.0,(PI / 4).]) &
y = (sec | [.0,(PI / 4).]) . x ) implies
y in [.1,(sqrt 2).] )
verum end;
hence
rng (sec | [.0,(PI / 4).]) = [.1,(sqrt 2).]
by FUNCT_1:def 3; verum