set D2 = IntIntervals ((1 / 2),(3 / 2));
set D1 = IntIntervals (0,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:
].((1 / 2) + 0),((3 / 2) + 0).[ in IntIntervals ((1 / 2),(3 / 2)) by Lm1;
then A1: CircleMap .: (union (IntIntervals ((1 / 2),(3 / 2)))) = CircleMap .: ].(1 / 2),(3 / 2).[ by Th40;
A2: ].(0 + 0),(1 + 0).[ in IntIntervals (0,1) by Lm1;
hence F = {(CircleMap .: ].0,1.[),(CircleMap .: ].(1 / 2),(3 / 2).[)} by A1, Th40; :: thesis:
thus F is Cover of (Tunit_circle 2) :: thesis:

proof

reconsider A = [.0,(0 + 1).[ as Subset of R^1 by TOPMETR:17;
reconsider f = CircleMap | A as Function of (R^1 | A),(Tunit_circle 2) by Lm21;
let a be object ; :: according to TARSKI:def 3,SETFAM_1:def 11 :: thesis:
A3: CircleMap .: (union (IntIntervals ((1 / 2),(3 / 2)))) in F by TARSKI:def 2;
f is onto by Th38;
then A4: rng f = the carrier of (Tunit_circle 2) ;
assume a in the carrier of (Tunit_circle 2) ; :: thesis:
then consider x being object such that
A5: x in dom f and
A6: f . x = a by A4, FUNCT_1:def 3;
A7: dom f = A by Lm18, RELAT_1:62;
then reconsider x = x as Element of REAL by A5;
A8: CircleMap . x = f . x by A5, FUNCT_1:47;

per cases by A5, A7, XXREAL_1:3;

suppose A9: x = 0 ; :: thesis:

0 in A by XXREAL_1:3;
then A10: f . 0 = CircleMap . 0 by FUNCT_1:49
.= c[10] by Th32
.= CircleMap . 1 by Th32 ;
1 in ].(1 / 2),(3 / 2).[ by XXREAL_1:4;
then a in CircleMap .: ].(1 / 2),(3 / 2).[ by A6, A9, A10, Lm18, FUNCT_1:def 6;
hence a in union F by A1, A3, TARSKI:def 4; :: thesis:

end;

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

A12: ].(0 + 0),(1 + 0).[ in IntIntervals (0,1) by Lm1;
x in ].0,1.[ by A11, XXREAL_1:4;
then x in union (IntIntervals (0,1)) by A12, TARSKI:def 4;
then A13: a in CircleMap .: (union (IntIntervals (0,1))) by A6, A8, Lm18, FUNCT_1:def 6;
CircleMap .: (union (IntIntervals (0,1))) in F by TARSKI:def 2;
hence a in union F by A13, TARSKI:def 4; :: thesis:

end;

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

hence a in union F ; :: thesis:

end;

A14: CircleMap .: (union (IntIntervals (0,1))) = CircleMap .: ].0,1.[ by A2, Th40;
thus F is open :: thesis:

proof

reconsider r = 0 as Integer ;

A15: now :: thesis:

let A be Subset of REAL; :: thesis:
A c= A ;
hence A is Subset of (R^1 | (R^1 A)) by PRE_TOPC:8; :: 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 A15;
let P be Subset of (Tunit_circle 2); :: according to TOPS_2:def 1 :: thesis:

A16: now :: thesis:

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

end;

then M is open ;
then A17: (CircleMap (R^1 r)) .: M is open by T_0TOPSP:def 2;
N is open by A16;
then A18: (CircleMap (R^1 ((1 / 2) + r))) .: N is open by T_0TOPSP:def 2;
CircleMap .: ].(1 / 2),(3 / 2).[ = (CircleMap (R^1 (1 / 2))) .: ].(1 / 2),(3 / 2).[ by RELAT_1:129;
then A19: CircleMap .: (union (IntIntervals ((1 / 2),(3 / 2)))) is open by A1, A18, TSEP_1:17;
CircleMap .: ].0,1.[ = (CircleMap (R^1 0)) .: ].0,1.[ by RELAT_1:129;
then CircleMap .: (union (IntIntervals (0,1))) is open by A14, A17, TSEP_1:17;
hence ( not P in F or P is open ) by A19, TARSKI:def 2; :: thesis:

end;

let U be Subset of (Tunit_circle 2); :: thesis:
A20: c[10] in {c[10]} by TARSKI:def 1;
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 A21: U = CircleMap .: ].0,1.[ ; :: thesis:
then reconsider U1 = U as non empty Subset of (Tunit_circle 2) by Lm18;
A22: [#] ((Tunit_circle 2) | U) = U by PRE_TOPC:def 5;
].(0 + 0),(1 + 0).[ in IntIntervals (0,1) by Lm1;
then A23: CircleMap .: ].0,1.[ = CircleMap .: (union (IntIntervals (0,1))) by Th40;

now :: thesis:

let x1, x2 be Element of R^1; :: thesis:
set k = [\x2/];
set K = ].(0 + [\x2/]),(1 + [\x2/]).[;
assume x1 in union (IntIntervals (0,1)) ; :: thesis:
then consider Z being set such that
A24: x1 in Z and
A25: Z in IntIntervals (0,1) by TARSKI:def 4;
consider n being Element of INT such that
A26: Z = ].(0 + n),(1 + n).[ by A25;
x1 < 1 + n by A24, A26, XXREAL_1:4;
then A27: x1 - 1 < (1 + n) - 1 by XREAL_1:9;
then (x1 - 1) - n < n - n by XREAL_1:9;
then ((x1 - n) - 1) + 1 < 0 + 1 by XREAL_1:8;
then A28: (2 * PI) * (x1 - n) < (2 * PI) * 1 by XREAL_1:68;
A29: CircleMap . (x2 - [\x2/]) = |[(cos ((2 * PI) * (x2 - [\x2/]))),(sin ((2 * PI) * (x2 - [\x2/])))]| by Def11;
x2 - 1 < [\x2/] by INT_1:def 6;
then (x2 - 1) - [\x2/] < [\x2/] - [\x2/] by XREAL_1:9;
then ((x2 - 1) - [\x2/]) + 1 < 0 + 1 by XREAL_1:6;
then A30: (2 * PI) * (x2 - [\x2/]) < (2 * PI) * 1 by XREAL_1:68;
assume A31: CircleMap . x1 = CircleMap . x2 ; :: thesis:
A32: n < x1 by A24, A26, XXREAL_1:4;
then A33: 0 < x1 - n by XREAL_1:50;
[\x2/] in INT by INT_1:def 2;
then A34: ].(0 + [\x2/]),(1 + [\x2/]).[ in IntIntervals (0,1) ;
A35: CircleMap . x2 = CircleMap . (x2 + (- [\x2/])) by Th31;
[\x1/] = n by A32, A27, INT_1:def 6;
then A36: not x1 in INT by A32, INT_1:26;

A37: now :: thesis:

assume [\x2/] = x2 ; :: thesis:
then CircleMap . x1 = c[10] by A31, Th32;
hence contradiction by A20, A36, Lm18, Th33, FUNCT_1:def 7, TOPMETR:17; :: thesis:

end;

A38: CircleMap . (x1 - n) = |[(cos ((2 * PI) * (x1 - n))),(sin ((2 * PI) * (x1 - n)))]| by Def11;
A39: CircleMap . x1 = CircleMap . (x1 + (- n)) by Th31;
then A40: cos ((2 * PI) * (x1 - n)) = cos ((2 * PI) * (x2 - [\x2/])) by A31, A35, A38, A29, SPPOL_2:1;
A41: sin ((2 * PI) * (x1 - n)) = sin ((2 * PI) * (x2 - [\x2/])) by A31, A39, A35, A38, A29, SPPOL_2:1;
[\x2/] <= x2 by INT_1:def 6;
then A42: [\x2/] < x2 by A37, XXREAL_0:1;
then 0 <= x2 - [\x2/] by XREAL_1:50;
then (2 * PI) * (x1 - n) = (2 * PI) * (x2 - [\x2/]) by A33, A28, A30, A40, A41, COMPLEX2:11;
then x1 - n = x2 - [\x2/] by XCMPLX_1:5;
then A43: x2 = (x1 - n) + [\x2/] ;
x1 < 1 + n by A24, A26, XXREAL_1:4;
then x1 - n < 1 by XREAL_1:19;
then x2 < 1 + [\x2/] by A43, XREAL_1:6;
then x2 in ].(0 + [\x2/]),(1 + [\x2/]).[ by A42, XXREAL_1:4;
hence x2 in union (IntIntervals (0,1)) by A34, TARSKI:def 4; :: thesis:

end;

hence union (IntIntervals (0,1)) = CircleMap " U by A21, A23, T_0TOPSP:1; :: thesis:
let d be Subset of R^1; :: thesis:
assume A44: d in IntIntervals (0,1) ; :: thesis:
then consider n being Element of INT such that
A45: d = ].(0 + n),(1 + n).[ ;
reconsider d1 = d as non empty Subset of R^1 by A45;
reconsider J = ].n,(n + p1).[ as non empty Subset of R^1 by TOPMETR:17;
A46: CircleMap | d = (CircleMap | J) | d1 by A45, RELAT_1:74;
let f be Function of (R^1 | d),((Tunit_circle 2) | U); :: thesis:
reconsider f1 = f as Function of (R^1 | d1),((Tunit_circle 2) | U1) ;
assume A47: f = CircleMap | d ; :: thesis:
then A48: f is continuous by TOPREALA:8;
d c= J by A45;
then reconsider d2 = d as Subset of (R^1 | J) by PRE_TOPC:8;
A49: (R^1 | J) | d2 = R^1 | d by A45, PRE_TOPC:7;
reconsider F = CircleMap | J as Function of (R^1 | J),(Tunit_circle 2) by Lm21;
CircleMap (R^1 n) is open ;
then A50: F is open by TOPREALA:12;
A51: CircleMap .: (union (IntIntervals (0,1))) = CircleMap .: d by A44, Th40;
A52: 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 object ; :: according to TARSKI:def 3 :: thesis:
A53: dom (CircleMap | d) = d by Lm18, RELAT_1:62, TOPMETR:17;
assume b in the carrier of ((Tunit_circle 2) | U1) ; :: thesis:
then consider a being Element of R^1 such that
A54: a in d and
A55: b = CircleMap . a by A21, A23, A22, A51, FUNCT_2:65;
(CircleMap | d) . a = CircleMap . a by A54, FUNCT_1:49;
hence b in rng f1 by A47, A54, A55, A53, FUNCT_1:def 3; :: thesis:

end;

f is one-to-one by A44, A47, Lm3, Th39;
hence f is being_homeomorphism by A47, A48, A49, A46, A52, A50, TOPREALA:10, TOPREALA:16; :: thesis:

end;

assume A56: U = CircleMap .: ].(1 / 2),(3 / 2).[ ; :: thesis:
then reconsider U1 = U as non empty Subset of (Tunit_circle 2) by Lm18;

now :: thesis:

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

per cases by XXREAL_0:1;

suppose x1 = 1 + n ; :: thesis:

then CircleMap . x2 = c[10] by A63, Th32;
then reconsider w = x2 as Element of INT by A20, Lm18, Th33, FUNCT_1:def 7, TOPMETR:17;
A66: 0 + w < (1 / 2) + w by XREAL_1:8;
w - 1 in INT by INT_1:def 2;
then A67: ].((1 / 2) + (w - 1)),((3 / 2) + (w - 1)).[ in IntIntervals ((1 / 2),(3 / 2)) ;
(- (1 / 2)) + w < 0 + w by XREAL_1:8;
then x2 in ].((1 / 2) + (w - 1)),((3 / 2) + (w - 1)).[ by A66, XXREAL_1:4;
hence x2 in union (IntIntervals ((1 / 2),(3 / 2))) by A67, TARSKI:def 4; :: thesis:

end;

suppose x1 < 1 + n ; :: thesis:

then x1 - 1 < (n + 1) - 1 by XREAL_1:9;
then (x1 - 1) - n < n - n by XREAL_1:9;
then ((x1 - n) - 1) + 1 < 0 + 1 by XREAL_1:8;
then A68: (2 * PI) * (x1 - n) < (2 * PI) * 1 by XREAL_1:68;
set K = ].((1 / 2) + [\x2/]),((3 / 2) + [\x2/]).[;
[\x2/] in INT by INT_1:def 2;
then A69: ].((1 / 2) + [\x2/]),((3 / 2) + [\x2/]).[ in IntIntervals ((1 / 2),(3 / 2)) ;
A70: x2 - x2 <= x2 - [\x2/] by A57, XREAL_1:13;
A71: 0 < x1 - n by A62, XREAL_1:50;
A72: CircleMap . (x2 - [\x2/]) = |[(cos ((2 * PI) * (x2 - [\x2/]))),(sin ((2 * PI) * (x2 - [\x2/])))]| by Def11;
x2 - 1 < [\x2/] by INT_1:def 6;
then (x2 - 1) - [\x2/] < [\x2/] - [\x2/] by XREAL_1:9;
then ((x2 - 1) - [\x2/]) + 1 < 0 + 1 by XREAL_1:6;
then A73: (2 * PI) * (x2 - [\x2/]) < (2 * PI) * 1 by XREAL_1:68;
A74: CircleMap . x2 = CircleMap . (x2 + (- [\x2/])) by Th31;
((1 / 2) + n) - n < x1 - n by A61, XREAL_1:9;
then A75: (1 / 2) + [\x2/] < (x1 - n) + [\x2/] by XREAL_1:8;
A76: CircleMap . (x1 - n) = |[(cos ((2 * PI) * (x1 - n))),(sin ((2 * PI) * (x1 - n)))]| by Def11;
A77: CircleMap . x1 = CircleMap . (x1 + (- n)) by Th31;
then A78: sin ((2 * PI) * (x1 - n)) = sin ((2 * PI) * (x2 - [\x2/])) by A63, A74, A76, A72, SPPOL_2:1;
cos ((2 * PI) * (x1 - n)) = cos ((2 * PI) * (x2 - [\x2/])) by A63, A77, A74, A76, A72, SPPOL_2:1;
then (2 * PI) * (x1 - n) = (2 * PI) * (x2 - [\x2/]) by A78, A71, A68, A70, A73, COMPLEX2:11;
then A79: x1 - n = x2 - [\x2/] by XCMPLX_1:5;
then x2 = (x1 - n) + [\x2/] ;
then x2 < (3 / 2) + [\x2/] by A65, XREAL_1:6;
then x2 in ].((1 / 2) + [\x2/]),((3 / 2) + [\x2/]).[ by A79, A75, XXREAL_1:4;
hence x2 in union (IntIntervals ((1 / 2),(3 / 2))) by A69, TARSKI:def 4; :: thesis:

end;

suppose x1 > 1 + n ; :: thesis:

then A80: (n + 1) - 1 < x1 - 1 by XREAL_1:9;
then A81: n - n < (x1 - 1) - n by XREAL_1:9;
set K = ].((1 / 2) + ([\x2/] - 1)),((3 / 2) + ([\x2/] - 1)).[;
A82: - (1 / 2) < 0 ;
n - n < (x1 - 1) - n by A80, XREAL_1:9;
then A83: (- (1 / 2)) + [\x2/] < ((x1 - 1) - n) + [\x2/] by A82, XREAL_1:8;
[\x2/] - 1 in INT by INT_1:def 2;
then A84: ].((1 / 2) + ([\x2/] - 1)),((3 / 2) + ([\x2/] - 1)).[ in IntIntervals ((1 / 2),(3 / 2)) ;
A85: (x1 - n) - 1 < (3 / 2) - 1 by A65, XREAL_1:9;
A86: x2 - x2 <= x2 - [\x2/] by A57, XREAL_1:13;
A87: CircleMap . (x2 - [\x2/]) = |[(cos ((2 * PI) * (x2 - [\x2/]))),(sin ((2 * PI) * (x2 - [\x2/])))]| by Def11;
x1 - 1 < ((3 / 2) + n) - 1 by A64, XREAL_1:9;
then (x1 - 1) - n < ((1 / 2) + n) - n by XREAL_1:9;
then (x1 - 1) - n < 1 by XXREAL_0:2;
then A88: (2 * PI) * ((x1 - 1) - n) < (2 * PI) * 1 by XREAL_1:68;
A89: CircleMap . x2 = CircleMap . (x2 + (- [\x2/])) by Th31;
x2 - 1 < [\x2/] by INT_1:def 6;
then (x2 - 1) - [\x2/] < [\x2/] - [\x2/] by XREAL_1:9;
then ((x2 - 1) - [\x2/]) + 1 < 0 + 1 by XREAL_1:6;
then A90: (2 * PI) * (x2 - [\x2/]) < (2 * PI) * 1 by XREAL_1:68;
A91: CircleMap . ((x1 - 1) - n) = |[(cos ((2 * PI) * ((x1 - 1) - n))),(sin ((2 * PI) * ((x1 - 1) - n)))]| by Def11;
A92: CircleMap . x1 = CircleMap . (x1 + ((- 1) - n)) by Th31;
then A93: sin ((2 * PI) * ((x1 - 1) - n)) = sin ((2 * PI) * (x2 - [\x2/])) by A63, A89, A91, A87, SPPOL_2:1;
cos ((2 * PI) * ((x1 - 1) - n)) = cos ((2 * PI) * (x2 - [\x2/])) by A63, A92, A89, A91, A87, SPPOL_2:1;
then (2 * PI) * ((x1 - 1) - n) = (2 * PI) * (x2 - [\x2/]) by A93, A81, A88, A86, A90, COMPLEX2:11;
then A94: (x1 - 1) - n = x2 - [\x2/] by XCMPLX_1:5;
then x2 = ((x1 - 1) - n) + [\x2/] ;
then x2 < (1 / 2) + [\x2/] by A85, XREAL_1:6;
then x2 in ].((1 / 2) + ([\x2/] - 1)),((3 / 2) + ([\x2/] - 1)).[ by A94, A83, XXREAL_1:4;
hence x2 in union (IntIntervals ((1 / 2),(3 / 2))) by A84, TARSKI:def 4; :: thesis:

end;

hence union (IntIntervals ((1 / 2),(3 / 2))) = CircleMap " U by A1, A56, T_0TOPSP:1; :: thesis:
let d be Subset of R^1; :: thesis:
assume A95: d in IntIntervals ((1 / 2),(3 / 2)) ; :: thesis:
then consider n being Element of INT such that
A96: d = ].((1 / 2) + n),((3 / 2) + n).[ ;
A97: 1 + n < (3 / 2) + n by XREAL_1:6;
(1 / 2) + n < 1 + n by XREAL_1:6;
then reconsider d1 = d as non empty Subset of R^1 by A96, A97, XXREAL_1:4;
A98: [#] ((Tunit_circle 2) | U) = U by PRE_TOPC:def 5;
let f be Function of (R^1 | d),((Tunit_circle 2) | U); :: thesis:
reconsider f1 = f as Function of (R^1 | d1),((Tunit_circle 2) | U1) ;
assume A99: f = CircleMap | d ; :: thesis:
then A100: f is continuous by TOPREALA:8;
reconsider J = ].((1 / 2) + n),(((1 / 2) + n) + p1).[ as non empty Subset of R^1 by TOPMETR:17;
A101: CircleMap | d = (CircleMap | J) | d1 by A96, RELAT_1:74;
d c= J by A96;
then reconsider d2 = d as Subset of (R^1 | J) by PRE_TOPC:8;
A102: (R^1 | J) | d2 = R^1 | d by A96, PRE_TOPC:7;
A103: CircleMap .: (union (IntIntervals ((1 / 2),(3 / 2)))) = CircleMap .: d by A95, Th40;
A104: 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 object ; :: according to TARSKI:def 3 :: thesis:
A105: dom (CircleMap | d) = d by Lm18, RELAT_1:62, TOPMETR:17;
assume b in the carrier of ((Tunit_circle 2) | U1) ; :: thesis:
then consider a being Element of R^1 such that
A106: a in d and
A107: b = CircleMap . a by A1, A56, A98, A103, FUNCT_2:65;
(CircleMap | d) . a = CircleMap . a by A106, FUNCT_1:49;
hence b in rng f1 by A99, A106, A107, A105, FUNCT_1:def 3; :: thesis:

end;

reconsider F = CircleMap | J as Function of (R^1 | J),(Tunit_circle 2) by Lm21;
CircleMap (R^1 ((1 / 2) + n)) is open ;
then A108: F is open by TOPREALA:12;
f is one-to-one by A95, A99, Lm4, Th39;
hence f is being_homeomorphism by A99, A100, A102, A101, A104, A108, TOPREALA:10, TOPREALA:16; :: thesis: