now

let y be set ; :: thesis: ( ( y in [.(PI / 4),((3 / 4) * PI ).] implies ex x being set st
( x in dom (arccot | [.(- 1),1.]) & y = (arccot | [.(- 1),1.]) . x ) ) & ( ex x being set 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 set st
( x in dom (arccot | [.(- 1),1.]) & y = (arccot | [.(- 1),1.]) . x ) ) :: thesis: ( ex x being set 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 set 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:16;
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:72, RELAT_1:91; :: thesis: verum

end;

thus ( ex x being set 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 set such that A4: x in dom (arccot | [.(- 1),1.]) and
A5: y = (arccot | [.(- 1),1.]) . x ; :: thesis: y in [.(PI / 4),((3 / 4) * PI ).]
reconsider x1 = x as Real by A4;
A6: dom (arccot | [.(- 1),1.]) = [.(- 1),1.] by Th24, RELAT_1:91;
then y = arccot . x by A4, A5, FUNCT_1:72;
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 5; :: thesis: verum