set D1 = IntIntervals 0 ,1;
set D2 = IntIntervals (1 / 2),(3 / 2);
A1: c[10] in {c[10] } by TARSKI:def 1;
set F1 = CircleMap .: (union (IntIntervals 0 ,1));
set F2 = CircleMap .: (union (IntIntervals (1 / 2),(3 / 2)));
set F = {(CircleMap .: (union (IntIntervals 0 ,1))),(CircleMap .: (union (IntIntervals (1 / 2),(3 / 2))))};
reconsider F = {(CircleMap .: (union (IntIntervals 0 ,1))),(CircleMap .: (union (IntIntervals (1 / 2),(3 / 2))))} as Subset-Family of (Tunit_circle 2) ;
take F ; :: thesis:
A2: ].(0 + 0 ),(1 + 0 ).[ in IntIntervals 0 ,1 by Lm1;
then A3: CircleMap .: (union (IntIntervals 0 ,1)) = CircleMap .: ].0 ,1.[ by Th41;
].((1 / 2) + 0 ),((3 / 2) + 0 ).[ in IntIntervals (1 / 2),(3 / 2) by Lm1;
then A4: CircleMap .: (union (IntIntervals (1 / 2),(3 / 2))) = CircleMap .: ].(1 / 2),(3 / 2).[ by Th41;
hence F = {(CircleMap .: ].0 ,1.[),(CircleMap .: ].(1 / 2),(3 / 2).[)} by A2, Th41; :: thesis:
thus F is Cover of (Tunit_circle 2) :: thesis:

proof

let a be set ; :: according to TARSKI:def 3,SETFAM_1:def 12 :: thesis:
assume A5: a in the carrier of (Tunit_circle 2) ; :: thesis:
reconsider A = [.0 ,(0 + 1).[ as Subset of R^1 by TOPMETR:24;
reconsider f = CircleMap | A as Function of (R^1 | A),(Tunit_circle 2) by Lm23;
f is onto by Th39;
then rng f = the carrier of (Tunit_circle 2) by FUNCT_2:def 3;
then consider x being set such that
A6: x in dom f and
A7: f . x = a by A5, FUNCT_1:def 5;
A8: dom f = A by Lm19, RELAT_1:91;
then reconsider x = x as Real by A6;
A9: CircleMap . x = f . x by A6, FUNCT_1:70;
A10: CircleMap .: (union (IntIntervals (1 / 2),(3 / 2))) in F by TARSKI:def 2;

per cases by A6, A8, XXREAL_1:3;

suppose A11: x = 0 ; :: thesis:

0 in A by XXREAL_1:3;
then A12: f . 0 = CircleMap . 0 by FUNCT_1:72
.= c[10] by Th33
.= CircleMap . 1 by Th33 ;
1 in ].(1 / 2),(3 / 2).[ by XXREAL_1:4;
then a in CircleMap .: ].(1 / 2),(3 / 2).[ by A7, A11, A12, Lm19, FUNCT_1:def 12;
hence a in union F by A4, A10, TARSKI:def 4; :: thesis:

end;

suppose ( 0 < x & x < 1 ) ; :: thesis:

then A13: x in ].0 ,1.[ by XXREAL_1:4;
].(0 + 0 ),(1 + 0 ).[ in IntIntervals 0 ,1 by Lm1;
then x in union (IntIntervals 0 ,1) by A13, TARSKI:def 4;
then A14: a in CircleMap .: (union (IntIntervals 0 ,1)) by A7, A9, Lm19, FUNCT_1:def 12;
CircleMap .: (union (IntIntervals 0 ,1)) in F by TARSKI:def 2;
hence a in union F by A14, TARSKI:def 4; :: thesis:

end;

suppose ( x >= 1 & x < 1 ) ; :: thesis:

hence a in union F ; :: thesis:

end;

thus F is open :: thesis:

proof

let P be Subset of (Tunit_circle 2); :: according to TOPS_2:def 1 :: thesis:
A15: CircleMap .: ].0 ,1.[ = (CircleMap (R^1 0 )) .: ].0 ,1.[ by RELAT_1:162;
A16: CircleMap .: ].(1 / 2),(3 / 2).[ = (CircleMap (R^1 (1 / 2))) .: ].(1 / 2),(3 / 2).[ by RELAT_1:162;
reconsider r = 0 as Integer ;

A17: now

let A be Subset of REAL ; :: thesis:
A c= A ;
hence A is Subset of (R^1 | (R^1 A)) by PRE_TOPC:29; :: thesis:

end;

then reconsider M = ].0 ,1.[ as Subset of (R^1 | (R^1 ].r,(r + 1).[)) ;
reconsider N = ].(1 / 2),(3 / 2).[ as Subset of (R^1 | (R^1 ].((1 / 2) + r),(((1 / 2) + r) + 1).[)) by A17;

A18: now

let A be open Subset of REAL ; :: thesis:
reconsider B = A as Subset of (R^1 | (R^1 A)) by A17;
the carrier of (R^1 | (R^1 A)) = A by PRE_TOPC:29;
then B = ([#] (R^1 | (R^1 A))) /\ (R^1 A) ;
hence A is open Subset of (R^1 | (R^1 A)) by TOPS_2:32; :: thesis:

end;

then M is open ;
then A19: (CircleMap (R^1 r)) .: M is open by T_0TOPSP:def 2;
N is open by A18;
then (CircleMap (R^1 ((1 / 2) + r))) .: N is open by T_0TOPSP:def 2;
then ( CircleMap .: (union (IntIntervals 0 ,1)) is open & CircleMap .: (union (IntIntervals (1 / 2),(3 / 2))) is open ) by A3, A4, A15, A16, A19, TSEP_1:17;
hence ( not P in F or P is open ) by TARSKI:def 2; :: thesis:

end;

let U be Subset of (Tunit_circle 2); :: thesis:
thus ( U = CircleMap .: ].0 ,1.[ implies ( union (IntIntervals 0 ,1) = CircleMap " U & ( for d being Subset of R^1 st d in IntIntervals 0 ,1 holds
for f being Function of (R^1 | d),((Tunit_circle 2) | U) st f = CircleMap | d holds
f is being_homeomorphism ) ) ) :: thesis:

proof

assume A20: U = CircleMap .: ].0 ,1.[ ; :: thesis:
].(0 + 0 ),(1 + 0 ).[ in IntIntervals 0 ,1 by Lm1;
then A21: CircleMap .: ].0 ,1.[ = CircleMap .: (union (IntIntervals 0 ,1)) by Th41;

now

let x1, x2 be Element of R^1 ; :: thesis:
assume x1 in union (IntIntervals 0 ,1) ; :: thesis:
then consider Z being set such that
A22: x1 in Z and
A23: Z in IntIntervals 0 ,1 by TARSKI:def 4;
consider n being Element of INT such that
A24: Z = ].(0 + n),(1 + n).[ by A23;
assume A25: CircleMap . x1 = CircleMap . x2 ; :: thesis:
set k = [\x2/];
set K = ].(0 + [\x2/]),(1 + [\x2/]).[;
[\x2/] in INT by INT_1:def 2;
then A26: ].(0 + [\x2/]),(1 + [\x2/]).[ in IntIntervals 0 ,1 ;
A27: n < x1 by A22, A24, XXREAL_1:4;
x1 < 1 + n by A22, A24, XXREAL_1:4;
then A28: x1 - 1 < (1 + n) - 1 by XREAL_1:11;
then A29: [\x1/] = n by A27, INT_1:def 4;
A30: [\x2/] <= x2 by INT_1:def 4;
not x1 is integer by A27, A29, INT_1:48;
then A31: not x1 in INT ;

now

assume [\x2/] = x2 ; :: thesis:
then CircleMap . x1 = c[10] by A25, Th33;
hence contradiction by A1, A31, Lm19, Th34, FUNCT_1:def 13, TOPMETR:24; :: thesis:

end;

then A32: [\x2/] < x2 by A30, XXREAL_0:1;
A33: ( CircleMap . x1 = CircleMap . (x1 + (- n)) & CircleMap . x2 = CircleMap . (x2 + (- [\x2/])) ) by Th32;
0 < x1 - n by A27, XREAL_1:52;
then A34: (2 * PI ) * 0 <= (2 * PI ) * (x1 - n) ;
(x1 - 1) - n < n - n by A28, XREAL_1:11;
then ((x1 - n) - 1) + 1 < 0 + 1 by XREAL_1:10;
then A35: (2 * PI ) * (x1 - n) < (2 * PI ) * 1 by XREAL_1:70;
0 <= x2 - [\x2/] by A32, XREAL_1:52;
then A36: (2 * PI ) * 0 <= (2 * PI ) * (x2 - [\x2/]) ;
x2 - 1 < [\x2/] by INT_1:def 4;
then (x2 - 1) - [\x2/] < [\x2/] - [\x2/] by XREAL_1:11;
then ((x2 - 1) - [\x2/]) + 1 < 0 + 1 by XREAL_1:8;
then A37: (2 * PI ) * (x2 - [\x2/]) < (2 * PI ) * 1 by XREAL_1:70;
( CircleMap . (x1 - n) = |[(cos ((2 * PI ) * (x1 - n))),(sin ((2 * PI ) * (x1 - n)))]| & CircleMap . (x2 - [\x2/]) = |[(cos ((2 * PI ) * (x2 - [\x2/]))),(sin ((2 * PI ) * (x2 - [\x2/])))]| ) by Def11;
then ( cos ((2 * PI ) * (x1 - n)) = cos ((2 * PI ) * (x2 - [\x2/])) & sin ((2 * PI ) * (x1 - n)) = sin ((2 * PI ) * (x2 - [\x2/])) ) by A25, A33, SPPOL_2:1;
then (2 * PI ) * (x1 - n) = (2 * PI ) * (x2 - [\x2/]) by A34, A35, A36, A37, COMPLEX2:12;
then x1 - n = x2 - [\x2/] by XCMPLX_1:5;
then A38: x2 = (x1 - n) + [\x2/] ;
x1 < 1 + n by A22, A24, XXREAL_1:4;
then x1 - n < 1 by XREAL_1:21;
then x2 < 1 + [\x2/] by A38, XREAL_1:8;
then x2 in ].(0 + [\x2/]),(1 + [\x2/]).[ by A32, XXREAL_1:4;
hence x2 in union (IntIntervals 0 ,1) by A26, TARSKI:def 4; :: thesis:

end;

hence union (IntIntervals 0 ,1) = CircleMap " U by A20, A21, T_0TOPSP:2; :: thesis:
let d be Subset of R^1 ; :: thesis:
assume A39: d in IntIntervals 0 ,1 ; :: thesis:
let f be Function of (R^1 | d),((Tunit_circle 2) | U); :: thesis:
assume A40: f = CircleMap | d ; :: thesis:
consider n being Element of INT such that
A41: d = ].(0 + n),(1 + n).[ by A39;
reconsider d1 = d as non empty Subset of R^1 by A41;
reconsider U1 = U as non empty Subset of (Tunit_circle 2) by A20, Lm19;
reconsider f1 = f as Function of (R^1 | d1),((Tunit_circle 2) | U1) ;
A42: [#] ((Tunit_circle 2) | U) = U by PRE_TOPC:def 10;
A43: CircleMap .: (union (IntIntervals 0 ,1)) = CircleMap .: d by A39, Th41;
A44: f is one-to-one by A39, A40, Lm3, Th40;
A45: f is continuous by A40, TOPREALA:29;
reconsider J = ].n,(n + p1).[ as non empty Subset of R^1 by TOPMETR:24;
reconsider F = CircleMap | J as Function of (R^1 | J),(Tunit_circle 2) by Lm23;
d c= J by A41;
then reconsider d2 = d as Subset of (R^1 | J) by PRE_TOPC:29;
A46: (R^1 | J) | d2 = R^1 | d by A41, PRE_TOPC:28;
A47: CircleMap | d = (CircleMap | J) | d1 by A41, RELAT_1:103;
A48: f1 is onto

proof

thus rng f1 c= the carrier of ((Tunit_circle 2) | U1) ; :: according to XBOOLE_0:def 10,FUNCT_2:def 3 :: thesis:
let b be set ; :: according to TARSKI:def 3 :: thesis:
assume b in the carrier of ((Tunit_circle 2) | U1) ; :: thesis:
then consider a being Element of R^1 such that
A49: a in d and
A50: b = CircleMap . a by A20, A21, A42, A43, FUNCT_2:116;
A51: dom (CircleMap | d) = d by Lm19, RELAT_1:91, TOPMETR:24;
(CircleMap | d) . a = CircleMap . a by A49, FUNCT_1:72;
hence b in rng f1 by A40, A49, A50, A51, FUNCT_1:def 5; :: thesis:

end;

CircleMap (R^1 n) is open ;
then A52: F is open by TOPREALA:33;
thus f is being_homeomorphism by A40, A44, A45, A46, A47, A48, A52, TOPREALA:31, TOPREALA:37; :: thesis:

end;

assume A53: U = CircleMap .: ].(1 / 2),(3 / 2).[ ; :: thesis:

now

let x1, x2 be Element of R^1 ; :: thesis:
assume x1 in union (IntIntervals (1 / 2),(3 / 2)) ; :: thesis:
then consider Z being set such that
A54: x1 in Z and
A55: Z in IntIntervals (1 / 2),(3 / 2) by TARSKI:def 4;
consider n being Element of INT such that
A56: Z = ].((1 / 2) + n),((3 / 2) + n).[ by A55;
assume A57: CircleMap . x1 = CircleMap . x2 ; :: thesis:
A58: (1 / 2) + n < x1 by A54, A56, XXREAL_1:4;
0 + n < (1 / 2) + n by XREAL_1:10;
then A59: n < x1 by A58, XXREAL_0:2;
A60: x1 < (3 / 2) + n by A54, A56, XXREAL_1:4;
then A61: x1 - n < 3 / 2 by XREAL_1:21;
set k = [\x2/];
A62: [\x2/] <= x2 by INT_1:def 4;

per cases by XXREAL_0:1;

suppose x1 = 1 + n ; :: thesis:

then CircleMap . x2 = c[10] by A57, Th33;
then reconsider w = x2 as Element of INT by A1, Lm19, Th34, FUNCT_1:def 13, TOPMETR:24;
w - 1 in INT by INT_1:def 2;
then A63: ].((1 / 2) + (w - 1)),((3 / 2) + (w - 1)).[ in IntIntervals (1 / 2),(3 / 2) ;
A64: (- (1 / 2)) + w < 0 + w by XREAL_1:10;
0 + w < (1 / 2) + w by XREAL_1:10;
then x2 in ].((1 / 2) + (w - 1)),((3 / 2) + (w - 1)).[ by A64, XXREAL_1:4;
hence x2 in union (IntIntervals (1 / 2),(3 / 2)) by A63, TARSKI:def 4; :: thesis:

end;

suppose A65: x1 < 1 + n ; :: thesis:

set K = ].((1 / 2) + [\x2/]),((3 / 2) + [\x2/]).[;
[\x2/] in INT by INT_1:def 2;
then A66: ].((1 / 2) + [\x2/]),((3 / 2) + [\x2/]).[ in IntIntervals (1 / 2),(3 / 2) ;
A67: ( CircleMap . x1 = CircleMap . (x1 + (- n)) & CircleMap . x2 = CircleMap . (x2 + (- [\x2/])) ) by Th32;
( CircleMap . (x1 - n) = |[(cos ((2 * PI ) * (x1 - n))),(sin ((2 * PI ) * (x1 - n)))]| & CircleMap . (x2 - [\x2/]) = |[(cos ((2 * PI ) * (x2 - [\x2/]))),(sin ((2 * PI ) * (x2 - [\x2/])))]| ) by Def11;
then A68: ( cos ((2 * PI ) * (x1 - n)) = cos ((2 * PI ) * (x2 - [\x2/])) & sin ((2 * PI ) * (x1 - n)) = sin ((2 * PI ) * (x2 - [\x2/])) ) by A57, A67, SPPOL_2:1;
0 < x1 - n by A59, XREAL_1:52;
then A69: (2 * PI ) * 0 <= (2 * PI ) * (x1 - n) ;
x1 - 1 < (n + 1) - 1 by A65, XREAL_1:11;
then (x1 - 1) - n < n - n by XREAL_1:11;
then ((x1 - n) - 1) + 1 < 0 + 1 by XREAL_1:10;
then A70: (2 * PI ) * (x1 - n) < (2 * PI ) * 1 by XREAL_1:70;
x2 - x2 <= x2 - [\x2/] by A62, XREAL_1:15;
then A71: (2 * PI ) * 0 <= (2 * PI ) * (x2 - [\x2/]) ;
x2 - 1 < [\x2/] by INT_1:def 4;
then (x2 - 1) - [\x2/] < [\x2/] - [\x2/] by XREAL_1:11;
then ((x2 - 1) - [\x2/]) + 1 < 0 + 1 by XREAL_1:8;
then (2 * PI ) * (x2 - [\x2/]) < (2 * PI ) * 1 by XREAL_1:70;
then (2 * PI ) * (x1 - n) = (2 * PI ) * (x2 - [\x2/]) by A68, A69, A70, A71, COMPLEX2:12;
then A72: x1 - n = x2 - [\x2/] by XCMPLX_1:5;
then A73: x2 = (x1 - n) + [\x2/] ;
((1 / 2) + n) - n < x1 - n by A58, XREAL_1:11;
then A74: (1 / 2) + [\x2/] < (x1 - n) + [\x2/] by XREAL_1:10;
x2 < (3 / 2) + [\x2/] by A61, A73, XREAL_1:8;
then x2 in ].((1 / 2) + [\x2/]),((3 / 2) + [\x2/]).[ by A72, A74, XXREAL_1:4;
hence x2 in union (IntIntervals (1 / 2),(3 / 2)) by A66, TARSKI:def 4; :: thesis:

end;

suppose A75: x1 > 1 + n ; :: thesis:

set K = ].((1 / 2) + ([\x2/] - 1)),((3 / 2) + ([\x2/] - 1)).[;
[\x2/] - 1 in INT by INT_1:def 2;
then A76: ].((1 / 2) + ([\x2/] - 1)),((3 / 2) + ([\x2/] - 1)).[ in IntIntervals (1 / 2),(3 / 2) ;
A77: ( CircleMap . x1 = CircleMap . (x1 + ((- 1) - n)) & CircleMap . x2 = CircleMap . (x2 + (- [\x2/])) ) by Th32;
( CircleMap . ((x1 - 1) - n) = |[(cos ((2 * PI ) * ((x1 - 1) - n))),(sin ((2 * PI ) * ((x1 - 1) - n)))]| & CircleMap . (x2 - [\x2/]) = |[(cos ((2 * PI ) * (x2 - [\x2/]))),(sin ((2 * PI ) * (x2 - [\x2/])))]| ) by Def11;
then A78: ( cos ((2 * PI ) * ((x1 - 1) - n)) = cos ((2 * PI ) * (x2 - [\x2/])) & sin ((2 * PI ) * ((x1 - 1) - n)) = sin ((2 * PI ) * (x2 - [\x2/])) ) by A57, A77, SPPOL_2:1;
A79: x1 - 1 < ((3 / 2) + n) - 1 by A60, XREAL_1:11;
A80: (n + 1) - 1 < x1 - 1 by A75, XREAL_1:11;
then n - n < (x1 - 1) - n by XREAL_1:11;
then A81: (2 * PI ) * 0 <= (2 * PI ) * ((x1 - 1) - n) ;
(x1 - 1) - n < ((1 / 2) + n) - n by A79, XREAL_1:11;
then (x1 - 1) - n < 1 by XXREAL_0:2;
then A82: (2 * PI ) * ((x1 - 1) - n) < (2 * PI ) * 1 by XREAL_1:70;
x2 - x2 <= x2 - [\x2/] by A62, XREAL_1:15;
then A83: (2 * PI ) * 0 <= (2 * PI ) * (x2 - [\x2/]) ;
x2 - 1 < [\x2/] by INT_1:def 4;
then (x2 - 1) - [\x2/] < [\x2/] - [\x2/] by XREAL_1:11;
then ((x2 - 1) - [\x2/]) + 1 < 0 + 1 by XREAL_1:8;
then (2 * PI ) * (x2 - [\x2/]) < (2 * PI ) * 1 by XREAL_1:70;
then (2 * PI ) * ((x1 - 1) - n) = (2 * PI ) * (x2 - [\x2/]) by A78, A81, A82, A83, COMPLEX2:12;
then A84: (x1 - 1) - n = x2 - [\x2/] by XCMPLX_1:5;
then A85: x2 = ((x1 - 1) - n) + [\x2/] ;
A86: n - n < (x1 - 1) - n by A80, XREAL_1:11;
- (1 / 2) < 0 ;
then A87: (- (1 / 2)) + [\x2/] < ((x1 - 1) - n) + [\x2/] by A86, XREAL_1:10;
(x1 - n) - 1 < (3 / 2) - 1 by A61, XREAL_1:11;
then x2 < (1 / 2) + [\x2/] by A85, XREAL_1:8;
then x2 in ].((1 / 2) + ([\x2/] - 1)),((3 / 2) + ([\x2/] - 1)).[ by A84, A87, XXREAL_1:4;
hence x2 in union (IntIntervals (1 / 2),(3 / 2)) by A76, TARSKI:def 4; :: thesis:

end;

hence union (IntIntervals (1 / 2),(3 / 2)) = CircleMap " U by A4, A53, T_0TOPSP:2; :: thesis:
let d be Subset of R^1 ; :: thesis:
assume A88: d in IntIntervals (1 / 2),(3 / 2) ; :: thesis:
let f be Function of (R^1 | d),((Tunit_circle 2) | U); :: thesis:
assume A89: f = CircleMap | d ; :: thesis:
consider n being Element of INT such that
A90: d = ].((1 / 2) + n),((3 / 2) + n).[ by A88;
( (1 / 2) + n < 1 + n & 1 + n < (3 / 2) + n ) by XREAL_1:8;
then reconsider d1 = d as non empty Subset of R^1 by A90, XXREAL_1:4;
reconsider U1 = U as non empty Subset of (Tunit_circle 2) by A53, Lm19;
reconsider f1 = f as Function of (R^1 | d1),((Tunit_circle 2) | U1) ;
A91: [#] ((Tunit_circle 2) | U) = U by PRE_TOPC:def 10;
A92: CircleMap .: (union (IntIntervals (1 / 2),(3 / 2))) = CircleMap .: d by A88, Th41;
A93: f is one-to-one by A88, A89, Lm4, Th40;
A94: f is continuous by A89, TOPREALA:29;
reconsider J = ].((1 / 2) + n),(((1 / 2) + n) + p1).[ as non empty Subset of R^1 by TOPMETR:24;
reconsider F = CircleMap | J as Function of (R^1 | J),(Tunit_circle 2) by Lm23;
d c= J by A90;
then reconsider d2 = d as Subset of (R^1 | J) by PRE_TOPC:29;
A95: (R^1 | J) | d2 = R^1 | d by A90, PRE_TOPC:28;
A96: CircleMap | d = (CircleMap | J) | d1 by A90, RELAT_1:103;
A97: f1 is onto

proof

thus rng f1 c= the carrier of ((Tunit_circle 2) | U1) ; :: according to XBOOLE_0:def 10,FUNCT_2:def 3 :: thesis:
let b be set ; :: according to TARSKI:def 3 :: thesis:
assume b in the carrier of ((Tunit_circle 2) | U1) ; :: thesis:
then consider a being Element of R^1 such that
A98: a in d and
A99: b = CircleMap . a by A4, A53, A91, A92, FUNCT_2:116;
A100: dom (CircleMap | d) = d by Lm19, RELAT_1:91, TOPMETR:24;
(CircleMap | d) . a = CircleMap . a by A98, FUNCT_1:72;
hence b in rng f1 by A89, A98, A99, A100, FUNCT_1:def 5; :: thesis:

end;

CircleMap (R^1 ((1 / 2) + n)) is open ;
then A101: F is open by TOPREALA:33;
thus f is being_homeomorphism by A89, A93, A94, A95, A96, A97, A101, TOPREALA:31, TOPREALA:37; :: thesis: