set f = CircleMap | [.0 ,1.[;
A1: dom (CircleMap | [.0 ,1.[) = [.0 ,1.[ by Lm19, RELAT_1:91;
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 )
assume A2: 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 A1;
assume A3: 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 A1;
assume A4: (CircleMap | [.0 ,1.[) . x1 = (CircleMap | [.0 ,1.[) . y1 ; :: thesis: x1 = y1
A5: (CircleMap | [.0 ,1.[) . x = CircleMap . x by A1, A2, FUNCT_1:72
.= |[(cos ((2 * PI ) * x)),(sin ((2 * PI ) * x))]| by Def11 ;
A6: (CircleMap | [.0 ,1.[) . y = CircleMap . y by A1, A3, FUNCT_1:72
.= |[(cos ((2 * PI ) * y)),(sin ((2 * PI ) * y))]| by Def11 ;
then A7: cos ((2 * PI ) * x) = cos ((2 * PI ) * y) by A4, A5, SPPOL_2:1;
A8: sin ((2 * PI ) * x) = sin ((2 * PI ) * y) by A4, A5, A6, SPPOL_2:1;
A9: sin ((2 * PI ) * x) = sin . ((2 * PI ) * x) by SIN_COS:def 21;
A10: sin ((2 * PI ) * y) = sin . ((2 * PI ) * y) by SIN_COS:def 21;
A11: cos ((2 * PI ) * x) = cos . ((2 * PI ) * x) by SIN_COS:def 23;
A12: cos ((2 * PI ) * y) = cos . ((2 * PI ) * y) by SIN_COS:def 23;
A13: [.0 ,(PI / 2).] c= [.(- (PI / 2)),(PI / 2).] by XXREAL_1:34;
A14: sin | [.(PI / 2),((3 / 2) * PI ).] is one-to-one ;

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 A1, A2, XXREAL_1:3;

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

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

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

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

then ( (2 * PI ) * 0 <= (2 * PI ) * y & (2 * PI ) * y <= (2 * PI ) * (1 / 4) ) by XREAL_1:66;
then A17: (2 * PI ) * y in [.0 ,(((2 * PI ) * 1) / 4).] by XXREAL_1:1;
set g = sin | [.0 ,(PI / 2).];
A18: 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 A15, FUNCT_1:72
.= sin . ((2 * PI ) * y) by A8, A9, SIN_COS:def 21
.= (sin | [.0 ,(PI / 2).]) . ((2 * PI ) * y) by A17, FUNCT_1:72 ;
then (2 * PI ) * x = (2 * PI ) * y by A15, A17, A18, 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 ( 1 / 4 < y & y < 3 / 4 ) ; :: thesis: x1 = y1

then ( (2 * PI ) * (1 / 4) < (2 * PI ) * y & (2 * PI ) * y < (2 * PI ) * (3 / 4) ) by XREAL_1:70;
then (2 * PI ) * y in ].(PI / 2),((3 / 2) * PI ).[ by XXREAL_1:4;
hence x1 = y1 by A7, A11, A12, A13, A15, COMPTRIG:28, COMPTRIG:29; :: thesis: verum

end;

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

then ( (2 * PI ) * (3 / 4) <= (2 * PI ) * y & (2 * PI ) * y < (2 * PI ) * 1 ) by XREAL_1:66, XREAL_1:70;
then A19: (2 * PI ) * y in [.((3 / 2) * PI ),(2 * PI ).[ by XXREAL_1:3;
[.((3 / 2) * PI ),(2 * PI ).[ c= ].PI ,(2 * PI ).[ by Lm6, XXREAL_1:48;
hence x1 = y1 by A8, A9, A10, A15, A16, A19, COMPTRIG:24, COMPTRIG:25; :: thesis: verum

end;

end;

end;

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

then ( (2 * PI ) * (1 / 4) < (2 * PI ) * x & (2 * PI ) * x <= (2 * PI ) * (1 / 2) ) by XREAL_1:66, XREAL_1:70;
then A20: (2 * PI ) * x in ].(PI / 2),((2 * PI ) * (1 / 2)).] by XXREAL_1:2;
A21: ].(PI / 2),PI .] c= ].(PI / 2),((3 / 2) * PI ).[ by Lm6, XXREAL_1:49;
A22: ].(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 A1, A3, XXREAL_1:3;

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

then ( (2 * PI ) * 0 <= (2 * PI ) * y & (2 * PI ) * y <= (2 * PI ) * (1 / 4) ) by XREAL_1:66;
then (2 * PI ) * y in [.0 ,((2 * PI ) * (1 / 4)).] by XXREAL_1:1;
hence x1 = y1 by A7, A11, A12, A13, A20, A21, COMPTRIG:28, COMPTRIG:29; :: thesis: verum

end;

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

then ( (2 * PI ) * (1 / 4) < (2 * PI ) * y & (2 * PI ) * y <= (2 * PI ) * (1 / 2) ) by XREAL_1:66, XREAL_1:70;
then A23: (2 * PI ) * y in ].((2 * PI ) * (1 / 4)),((2 * PI ) * (1 / 2)).] by XXREAL_1:2;
set g = sin | ].(PI / 2),PI .];
A24: sin | ].(PI / 2),PI .] is one-to-one by A14, Lm6, SIN_COS6:2, XXREAL_1:36;
A25: dom (sin | ].(PI / 2),PI .]) = ].(PI / 2),PI .] by RELAT_1:91, SIN_COS:27;
(sin | ].(PI / 2),PI .]) . ((2 * PI ) * x) = sin . ((2 * PI ) * x) by A20, FUNCT_1:72
.= sin . ((2 * PI ) * y) by A8, A9, SIN_COS:def 21
.= (sin | ].(PI / 2),PI .]) . ((2 * PI ) * y) by A23, FUNCT_1:72 ;
then (2 * PI ) * x = (2 * PI ) * y by A20, A23, A24, A25, 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 ( 1 / 2 < y & y < 1 ) ; :: thesis: x1 = y1

then ( (2 * PI ) * (1 / 2) < (2 * PI ) * y & (2 * PI ) * y < (2 * PI ) * 1 ) by XREAL_1:70;
then (2 * PI ) * y in ].PI ,(2 * PI ).[ by XXREAL_1:4;
hence x1 = y1 by A8, A9, A10, A20, A22, COMPTRIG:24, COMPTRIG:25; :: thesis: verum

end;

end;

end;

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

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

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

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

then ( (2 * PI ) * 0 <= (2 * PI ) * y & (2 * PI ) * y <= (2 * PI ) * (1 / 2) ) by XREAL_1:66;
then (2 * PI ) * y in [.0 ,PI .] by XXREAL_1:1;
hence x1 = y1 by A8, A9, A10, A26, A27, COMPTRIG:24, COMPTRIG:25; :: thesis: verum

end;

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

then ( (2 * PI ) * (1 / 2) < (2 * PI ) * y & (2 * PI ) * y <= (2 * PI ) * (3 / 4) ) by XREAL_1:66, XREAL_1:70;
then A29: (2 * PI ) * y in ].PI ,((2 * PI ) * (3 / 4)).] by XXREAL_1:2;
set g = sin | ].PI ,((3 / 2) * PI ).];
A30: sin | ].PI ,((3 / 2) * PI ).] is one-to-one by A14, Lm5, SIN_COS6:2, XXREAL_1:36;
A31: dom (sin | ].PI ,((3 / 2) * PI ).]) = ].PI ,((3 / 2) * PI ).] by RELAT_1:91, SIN_COS:27;
(sin | ].PI ,((3 / 2) * PI ).]) . ((2 * PI ) * x) = sin . ((2 * PI ) * x) by A26, FUNCT_1:72
.= sin . ((2 * PI ) * y) by A8, A9, SIN_COS:def 21
.= (sin | ].PI ,((3 / 2) * PI ).]) . ((2 * PI ) * y) by A29, FUNCT_1:72 ;
then (2 * PI ) * x = (2 * PI ) * y by A26, A29, A30, A31, 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 ( 3 / 4 < y & y < 1 ) ; :: thesis: x1 = y1

then ( (2 * PI ) * (3 / 4) < (2 * PI ) * y & (2 * PI ) * y < (2 * PI ) * 1 ) by XREAL_1:70;
then (2 * PI ) * y in ].((3 / 2) * PI ),(2 * PI ).[ by XXREAL_1:4;
hence x1 = y1 by A7, A11, A12, A26, A28, COMPTRIG:30, COMPTRIG:31; :: thesis: verum

end;

end;

end;

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

then ( (2 * PI ) * (3 / 4) < (2 * PI ) * x & (2 * PI ) * x < (2 * PI ) * 1 ) by XREAL_1:70;
then A32: (2 * PI ) * x in ].((3 / 2) * PI ),(2 * PI ).[ by XXREAL_1:4;
A33: ].((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 A1, A3, XXREAL_1:3;

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

then ( (2 * PI ) * 0 <= (2 * PI ) * y & (2 * PI ) * y <= (2 * PI ) * (1 / 2) ) by XREAL_1:66;
then (2 * PI ) * y in [.0 ,PI .] by XXREAL_1:1;
hence x1 = y1 by A8, A9, A10, A32, A33, COMPTRIG:24, COMPTRIG:25; :: thesis: verum

end;

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

then ( (2 * PI ) * (1 / 2) < (2 * PI ) * y & (2 * PI ) * y <= (2 * PI ) * (3 / 4) ) by XREAL_1:66, XREAL_1:70;
then A34: (2 * PI ) * y in ].PI ,((3 / 2) * PI ).] by XXREAL_1:2;
].PI ,((3 / 2) * PI ).] c= [.(PI / 2),((3 / 2) * PI ).] by Lm5, XXREAL_1:36;
hence x1 = y1 by A7, A11, A12, A32, A34, COMPTRIG:30, COMPTRIG:31; :: thesis: verum

end;

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

then ( (2 * PI ) * (3 / 4) < (2 * PI ) * y & (2 * PI ) * y < (2 * PI ) * 1 ) by XREAL_1:70;
then A35: (2 * PI ) * y in ].((3 / 2) * PI ),(2 * PI ).[ by XXREAL_1:4;
set g = sin | ].((3 / 2) * PI ),(2 * PI ).[;
A36: 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 A32, FUNCT_1:72
.= sin . ((2 * PI ) * y) by A8, A9, SIN_COS:def 21
.= (sin | ].((3 / 2) * PI ),(2 * PI ).[) . ((2 * PI ) * y) by A35, FUNCT_1:72 ;
then (2 * PI ) * x = (2 * PI ) * y by A32, A35, A36, 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;