now :: thesis: for y being object holds
( ( y in [.1,(sqrt 2).] implies ex x being object st
( x in dom (cosec | [.(PI / 4),(PI / 2).]) & y = (cosec | [.(PI / 4),(PI / 2).]) . x ) ) & ( ex x being object st
( x in dom (cosec | [.(PI / 4),(PI / 2).]) & y = (cosec | [.(PI / 4),(PI / 2).]) . 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 (cosec | [.(PI / 4),(PI / 2).]) & y = (cosec | [.(PI / 4),(PI / 2).]) . x ) ) & ( ex x being object st
( x in dom (cosec | [.(PI / 4),(PI / 2).]) & y = (cosec | [.(PI / 4),(PI / 2).]) . x ) implies y in [.1,(sqrt 2).] ) )
thus ( y in [.1,(sqrt 2).] implies ex x being object st
( x in dom (cosec | [.(PI / 4),(PI / 2).]) & y = (cosec | [.(PI / 4),(PI / 2).]) . x ) ) :: thesis: ( ex x being object st
( x in dom (cosec | [.(PI / 4),(PI / 2).]) & y = (cosec | [.(PI / 4),(PI / 2).]) . x ) implies y in [.1,(sqrt 2).] )

proof

[.(PI / 4),(PI / 2).] c= ].0,(PI / 2).] by Lm8, XXREAL_2:def 12;
then A1: cosec | [.(PI / 4),(PI / 2).] is continuous by Th40, FCONT_1:16;
assume A2: y in [.1,(sqrt 2).] ; :: thesis: ex x being object st
( x in dom (cosec | [.(PI / 4),(PI / 2).]) & y = (cosec | [.(PI / 4),(PI / 2).]) . x )
then reconsider y1 = y as Real ;
A3: PI / 4 <= PI / 2 by Lm8, XXREAL_1:2;
y1 in [.(cosec . (PI / 2)),(cosec . (PI / 4)).] \/ [.(cosec . (PI / 4)),(cosec . (PI / 2)).] by A2, Th32, XBOOLE_0:def 3;
then consider x being Real such that
A4: ( x in [.(PI / 4),(PI / 2).] & y1 = cosec . x ) by A3, A1, Lm20, Th4, FCONT_2:15, XBOOLE_1:1;
take x ; :: thesis: ( x in dom (cosec | [.(PI / 4),(PI / 2).]) & y = (cosec | [.(PI / 4),(PI / 2).]) . x )
thus ( x in dom (cosec | [.(PI / 4),(PI / 2).]) & y = (cosec | [.(PI / 4),(PI / 2).]) . x ) by A4, Lm32, FUNCT_1:49; :: thesis: verum

end;

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

proof

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

end;

end;

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