now

let y be set ; :: thesis: ( ( y in [.1,(sqrt 2).] implies ex x being set st
( x in dom (sec | [.0 ,(PI / 4).]) & y = (sec | [.0 ,(PI / 4).]) . x ) ) & ( ex x being set 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 set st
( x in dom (sec | [.0 ,(PI / 4).]) & y = (sec | [.0 ,(PI / 4).]) . x ) ) :: thesis: ( ex x being set 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).] ; :: thesis: ex x being set 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 Lm9, XXREAL_2:def 12;
then A4: sec | [.0 ,(PI / 4).] is continuous by Th37, FCONT_1:17;
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
A5: x in [.0 ,(PI / 4).] and
A6: y1 = sec . x by A4, X5, FCONT_2:16;
take x ; :: thesis: ( 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 A5, A6, Lm13, FUNCT_1:72; :: thesis: verum

end;

thus ( ex x being set st
( x in dom (sec | [.0 ,(PI / 4).]) & y = (sec | [.0 ,(PI / 4).]) . x ) implies y in [.1,(sqrt 2).] ) :: thesis: verum

proof

given x being set such that A7: x in dom (sec | [.0 ,(PI / 4).]) and
A8: y = (sec | [.0 ,(PI / 4).]) . x ; :: thesis: y in [.1,(sqrt 2).]
reconsider x1 = x as Real by A7;
y = sec . x1 by A7, A8, Lm13, FUNCT_1:72;
hence y in [.1,(sqrt 2).] by A7, Lm13, Th33; :: thesis: verum

end;

end;

hence rng (sec | [.0 ,(PI / 4).]) = [.1,(sqrt 2).] by FUNCT_1:def 5; :: thesis: verum