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

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 A1: (PI / 4) * 3 > PI / 4 by XREAL_1:157;
assume A2: 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 ;
A3: y1 in [.(cot . ((3 / 4) * PI )),(cot . (PI / 4)).] \/ [.(cot . (PI / 4)),(cot . ((3 / 4) * PI )).] by A2, Th18, XBOOLE_0:def 3;
A4: [.(PI / 4),((3 / 4) * PI ).] c= ].0 ,PI .[ by Lm9, Lm10, XXREAL_2:def 12;
cot | ].0 ,PI .[ is continuous by Lm2, FDIFF_1:33;
then cot | [.(PI / 4),((3 / 4) * PI ).] is continuous by A4, FCONT_1:17;
then consider x being Real such that
A5: x in [.(PI / 4),((3 / 4) * PI ).] and
A6: y1 = cot . x by A1, A4, A3, Th2, FCONT_2:16, XBOOLE_1:1;
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 A5, A6, 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 A7: x in dom (cot | [.(PI / 4),((3 / 4) * PI ).]) and
A8: y = (cot | [.(PI / 4),((3 / 4) * PI ).]) . x ; :: thesis: y in [.(- 1),1.]
reconsider x1 = x as Real by A7;
y = cot . x1 by A7, A8, Lm12, FUNCT_1:72;
hence y in [.(- 1),1.] by A7, Lm12, Th20; :: thesis: verum

end;

end;

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