now

let y be set ; :: thesis: ( ( y in [.(- 1),1.] implies ex x being set st
( x in dom cos & y = cos . x ) ) & ( ex x being set st
( x in dom cos & y = cos . x ) implies y in [.(- 1),1.] ) )
thus ( y in [.(- 1),1.] implies ex x being set st
( x in dom cos & y = cos . x ) ) :: thesis: ( ex x being set st
( x in dom cos & y = cos . x ) implies y in [.(- 1),1.] )

proof

assume A1: y in [.(- 1),1.] ; :: thesis: ex x being set st
( x in dom cos & y = cos . x )
then reconsider y1 = y as Real ;
( cos | [.0 ,PI .] is continuous & y1 in [.(cos . 0 ),(cos . PI ).] \/ [.(cos . PI ),(cos . 0 ).] ) by A1, SIN_COS:33, SIN_COS:81, XBOOLE_0:def 3;
then consider x being Real such that
x in [.0 ,PI .] and
A2: y1 = cos . x by FCONT_2:16, SIN_COS:27;
take x ; :: thesis: ( x in dom cos & y = cos . x )
thus ( x in dom cos & y = cos . x ) by A2, SIN_COS:27; :: thesis: verum

end;

thus ( ex x being set st
( x in dom cos & y = cos . x ) implies y in [.(- 1),1.] ) by Th45, SIN_COS:27; :: thesis: verum

end;

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