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

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

proof

assume A1: y in [.(- 1),1.] ; :: thesis: ex x being object st
( x in dom (tan | [.(- (PI / 4)),(PI / 4).]) & y = (tan | [.(- (PI / 4)),(PI / 4).]) . x )
then reconsider y1 = y as Real ;
y1 in [.(tan . (- (PI / 4))),(tan . (PI / 4)).] by A1, Th17, SIN_COS:def 28;
then A2: y1 in [.(tan . (- (PI / 4))),(tan . (PI / 4)).] \/ [.(tan . (PI / 4)),(tan . (- (PI / 4))).] by XBOOLE_0:def 3;
A3: [.(- (PI / 4)),(PI / 4).] c= ].(- (PI / 2)),(PI / 2).[ by Lm7, Lm8, XXREAL_2:def 12;
tan | ].(- (PI / 2)),(PI / 2).[ is continuous by Lm1, FDIFF_1:25;
then tan | [.(- (PI / 4)),(PI / 4).] is continuous by A3, FCONT_1:16;
then consider x being Real such that
A4: x in [.(- (PI / 4)),(PI / 4).] and
A5: y1 = tan . x by A3, A2, Th1, FCONT_2:15, XBOOLE_1:1;
take x ; :: thesis: ( x in dom (tan | [.(- (PI / 4)),(PI / 4).]) & y = (tan | [.(- (PI / 4)),(PI / 4).]) . x )
thus ( x in dom (tan | [.(- (PI / 4)),(PI / 4).]) & y = (tan | [.(- (PI / 4)),(PI / 4).]) . x ) by A4, A5, Lm11, FUNCT_1:49; :: thesis: verum

end;

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

proof

given x being object such that A6: x in dom (tan | [.(- (PI / 4)),(PI / 4).]) and
A7: y = (tan | [.(- (PI / 4)),(PI / 4).]) . x ; :: thesis: y in [.(- 1),1.]
reconsider x1 = x as Real by A6;
y = tan . x1 by A6, A7, Lm11, FUNCT_1:49;
hence y in [.(- 1),1.] by A6, Lm11, Th19; :: thesis: verum

end;

end;

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