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

now :: thesis: for y being object holds
( ( y in [.(- 1),1.] implies ex x being object st
( x in dom (sin | [.(PI / 2),((3 / 2) * PI).]) & y = (sin | [.(PI / 2),((3 / 2) * PI).]) . x ) ) & ( ex x being object st
( x in dom (sin | [.(PI / 2),((3 / 2) * PI).]) & y = (sin | [.(PI / 2),((3 / 2) * PI).]) . 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 | [.(PI / 2),((3 / 2) * PI).]) & y = (sin | [.(PI / 2),((3 / 2) * PI).]) . x ) ) & ( ex x being object 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 object st
( x in dom (sin | [.(PI / 2),((3 / 2) * PI).]) & y = (sin | [.(PI / 2),((3 / 2) * PI).]) . x ) ) :: thesis: ( ex x being object st
( x in dom (sin | [.(PI / 2),((3 / 2) * PI).]) & y = (sin | [.(PI / 2),((3 / 2) * PI).]) . x ) implies y in [.(- 1),1.] )

proof

(3 / 2) * PI in [.(PI / 2),((3 / 2) * PI).] by Lm4, XXREAL_1:1;
then A1: (sin | [.(PI / 2),((3 / 2) * PI).]) . ((3 / 2) * PI) = sin . ((3 / 2) * PI) by FUNCT_1:49;
assume A2: y in [.(- 1),1.] ; :: thesis: ex x being object st
( x in dom (sin | [.(PI / 2),((3 / 2) * PI).]) & y = (sin | [.(PI / 2),((3 / 2) * PI).]) . x )
then reconsider y1 = y as Real ;
A3: dom (sin | [.(PI / 2),((3 / 2) * PI).]) = [.(PI / 2),((3 / 2) * PI).] /\ REAL by RELAT_1:61, SIN_COS:24
.= [.(PI / 2),((3 / 2) * PI).] by XBOOLE_1:28 ;
PI / 2 in [.(PI / 2),((3 / 2) * PI).] by Lm4, XXREAL_1:1;
then (sin | [.(PI / 2),((3 / 2) * PI).]) . (PI / 2) = sin . (PI / 2) by FUNCT_1:49;
then ( (sin | [.(PI / 2),((3 / 2) * PI).]) | [.(PI / 2),((3 / 2) * PI).] is continuous & 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 A2, A1, SIN_COS:76, XBOOLE_0:def 3;
then consider x being Real such that
A4: x in [.(PI / 2),((3 / 2) * PI).] and
A5: y1 = (sin | [.(PI / 2),((3 / 2) * PI).]) . x by A3, Lm4, FCONT_2:15;
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 A4, XBOOLE_0:def 4;
hence ( x in dom (sin | [.(PI / 2),((3 / 2) * PI).]) & y = (sin | [.(PI / 2),((3 / 2) * PI).]) . x ) by A5, RELAT_1:61, SIN_COS:24; :: thesis: verum

end;

thus ( ex x being object 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 object such that A6: x in dom (sin | [.(PI / 2),((3 / 2) * PI).]) and
A7: 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:60;
then reconsider x1 = x as Real by A6, SIN_COS:24;
y = sin . x1 by A6, A7, FUNCT_1:47;
hence y in [.(- 1),1.] by Th27; :: thesis: verum

end;

end;

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