now

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

proof

assume A1: y in [.(- 1),1.] ; :: thesis: ex x being set st
( x in dom (cot | [.(PI / 4),((3 / 4) * PI ).]) & y = (cot | [.(PI / 4),((3 / 4) * PI ).]) . x )
then reconsider y1 = y as Real ;
A2: PI / 4 <= (3 / 4) * PI

proof

PI in ].0 ,4.[ by SIN_COS:def 32;
then PI > 0 by XXREAL_1:4;
then PI / 4 > 0 / 4 by XREAL_1:76;
then (PI / 4) * 3 > PI / 4 by XREAL_1:157;
hence PI / 4 <= (3 / 4) * PI ; :: thesis: verum

end;

A3: cot | ].0 ,PI .[ is continuous by Lm2, FDIFF_1:33;
F: [.(PI / 4),((3 / 4) * PI ).] c= ].0 ,PI .[ by Lm9, Lm10, XXREAL_2:def 12;
A5: cot | [.(PI / 4),((3 / 4) * PI ).] is continuous by A3, F, FCONT_1:17;
Y: [.(PI / 4),((3 / 4) * PI ).] c= dom cot by F, Th2, XBOOLE_1:1;
y1 in [.(cot . ((3 / 4) * PI )),(cot . (PI / 4)).] \/ [.(cot . (PI / 4)),(cot . ((3 / 4) * PI )).] by A1, Th16, XBOOLE_0:def 3;
then consider x being Real such that
A6: x in [.(PI / 4),((3 / 4) * PI ).] and
A7: y1 = cot . x by A2, A5, Y, FCONT_2:16;
take x ; :: thesis: ( x in dom (cot | [.(PI / 4),((3 / 4) * PI ).]) & y = (cot | [.(PI / 4),((3 / 4) * PI ).]) . x )
thus ( x in dom (cot | [.(PI / 4),((3 / 4) * PI ).]) & y = (cot | [.(PI / 4),((3 / 4) * PI ).]) . x ) by A6, A7, Lm12, FUNCT_1:72; :: thesis: verum

end;

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

proof

given x being set such that A8: x in dom (cot | [.(PI / 4),((3 / 4) * PI ).]) and
A9: y = (cot | [.(PI / 4),((3 / 4) * PI ).]) . x ; :: thesis: y in [.(- 1),1.]
reconsider x1 = x as Real by A8;
y = cot . x1 by A8, A9, Lm12, FUNCT_1:72;
hence y in [.(- 1),1.] by A8, Lm12, Th18; :: thesis: verum

end;

end;

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