now

let y be set ; :: thesis: ( ( y in [.(- (sqrt 2)),(- 1).] implies ex x being set st
( x in dom (sec | [.((3 / 4) * PI ),PI .]) & y = (sec | [.((3 / 4) * PI ),PI .]) . x ) ) & ( ex x being set st
( x in dom (sec | [.((3 / 4) * PI ),PI .]) & y = (sec | [.((3 / 4) * PI ),PI .]) . x ) implies y in [.(- (sqrt 2)),(- 1).] ) )
thus ( y in [.(- (sqrt 2)),(- 1).] implies ex x being set st
( x in dom (sec | [.((3 / 4) * PI ),PI .]) & y = (sec | [.((3 / 4) * PI ),PI .]) . x ) ) :: thesis: ( ex x being set st
( x in dom (sec | [.((3 / 4) * PI ),PI .]) & y = (sec | [.((3 / 4) * PI ),PI .]) . x ) implies y in [.(- (sqrt 2)),(- 1).] )

proof

assume A1: y in [.(- (sqrt 2)),(- 1).] ; :: thesis: ex x being set st
( x in dom (sec | [.((3 / 4) * PI ),PI .]) & y = (sec | [.((3 / 4) * PI ),PI .]) . x )
then reconsider y1 = y as Real ;
A2: (3 / 4) * PI <= PI by Lm10, XXREAL_1:2;
[.((3 / 4) * PI ),PI .] c= ].(PI / 2),PI .] by Lm10, XXREAL_2:def 12;
then A4: sec | [.((3 / 4) * PI ),PI .] is continuous by Th38, FCONT_1:17;
y1 in [.(sec . ((3 / 4) * PI )),(sec . PI ).] \/ [.(sec . PI ),(sec . ((3 / 4) * PI )).] by A1, Th31, XBOOLE_0:def 3;
then consider x being Real such that
A5: x in [.((3 / 4) * PI ),PI .] and
A6: y1 = sec . x by A2, A4, X6, FCONT_2:16;
take x ; :: thesis: ( x in dom (sec | [.((3 / 4) * PI ),PI .]) & y = (sec | [.((3 / 4) * PI ),PI .]) . x )
thus ( x in dom (sec | [.((3 / 4) * PI ),PI .]) & y = (sec | [.((3 / 4) * PI ),PI .]) . x ) by A5, A6, Lm14, FUNCT_1:72; :: thesis: verum

end;

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

proof

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

end;

end;

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