:: by Artur Korni{\l}owicz and Yasunari Shidama

::

:: Received October 18, 2004

:: Copyright (c) 2004 Association of Mizar Users

begin

set P2 = 2 * PI;

set o = |[0,0]|;

set R = the carrier of R^1;

Lm1: 0 in INT

by INT_1:def 1;

reconsider p0 = - 1 as real negative number ;

reconsider p1 = 1 as real positive number ;

set CIT = Closed-Interval-TSpace ((- 1),1);

set cCIT = the carrier of (Closed-Interval-TSpace ((- 1),1));

Lm2: the carrier of (Closed-Interval-TSpace ((- 1),1)) = [.(- 1),1.]

by TOPMETR:25;

Lm3: 1 - 0 <= 1

;

Lm4: (3 / 2) - (1 / 2) <= 1

;

registration

cluster K107(0,1) -> non empty ;

coherence

not ].0,1.[ is empty ;

cluster K104((- 1),1) -> non empty ;

coherence

not [.(- 1),1.] is empty ;

cluster K107((1 / 2),(3 / 2)) -> non empty ;

coherence

not ].(1 / 2),(3 / 2).[ is empty

end;
coherence

not ].0,1.[ is empty ;

cluster K104((- 1),1) -> non empty ;

coherence

not [.(- 1),1.] is empty ;

cluster K107((1 / 2),(3 / 2)) -> non empty ;

coherence

not ].(1 / 2),(3 / 2).[ is empty

proof end;

Lm5: PI / 2 < PI / 1

by XREAL_1:78;

Lm6: 1 * PI < (3 / 2) * PI

by XREAL_1:70;

Lm7: (3 / 2) * PI < 2 * PI

by XREAL_1:70;

Lm8: for X being non empty TopSpace

for Y being non empty SubSpace of X

for Z being non empty SubSpace of Y

for p being Point of Z holds p is Point of X

proof end;

Lm9: for X being TopSpace

for Y being SubSpace of X

for Z being SubSpace of Y

for A being Subset of Z holds A is Subset of X

proof end;

registration

cluster sin -> continuous ;

coherence

sin is continuous ;

cluster cos -> continuous ;

coherence

cos is continuous ;

cluster arcsin -> continuous ;

coherence

arcsin is continuous by RELAT_1:98, SIN_COS6:64, SIN_COS6:85;

cluster arccos -> continuous ;

coherence

arccos is continuous by RELAT_1:98, SIN_COS6:88, SIN_COS6:109;

end;
coherence

sin is continuous ;

cluster cos -> continuous ;

coherence

cos is continuous ;

cluster arcsin -> continuous ;

coherence

arcsin is continuous by RELAT_1:98, SIN_COS6:64, SIN_COS6:85;

cluster arccos -> continuous ;

coherence

arccos is continuous by RELAT_1:98, SIN_COS6:88, SIN_COS6:109;

theorem Th1: :: TOPREALB:1

proof end;

theorem Th2: :: TOPREALB:2

proof end;

registration

let a be non zero real number ;

let b be real number ;

cluster AffineMap (a,b) -> one-to-one onto ;

coherence

( AffineMap (a,b) is onto & AffineMap (a,b) is one-to-one )

end;
let b be real number ;

cluster AffineMap (a,b) -> one-to-one onto ;

coherence

( AffineMap (a,b) is onto & AffineMap (a,b) is one-to-one )

proof end;

definition

let a, b be real number ;

func IntIntervals (a,b) -> set equals :: TOPREALB:def 1

{ ].(a + n),(b + n).[ where n is Element of INT : verum } ;

coherence

{ ].(a + n),(b + n).[ where n is Element of INT : verum } is set ;

end;
func IntIntervals (a,b) -> set equals :: TOPREALB:def 1

{ ].(a + n),(b + n).[ where n is Element of INT : verum } ;

coherence

{ ].(a + n),(b + n).[ where n is Element of INT : verum } is set ;

:: deftheorem defines IntIntervals TOPREALB:def 1 :

for a, b being real number holds IntIntervals (a,b) = { ].(a + n),(b + n).[ where n is Element of INT : verum } ;

theorem :: TOPREALB:3

for a, b being real number

for x being set holds

( x in IntIntervals (a,b) iff ex n being Element of INT st x = ].(a + n),(b + n).[ ) ;

for x being set holds

( x in IntIntervals (a,b) iff ex n being Element of INT st x = ].(a + n),(b + n).[ ) ;

registration

let a, b be real number ;

cluster IntIntervals (a,b) -> non empty ;

coherence

not IntIntervals (a,b) is empty

end;
cluster IntIntervals (a,b) -> non empty ;

coherence

not IntIntervals (a,b) is empty

proof end;

theorem :: TOPREALB:4

proof end;

definition

let a, b be real number ;

:: original: IntIntervals

redefine func IntIntervals (a,b) -> Subset-Family of R^1;

coherence

IntIntervals (a,b) is Subset-Family of R^1

end;
:: original: IntIntervals

redefine func IntIntervals (a,b) -> Subset-Family of R^1;

coherence

IntIntervals (a,b) is Subset-Family of R^1

proof end;

definition

let a, b be real number ;

:: original: IntIntervals

redefine func IntIntervals (a,b) -> open Subset-Family of R^1;

coherence

IntIntervals (a,b) is open Subset-Family of R^1

end;
:: original: IntIntervals

redefine func IntIntervals (a,b) -> open Subset-Family of R^1;

coherence

IntIntervals (a,b) is open Subset-Family of R^1

proof end;

begin

definition

let r be real number ;

func R^1 r -> Point of R^1 equals :: TOPREALB:def 2

r;

coherence

r is Point of R^1 by TOPMETR:24, XREAL_0:def 1;

end;
func R^1 r -> Point of R^1 equals :: TOPREALB:def 2

r;

coherence

r is Point of R^1 by TOPMETR:24, XREAL_0:def 1;

:: deftheorem defines R^1 TOPREALB:def 2 :

for r being real number holds R^1 r = r;

definition

let A be Subset of REAL;

func R^1 A -> Subset of R^1 equals :: TOPREALB:def 3

A;

coherence

A is Subset of R^1 by TOPMETR:24;

end;
func R^1 A -> Subset of R^1 equals :: TOPREALB:def 3

A;

coherence

A is Subset of R^1 by TOPMETR:24;

:: deftheorem defines R^1 TOPREALB:def 3 :

for A being Subset of REAL holds R^1 A = A;

registration
end;

registration
end;

registration
end;

registration

let A be open Subset of REAL;

cluster R^1 | (R^1 A) -> open ;

coherence

R^1 | (R^1 A) is open

end;
cluster R^1 | (R^1 A) -> open ;

coherence

R^1 | (R^1 A) is open

proof end;

registration

let A be closed Subset of REAL;

cluster R^1 | (R^1 A) -> closed ;

coherence

R^1 | (R^1 A) is closed

end;
cluster R^1 | (R^1 A) -> closed ;

coherence

R^1 | (R^1 A) is closed

proof end;

definition

let f be PartFunc of REAL,REAL;

func R^1 f -> Function of (R^1 | (R^1 (dom f))),(R^1 | (R^1 (rng f))) equals :: TOPREALB:def 4

f;

coherence

f is Function of (R^1 | (R^1 (dom f))),(R^1 | (R^1 (rng f)))

end;
func R^1 f -> Function of (R^1 | (R^1 (dom f))),(R^1 | (R^1 (rng f))) equals :: TOPREALB:def 4

f;

coherence

f is Function of (R^1 | (R^1 (dom f))),(R^1 | (R^1 (rng f)))

proof end;

:: deftheorem defines R^1 TOPREALB:def 4 :

for f being PartFunc of REAL,REAL holds R^1 f = f;

registration
end;

registration

let f be one-to-one PartFunc of REAL,REAL;

cluster R^1 f -> one-to-one ;

coherence

R^1 f is one-to-one ;

end;
cluster R^1 f -> one-to-one ;

coherence

R^1 f is one-to-one ;

theorem Th5: :: TOPREALB:5

proof end;

theorem Th6: :: TOPREALB:6

proof end;

theorem Th7: :: TOPREALB:7

proof end;

theorem Th8: :: TOPREALB:8

proof end;

Lm10: sin is Function of R^1,R^1

proof end;

Lm11: cos is Function of R^1,R^1

proof end;

registration

let f be continuous PartFunc of REAL,REAL;

cluster R^1 f -> continuous ;

coherence

R^1 f is continuous

end;
cluster R^1 f -> continuous ;

coherence

R^1 f is continuous

proof end;

set A = R^1 ].0,1.[;

Lm12: now

let a be non zero real number ; :: thesis: for b being real number holds

( R^1 = R^1 | (R^1 (dom (AffineMap (a,b)))) & R^1 = R^1 | (R^1 (rng (AffineMap (a,b)))) )

let b be real number ; :: thesis: ( R^1 = R^1 | (R^1 (dom (AffineMap (a,b)))) & R^1 = R^1 | (R^1 (rng (AffineMap (a,b)))) )

A1: rng (AffineMap (a,b)) = REAL by JORDAN16:32;

A2: [#] R^1 = REAL by TOPMETR:24;

dom (AffineMap (a,b)) = REAL by FUNCT_2:def 1;

hence ( R^1 = R^1 | (R^1 (dom (AffineMap (a,b)))) & R^1 = R^1 | (R^1 (rng (AffineMap (a,b)))) ) by A1, A2, TSEP_1:3; :: thesis: verum

end;
( R^1 = R^1 | (R^1 (dom (AffineMap (a,b)))) & R^1 = R^1 | (R^1 (rng (AffineMap (a,b)))) )

let b be real number ; :: thesis: ( R^1 = R^1 | (R^1 (dom (AffineMap (a,b)))) & R^1 = R^1 | (R^1 (rng (AffineMap (a,b)))) )

A1: rng (AffineMap (a,b)) = REAL by JORDAN16:32;

A2: [#] R^1 = REAL by TOPMETR:24;

dom (AffineMap (a,b)) = REAL by FUNCT_2:def 1;

hence ( R^1 = R^1 | (R^1 (dom (AffineMap (a,b)))) & R^1 = R^1 | (R^1 (rng (AffineMap (a,b)))) ) by A1, A2, TSEP_1:3; :: thesis: verum

registration

let a be non zero real number ;

let b be real number ;

cluster R^1 (AffineMap (a,b)) -> open ;

coherence

R^1 (AffineMap (a,b)) is open

end;
let b be real number ;

cluster R^1 (AffineMap (a,b)) -> open ;

coherence

R^1 (AffineMap (a,b)) is open

proof end;

begin

definition

let S be SubSpace of TOP-REAL 2;

attr S is being_simple_closed_curve means :Def5: :: TOPREALB:def 5

the carrier of S is Simple_closed_curve;

end;
attr S is being_simple_closed_curve means :Def5: :: TOPREALB:def 5

the carrier of S is Simple_closed_curve;

:: deftheorem Def5 defines being_simple_closed_curve TOPREALB:def 5 :

for S being SubSpace of TOP-REAL 2 holds

( S is being_simple_closed_curve iff the carrier of S is Simple_closed_curve );

registration

cluster being_simple_closed_curve -> non empty compact pathwise_connected SubSpace of TOP-REAL 2;

coherence

for b_{1} being SubSpace of TOP-REAL 2 st b_{1} is being_simple_closed_curve holds

( not b_{1} is empty & b_{1} is pathwise_connected & b_{1} is compact )

end;
coherence

for b

( not b

proof end;

registration

let r be real positive number ;

let x be Point of (TOP-REAL 2);

cluster Sphere (x,r) -> being_simple_closed_curve ;

coherence

Sphere (x,r) is being_simple_closed_curve

end;
let x be Point of (TOP-REAL 2);

cluster Sphere (x,r) -> being_simple_closed_curve ;

coherence

Sphere (x,r) is being_simple_closed_curve

proof end;

definition

let n be Nat;

let x be Point of (TOP-REAL n);

let r be real number ;

func Tcircle (x,r) -> SubSpace of TOP-REAL n equals :: TOPREALB:def 6

(TOP-REAL n) | (Sphere (x,r));

coherence

(TOP-REAL n) | (Sphere (x,r)) is SubSpace of TOP-REAL n ;

end;
let x be Point of (TOP-REAL n);

let r be real number ;

func Tcircle (x,r) -> SubSpace of TOP-REAL n equals :: TOPREALB:def 6

(TOP-REAL n) | (Sphere (x,r));

coherence

(TOP-REAL n) | (Sphere (x,r)) is SubSpace of TOP-REAL n ;

:: deftheorem defines Tcircle TOPREALB:def 6 :

for n being Nat

for x being Point of (TOP-REAL n)

for r being real number holds Tcircle (x,r) = (TOP-REAL n) | (Sphere (x,r));

registration

let n be non empty Nat;

let x be Point of (TOP-REAL n);

let r be real non negative number ;

cluster Tcircle (x,r) -> non empty strict ;

coherence

( Tcircle (x,r) is strict & not Tcircle (x,r) is empty ) ;

end;
let x be Point of (TOP-REAL n);

let r be real non negative number ;

cluster Tcircle (x,r) -> non empty strict ;

coherence

( Tcircle (x,r) is strict & not Tcircle (x,r) is empty ) ;

theorem Th9: :: TOPREALB:9

for n being Element of NAT

for r being real number

for x being Point of (TOP-REAL n) holds the carrier of (Tcircle (x,r)) = Sphere (x,r)

for r being real number

for x being Point of (TOP-REAL n) holds the carrier of (Tcircle (x,r)) = Sphere (x,r)

proof end;

registration

let n be Nat;

let x be Point of (TOP-REAL n);

let r be empty real number ;

cluster Tcircle (x,r) -> trivial ;

coherence

Tcircle (x,r) is trivial

end;
let x be Point of (TOP-REAL n);

let r be empty real number ;

cluster Tcircle (x,r) -> trivial ;

coherence

Tcircle (x,r) is trivial

proof end;

theorem Th10: :: TOPREALB:10

for r being real number holds Tcircle ((0. (TOP-REAL 2)),r) is SubSpace of Trectangle ((- r),r,(- r),r)

proof end;

registration

let x be Point of (TOP-REAL 2);

let r be real positive number ;

cluster Tcircle (x,r) -> being_simple_closed_curve ;

coherence

Tcircle (x,r) is being_simple_closed_curve

end;
let r be real positive number ;

cluster Tcircle (x,r) -> being_simple_closed_curve ;

coherence

Tcircle (x,r) is being_simple_closed_curve

proof end;

registration

cluster strict TopSpace-like V210() V211() being_simple_closed_curve SubSpace of TOP-REAL 2;

existence

ex b_{1} being SubSpace of TOP-REAL 2 st

( b_{1} is being_simple_closed_curve & b_{1} is strict )

end;
existence

ex b

( b

proof end;

theorem :: TOPREALB:11

proof end;

definition

let n be Nat;

func Tunit_circle n -> SubSpace of TOP-REAL n equals :: TOPREALB:def 7

Tcircle ((0. (TOP-REAL n)),1);

coherence

Tcircle ((0. (TOP-REAL n)),1) is SubSpace of TOP-REAL n ;

end;
func Tunit_circle n -> SubSpace of TOP-REAL n equals :: TOPREALB:def 7

Tcircle ((0. (TOP-REAL n)),1);

coherence

Tcircle ((0. (TOP-REAL n)),1) is SubSpace of TOP-REAL n ;

:: deftheorem defines Tunit_circle TOPREALB:def 7 :

for n being Nat holds Tunit_circle n = Tcircle ((0. (TOP-REAL n)),1);

set TUC = Tunit_circle 2;

set cS1 = the carrier of (Tunit_circle 2);

Lm13: the carrier of (Tunit_circle 2) = Sphere (|[0,0]|,1)

by Th9, EUCLID:58;

registration

let n be non empty Nat;

cluster Tunit_circle n -> non empty ;

coherence

not Tunit_circle n is empty ;

end;
cluster Tunit_circle n -> non empty ;

coherence

not Tunit_circle n is empty ;

theorem Th12: :: TOPREALB:12

for n being non empty Element of NAT

for x being Point of (TOP-REAL n) st x is Point of (Tunit_circle n) holds

|.x.| = 1

for x being Point of (TOP-REAL n) st x is Point of (Tunit_circle n) holds

|.x.| = 1

proof end;

theorem Th13: :: TOPREALB:13

for x being Point of (TOP-REAL 2) st x is Point of (Tunit_circle 2) holds

( - 1 <= x `1 & x `1 <= 1 & - 1 <= x `2 & x `2 <= 1 )

( - 1 <= x `1 & x `1 <= 1 & - 1 <= x `2 & x `2 <= 1 )

proof end;

theorem Th14: :: TOPREALB:14

proof end;

theorem Th15: :: TOPREALB:15

proof end;

theorem :: TOPREALB:16

proof end;

theorem :: TOPREALB:17

proof end;

set TREC = Trectangle (p0,p1,p0,p1);

theorem :: TOPREALB:18

theorem Th19: :: TOPREALB:19

for n being non empty Element of NAT

for r being real positive number

for x being Point of (TOP-REAL n)

for f being Function of (Tunit_circle n),(Tcircle (x,r)) st ( for a being Point of (Tunit_circle n)

for b being Point of (TOP-REAL n) st a = b holds

f . a = (r * b) + x ) holds

f is being_homeomorphism

for r being real positive number

for x being Point of (TOP-REAL n)

for f being Function of (Tunit_circle n),(Tcircle (x,r)) st ( for a being Point of (Tunit_circle n)

for b being Point of (TOP-REAL n) st a = b holds

f . a = (r * b) + x ) holds

f is being_homeomorphism

proof end;

registration

cluster Tunit_circle 2 -> being_simple_closed_curve ;

coherence

Tunit_circle 2 is being_simple_closed_curve ;

end;
coherence

Tunit_circle 2 is being_simple_closed_curve ;

Lm14: for n being non empty Element of NAT

for r being real positive number

for x being Point of (TOP-REAL n) holds Tunit_circle n, Tcircle (x,r) are_homeomorphic

proof end;

theorem :: TOPREALB:20

for n being non empty Element of NAT

for r, s being real positive number

for x, y being Point of (TOP-REAL n) holds Tcircle (x,r), Tcircle (y,s) are_homeomorphic

for r, s being real positive number

for x, y being Point of (TOP-REAL n) holds Tcircle (x,r), Tcircle (y,s) are_homeomorphic

proof end;

registration

let x be Point of (TOP-REAL 2);

let r be real non negative number ;

cluster Tcircle (x,r) -> pathwise_connected ;

coherence

Tcircle (x,r) is pathwise_connected

end;
let r be real non negative number ;

cluster Tcircle (x,r) -> pathwise_connected ;

coherence

Tcircle (x,r) is pathwise_connected

proof end;

definition

func c[10] -> Point of (Tunit_circle 2) equals :: TOPREALB:def 8

|[1,0]|;

coherence

|[1,0]| is Point of (Tunit_circle 2)

|[(- 1),0]|;

coherence

|[(- 1),0]| is Point of (Tunit_circle 2)

end;
|[1,0]|;

coherence

|[1,0]| is Point of (Tunit_circle 2)

proof end;

func c[-10] -> Point of (Tunit_circle 2) equals :: TOPREALB:def 9|[(- 1),0]|;

coherence

|[(- 1),0]| is Point of (Tunit_circle 2)

proof end;

:: deftheorem defines c[10] TOPREALB:def 8 :

c[10] = |[1,0]|;

:: deftheorem defines c[-10] TOPREALB:def 9 :

c[-10] = |[(- 1),0]|;

Lm15: c[10] <> c[-10]

by SPPOL_2:1;

definition

let p be Point of (Tunit_circle 2);

func Topen_unit_circle p -> strict SubSpace of Tunit_circle 2 means :Def10: :: TOPREALB:def 10

the carrier of it = the carrier of (Tunit_circle 2) \ {p};

existence

ex b_{1} being strict SubSpace of Tunit_circle 2 st the carrier of b_{1} = the carrier of (Tunit_circle 2) \ {p}

for b_{1}, b_{2} being strict SubSpace of Tunit_circle 2 st the carrier of b_{1} = the carrier of (Tunit_circle 2) \ {p} & the carrier of b_{2} = the carrier of (Tunit_circle 2) \ {p} holds

b_{1} = b_{2}
by TSEP_1:5;

end;
func Topen_unit_circle p -> strict SubSpace of Tunit_circle 2 means :Def10: :: TOPREALB:def 10

the carrier of it = the carrier of (Tunit_circle 2) \ {p};

existence

ex b

proof end;

uniqueness for b

b

:: deftheorem Def10 defines Topen_unit_circle TOPREALB:def 10 :

for p being Point of (Tunit_circle 2)

for b

( b

registration

let p be Point of (Tunit_circle 2);

cluster Topen_unit_circle p -> non empty strict ;

coherence

not Topen_unit_circle p is empty

end;
cluster Topen_unit_circle p -> non empty strict ;

coherence

not Topen_unit_circle p is empty

proof end;

theorem :: TOPREALB:21

canceled;

theorem Th22: :: TOPREALB:22

proof end;

theorem Th23: :: TOPREALB:23

for p being Point of (Tunit_circle 2) holds Topen_unit_circle p = (Tunit_circle 2) | (([#] (Tunit_circle 2)) \ {p})

proof end;

theorem Th24: :: TOPREALB:24

proof end;

theorem Th25: :: TOPREALB:25

for p being Point of (TOP-REAL 2) st p is Point of (Topen_unit_circle c[10]) & p `2 = 0 holds

p = c[-10]

p = c[-10]

proof end;

theorem Th26: :: TOPREALB:26

for p being Point of (TOP-REAL 2) st p is Point of (Topen_unit_circle c[-10]) & p `2 = 0 holds

p = c[10]

p = c[10]

proof end;

set TOUC = Topen_unit_circle c[10];

set TOUCm = Topen_unit_circle c[-10];

set X = the carrier of (Topen_unit_circle c[10]);

set Xm = the carrier of (Topen_unit_circle c[-10]);

set Y = the carrier of (R^1 | (R^1 ].0,(0 + p1).[));

set Ym = the carrier of (R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[));

Lm16: the carrier of (Topen_unit_circle c[10]) = [#] (Topen_unit_circle c[10])

;

Lm17: the carrier of (Topen_unit_circle c[-10]) = [#] (Topen_unit_circle c[-10])

;

theorem Th27: :: TOPREALB:27

for p being Point of (Tunit_circle 2)

for x being Point of (TOP-REAL 2) st x is Point of (Topen_unit_circle p) holds

( - 1 <= x `1 & x `1 <= 1 & - 1 <= x `2 & x `2 <= 1 )

for x being Point of (TOP-REAL 2) st x is Point of (Topen_unit_circle p) holds

( - 1 <= x `1 & x `1 <= 1 & - 1 <= x `2 & x `2 <= 1 )

proof end;

theorem Th28: :: TOPREALB:28

for x being Point of (TOP-REAL 2) st x is Point of (Topen_unit_circle c[10]) holds

( - 1 <= x `1 & x `1 < 1 )

( - 1 <= x `1 & x `1 < 1 )

proof end;

theorem Th29: :: TOPREALB:29

for x being Point of (TOP-REAL 2) st x is Point of (Topen_unit_circle c[-10]) holds

( - 1 < x `1 & x `1 <= 1 )

( - 1 < x `1 & x `1 <= 1 )

proof end;

registration

let p be Point of (Tunit_circle 2);

cluster Topen_unit_circle p -> strict open ;

coherence

Topen_unit_circle p is open

end;
cluster Topen_unit_circle p -> strict open ;

coherence

Topen_unit_circle p is open

proof end;

theorem :: TOPREALB:30

proof end;

theorem :: TOPREALB:31

for p, q being Point of (Tunit_circle 2) holds Topen_unit_circle p, Topen_unit_circle q are_homeomorphic

proof end;

begin

definition

func CircleMap -> Function of R^1,(Tunit_circle 2) means :Def11: :: TOPREALB:def 11

for x being real number holds it . x = |[(cos ((2 * PI) * x)),(sin ((2 * PI) * x))]|;

existence

ex b_{1} being Function of R^1,(Tunit_circle 2) st

for x being real number holds b_{1} . x = |[(cos ((2 * PI) * x)),(sin ((2 * PI) * x))]|

for b_{1}, b_{2} being Function of R^1,(Tunit_circle 2) st ( for x being real number holds b_{1} . x = |[(cos ((2 * PI) * x)),(sin ((2 * PI) * x))]| ) & ( for x being real number holds b_{2} . x = |[(cos ((2 * PI) * x)),(sin ((2 * PI) * x))]| ) holds

b_{1} = b_{2}

end;
for x being real number holds it . x = |[(cos ((2 * PI) * x)),(sin ((2 * PI) * x))]|;

existence

ex b

for x being real number holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def11 defines CircleMap TOPREALB:def 11 :

for b

( b

Lm18: dom CircleMap = REAL

by FUNCT_2:def 1, TOPMETR:24;

theorem Th32: :: TOPREALB:32

proof end;

theorem Th33: :: TOPREALB:33

proof end;

theorem Th34: :: TOPREALB:34

proof end;

Lm19: CircleMap . (1 / 2) = |[(- 1),0]|

proof end;

theorem Th35: :: TOPREALB:35

proof end;

theorem :: TOPREALB:36

proof end;

theorem :: TOPREALB:37

proof end;

Lm20: for r being real number holds CircleMap . r = |[((cos * (AffineMap ((2 * PI),0))) . r),((sin * (AffineMap ((2 * PI),0))) . r)]|

proof end;

theorem :: TOPREALB:38

for r being real number

for i, j being Integer holds CircleMap . r = |[((cos * (AffineMap ((2 * PI),((2 * PI) * i)))) . r),((sin * (AffineMap ((2 * PI),((2 * PI) * j)))) . r)]|

for i, j being Integer holds CircleMap . r = |[((cos * (AffineMap ((2 * PI),((2 * PI) * i)))) . r),((sin * (AffineMap ((2 * PI),((2 * PI) * j)))) . r)]|

proof end;

Lm21: for A being Subset of R^1 holds CircleMap | A is Function of (R^1 | A),(Tunit_circle 2)

proof end;

Lm22: for r being real number st - 1 <= r & r <= 1 holds

( 0 <= (arccos r) / (2 * PI) & (arccos r) / (2 * PI) <= 1 / 2 )

proof end;

theorem Th39: :: TOPREALB:39

for A being Subset of R^1

for f being Function of (R^1 | A),(Tunit_circle 2) st [.0,1.[ c= A & f = CircleMap | A holds

f is onto

for f being Function of (R^1 | A),(Tunit_circle 2) st [.0,1.[ c= A & f = CircleMap | A holds

f is onto

proof end;

Lm23: CircleMap | [.0,1.[ is one-to-one

proof end;

registration

let r be real number ;

cluster K76(CircleMap,[.r,(r + 1).[) -> one-to-one ;

coherence

CircleMap | [.r,(r + 1).[ is one-to-one

end;
cluster K76(CircleMap,[.r,(r + 1).[) -> one-to-one ;

coherence

CircleMap | [.r,(r + 1).[ is one-to-one

proof end;

registration

let r be real number ;

cluster K76(CircleMap,].r,(r + 1).[) -> one-to-one ;

coherence

CircleMap | ].r,(r + 1).[ is one-to-one

end;
cluster K76(CircleMap,].r,(r + 1).[) -> one-to-one ;

coherence

CircleMap | ].r,(r + 1).[ is one-to-one

proof end;

theorem Th40: :: TOPREALB:40

for b, a being real number st b - a <= 1 holds

for d being set st d in IntIntervals (a,b) holds

CircleMap | d is one-to-one

for d being set st d in IntIntervals (a,b) holds

CircleMap | d is one-to-one

proof end;

theorem Th41: :: TOPREALB:41

for a, b being real number

for d being set st d in IntIntervals (a,b) holds

CircleMap .: d = CircleMap .: (union (IntIntervals (a,b)))

for d being set st d in IntIntervals (a,b) holds

CircleMap .: d = CircleMap .: (union (IntIntervals (a,b)))

proof end;

definition

let r be Point of R^1;

func CircleMap r -> Function of (R^1 | (R^1 ].r,(r + 1).[)),(Topen_unit_circle (CircleMap . r)) equals :: TOPREALB:def 12

CircleMap | ].r,(r + 1).[;

coherence

CircleMap | ].r,(r + 1).[ is Function of (R^1 | (R^1 ].r,(r + 1).[)),(Topen_unit_circle (CircleMap . r))

end;
func CircleMap r -> Function of (R^1 | (R^1 ].r,(r + 1).[)),(Topen_unit_circle (CircleMap . r)) equals :: TOPREALB:def 12

CircleMap | ].r,(r + 1).[;

coherence

CircleMap | ].r,(r + 1).[ is Function of (R^1 | (R^1 ].r,(r + 1).[)),(Topen_unit_circle (CircleMap . r))

proof end;

:: deftheorem defines CircleMap TOPREALB:def 12 :

for r being Point of R^1 holds CircleMap r = CircleMap | ].r,(r + 1).[;

Lm24: for a, r being real number holds rng ((AffineMap (1,(- a))) | ].(r + a),((r + a) + 1).[) = ].r,(r + 1).[

proof end;

theorem Th42: :: TOPREALB:42

for i being Integer

for a being real number holds CircleMap (R^1 (a + i)) = (CircleMap (R^1 a)) * ((AffineMap (1,(- i))) | ].(a + i),((a + i) + 1).[)

for a being real number holds CircleMap (R^1 (a + i)) = (CircleMap (R^1 a)) * ((AffineMap (1,(- i))) | ].(a + i),((a + i) + 1).[)

proof end;

registration

let r be Point of R^1;

cluster CircleMap r -> one-to-one onto continuous ;

coherence

( CircleMap r is one-to-one & CircleMap r is onto & CircleMap r is continuous )

end;
cluster CircleMap r -> one-to-one onto continuous ;

coherence

( CircleMap r is one-to-one & CircleMap r is onto & CircleMap r is continuous )

proof end;

definition

func Circle2IntervalR -> Function of (Topen_unit_circle c[10]),(R^1 | (R^1 ].0,1.[)) means :Def13: :: TOPREALB:def 13

for p being Point of (Topen_unit_circle c[10]) ex x, y being real number st

( p = |[x,y]| & ( y >= 0 implies it . p = (arccos x) / (2 * PI) ) & ( y <= 0 implies it . p = 1 - ((arccos x) / (2 * PI)) ) );

existence

ex b_{1} being Function of (Topen_unit_circle c[10]),(R^1 | (R^1 ].0,1.[)) st

for p being Point of (Topen_unit_circle c[10]) ex x, y being real number st

( p = |[x,y]| & ( y >= 0 implies b_{1} . p = (arccos x) / (2 * PI) ) & ( y <= 0 implies b_{1} . p = 1 - ((arccos x) / (2 * PI)) ) )

for b_{1}, b_{2} being Function of (Topen_unit_circle c[10]),(R^1 | (R^1 ].0,1.[)) st ( for p being Point of (Topen_unit_circle c[10]) ex x, y being real number st

( p = |[x,y]| & ( y >= 0 implies b_{1} . p = (arccos x) / (2 * PI) ) & ( y <= 0 implies b_{1} . p = 1 - ((arccos x) / (2 * PI)) ) ) ) & ( for p being Point of (Topen_unit_circle c[10]) ex x, y being real number st

( p = |[x,y]| & ( y >= 0 implies b_{2} . p = (arccos x) / (2 * PI) ) & ( y <= 0 implies b_{2} . p = 1 - ((arccos x) / (2 * PI)) ) ) ) holds

b_{1} = b_{2}

end;
for p being Point of (Topen_unit_circle c[10]) ex x, y being real number st

( p = |[x,y]| & ( y >= 0 implies it . p = (arccos x) / (2 * PI) ) & ( y <= 0 implies it . p = 1 - ((arccos x) / (2 * PI)) ) );

existence

ex b

for p being Point of (Topen_unit_circle c[10]) ex x, y being real number st

( p = |[x,y]| & ( y >= 0 implies b

proof end;

uniqueness for b

( p = |[x,y]| & ( y >= 0 implies b

( p = |[x,y]| & ( y >= 0 implies b

b

proof end;

:: deftheorem Def13 defines Circle2IntervalR TOPREALB:def 13 :

for b

( b

( p = |[x,y]| & ( y >= 0 implies b

set A1 = R^1 ].(1 / 2),((1 / 2) + p1).[;

definition

func Circle2IntervalL -> Function of (Topen_unit_circle c[-10]),(R^1 | (R^1 ].(1 / 2),(3 / 2).[)) means :Def14: :: TOPREALB:def 14

for p being Point of (Topen_unit_circle c[-10]) ex x, y being real number st

( p = |[x,y]| & ( y >= 0 implies it . p = 1 + ((arccos x) / (2 * PI)) ) & ( y <= 0 implies it . p = 1 - ((arccos x) / (2 * PI)) ) );

existence

ex b_{1} being Function of (Topen_unit_circle c[-10]),(R^1 | (R^1 ].(1 / 2),(3 / 2).[)) st

for p being Point of (Topen_unit_circle c[-10]) ex x, y being real number st

( p = |[x,y]| & ( y >= 0 implies b_{1} . p = 1 + ((arccos x) / (2 * PI)) ) & ( y <= 0 implies b_{1} . p = 1 - ((arccos x) / (2 * PI)) ) )

for b_{1}, b_{2} being Function of (Topen_unit_circle c[-10]),(R^1 | (R^1 ].(1 / 2),(3 / 2).[)) st ( for p being Point of (Topen_unit_circle c[-10]) ex x, y being real number st

( p = |[x,y]| & ( y >= 0 implies b_{1} . p = 1 + ((arccos x) / (2 * PI)) ) & ( y <= 0 implies b_{1} . p = 1 - ((arccos x) / (2 * PI)) ) ) ) & ( for p being Point of (Topen_unit_circle c[-10]) ex x, y being real number st

( p = |[x,y]| & ( y >= 0 implies b_{2} . p = 1 + ((arccos x) / (2 * PI)) ) & ( y <= 0 implies b_{2} . p = 1 - ((arccos x) / (2 * PI)) ) ) ) holds

b_{1} = b_{2}

end;
for p being Point of (Topen_unit_circle c[-10]) ex x, y being real number st

( p = |[x,y]| & ( y >= 0 implies it . p = 1 + ((arccos x) / (2 * PI)) ) & ( y <= 0 implies it . p = 1 - ((arccos x) / (2 * PI)) ) );

existence

ex b

for p being Point of (Topen_unit_circle c[-10]) ex x, y being real number st

( p = |[x,y]| & ( y >= 0 implies b

proof end;

uniqueness for b

( p = |[x,y]| & ( y >= 0 implies b

( p = |[x,y]| & ( y >= 0 implies b

b

proof end;

:: deftheorem Def14 defines Circle2IntervalL TOPREALB:def 14 :

for b

( b

( p = |[x,y]| & ( y >= 0 implies b

set C = Circle2IntervalR ;

set Cm = Circle2IntervalL ;

theorem Th43: :: TOPREALB:43

proof end;

theorem Th44: :: TOPREALB:44

proof end;

set A = ].0,1.[;

set Q = [.(- 1),1.[;

set E = ].0,PI.];

set j = 1 / (2 * PI);

reconsider Q = [.(- 1),1.[, E = ].0,PI.] as non empty Subset of REAL ;

Lm25: the carrier of (R^1 | (R^1 Q)) = R^1 Q

by PRE_TOPC:29;

Lm26: the carrier of (R^1 | (R^1 E)) = R^1 E

by PRE_TOPC:29;

Lm27: the carrier of (R^1 | (R^1 ].0,1.[)) = R^1 ].0,1.[

by PRE_TOPC:29;

set Af = (AffineMap ((1 / (2 * PI)),0)) | (R^1 E);

dom (AffineMap ((1 / (2 * PI)),0)) = the carrier of R^1

by FUNCT_2:def 1, TOPMETR:24;

then Lm28: dom ((AffineMap ((1 / (2 * PI)),0)) | (R^1 E)) = R^1 E

by RELAT_1:91;

rng ((AffineMap ((1 / (2 * PI)),0)) | (R^1 E)) c= ].0,1.[

proof end;

then reconsider Af = (AffineMap ((1 / (2 * PI)),0)) | (R^1 E) as Function of (R^1 | (R^1 E)),(R^1 | (R^1 ].0,1.[)) by Lm26, Lm27, Lm28, FUNCT_2:4;

Lm29: R^1 (AffineMap ((1 / (2 * PI)),0)) = AffineMap ((1 / (2 * PI)),0)

;

Lm30: dom (AffineMap ((1 / (2 * PI)),0)) = REAL

by FUNCT_2:def 1;

Lm31: rng (AffineMap ((1 / (2 * PI)),0)) = REAL

by JORDAN16:32;

R^1 | ([#] R^1) = R^1

by TSEP_1:3;

then reconsider Af = Af as continuous Function of (R^1 | (R^1 E)),(R^1 | (R^1 ].0,1.[)) by Lm29, Lm30, Lm31, TOPMETR:24, TOPREALA:29;

set L = (R^1 (AffineMap ((- 1),1))) | (R^1 ].0,1.[);

Lm32: dom (AffineMap ((- 1),1)) = REAL

by FUNCT_2:def 1;

then Lm33: dom ((R^1 (AffineMap ((- 1),1))) | (R^1 ].0,1.[)) = ].0,1.[

by RELAT_1:91;

rng ((R^1 (AffineMap ((- 1),1))) | (R^1 ].0,1.[)) c= ].0,1.[

proof end;

then reconsider L = (R^1 (AffineMap ((- 1),1))) | (R^1 ].0,1.[) as Function of (R^1 | (R^1 ].0,1.[)),(R^1 | (R^1 ].0,1.[)) by Lm27, Lm33, FUNCT_2:4;

Lm34: rng (AffineMap ((- 1),1)) = REAL

by JORDAN16:32;

Lm35: R^1 | ([#] R^1) = R^1

by TSEP_1:3;

then reconsider L = L as continuous Function of (R^1 | (R^1 ].0,1.[)),(R^1 | (R^1 ].0,1.[)) by Lm32, Lm34, TOPMETR:24, TOPREALA:29;

reconsider ac = R^1 arccos as continuous Function of (R^1 | (R^1 [.(- 1),1.])),(R^1 | (R^1 [.0,PI.])) by SIN_COS6:87, SIN_COS6:88;

set c = ac | (R^1 Q);

Lm36: dom (ac | (R^1 Q)) = Q

by RELAT_1:91, SIN_COS6:88, XXREAL_1:35;

Lm37: rng (ac | (R^1 Q)) c= E

proof end;

then reconsider c = ac | (R^1 Q) as Function of (R^1 | (R^1 Q)),(R^1 | (R^1 E)) by Lm25, Lm26, Lm36, FUNCT_2:4;

the carrier of (R^1 | (R^1 [.(- 1),1.])) = [.(- 1),1.]

by PRE_TOPC:29;

then reconsider QQ = R^1 Q as Subset of (R^1 | (R^1 [.(- 1),1.])) by XXREAL_1:35;

the carrier of (R^1 | (R^1 [.0,PI.])) = [.0,PI.]

by PRE_TOPC:29;

then reconsider EE = R^1 E as Subset of (R^1 | (R^1 [.0,PI.])) by XXREAL_1:36;

Lm38: (R^1 | (R^1 [.(- 1),1.])) | QQ = R^1 | (R^1 Q)

by GOBOARD9:4;

(R^1 | (R^1 [.0,PI.])) | EE = R^1 | (R^1 E)

by GOBOARD9:4;

then Lm39: c is continuous

by Lm38, TOPREALA:29;

reconsider p = proj1 as Function of (TOP-REAL 2),R^1 by TOPMETR:24;

Lm40: dom p = the carrier of (TOP-REAL 2)

by FUNCT_2:def 1;

Lm41: p is continuous

by TOPREAL6:83;

Lm42: for aX1 being Subset of (Topen_unit_circle c[10]) st aX1 = { q where q is Point of (TOP-REAL 2) : ( q in the carrier of (Topen_unit_circle c[10]) & 0 <= q `2 ) } holds

Circle2IntervalR | ((Topen_unit_circle c[10]) | aX1) is continuous

proof end;

Lm43: for aX1 being Subset of (Topen_unit_circle c[10]) st aX1 = { q where q is Point of (TOP-REAL 2) : ( q in the carrier of (Topen_unit_circle c[10]) & 0 >= q `2 ) } holds

Circle2IntervalR | ((Topen_unit_circle c[10]) | aX1) is continuous

proof end;

Lm44: for p being Point of (Topen_unit_circle c[10]) st p = c[-10] holds

Circle2IntervalR is_continuous_at p

proof end;

set h1 = REAL --> 1;

reconsider h1 = REAL --> 1 as PartFunc of REAL,REAL ;

Lm45: Circle2IntervalR is continuous

proof end;

set A = ].(1 / 2),((1 / 2) + p1).[;

set Q = ].(- 1),1.];

set E = [.0,PI.[;

reconsider Q = ].(- 1),1.], E = [.0,PI.[ as non empty Subset of REAL ;

Lm46: the carrier of (R^1 | (R^1 Q)) = R^1 Q

by PRE_TOPC:29;

Lm47: the carrier of (R^1 | (R^1 E)) = R^1 E

by PRE_TOPC:29;

Lm48: the carrier of (R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[)) = R^1 ].(1 / 2),((1 / 2) + p1).[

by PRE_TOPC:29;

set Af = (AffineMap ((- (1 / (2 * PI))),1)) | (R^1 E);

dom (AffineMap ((- (1 / (2 * PI))),1)) = the carrier of R^1

by FUNCT_2:def 1, TOPMETR:24;

then Lm49: dom ((AffineMap ((- (1 / (2 * PI))),1)) | (R^1 E)) = R^1 E

by RELAT_1:91;

rng ((AffineMap ((- (1 / (2 * PI))),1)) | (R^1 E)) c= ].(1 / 2),((1 / 2) + p1).[

proof end;

then reconsider Af = (AffineMap ((- (1 / (2 * PI))),1)) | (R^1 E) as Function of (R^1 | (R^1 E)),(R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[)) by Lm47, Lm48, Lm49, FUNCT_2:4;

Lm50: R^1 (AffineMap ((- (1 / (2 * PI))),1)) = AffineMap ((- (1 / (2 * PI))),1)

;

Lm51: dom (AffineMap ((- (1 / (2 * PI))),1)) = REAL

by FUNCT_2:def 1;

rng (AffineMap ((- (1 / (2 * PI))),1)) = REAL

by JORDAN16:32;

then reconsider Af = Af as continuous Function of (R^1 | (R^1 E)),(R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[)) by Lm35, Lm50, Lm51, TOPMETR:24, TOPREALA:29;

set Af1 = (AffineMap ((1 / (2 * PI)),1)) | (R^1 E);

dom (AffineMap ((1 / (2 * PI)),1)) = the carrier of R^1

by FUNCT_2:def 1, TOPMETR:24;

then Lm52: dom ((AffineMap ((1 / (2 * PI)),1)) | (R^1 E)) = R^1 E

by RELAT_1:91;

rng ((AffineMap ((1 / (2 * PI)),1)) | (R^1 E)) c= ].(1 / 2),((1 / 2) + p1).[

proof end;

then reconsider Af1 = (AffineMap ((1 / (2 * PI)),1)) | (R^1 E) as Function of (R^1 | (R^1 E)),(R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[)) by Lm47, Lm48, Lm52, FUNCT_2:4;

Lm53: R^1 (AffineMap ((1 / (2 * PI)),1)) = AffineMap ((1 / (2 * PI)),1)

;

Lm54: dom (AffineMap ((1 / (2 * PI)),1)) = REAL

by FUNCT_2:def 1;

rng (AffineMap ((1 / (2 * PI)),1)) = REAL

by JORDAN16:32;

then reconsider Af1 = Af1 as continuous Function of (R^1 | (R^1 E)),(R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[)) by Lm35, Lm53, Lm54, TOPMETR:24, TOPREALA:29;

set c = ac | (R^1 Q);

Lm55: dom (ac | (R^1 Q)) = Q

by RELAT_1:91, SIN_COS6:88, XXREAL_1:36;

Lm56: rng (ac | (R^1 Q)) c= E

proof end;

then reconsider c = ac | (R^1 Q) as Function of (R^1 | (R^1 Q)),(R^1 | (R^1 E)) by Lm46, Lm47, Lm55, FUNCT_2:4;

the carrier of (R^1 | (R^1 [.(- 1),1.])) = [.(- 1),1.]

by PRE_TOPC:29;

then reconsider QQ = R^1 Q as Subset of (R^1 | (R^1 [.(- 1),1.])) by XXREAL_1:36;

the carrier of (R^1 | (R^1 [.0,PI.])) = [.0,PI.]

by PRE_TOPC:29;

then reconsider EE = R^1 E as Subset of (R^1 | (R^1 [.0,PI.])) by XXREAL_1:35;

Lm57: (R^1 | (R^1 [.(- 1),1.])) | QQ = R^1 | (R^1 Q)

by GOBOARD9:4;

(R^1 | (R^1 [.0,PI.])) | EE = R^1 | (R^1 E)

by GOBOARD9:4;

then Lm58: c is continuous

by Lm57, TOPREALA:29;

Lm59: for aX1 being Subset of (Topen_unit_circle c[-10]) st aX1 = { q where q is Point of (TOP-REAL 2) : ( q in the carrier of (Topen_unit_circle c[-10]) & 0 <= q `2 ) } holds

Circle2IntervalL | ((Topen_unit_circle c[-10]) | aX1) is continuous

proof end;

Lm60: for aX1 being Subset of (Topen_unit_circle c[-10]) st aX1 = { q where q is Point of (TOP-REAL 2) : ( q in the carrier of (Topen_unit_circle c[-10]) & 0 >= q `2 ) } holds

Circle2IntervalL | ((Topen_unit_circle c[-10]) | aX1) is continuous

proof end;

Lm61: for p being Point of (Topen_unit_circle c[-10]) st p = c[10] holds

Circle2IntervalL is_continuous_at p

proof end;

Lm62: Circle2IntervalL is continuous

proof end;

registration

cluster Circle2IntervalR -> one-to-one onto continuous ;

coherence

( Circle2IntervalR is one-to-one & Circle2IntervalR is onto & Circle2IntervalR is continuous ) by Lm45, Th43, GRCAT_1:56;

cluster Circle2IntervalL -> one-to-one onto continuous ;

coherence

( Circle2IntervalL is one-to-one & Circle2IntervalL is onto & Circle2IntervalL is continuous ) by Lm62, Th44, GRCAT_1:56;

end;
coherence

( Circle2IntervalR is one-to-one & Circle2IntervalR is onto & Circle2IntervalR is continuous ) by Lm45, Th43, GRCAT_1:56;

cluster Circle2IntervalL -> one-to-one onto continuous ;

coherence

( Circle2IntervalL is one-to-one & Circle2IntervalL is onto & Circle2IntervalL is continuous ) by Lm62, Th44, GRCAT_1:56;

Lm63: CircleMap (R^1 0) is open

proof end;

Lm64: CircleMap (R^1 (1 / 2)) is open

by Lm19, Th44, TOPREALA:35;

registration

let i be Integer;

cluster CircleMap (R^1 i) -> open ;

coherence

CircleMap (R^1 i) is open

coherence

CircleMap (R^1 ((1 / 2) + i)) is open

end;
cluster CircleMap (R^1 i) -> open ;

coherence

CircleMap (R^1 i) is open

proof end;

cluster CircleMap (R^1 ((1 / 2) + i)) -> open ;coherence

CircleMap (R^1 ((1 / 2) + i)) is open

proof end;

registration

cluster Circle2IntervalR -> open ;

coherence

Circle2IntervalR is open

coherence

Circle2IntervalL is open by Lm19, Th44, TOPREALA:34;

end;
coherence

Circle2IntervalR is open

proof end;

cluster Circle2IntervalL -> open ;coherence

Circle2IntervalL is open by Lm19, Th44, TOPREALA:34;

theorem :: TOPREALB:45

canceled;

theorem :: TOPREALB:46

proof end;

theorem :: TOPREALB:47

canceled;

theorem :: TOPREALB:48

canceled;

theorem :: TOPREALB:49

ex F being Subset-Family of (Tunit_circle 2) st

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

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

proof end;