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 () ;
take F ; :: thesis: ( F = {(),(CircleMap .: ].(1 / 2),(3 / 2).[)} & F is Cover of () & F is open & ( for U being Subset of () holds
( ( 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),(() | U) st f = CircleMap | d holds
f is being_homeomorphism ) ) ) & ( U = CircleMap .: ].(1 / 2),(3 / 2).[ implies ( union (IntIntervals ((1 / 2),(3 / 2))) = CircleMap " U & ( for d being Subset of R^1 st d in IntIntervals ((1 / 2),(3 / 2)) holds
for f being Function of (R^1 | d),(() | U) st f = CircleMap | d holds
f is being_homeomorphism ) ) ) ) ) )

].((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: ].(),(1 + 0).[ in IntIntervals (0,1) by Lm1;
hence F = {(),(CircleMap .: ].(1 / 2),(3 / 2).[)} by ; :: thesis: ( F is Cover of () & F is open & ( for U being Subset of () holds
( ( 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),(() | U) st f = CircleMap | d holds
f is being_homeomorphism ) ) ) & ( U = CircleMap .: ].(1 / 2),(3 / 2).[ implies ( union (IntIntervals ((1 / 2),(3 / 2))) = CircleMap " U & ( for d being Subset of R^1 st d in IntIntervals ((1 / 2),(3 / 2)) holds
for f being Function of (R^1 | d),(() | U) st f = CircleMap | d holds
f is being_homeomorphism ) ) ) ) ) )

thus F is Cover of () :: thesis: ( F is open & ( for U being Subset of () holds
( ( 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),(() | U) st f = CircleMap | d holds
f is being_homeomorphism ) ) ) & ( U = CircleMap .: ].(1 / 2),(3 / 2).[ implies ( union (IntIntervals ((1 / 2),(3 / 2))) = CircleMap " U & ( for d being Subset of R^1 st d in IntIntervals ((1 / 2),(3 / 2)) holds
for f being Function of (R^1 | d),(() | U) st f = CircleMap | d holds
f is being_homeomorphism ) ) ) ) ) )
proof
reconsider A = [.0,(0 + 1).[ as Subset of R^1 by TOPMETR:17;
reconsider f = CircleMap | A as Function of (R^1 | A),() by Lm21;
let a be object ; :: according to TARSKI:def 3,SETFAM_1:def 11 :: thesis: ( not a in the carrier of () or a in union F )
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 () ;
assume a in the carrier of () ; :: thesis: a in union F
then consider x being object such that
A5: x in dom f and
A6: f . x = a by ;
A7: dom f = A by ;
then reconsider x = x as Element of REAL by A5;
A8: CircleMap . x = f . x by ;
per cases ( x = 0 or ( 0 < x & x < 1 ) or ( x >= 1 & x < 1 ) ) by ;
end;
end;
A14: CircleMap .: (union (IntIntervals (0,1))) = CircleMap .: ].0,1.[ by ;
thus F is open :: thesis: for U being Subset of () holds
( ( 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),(() | U) st f = CircleMap | d holds
f is being_homeomorphism ) ) ) & ( U = CircleMap .: ].(1 / 2),(3 / 2).[ implies ( union (IntIntervals ((1 / 2),(3 / 2))) = CircleMap " U & ( for d being Subset of R^1 st d in IntIntervals ((1 / 2),(3 / 2)) holds
for f being Function of (R^1 | d),(() | U) st f = CircleMap | d holds
f is being_homeomorphism ) ) ) )
proof
reconsider r = 0 as Integer ;
A15: now :: thesis: for A being Subset of REAL holds A is Subset of (R^1 | (R^1 A))
let A be Subset of REAL; :: thesis: A is Subset of (R^1 | (R^1 A))
A c= A ;
hence A is Subset of (R^1 | (R^1 A)) by PRE_TOPC:8; :: thesis: verum
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 (); :: according to TOPS_2:def 1 :: thesis: ( not P in F or P is open )
A16: now :: thesis: for A being open Subset of REAL holds A is open Subset of (R^1 | (R^1 A))
let A be open Subset of REAL; :: thesis: A is open Subset of (R^1 | (R^1 A))
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: verum
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 ;
CircleMap .: ].0,1.[ = () .: ].0,1.[ by RELAT_1:129;
then CircleMap .: (union (IntIntervals (0,1))) is open by ;
hence ( not P in F or P is open ) by ; :: thesis: verum
end;
let U be Subset of (); :: thesis: ( ( 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),(() | U) st f = CircleMap | d holds
f is being_homeomorphism ) ) ) & ( U = CircleMap .: ].(1 / 2),(3 / 2).[ implies ( union (IntIntervals ((1 / 2),(3 / 2))) = CircleMap " U & ( for d being Subset of R^1 st d in IntIntervals ((1 / 2),(3 / 2)) holds
for f being Function of (R^1 | d),(() | U) st f = CircleMap | d holds
f is being_homeomorphism ) ) ) )

A20: c[10] in 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),(() | U) st f = CircleMap | d holds
f is being_homeomorphism ) ) ) :: thesis: ( U = CircleMap .: ].(1 / 2),(3 / 2).[ implies ( union (IntIntervals ((1 / 2),(3 / 2))) = CircleMap " U & ( for d being Subset of R^1 st d in IntIntervals ((1 / 2),(3 / 2)) holds
for f being Function of (R^1 | d),(() | U) st f = CircleMap | d holds
f is being_homeomorphism ) ) )
proof
assume A21: U = CircleMap .: ].0,1.[ ; :: thesis: ( 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),(() | U) st f = CircleMap | d holds
f is being_homeomorphism ) )

then reconsider U1 = U as non empty Subset of () by Lm18;
A22: [#] (() | U) = U by PRE_TOPC:def 5;
].(),(1 + 0).[ in IntIntervals (0,1) by Lm1;
then A23: CircleMap .: ].0,1.[ = CircleMap .: (union (IntIntervals (0,1))) by Th40;
now :: thesis: for x1, x2 being Element of R^1 st x1 in union (IntIntervals (0,1)) & CircleMap . x1 = CircleMap . x2 holds
x2 in union (IntIntervals (0,1))
let x1, x2 be Element of R^1; :: thesis: ( x1 in union (IntIntervals (0,1)) & CircleMap . x1 = CircleMap . x2 implies x2 in union (IntIntervals (0,1)) )
set k = [\x2/];
set K = ].(0 + [\x2/]),(1 + [\x2/]).[;
assume x1 in union (IntIntervals (0,1)) ; :: thesis: ( CircleMap . x1 = CircleMap . x2 implies x2 in union (IntIntervals (0,1)) )
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 ;
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: x2 in union (IntIntervals (0,1))
A32: n < x1 by ;
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 ;
then A36: not x1 in INT by ;
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 ;
A41: sin ((2 * PI) * (x1 - n)) = sin ((2 * PI) * (x2 - [\x2/])) by ;
[\x2/] <= x2 by INT_1:def 6;
then A42: [\x2/] < x2 by ;
then 0 <= x2 - [\x2/] by XREAL_1:50;
then (2 * PI) * (x1 - n) = (2 * PI) * (x2 - [\x2/]) by ;
then x1 - n = x2 - [\x2/] by XCMPLX_1:5;
then A43: x2 = (x1 - n) + [\x2/] ;
x1 < 1 + n by ;
then x1 - n < 1 by XREAL_1:19;
then x2 < 1 + [\x2/] by ;
then x2 in ].(0 + [\x2/]),(1 + [\x2/]).[ by ;
hence x2 in union (IntIntervals (0,1)) by ; :: thesis: verum
end;
hence union (IntIntervals (0,1)) = CircleMap " U by ; :: thesis: for d being Subset of R^1 st d in IntIntervals (0,1) holds
for f being Function of (R^1 | d),(() | U) st f = CircleMap | d holds
f is being_homeomorphism

let d be Subset of R^1; :: thesis: ( d in IntIntervals (0,1) implies for f being Function of (R^1 | d),(() | U) st f = CircleMap | d holds
f is being_homeomorphism )

assume A44: d in IntIntervals (0,1) ; :: thesis: for f being Function of (R^1 | d),(() | U) st f = CircleMap | d holds
f is being_homeomorphism

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 = () | d1 by ;
let f be Function of (R^1 | d),(() | U); :: thesis: ( f = CircleMap | d implies f is being_homeomorphism )
reconsider f1 = f as Function of (R^1 | d1),(() | 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 ;
reconsider F = CircleMap | J as Function of (R^1 | J),() 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 ;
A52: f1 is onto
proof
thus rng f1 c= the carrier of (() | U1) ; :: according to XBOOLE_0:def 10,FUNCT_2:def 3 :: thesis: the carrier of (() | U1) c= rng f1
let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in the carrier of (() | U1) or b in rng f1 )
A53: dom () = d by ;
assume b in the carrier of (() | U1) ; :: thesis: b in rng f1
then consider a being Element of R^1 such that
A54: a in d and
A55: b = CircleMap . a by ;
(CircleMap | d) . a = CircleMap . a by ;
hence b in rng f1 by ; :: thesis: verum
end;
f is one-to-one by ;
hence f is being_homeomorphism by ; :: thesis: verum
end;
assume A56: U = CircleMap .: ].(1 / 2),(3 / 2).[ ; :: thesis: ( union (IntIntervals ((1 / 2),(3 / 2))) = CircleMap " U & ( for d being Subset of R^1 st d in IntIntervals ((1 / 2),(3 / 2)) holds
for f being Function of (R^1 | d),(() | U) st f = CircleMap | d holds
f is being_homeomorphism ) )

then reconsider U1 = U as non empty Subset of () by Lm18;
now :: thesis: for x1, x2 being Element of R^1 st x1 in union (IntIntervals ((1 / 2),(3 / 2))) & CircleMap . x1 = CircleMap . x2 holds
x2 in union (IntIntervals ((1 / 2),(3 / 2)))
let x1, x2 be Element of R^1; :: thesis: ( x1 in union (IntIntervals ((1 / 2),(3 / 2))) & CircleMap . x1 = CircleMap . x2 implies b2 in union (IntIntervals ((1 / 2),(3 / 2))) )
set k = [\x2/];
A57: [\x2/] <= x2 by INT_1:def 6;
assume x1 in union (IntIntervals ((1 / 2),(3 / 2))) ; :: thesis: ( CircleMap . x1 = CircleMap . x2 implies b2 in union (IntIntervals ((1 / 2),(3 / 2))) )
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 ;
0 + n < (1 / 2) + n by XREAL_1:8;
then A62: n < x1 by ;
assume A63: CircleMap . x1 = CircleMap . x2 ; :: thesis: b2 in union (IntIntervals ((1 / 2),(3 / 2)))
A64: x1 < (3 / 2) + n by ;
then A65: x1 - n < 3 / 2 by XREAL_1:19;
per cases ( x1 = 1 + n or x1 < 1 + n or x1 > 1 + n ) by XXREAL_0:1;
suppose x1 = 1 + n ; :: thesis: b2 in union (IntIntervals ((1 / 2),(3 / 2)))
then CircleMap . x2 = c[10] by ;
then reconsider w = x2 as Element of INT by ;
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 ;
hence x2 in union (IntIntervals ((1 / 2),(3 / 2))) by ; :: thesis: verum
end;
suppose x1 < 1 + n ; :: thesis: b2 in union (IntIntervals ((1 / 2),(3 / 2)))
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 ;
A71: 0 < x1 - n by ;
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 ;
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 ;
cos ((2 * PI) * (x1 - n)) = cos ((2 * PI) * (x2 - [\x2/])) by ;
then (2 * PI) * (x1 - n) = (2 * PI) * (x2 - [\x2/]) by ;
then A79: x1 - n = x2 - [\x2/] by XCMPLX_1:5;
then x2 = (x1 - n) + [\x2/] ;
then x2 < (3 / 2) + [\x2/] by ;
then x2 in ].((1 / 2) + [\x2/]),((3 / 2) + [\x2/]).[ by ;
hence x2 in union (IntIntervals ((1 / 2),(3 / 2))) by ; :: thesis: verum
end;
suppose x1 > 1 + n ; :: thesis: b2 in union (IntIntervals ((1 / 2),(3 / 2)))
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 ;
then A83: (- (1 / 2)) + [\x2/] < ((x1 - 1) - n) + [\x2/] by ;
[\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 ;
A86: x2 - x2 <= x2 - [\x2/] by ;
A87: CircleMap . (x2 - [\x2/]) = |[(cos ((2 * PI) * (x2 - [\x2/]))),(sin ((2 * PI) * (x2 - [\x2/])))]| by Def11;
x1 - 1 < ((3 / 2) + n) - 1 by ;
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 ;
cos ((2 * PI) * ((x1 - 1) - n)) = cos ((2 * PI) * (x2 - [\x2/])) by ;
then (2 * PI) * ((x1 - 1) - n) = (2 * PI) * (x2 - [\x2/]) by ;
then A94: (x1 - 1) - n = x2 - [\x2/] by XCMPLX_1:5;
then x2 = ((x1 - 1) - n) + [\x2/] ;
then x2 < (1 / 2) + [\x2/] by ;
then x2 in ].((1 / 2) + ([\x2/] - 1)),((3 / 2) + ([\x2/] - 1)).[ by ;
hence x2 in union (IntIntervals ((1 / 2),(3 / 2))) by ; :: thesis: verum
end;
end;
end;
hence union (IntIntervals ((1 / 2),(3 / 2))) = CircleMap " U by ; :: thesis: for d being Subset of R^1 st d in IntIntervals ((1 / 2),(3 / 2)) holds
for f being Function of (R^1 | d),(() | U) st f = CircleMap | d holds
f is being_homeomorphism

let d be Subset of R^1; :: thesis: ( d in IntIntervals ((1 / 2),(3 / 2)) implies for f being Function of (R^1 | d),(() | U) st f = CircleMap | d holds
f is being_homeomorphism )

assume A95: d in IntIntervals ((1 / 2),(3 / 2)) ; :: thesis: for f being Function of (R^1 | d),(() | U) st f = CircleMap | d holds
f is being_homeomorphism

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 ;
A98: [#] (() | U) = U by PRE_TOPC:def 5;
let f be Function of (R^1 | d),(() | U); :: thesis: ( f = CircleMap | d implies f is being_homeomorphism )
reconsider f1 = f as Function of (R^1 | d1),(() | 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 = () | d1 by ;
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 ;
A103: CircleMap .: (union (IntIntervals ((1 / 2),(3 / 2)))) = CircleMap .: d by ;
A104: f1 is onto
proof
thus rng f1 c= the carrier of (() | U1) ; :: according to XBOOLE_0:def 10,FUNCT_2:def 3 :: thesis: the carrier of (() | U1) c= rng f1
let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in the carrier of (() | U1) or b in rng f1 )
A105: dom () = d by ;
assume b in the carrier of (() | U1) ; :: thesis: b in rng f1
then consider a being Element of R^1 such that
A106: a in d and
A107: b = CircleMap . a by ;
(CircleMap | d) . a = CircleMap . a by ;
hence b in rng f1 by ; :: thesis: verum
end;
reconsider F = CircleMap | J as Function of (R^1 | J),() by Lm21;
CircleMap (R^1 ((1 / 2) + n)) is open ;
then A108: F is open by TOPREALA:12;
f is one-to-one by ;
hence f is being_homeomorphism by ; :: thesis: verum