A1: sin | [.(PI / 2),((3 / 2) * PI ).] is one-to-one ;
let x1, y1 be set ; :: according to FUNCT_1:def 8 :: thesis: ( not x1 in K1((CircleMap | [.0 ,1.[)) or not y1 in K1((CircleMap | [.0 ,1.[)) or not (CircleMap | [.0 ,1.[) . x1 = (CircleMap | [.0 ,1.[) . y1 or x1 = y1 )
set f = CircleMap | [.0 ,1.[;
A2: [.0 ,(PI / 2).] c= [.(- (PI / 2)),(PI / 2).] by XXREAL_1:34;
A3: dom (CircleMap | [.0 ,1.[) = [.0 ,1.[ by Lm18, RELAT_1:91;
assume A4: x1 in dom (CircleMap | [.0 ,1.[) ; :: thesis: ( not y1 in K1((CircleMap | [.0 ,1.[)) or not (CircleMap | [.0 ,1.[) . x1 = (CircleMap | [.0 ,1.[) . y1 or x1 = y1 )
then reconsider x = x1 as Real by A3;
A5: (CircleMap | [.0 ,1.[) . x = CircleMap . x by A3, A4, FUNCT_1:72
.= |[(cos ((2 * PI ) * x)),(sin ((2 * PI ) * x))]| by Def11 ;
assume A6: y1 in dom (CircleMap | [.0 ,1.[) ; :: thesis: ( not (CircleMap | [.0 ,1.[) . x1 = (CircleMap | [.0 ,1.[) . y1 or x1 = y1 )
then reconsider y = y1 as Real by A3;
assume A7: (CircleMap | [.0 ,1.[) . x1 = (CircleMap | [.0 ,1.[) . y1 ; :: thesis: x1 = y1
A8: (CircleMap | [.0 ,1.[) . y = CircleMap . y by A3, A6, FUNCT_1:72
.= |[(cos ((2 * PI ) * y)),(sin ((2 * PI ) * y))]| by Def11 ;
then A9: cos ((2 * PI ) * x) = cos ((2 * PI ) * y) by A7, A5, SPPOL_2:1;
A10: cos ((2 * PI ) * y) = cos . ((2 * PI ) * y) by SIN_COS:def 23;
A11: cos ((2 * PI ) * x) = cos . ((2 * PI ) * x) by SIN_COS:def 23;
A12: sin ((2 * PI ) * x) = sin ((2 * PI ) * y) by A7, A5, A8, SPPOL_2:1;
A13: sin ((2 * PI ) * y) = sin . ((2 * PI ) * y) by SIN_COS:def 21;
A14: sin ((2 * PI ) * x) = sin . ((2 * PI ) * x) by SIN_COS:def 21;

per cases ( ( 0 <= x & x <= 1 / 4 ) or ( 1 / 4 < x & x <= 1 / 2 ) or ( 1 / 2 < x & x <= 3 / 4 ) or ( 3 / 4 < x & x < 1 ) ) by A3, A4, XXREAL_1:3;

suppose A15: ( 0 <= x & x <= 1 / 4 ) ; :: thesis: x1 = y1

A16: [.0 ,(PI / 2).] c= [.0 ,PI .] by Lm5, XXREAL_1:34;
(2 * PI ) * x <= (2 * PI ) * (1 / 4) by A15, XREAL_1:66;
then A17: (2 * PI ) * x in [.0 ,(((2 * PI ) * 1) / 4).] by A15, XXREAL_1:1;

per cases ( ( 0 <= y & y <= 1 / 4 ) or ( 1 / 4 < y & y < 3 / 4 ) or ( 3 / 4 <= y & y < 1 ) ) by A3, A6, XXREAL_1:3;

suppose A18: ( 0 <= y & y <= 1 / 4 ) ; :: thesis: x1 = y1

then (2 * PI ) * y <= (2 * PI ) * (1 / 4) by XREAL_1:66;
then A19: (2 * PI ) * y in [.0 ,(((2 * PI ) * 1) / 4).] by A18, XXREAL_1:1;
set g = sin | [.0 ,(PI / 2).];
A20: dom (sin | [.0 ,(PI / 2).]) = [.0 ,(PI / 2).] by RELAT_1:91, SIN_COS:27;
(sin | [.0 ,(PI / 2).]) . ((2 * PI ) * x) = sin . ((2 * PI ) * x) by A17, FUNCT_1:72
.= sin . ((2 * PI ) * y) by A12, A14, SIN_COS:def 21
.= (sin | [.0 ,(PI / 2).]) . ((2 * PI ) * y) by A19, FUNCT_1:72 ;
then (2 * PI ) * x = (2 * PI ) * y by A17, A19, A20, FUNCT_1:def 8;
then x = ((2 * PI ) * y) / (2 * PI ) by XCMPLX_1:90;
hence x1 = y1 by XCMPLX_1:90; :: thesis: verum

end;

suppose A21: ( 1 / 4 < y & y < 3 / 4 ) ; :: thesis: x1 = y1

then A22: (2 * PI ) * y < (2 * PI ) * (3 / 4) by XREAL_1:70;
(2 * PI ) * (1 / 4) < (2 * PI ) * y by A21, XREAL_1:70;
then (2 * PI ) * y in ].(PI / 2),((3 / 2) * PI ).[ by A22, XXREAL_1:4;
hence x1 = y1 by A9, A11, A10, A2, A17, COMPTRIG:28, COMPTRIG:29; :: thesis: verum

end;

suppose A23: ( 3 / 4 <= y & y < 1 ) ; :: thesis: x1 = y1

then A24: (2 * PI ) * y < (2 * PI ) * 1 by XREAL_1:70;
A25: [.((3 / 2) * PI ),(2 * PI ).[ c= ].PI ,(2 * PI ).[ by Lm6, XXREAL_1:48;
(2 * PI ) * (3 / 4) <= (2 * PI ) * y by A23, XREAL_1:66;
then (2 * PI ) * y in [.((3 / 2) * PI ),(2 * PI ).[ by A24, XXREAL_1:3;
hence x1 = y1 by A12, A14, A13, A17, A16, A25, COMPTRIG:24, COMPTRIG:25; :: thesis: verum

end;

end;

end;

suppose A26: ( 1 / 4 < x & x <= 1 / 2 ) ; :: thesis: x1 = y1

then A27: (2 * PI ) * x <= (2 * PI ) * (1 / 2) by XREAL_1:66;
(2 * PI ) * (1 / 4) < (2 * PI ) * x by A26, XREAL_1:70;
then A28: (2 * PI ) * x in ].(PI / 2),((2 * PI ) * (1 / 2)).] by A27, XXREAL_1:2;
A29: ].(PI / 2),PI .] c= ].(PI / 2),((3 / 2) * PI ).[ by Lm6, XXREAL_1:49;
A30: ].(PI / 2),PI .] c= [.0 ,PI .] by XXREAL_1:36;

per cases ( ( 0 <= y & y <= 1 / 4 ) or ( 1 / 4 < y & y <= 1 / 2 ) or ( 1 / 2 < y & y < 1 ) ) by A3, A6, XXREAL_1:3;

suppose A31: ( 0 <= y & y <= 1 / 4 ) ; :: thesis: x1 = y1

then (2 * PI ) * y <= (2 * PI ) * (1 / 4) by XREAL_1:66;
then (2 * PI ) * y in [.0 ,((2 * PI ) * (1 / 4)).] by A31, XXREAL_1:1;
hence x1 = y1 by A9, A11, A10, A2, A28, A29, COMPTRIG:28, COMPTRIG:29; :: thesis: verum

end;

suppose A32: ( 1 / 4 < y & y <= 1 / 2 ) ; :: thesis: x1 = y1

then A33: (2 * PI ) * y <= (2 * PI ) * (1 / 2) by XREAL_1:66;
(2 * PI ) * (1 / 4) < (2 * PI ) * y by A32, XREAL_1:70;
then A34: (2 * PI ) * y in ].((2 * PI ) * (1 / 4)),((2 * PI ) * (1 / 2)).] by A33, XXREAL_1:2;
set g = sin | ].(PI / 2),PI .];
A35: dom (sin | ].(PI / 2),PI .]) = ].(PI / 2),PI .] by RELAT_1:91, SIN_COS:27;
A36: sin | ].(PI / 2),PI .] is one-to-one by A1, Lm6, SIN_COS6:2, XXREAL_1:36;
(sin | ].(PI / 2),PI .]) . ((2 * PI ) * x) = sin . ((2 * PI ) * x) by A28, FUNCT_1:72
.= sin . ((2 * PI ) * y) by A12, A14, SIN_COS:def 21
.= (sin | ].(PI / 2),PI .]) . ((2 * PI ) * y) by A34, FUNCT_1:72 ;
then (2 * PI ) * x = (2 * PI ) * y by A28, A34, A36, A35, FUNCT_1:def 8;
then x = ((2 * PI ) * y) / (2 * PI ) by XCMPLX_1:90;
hence x1 = y1 by XCMPLX_1:90; :: thesis: verum

end;

suppose A37: ( 1 / 2 < y & y < 1 ) ; :: thesis: x1 = y1

then A38: (2 * PI ) * y < (2 * PI ) * 1 by XREAL_1:70;
(2 * PI ) * (1 / 2) < (2 * PI ) * y by A37, XREAL_1:70;
then (2 * PI ) * y in ].PI ,(2 * PI ).[ by A38, XXREAL_1:4;
hence x1 = y1 by A12, A14, A13, A28, A30, COMPTRIG:24, COMPTRIG:25; :: thesis: verum

end;

end;

end;

suppose A39: ( 1 / 2 < x & x <= 3 / 4 ) ; :: thesis: x1 = y1

then A40: (2 * PI ) * x <= (2 * PI ) * (3 / 4) by XREAL_1:66;
(2 * PI ) * (1 / 2) < (2 * PI ) * x by A39, XREAL_1:70;
then A41: (2 * PI ) * x in ].PI ,((2 * PI ) * (3 / 4)).] by A40, XXREAL_1:2;
A42: ].PI ,((3 / 2) * PI ).] c= [.(PI / 2),((3 / 2) * PI ).] by Lm5, XXREAL_1:36;
A43: ].PI ,((3 / 2) * PI ).] c= ].PI ,(2 * PI ).[ by Lm7, XXREAL_1:49;

per cases ( ( 0 <= y & y <= 1 / 2 ) or ( 1 / 2 < y & y <= 3 / 4 ) or ( 3 / 4 < y & y < 1 ) ) by A3, A6, XXREAL_1:3;

suppose A44: ( 0 <= y & y <= 1 / 2 ) ; :: thesis: x1 = y1

then (2 * PI ) * y <= (2 * PI ) * (1 / 2) by XREAL_1:66;
then (2 * PI ) * y in [.0 ,PI .] by A44, XXREAL_1:1;
hence x1 = y1 by A12, A14, A13, A41, A43, COMPTRIG:24, COMPTRIG:25; :: thesis: verum

end;

suppose A45: ( 1 / 2 < y & y <= 3 / 4 ) ; :: thesis: x1 = y1

then A46: (2 * PI ) * y <= (2 * PI ) * (3 / 4) by XREAL_1:66;
(2 * PI ) * (1 / 2) < (2 * PI ) * y by A45, XREAL_1:70;
then A47: (2 * PI ) * y in ].PI ,((2 * PI ) * (3 / 4)).] by A46, XXREAL_1:2;
set g = sin | ].PI ,((3 / 2) * PI ).];
A48: dom (sin | ].PI ,((3 / 2) * PI ).]) = ].PI ,((3 / 2) * PI ).] by RELAT_1:91, SIN_COS:27;
A49: sin | ].PI ,((3 / 2) * PI ).] is one-to-one by A1, Lm5, SIN_COS6:2, XXREAL_1:36;
(sin | ].PI ,((3 / 2) * PI ).]) . ((2 * PI ) * x) = sin . ((2 * PI ) * x) by A41, FUNCT_1:72
.= sin . ((2 * PI ) * y) by A12, A14, SIN_COS:def 21
.= (sin | ].PI ,((3 / 2) * PI ).]) . ((2 * PI ) * y) by A47, FUNCT_1:72 ;
then (2 * PI ) * x = (2 * PI ) * y by A41, A47, A49, A48, FUNCT_1:def 8;
then x = ((2 * PI ) * y) / (2 * PI ) by XCMPLX_1:90;
hence x1 = y1 by XCMPLX_1:90; :: thesis: verum

end;

suppose A50: ( 3 / 4 < y & y < 1 ) ; :: thesis: x1 = y1

then A51: (2 * PI ) * y < (2 * PI ) * 1 by XREAL_1:70;
(2 * PI ) * (3 / 4) < (2 * PI ) * y by A50, XREAL_1:70;
then (2 * PI ) * y in ].((3 / 2) * PI ),(2 * PI ).[ by A51, XXREAL_1:4;
hence x1 = y1 by A9, A11, A10, A41, A42, COMPTRIG:30, COMPTRIG:31; :: thesis: verum

end;

end;

end;

suppose A52: ( 3 / 4 < x & x < 1 ) ; :: thesis: x1 = y1

then A53: (2 * PI ) * x < (2 * PI ) * 1 by XREAL_1:70;
(2 * PI ) * (3 / 4) < (2 * PI ) * x by A52, XREAL_1:70;
then A54: (2 * PI ) * x in ].((3 / 2) * PI ),(2 * PI ).[ by A53, XXREAL_1:4;
A55: ].((3 / 2) * PI ),(2 * PI ).[ c= ].PI ,(2 * PI ).[ by Lm6, XXREAL_1:46;

per cases ( ( 0 <= y & y <= 1 / 2 ) or ( 1 / 2 < y & y <= 3 / 4 ) or ( 3 / 4 < y & y < 1 ) ) by A3, A6, XXREAL_1:3;

suppose A56: ( 0 <= y & y <= 1 / 2 ) ; :: thesis: x1 = y1

then (2 * PI ) * y <= (2 * PI ) * (1 / 2) by XREAL_1:66;
then (2 * PI ) * y in [.0 ,PI .] by A56, XXREAL_1:1;
hence x1 = y1 by A12, A14, A13, A54, A55, COMPTRIG:24, COMPTRIG:25; :: thesis: verum

end;

suppose A57: ( 1 / 2 < y & y <= 3 / 4 ) ; :: thesis: x1 = y1

then A58: (2 * PI ) * y <= (2 * PI ) * (3 / 4) by XREAL_1:66;
A59: ].PI ,((3 / 2) * PI ).] c= [.(PI / 2),((3 / 2) * PI ).] by Lm5, XXREAL_1:36;
(2 * PI ) * (1 / 2) < (2 * PI ) * y by A57, XREAL_1:70;
then (2 * PI ) * y in ].PI ,((3 / 2) * PI ).] by A58, XXREAL_1:2;
hence x1 = y1 by A9, A11, A10, A54, A59, COMPTRIG:30, COMPTRIG:31; :: thesis: verum

end;

suppose A60: ( 3 / 4 < y & y < 1 ) ; :: thesis: x1 = y1

then A61: (2 * PI ) * y < (2 * PI ) * 1 by XREAL_1:70;
(2 * PI ) * (3 / 4) < (2 * PI ) * y by A60, XREAL_1:70;
then A62: (2 * PI ) * y in ].((3 / 2) * PI ),(2 * PI ).[ by A61, XXREAL_1:4;
set g = sin | ].((3 / 2) * PI ),(2 * PI ).[;
A63: dom (sin | ].((3 / 2) * PI ),(2 * PI ).[) = ].((3 / 2) * PI ),(2 * PI ).[ by RELAT_1:91, SIN_COS:27;
(sin | ].((3 / 2) * PI ),(2 * PI ).[) . ((2 * PI ) * x) = sin . ((2 * PI ) * x) by A54, FUNCT_1:72
.= sin . ((2 * PI ) * y) by A12, A14, SIN_COS:def 21
.= (sin | ].((3 / 2) * PI ),(2 * PI ).[) . ((2 * PI ) * y) by A62, FUNCT_1:72 ;
then (2 * PI ) * x = (2 * PI ) * y by A54, A62, A63, FUNCT_1:def 8;
then x = ((2 * PI ) * y) / (2 * PI ) by XCMPLX_1:90;
hence x1 = y1 by XCMPLX_1:90; :: thesis: verum

end;

end;

end;

end;