now :: thesis: 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 ; :: thesis: ( ( 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 ) ) :: thesis: ( 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).] ; :: thesis: 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 ; :: 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 A3, Lm29, FUNCT_1:49; :: thesis: 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).] ) :: thesis: verum

proof

given x being object such that A4: x in dom (sec | [.0,(PI / 4).]) and
A5: y = (sec | [.0,(PI / 4).]) . x ; :: thesis: y in [.1,(sqrt 2).]
reconsider x1 = x as Real by A4;
y = sec . x1 by A4, A5, Lm29, FUNCT_1:49;
hence y in [.1,(sqrt 2).] by A4, Lm29, Th33; :: thesis: verum

end;

end;

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