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