set cos1 = cos | [.PI,(2 * PI).];
now for y being object holds
( ( y in [.(- 1),1.] implies ex x being object st
( x in dom (cos | [.PI,(2 * PI).]) & y = (cos | [.PI,(2 * PI).]) . x ) ) & ( ex x being object st
( x in dom (cos | [.PI,(2 * PI).]) & y = (cos | [.PI,(2 * PI).]) . x ) implies y in [.(- 1),1.] ) )let y be
object ;
( ( y in [.(- 1),1.] implies ex x being object st
( x in dom (cos | [.PI,(2 * PI).]) & y = (cos | [.PI,(2 * PI).]) . x ) ) & ( ex x being object st
( x in dom (cos | [.PI,(2 * PI).]) & y = (cos | [.PI,(2 * PI).]) . x ) implies y in [.(- 1),1.] ) )thus
(
y in [.(- 1),1.] implies ex
x being
object st
(
x in dom (cos | [.PI,(2 * PI).]) &
y = (cos | [.PI,(2 * PI).]) . x ) )
( ex x being object st
( x in dom (cos | [.PI,(2 * PI).]) & y = (cos | [.PI,(2 * PI).]) . x ) implies y in [.(- 1),1.] )proof
2
* PI in [.PI,(2 * PI).]
by Lm3, XXREAL_1:1;
then A1:
(cos | [.PI,(2 * PI).]) . (2 * PI) = cos . (2 * PI)
by FUNCT_1:49;
assume A2:
y in [.(- 1),1.]
;
ex x being object st
( x in dom (cos | [.PI,(2 * PI).]) & y = (cos | [.PI,(2 * PI).]) . x )
then reconsider y1 =
y as
Real ;
A3:
dom (cos | [.PI,(2 * PI).]) =
[.PI,(2 * PI).] /\ REAL
by RELAT_1:61, SIN_COS:24
.=
[.PI,(2 * PI).]
by XBOOLE_1:28
;
PI in [.PI,(2 * PI).]
by Lm3, XXREAL_1:1;
then
(cos | [.PI,(2 * PI).]) . PI = cos . PI
by FUNCT_1:49;
then
(
(cos | [.PI,(2 * PI).]) | [.PI,(2 * PI).] is
continuous &
y1 in [.((cos | [.PI,(2 * PI).]) . PI),((cos | [.PI,(2 * PI).]) . (2 * PI)).] \/ [.((cos | [.PI,(2 * PI).]) . (2 * PI)),((cos | [.PI,(2 * PI).]) . PI).] )
by A2, A1, SIN_COS:76, XBOOLE_0:def 3;
then consider x being
Real such that A4:
x in [.PI,(2 * PI).]
and A5:
y1 = (cos | [.PI,(2 * PI).]) . x
by A3, Lm3, FCONT_2:15;
take
x
;
( x in dom (cos | [.PI,(2 * PI).]) & y = (cos | [.PI,(2 * PI).]) . x )
x in REAL /\ [.PI,(2 * PI).]
by A4, XBOOLE_0:def 4;
hence
(
x in dom (cos | [.PI,(2 * PI).]) &
y = (cos | [.PI,(2 * PI).]) . x )
by A5, RELAT_1:61, SIN_COS:24;
verum
end; thus
( ex
x being
object st
(
x in dom (cos | [.PI,(2 * PI).]) &
y = (cos | [.PI,(2 * PI).]) . x ) implies
y in [.(- 1),1.] )
verum end;
hence
rng (cos | [.PI,(2 * PI).]) = [.(- 1),1.]
by FUNCT_1:def 3; verum