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

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

proof

assume A1: y in [.(PI / 4),((3 / 4) * PI).] ; :: thesis: ex x being object st
( x in dom (arccot | [.(- 1),1.]) & y = (arccot | [.(- 1),1.]) . x )
then reconsider y1 = y as Real ;
y1 in [.(arccot . 1),(arccot . (- 1)).] \/ [.(arccot . (- 1)),(arccot . 1).] by A1, Th38, Th40, XBOOLE_0:def 3;
then consider x being Real such that
A2: x in [.(- 1),1.] and
A3: y1 = arccot . x by Th24, Th54, FCONT_2:15;
take x ; :: thesis: ( x in dom (arccot | [.(- 1),1.]) & y = (arccot | [.(- 1),1.]) . x )
thus ( x in dom (arccot | [.(- 1),1.]) & y = (arccot | [.(- 1),1.]) . x ) by A2, A3, Th24, FUNCT_1:49, RELAT_1:62; :: thesis: verum

end;

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

proof

given x being object such that A4: x in dom (arccot | [.(- 1),1.]) and
A5: y = (arccot | [.(- 1),1.]) . x ; :: thesis: y in [.(PI / 4),((3 / 4) * PI).]
A6: dom (arccot | [.(- 1),1.]) = [.(- 1),1.] by Th24, RELAT_1:62;
then y = arccot . x by A4, A5, FUNCT_1:49;
hence y in [.(PI / 4),((3 / 4) * PI).] by A4, A6, Th50; :: thesis: verum

end;

end;

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