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: ( F = {(CircleMap .: ].0,1.[),(CircleMap .: ].(1 / 2),(3 / 2).[)} & F is Cover of (Tunit_circle 2) & F is open & ( for U being Subset of (Tunit_circle 2) 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),((Tunit_circle 2) | 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),((Tunit_circle 2) | 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: ].(0 + 0),(1 + 0).[ in IntIntervals (0,1) by Lm1;

hence F = {(CircleMap .: ].0,1.[),(CircleMap .: ].(1 / 2),(3 / 2).[)} by A1, Th40; :: thesis: ( F is Cover of (Tunit_circle 2) & F is open & ( for U being Subset of (Tunit_circle 2) 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),((Tunit_circle 2) | 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),((Tunit_circle 2) | U) st f = CircleMap | d holds

f is being_homeomorphism ) ) ) ) ) )

thus F is Cover of (Tunit_circle 2) :: thesis: ( F is open & ( for U being Subset of (Tunit_circle 2) 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),((Tunit_circle 2) | 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),((Tunit_circle 2) | U) st f = CircleMap | d holds

f is being_homeomorphism ) ) ) ) ) )

thus F is open :: thesis: for U being Subset of (Tunit_circle 2) 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),((Tunit_circle 2) | 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),((Tunit_circle 2) | U) st f = CircleMap | d holds

f is being_homeomorphism ) ) ) )

for f being Function of (R^1 | d),((Tunit_circle 2) | 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),((Tunit_circle 2) | U) st f = CircleMap | d holds

f is being_homeomorphism ) ) ) )

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: ( 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),((Tunit_circle 2) | U) st f = CircleMap | d holds

f is being_homeomorphism ) ) )

for f being Function of (R^1 | d),((Tunit_circle 2) | U) st f = CircleMap | d holds

f is being_homeomorphism ) )

then reconsider U1 = U as non empty Subset of (Tunit_circle 2) by Lm18;

for f being Function of (R^1 | d),((Tunit_circle 2) | 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),((Tunit_circle 2) | 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),((Tunit_circle 2) | 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 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: ( f = CircleMap | d implies f is being_homeomorphism )

reconsider f1 = f as Function of (R^1 | d1),((Tunit_circle 2) | U1) ;

assume A99: f = CircleMap | d ; :: thesis: f is being_homeomorphism

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

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: verum

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: ( F = {(CircleMap .: ].0,1.[),(CircleMap .: ].(1 / 2),(3 / 2).[)} & F is Cover of (Tunit_circle 2) & F is open & ( for U being Subset of (Tunit_circle 2) 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),((Tunit_circle 2) | 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),((Tunit_circle 2) | 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: ].(0 + 0),(1 + 0).[ in IntIntervals (0,1) by Lm1;

hence F = {(CircleMap .: ].0,1.[),(CircleMap .: ].(1 / 2),(3 / 2).[)} by A1, Th40; :: thesis: ( F is Cover of (Tunit_circle 2) & F is open & ( for U being Subset of (Tunit_circle 2) 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),((Tunit_circle 2) | 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),((Tunit_circle 2) | U) st f = CircleMap | d holds

f is being_homeomorphism ) ) ) ) ) )

thus F is Cover of (Tunit_circle 2) :: thesis: ( F is open & ( for U being Subset of (Tunit_circle 2) 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),((Tunit_circle 2) | 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),((Tunit_circle 2) | U) st f = CircleMap | d holds

f is being_homeomorphism ) ) ) ) ) )

proof

A14:
CircleMap .: (union (IntIntervals (0,1))) = CircleMap .: ].0,1.[
by A2, Th40;
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: ( not a in the carrier of (Tunit_circle 2) 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 (Tunit_circle 2) ;

assume a in the carrier of (Tunit_circle 2) ; :: thesis: a in union F

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;

end;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: ( not a in the carrier of (Tunit_circle 2) 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 (Tunit_circle 2) ;

assume a in the carrier of (Tunit_circle 2) ; :: thesis: a in union F

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
( x = 0 or ( 0 < x & x < 1 ) or ( x >= 1 & x < 1 ) )
by A5, A7, XXREAL_1:3;

end;

suppose A9:
x = 0
; :: thesis: a in union F

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: verum

end;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: verum

suppose A11:
( 0 < x & x < 1 )
; :: thesis: a in union F

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: verum

end;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: verum

thus F is open :: thesis: for U being Subset of (Tunit_circle 2) 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),((Tunit_circle 2) | 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),((Tunit_circle 2) | U) st f = CircleMap | d holds

f is being_homeomorphism ) ) ) )

proof

let U be Subset of (Tunit_circle 2); :: 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
reconsider r = 0 as Integer ;

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: ( not P in F or P 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: verum

end;A15: now :: thesis: for A being Subset of REAL holds A is Subset of (R^1 | (R^1 A))

then reconsider M = ].0,1.[ as Subset of (R^1 | (R^1 ].r,(r + 1).[)) ;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;A c= A ;

hence A is Subset of (R^1 | (R^1 A)) by PRE_TOPC:8; :: thesis: verum

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: ( 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))

then
M is open
;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;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

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: verum

for f being Function of (R^1 | d),((Tunit_circle 2) | 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),((Tunit_circle 2) | U) st f = CircleMap | d holds

f is being_homeomorphism ) ) ) )

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: ( 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),((Tunit_circle 2) | U) st f = CircleMap | d holds

f is being_homeomorphism ) ) )

proof

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
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),((Tunit_circle 2) | U) st f = CircleMap | d holds

f is being_homeomorphism ) )

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;

for f being Function of (R^1 | d),((Tunit_circle 2) | 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),((Tunit_circle 2) | 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),((Tunit_circle 2) | 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 = (CircleMap | J) | d1 by A45, RELAT_1:74;

let f be Function of (R^1 | d),((Tunit_circle 2) | U); :: thesis: ( f = CircleMap | d implies f is being_homeomorphism )

reconsider f1 = f as Function of (R^1 | d1),((Tunit_circle 2) | U1) ;

assume A47: f = CircleMap | d ; :: thesis: f is being_homeomorphism

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

hence f is being_homeomorphism by A47, A48, A49, A46, A52, A50, TOPREALA:10, TOPREALA:16; :: thesis: verum

end;for f being Function of (R^1 | d),((Tunit_circle 2) | U) st f = CircleMap | d holds

f is being_homeomorphism ) )

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: 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))

hence
union (IntIntervals (0,1)) = CircleMap " U
by A21, A23, T_0TOPSP:1; :: thesis: for d being Subset of R^1 st d in IntIntervals (0,1) 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 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: x2 in union (IntIntervals (0,1))

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;

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: verum

end;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 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: x2 in union (IntIntervals (0,1))

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: not [\x2/] = x2

A38:
CircleMap . (x1 - n) = |[(cos ((2 * PI) * (x1 - n))),(sin ((2 * PI) * (x1 - n)))]|
by Def11;assume
[\x2/] = x2
; :: thesis: contradiction

then CircleMap . x1 = c[10] by A31, Th32;

hence contradiction by A20, A36, Lm18, Th33, FUNCT_1:def 7, TOPMETR:17; :: thesis: verum

end;then CircleMap . x1 = c[10] by A31, Th32;

hence contradiction by A20, A36, Lm18, Th33, FUNCT_1:def 7, TOPMETR:17; :: thesis: verum

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: verum

for f being Function of (R^1 | d),((Tunit_circle 2) | 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),((Tunit_circle 2) | 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),((Tunit_circle 2) | 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 = (CircleMap | J) | d1 by A45, RELAT_1:74;

let f be Function of (R^1 | d),((Tunit_circle 2) | U); :: thesis: ( f = CircleMap | d implies f is being_homeomorphism )

reconsider f1 = f as Function of (R^1 | d1),((Tunit_circle 2) | U1) ;

assume A47: f = CircleMap | d ; :: thesis: f is being_homeomorphism

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

f is one-to-one
by A44, A47, Lm3, Th39;
thus
rng f1 c= the carrier of ((Tunit_circle 2) | U1)
; :: according to XBOOLE_0:def 10,FUNCT_2:def 3 :: thesis: the carrier of ((Tunit_circle 2) | U1) c= rng f1

let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in the carrier of ((Tunit_circle 2) | U1) or b in rng f1 )

A53: dom (CircleMap | d) = d by Lm18, RELAT_1:62, TOPMETR:17;

assume b in the carrier of ((Tunit_circle 2) | 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 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: verum

end;let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in the carrier of ((Tunit_circle 2) | U1) or b in rng f1 )

A53: dom (CircleMap | d) = d by Lm18, RELAT_1:62, TOPMETR:17;

assume b in the carrier of ((Tunit_circle 2) | 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 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: verum

hence f is being_homeomorphism by A47, A48, A49, A46, A52, A50, TOPREALA:10, TOPREALA:16; :: thesis: verum

for f being Function of (R^1 | d),((Tunit_circle 2) | U) st f = CircleMap | d holds

f is being_homeomorphism ) )

then reconsider U1 = U as non empty Subset of (Tunit_circle 2) 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)))

hence
union (IntIntervals ((1 / 2),(3 / 2))) = CircleMap " U
by A1, A56, T_0TOPSP:1; :: thesis: for d being Subset of R^1 st d in IntIntervals ((1 / 2),(3 / 2)) 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 b_{2} 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 b_{2} 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 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: b_{2} in union (IntIntervals ((1 / 2),(3 / 2)))

A64: x1 < (3 / 2) + n by A58, A60, XXREAL_1:4;

then A65: x1 - n < 3 / 2 by XREAL_1:19;

end;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 b

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: b

A64: x1 < (3 / 2) + n by A58, A60, XXREAL_1:4;

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;

end;

suppose
x1 = 1 + n
; :: thesis: b_{2} in union (IntIntervals ((1 / 2),(3 / 2)))

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: verum

end;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: verum

suppose
x1 < 1 + n
; :: thesis: b_{2} 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 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: verum

end;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: verum

suppose
x1 > 1 + n
; :: thesis: b_{2} 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 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: verum

end;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: verum

for f being Function of (R^1 | d),((Tunit_circle 2) | 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),((Tunit_circle 2) | 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),((Tunit_circle 2) | 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 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: ( f = CircleMap | d implies f is being_homeomorphism )

reconsider f1 = f as Function of (R^1 | d1),((Tunit_circle 2) | U1) ;

assume A99: f = CircleMap | d ; :: thesis: f is being_homeomorphism

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

reconsider F = CircleMap | J as Function of (R^1 | J),(Tunit_circle 2) by Lm21;
thus
rng f1 c= the carrier of ((Tunit_circle 2) | U1)
; :: according to XBOOLE_0:def 10,FUNCT_2:def 3 :: thesis: the carrier of ((Tunit_circle 2) | U1) c= rng f1

let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in the carrier of ((Tunit_circle 2) | U1) or b in rng f1 )

A105: dom (CircleMap | d) = d by Lm18, RELAT_1:62, TOPMETR:17;

assume b in the carrier of ((Tunit_circle 2) | 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 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: verum

end;let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in the carrier of ((Tunit_circle 2) | U1) or b in rng f1 )

A105: dom (CircleMap | d) = d by Lm18, RELAT_1:62, TOPMETR:17;

assume b in the carrier of ((Tunit_circle 2) | 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 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: verum

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: verum