now

let y be set ; :: thesis: ( ( y in [.(- 1),1.] implies ex x being set st
( x in dom (tan | [.(- (PI / 4)),(PI / 4).]) & y = (tan | [.(- (PI / 4)),(PI / 4).]) . x ) ) & ( ex x being set 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 set st
( x in dom (tan | [.(- (PI / 4)),(PI / 4).]) & y = (tan | [.(- (PI / 4)),(PI / 4).]) . x ) ) :: thesis: ( ex x being set 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 set st
( x in dom (tan | [.(- (PI / 4)),(PI / 4).]) & y = (tan | [.(- (PI / 4)),(PI / 4).]) . x )
then reconsider y1 = y as Real ;
A2: tan | ].(- (PI / 2)),(PI / 2).[ is continuous by Lm1, FDIFF_1:33;
F: [.(- (PI / 4)),(PI / 4).] c= ].(- (PI / 2)),(PI / 2).[ by Lm7, Lm8, XXREAL_2:def 12;
Y: [.(- (PI / 4)),(PI / 4).] c= dom tan by Th1, F, XBOOLE_1:1;
A4: tan | [.(- (PI / 4)),(PI / 4).] is continuous by A2, F, FCONT_1:17;
y1 in [.(tan . (- (PI / 4))),(tan . (PI / 4)).] by A1, Th15, SIN_COS:def 32;
then y1 in [.(tan . (- (PI / 4))),(tan . (PI / 4)).] \/ [.(tan . (PI / 4)),(tan . (- (PI / 4))).] by XBOOLE_0:def 3;
then consider x being Real such that
A5: x in [.(- (PI / 4)),(PI / 4).] and
A6: y1 = tan . x by A4, Y, FCONT_2:16;
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 A5, A6, Lm11, FUNCT_1:72; :: thesis: verum

end;

thus ( ex x being set 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 set such that A7: x in dom (tan | [.(- (PI / 4)),(PI / 4).]) and
A8: y = (tan | [.(- (PI / 4)),(PI / 4).]) . x ; :: thesis: y in [.(- 1),1.]
reconsider x1 = x as Real by A7;
y = tan . x1 by A7, A8, Lm11, FUNCT_1:72;
hence y in [.(- 1),1.] by A7, Lm11, Th17; :: thesis: verum

end;

end;

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