now :: thesis: for y being object holds
( ( y in [.(- 1),1.] implies ex x being object st
( x in dom (cot | [.(PI / 4),((3 / 4) * PI).]) & y = (cot | [.(PI / 4),((3 / 4) * PI).]) . x ) ) & ( ex x being object st
( x in dom (cot | [.(PI / 4),((3 / 4) * PI).]) & y = (cot | [.(PI / 4),((3 / 4) * PI).]) . x ) implies y in [.(- 1),1.] ) )

let y be object ; :: thesis: ( ( y in [.(- 1),1.] implies ex x being object st
( x in dom (cot | [.(PI / 4),((3 / 4) * PI).]) & y = (cot | [.(PI / 4),((3 / 4) * PI).]) . x ) ) & ( ex x being object 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 object st
( x in dom (cot | [.(PI / 4),((3 / 4) * PI).]) & y = (cot | [.(PI / 4),((3 / 4) * PI).]) . x ) ) :: thesis: ( ex x being object st
( x in dom (cot | [.(PI / 4),((3 / 4) * PI).]) & y = (cot | [.(PI / 4),((3 / 4) * PI).]) . x ) implies y in [.(- 1),1.] )

proof

A1: (PI / 4) * 3 > PI / 4 by XREAL_1:155;
assume A2: y in [.(- 1),1.] ; :: thesis: ex x being object 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:25;
then cot | [.(PI / 4),((3 / 4) * PI).] is continuous by A4, FCONT_1:16;
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:15, 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:49; :: thesis: verum

end;

thus ( ex x being object 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 object 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:49;
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 3; :: thesis: verum