set cos1 = cos | [.PI ,(2 * PI ).];

now

let y be set ; :: thesis: ( ( y in [.(- 1),1.] implies ex x being set st
( x in dom (cos | [.PI ,(2 * PI ).]) & y = (cos | [.PI ,(2 * PI ).]) . x ) ) & ( ex x being set 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 set st
( x in dom (cos | [.PI ,(2 * PI ).]) & y = (cos | [.PI ,(2 * PI ).]) . x ) ) :: thesis: ( ex x being set 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:72;
assume A2: y in [.(- 1),1.] ; :: thesis: ex x being set 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:90, SIN_COS:27
.= [.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:72;
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:81, 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:16;
take x ; :: thesis: ( 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:90, SIN_COS:27; :: thesis: verum

end;

thus ( ex x being set st
( x in dom (cos | [.PI ,(2 * PI ).]) & y = (cos | [.PI ,(2 * PI ).]) . x ) implies y in [.(- 1),1.] ) :: thesis: verum

proof

given x being set such that A6: x in dom (cos | [.PI ,(2 * PI ).]) and
A7: y = (cos | [.PI ,(2 * PI ).]) . x ; :: thesis: y in [.(- 1),1.]
dom (cos | [.PI ,(2 * PI ).]) c= dom cos by RELAT_1:89;
then reconsider x1 = x as Real by A6, SIN_COS:27;
y = cos . x1 by A6, A7, FUNCT_1:70;
hence y in [.(- 1),1.] by Th45; :: thesis: verum

end;

end;

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