now 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 ;
( ( 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 ) )
( 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.]
;
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
;
( 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;
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.] )
verum end;
hence
rng (tan | [.(- (PI / 4)),(PI / 4).]) = [.(- 1),1.]
by FUNCT_1:def 3; verum