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

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

proof

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

end;

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

proof

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

end;

end;

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