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