now :: thesis: 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 ; :: thesis: ( ( 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 ) ) :: thesis: ( ex x being object st
( x in dom sin & y = sin . x ) implies y in [.(- 1),1.] )

proof

assume A1: y in [.(- 1),1.] ; :: thesis: 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 ; :: thesis: ( 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; :: thesis: 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; :: thesis: verum

end;

hence rng sin = [.(- 1),1.] by FUNCT_1:def 3; :: thesis: verum