sin | ].(- (PI / 2)),(PI / 2).[ c= sin | [.(- (PI / 2)),(PI / 2).] by Lm16, RELAT_1:104;
then A1: rng (sin | ].(- (PI / 2)),(PI / 2).[) c= rng (sin | [.(- (PI / 2)),(PI / 2).]) by RELAT_1:25;
A2: rng (sin | ].(- (PI / 2)),(PI / 2).[) = sin .: ].(- (PI / 2)),(PI / 2).[ by RELAT_1:148;
thus sin .: ].(- (PI / 2)),(PI / 2).[ c= ].(- 1),1.[ :: according to XBOOLE_0:def 10 :: thesis: ].(- 1),1.[ c= sin .: ].(- (PI / 2)),(PI / 2).[

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in sin .: ].(- (PI / 2)),(PI / 2).[ or x in ].(- 1),1.[ )
assume A3: x in sin .: ].(- (PI / 2)),(PI / 2).[ ; :: thesis: x in ].(- 1),1.[
then consider a being set such that
A4: a in dom sin and
A5: a in ].(- (PI / 2)),(PI / 2).[ and
A6: sin . a = x by FUNCT_1:def 12;
reconsider a = a, x = x as Real by A4, A6;
A7: sin . a = sin a by SIN_COS:def 21;
A8: ( - 1 <= x & x <= 1 ) by A1, A2, A3, COMPTRIG:48, XXREAL_1:1;
set i = [\(a / (2 * PI ))/];
A9: H₁([\(a / (2 * PI ))/]) / ((2 * PI ) * 1) = [\(a / (2 * PI ))/] / 1 by XCMPLX_1:92;

A10: now

assume x = - 1 ; :: thesis: contradiction
then a = ((3 / 2) * PI ) + H₁([\(a / (2 * PI ))/]) by A6, A7, Th23;
then ( - (PI / 2) < ((3 / 2) * PI ) + H₁([\(a / (2 * PI ))/]) & ((3 / 2) * PI ) + H₁([\(a / (2 * PI ))/]) < PI / 2 ) by A5, XXREAL_1:4;
then ( (- (PI / 2)) - ((3 / 2) * PI ) < (((3 / 2) * PI ) + H₁([\(a / (2 * PI ))/])) - ((3 / 2) * PI ) & (((3 / 2) * PI ) + H₁([\(a / (2 * PI ))/])) - ((3 / 2) * PI ) < (PI / 2) - ((3 / 2) * PI ) ) by XREAL_1:11;
then ( (- (2 * PI )) / (2 * PI ) < [\(a / (2 * PI ))/] & [\(a / (2 * PI ))/] < (- PI ) / (2 * PI ) ) by A9, XREAL_1:76;
then ( - ((2 * PI ) / (2 * PI )) < [\(a / (2 * PI ))/] & [\(a / (2 * PI ))/] < - (PI / (2 * PI )) ) by XCMPLX_1:188;
then ( - 1 < [\(a / (2 * PI ))/] & [\(a / (2 * PI ))/] < - ((1 * PI ) / (2 * PI )) ) by XCMPLX_1:60;
then ( (- 1) + 1 <= [\(a / (2 * PI ))/] & [\(a / (2 * PI ))/] < - (1 / 2) ) by INT_1:20, XCMPLX_1:92;
hence contradiction by XXREAL_0:2; :: thesis: verum

end;

now

assume x = 1 ; :: thesis: contradiction
then a = (PI / 2) + H₁([\(a / (2 * PI ))/]) by A6, A7, Th24;
then ( - (PI / 2) < (PI / 2) + H₁([\(a / (2 * PI ))/]) & (PI / 2) + H₁([\(a / (2 * PI ))/]) < PI / 2 ) by A5, XXREAL_1:4;
then ( (- (PI / 2)) - (PI / 2) < ((PI / 2) + H₁([\(a / (2 * PI ))/])) - (PI / 2) & ((PI / 2) + H₁([\(a / (2 * PI ))/])) - (PI / 2) < (PI / 2) - (PI / 2) ) by XREAL_1:11;
then ( (- PI ) / (2 * PI ) < H₁([\(a / (2 * PI ))/]) / (2 * PI ) & H₁([\(a / (2 * PI ))/]) / (2 * PI ) < 0 / (2 * PI ) ) by XREAL_1:76;
then ( ((- 1) * PI ) / (2 * PI ) < [\(a / (2 * PI ))/] & [\(a / (2 * PI ))/] < 0 ) by A9;
then ( (- 1) / 2 < [\(a / (2 * PI ))/] & [\(a / (2 * PI ))/] < 0 ) by XCMPLX_1:92;
then ( - (1 / 2) < [\(a / (2 * PI ))/] & [\(a / (2 * PI ))/] <= - 1 ) by INT_1:21;
hence contradiction by XXREAL_0:2; :: thesis: verum

end;

then ( - 1 < x & x < 1 ) by A8, A10, XXREAL_0:1;
hence x in ].(- 1),1.[ by XXREAL_1:4; :: thesis: verum

end;

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in ].(- 1),1.[ or a in sin .: ].(- (PI / 2)),(PI / 2).[ )
assume A11: a in ].(- 1),1.[ ; :: thesis: a in sin .: ].(- (PI / 2)),(PI / 2).[
then reconsider a = a as Real ;
( - 1 < a & a < 1 ) by A11, XXREAL_1:4;
then a in rng (sin | [.(- (PI / 2)),(PI / 2).]) by COMPTRIG:48, XXREAL_1:1;
then consider x being set such that
A12: x in dom (sin | [.(- (PI / 2)),(PI / 2).]) and
A13: (sin | [.(- (PI / 2)),(PI / 2).]) . x = a by FUNCT_1:def 5;
A14: dom (sin | [.(- (PI / 2)),(PI / 2).]) = [.(- (PI / 2)),(PI / 2).] by Lm1, RELAT_1:91;
reconsider x = x as Real by A12;
A15: sin . x = a by A12, A13, FUNCT_1:70;
( - (PI / 2) <= x & x <= PI / 2 ) by A12, A14, XXREAL_1:1;
then ( ( - (PI / 2) < x & x < PI / 2 ) or - (PI / 2) = x or PI / 2 = x ) by XXREAL_0:1;
then x in ].(- (PI / 2)),(PI / 2).[ by A11, A15, Th7, SIN_COS:81, XXREAL_1:4;
hence a in sin .: ].(- (PI / 2)),(PI / 2).[ by A15, Lm1, FUNCT_1:def 12; :: thesis: verum