set sin1 = sin | [.(PI / 2),((3 / 2) * PI ).];

now

let y be set ; :: thesis: ( ( y in [.(- 1),1.] implies ex x being set st
( x in dom (sin | [.(PI / 2),((3 / 2) * PI ).]) & y = (sin | [.(PI / 2),((3 / 2) * PI ).]) . x ) ) & ( ex x being set st
( x in dom (sin | [.(PI / 2),((3 / 2) * PI ).]) & y = (sin | [.(PI / 2),((3 / 2) * PI ).]) . x ) implies y in [.(- 1),1.] ) )
thus ( y in [.(- 1),1.] implies ex x being set st
( x in dom (sin | [.(PI / 2),((3 / 2) * PI ).]) & y = (sin | [.(PI / 2),((3 / 2) * PI ).]) . x ) ) :: thesis: ( ex x being set st
( x in dom (sin | [.(PI / 2),((3 / 2) * PI ).]) & y = (sin | [.(PI / 2),((3 / 2) * PI ).]) . x ) implies y in [.(- 1),1.] )

proof

assume A1: y in [.(- 1),1.] ; :: thesis: ex x being set st
( x in dom (sin | [.(PI / 2),((3 / 2) * PI ).]) & y = (sin | [.(PI / 2),((3 / 2) * PI ).]) . x )
then reconsider y1 = y as Real ;
A2: (sin | [.(PI / 2),((3 / 2) * PI ).]) | [.(PI / 2),((3 / 2) * PI ).] is continuous ;
X: dom (sin | [.(PI / 2),((3 / 2) * PI ).]) = [.(PI / 2),((3 / 2) * PI ).] /\ REAL by RELAT_1:90, SIN_COS:27
.= [.(PI / 2),((3 / 2) * PI ).] by XBOOLE_1:28 ;
( PI / 2 in [.(PI / 2),((3 / 2) * PI ).] & (3 / 2) * PI in [.(PI / 2),((3 / 2) * PI ).] ) by Lx4, XXREAL_1:1;
then ( (sin | [.(PI / 2),((3 / 2) * PI ).]) . (PI / 2) = sin . (PI / 2) & (sin | [.(PI / 2),((3 / 2) * PI ).]) . ((3 / 2) * PI ) = sin . ((3 / 2) * PI ) ) by FUNCT_1:72;
then y1 in [.((sin | [.(PI / 2),((3 / 2) * PI ).]) . (PI / 2)),((sin | [.(PI / 2),((3 / 2) * PI ).]) . ((3 / 2) * PI )).] \/ [.((sin | [.(PI / 2),((3 / 2) * PI ).]) . ((3 / 2) * PI )),((sin | [.(PI / 2),((3 / 2) * PI ).]) . (PI / 2)).] by A1, SIN_COS:81, XBOOLE_0:def 3;
then consider x being Real such that
A3: x in [.(PI / 2),((3 / 2) * PI ).] and
A4: y1 = (sin | [.(PI / 2),((3 / 2) * PI ).]) . x by A2, Lx4, X, FCONT_2:16;
take x ; :: thesis: ( x in dom (sin | [.(PI / 2),((3 / 2) * PI ).]) & y = (sin | [.(PI / 2),((3 / 2) * PI ).]) . x )
x in REAL /\ [.(PI / 2),((3 / 2) * PI ).] by A3, XBOOLE_0:def 4;
hence ( x in dom (sin | [.(PI / 2),((3 / 2) * PI ).]) & y = (sin | [.(PI / 2),((3 / 2) * PI ).]) . x ) by A4, RELAT_1:90, SIN_COS:27; :: thesis: verum

end;

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

proof

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

end;

end;

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