:: TOPREALB semantic presentation

set c1 = 2 * PI ;

set c2 = |[0,0]|;

set c3 = the carrier of R^1 ;

Lemma1: 0 in INT
by INT_1:def 1;

reconsider c4 = - 1 as real negative number ;

reconsider c5 = 1 as real positive number ;

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

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

Lemma2: the carrier of (Closed-Interval-TSpace (- 1),1) = [.(- 1),1.]
by TOPMETR:25;

Lemma3: 1 - 0 <= 1
;

Lemma4: (3 / 2) - (1 / 2) <= 1
;

registration
cluster ].0,1.[ -> non empty ;
coherence
not ].0,1.[ is empty ;
cluster [.(- 1),1.] -> non empty ;
coherence
not [.(- 1),1.] is empty ;
cluster ].(1 / 2),(3 / 2).[ -> non empty ;
coherence
not ].(1 / 2),(3 / 2).[ is empty
proof end;
end;

Lemma5: PI / 2 < PI / 1
by REAL_2:200;

Lemma6: 1 * PI < (3 / 2) * PI
by XREAL_1:70;

Lemma7: (3 / 2) * PI < 2 * PI
by XREAL_1:70;

Lemma8: dom sin = REAL
by SIN_COS:def 20;

Lemma9: for b1 being non empty TopSpace
for b2 being non empty SubSpace of b1
for b3 being non empty SubSpace of b2
for b4 being Point of b3 holds b4 is Point of b1
proof end;

Lemma10: for b1 being TopSpace
for b2 being SubSpace of b1
for b3 being SubSpace of b2
for b4 being Subset of b3 holds b4 is Subset of b1
proof end;

registration
cluster sin -> continuous ;
coherence
sin is continuous
proof end;
cluster cos -> continuous ;
coherence
cos is continuous
proof end;
cluster arcsin -> continuous ;
coherence
arcsin is continuous
proof end;
cluster arccos -> continuous ;
coherence
arccos is continuous
proof end;
end;

theorem Th1: :: TOPREALB:1
for b1, b2, b3 being real number holds sin ((b1 * b2) + b3) = (sin * (AffineMap b1,b3)) . b2
proof end;

theorem Th2: :: TOPREALB:2
for b1, b2, b3 being real number holds cos ((b1 * b2) + b3) = (cos * (AffineMap b1,b3)) . b2
proof end;

registration
let c8 be non zero real number ;
let c9 be real number ;
cluster AffineMap a1,a2 -> one-to-one onto ;
coherence
( AffineMap c8,c9 is onto & AffineMap c8,c9 is one-to-one )
proof end;
end;

definition
let c8, c9 be real number ;
func IntIntervals c1,c2 -> set equals :: TOPREALB:def 1
{ ].(a1 + b1),(a2 + b1).[ where B is Element of INT : verum } ;
coherence
{ ].(c8 + b1),(c9 + b1).[ where B is Element of INT : verum } is set ;
end;

:: deftheorem Def1 defines IntIntervals TOPREALB:def 1 :
for b1, b2 being real number holds IntIntervals b1,b2 = { ].(b1 + b3),(b2 + b3).[ where B is Element of INT : verum } ;

theorem Th3: :: TOPREALB:3
for b1, b2 being real number
for b3 being set holds
( b3 in IntIntervals b1,b2 iff ex b4 being Element of INT st b3 = ].(b1 + b4),(b2 + b4).[ ) ;

registration
let c8, c9 be real number ;
cluster IntIntervals a1,a2 -> non empty ;
coherence
not IntIntervals c8,c9 is empty
proof end;
end;

theorem Th4: :: TOPREALB:4
for b1, b2 being real number st b1 - b2 <= 1 holds
IntIntervals b2,b1 is mutually-disjoint
proof end;

definition
let c8, c9 be real number ;
redefine func IntIntervals as IntIntervals c1,c2 -> Subset-Family of R^1 ;
coherence
IntIntervals c8,c9 is Subset-Family of R^1
proof end;
end;

definition
let c8, c9 be real number ;
redefine func IntIntervals as IntIntervals c1,c2 -> open Subset-Family of R^1 ;
coherence
IntIntervals c8,c9 is open Subset-Family of R^1
proof end;
end;

definition
let c8 be real number ;
func R^1 c1 -> Point of R^1 equals :: TOPREALB:def 2
a1;
coherence
c8 is Point of R^1 by TOPMETR:24, XREAL_0:def 1;
end;

:: deftheorem Def2 defines R^1 TOPREALB:def 2 :
for b1 being real number holds R^1 b1 = b1;

definition
let c8 be Subset of REAL ;
func R^1 c1 -> Subset of R^1 equals :: TOPREALB:def 3
a1;
coherence
c8 is Subset of R^1 by TOPMETR:24;
end;

:: deftheorem Def3 defines R^1 TOPREALB:def 3 :
for b1 being Subset of REAL holds R^1 b1 = b1;

registration
let c8 be non empty Subset of REAL ;
cluster R^1 a1 -> non empty ;
coherence
not R^1 c8 is empty ;
end;

registration
let c8 be open Subset of REAL ;
cluster R^1 a1 -> open ;
coherence
R^1 c8 is open by BORSUK_5:62;
end;

registration
let c8 be closed Subset of REAL ;
cluster R^1 a1 -> closed ;
coherence
R^1 c8 is closed by TOPREAL6:79;
end;

registration
let c8 be open Subset of REAL ;
cluster R^1 | (R^1 a1) -> open ;
coherence
R^1 | (R^1 c8) is open
proof end;
end;

registration
let c8 be closed Subset of REAL ;
cluster R^1 | (R^1 a1) -> closed ;
coherence
R^1 | (R^1 c8) is closed
proof end;
end;

definition
let c8 be PartFunc of REAL , REAL ;
func R^1 c1 -> Function of (R^1 | (R^1 (dom a1))),(R^1 | (R^1 (rng a1))) equals :: TOPREALB:def 4
a1;
coherence
c8 is Function of (R^1 | (R^1 (dom c8))),(R^1 | (R^1 (rng c8)))
proof end;
end;

:: deftheorem Def4 defines R^1 TOPREALB:def 4 :
for b1 being PartFunc of REAL , REAL holds R^1 b1 = b1;

registration
let c8 be PartFunc of REAL , REAL ;
cluster R^1 a1 -> onto ;
coherence
R^1 c8 is onto
proof end;
end;

registration
let c8 be one-to-one PartFunc of REAL , REAL ;
cluster R^1 a1 -> one-to-one onto ;
coherence
R^1 c8 is one-to-one ;
end;

theorem Th5: :: TOPREALB:5
R^1 | (R^1 ([#] REAL )) = R^1
proof end;

theorem Th6: :: TOPREALB:6
for b1 being PartFunc of REAL , REAL st dom b1 = REAL holds
R^1 | (R^1 (dom b1)) = R^1
proof end;

theorem Th7: :: TOPREALB:7
for b1 being Function of REAL , REAL holds b1 is Function of R^1 ,(R^1 | (R^1 (rng b1)))
proof end;

theorem Th8: :: TOPREALB:8
for b1 being Function of REAL , REAL holds b1 is Function of R^1 ,R^1
proof end;

Lemma17: sin is Function of R^1 ,R^1
proof end;

Lemma18: cos is Function of R^1 ,R^1
proof end;

registration
let c8 be continuous PartFunc of REAL , REAL ;
cluster R^1 a1 -> onto continuous ;
coherence
R^1 c8 is continuous
proof end;
end;

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

E19: now
let c9 be non zero real number ;
let c10 be real number ;
E20: dom (AffineMap c9,c10) = REAL by FUNCT_2:def 1;
E21: rng (AffineMap c9,c10) = REAL by JORDAN16:32;
E22: [#] R^1 = REAL by TOPMETR:24;
R^1 | ([#] R^1 ) = R^1 by TSEP_1:3;
hence ( R^1 = R^1 | (R^1 (dom (AffineMap c9,c10))) & R^1 = R^1 | (R^1 (rng (AffineMap c9,c10))) ) by E20, E21, E22;
end;

registration
let c9 be non zero real number ;
let c10 be real number ;
cluster R^1 (AffineMap a1,a2) -> one-to-one onto continuous open ;
coherence
R^1 (AffineMap c9,c10) is open
proof end;
end;

definition
let c9 be SubSpace of TOP-REAL 2;
attr a1 is being_simple_closed_curve means :Def5: :: TOPREALB:def 5
the carrier of a1 is Simple_closed_curve;
end;

:: deftheorem Def5 defines being_simple_closed_curve TOPREALB:def 5 :
for b1 being SubSpace of TOP-REAL 2 holds
( b1 is being_simple_closed_curve iff the carrier of b1 is Simple_closed_curve );

registration
cluster being_simple_closed_curve -> non empty compact arcwise_connected SubSpace of TOP-REAL 2;
coherence
for b1 being SubSpace of TOP-REAL 2 st b1 is being_simple_closed_curve holds
( not b1 is empty & b1 is arcwise_connected & b1 is compact )
proof end;
end;

registration
let c9 be real positive number ;
let c10 be Point of (TOP-REAL 2);
cluster Sphere a2,a1 -> being_simple_closed_curve ;
coherence
Sphere c10,c9 is being_simple_closed_curve
proof end;
end;

definition
let c9 be Nat;
let c10 be Point of (TOP-REAL c9);
let c11 be real number ;
func Tcircle c2,c3 -> SubSpace of TOP-REAL a1 equals :: TOPREALB:def 6
(TOP-REAL a1) | (Sphere a2,a3);
coherence
(TOP-REAL c9) | (Sphere c10,c11) is SubSpace of TOP-REAL c9 ;
end;

:: deftheorem Def6 defines Tcircle TOPREALB:def 6 :
for b1 being Nat
for b2 being Point of (TOP-REAL b1)
for b3 being real number holds Tcircle b2,b3 = (TOP-REAL b1) | (Sphere b2,b3);

registration
let c9 be non empty Nat;
let c10 be Point of (TOP-REAL c9);
let c11 be real non negative number ;
cluster Tcircle a2,a3 -> non empty strict ;
coherence
( Tcircle c10,c11 is strict & not Tcircle c10,c11 is empty ) ;
end;

theorem Th9: :: TOPREALB:9
for b1 being Nat
for b2 being real number
for b3 being Point of (TOP-REAL b1) holds the carrier of (Tcircle b3,b2) = Sphere b3,b2
proof end;

registration
let c9 be Nat;
let c10 be Point of (TOP-REAL c9);
let c11 be empty real number ;
cluster Tcircle a2,a3 -> trivial ;
coherence
Tcircle c10,c11 is trivial
proof end;
end;

theorem Th10: :: TOPREALB:10
for b1 being real number holds Tcircle (0.REAL 2),b1 is SubSpace of Trectangle (- b1),b1,(- b1),b1
proof end;

registration
let c9 be Point of (TOP-REAL 2);
let c10 be real positive number ;
cluster Tcircle a1,a2 -> non empty strict compact arcwise_connected being_simple_closed_curve ;
coherence
Tcircle c9,c10 is being_simple_closed_curve
proof end;
end;

registration
cluster non empty strict compact arcwise_connected being_simple_closed_curve SubSpace of TOP-REAL 2;
existence
ex b1 being SubSpace of TOP-REAL 2 st
( b1 is being_simple_closed_curve & b1 is strict )
proof end;
end;

theorem Th11: :: TOPREALB:11
for b1, b2 being being_simple_closed_curve SubSpace of TOP-REAL 2 holds b1,b2 are_homeomorphic
proof end;

definition
let c9 be Nat;
func Tunit_circle c1 -> SubSpace of TOP-REAL a1 equals :: TOPREALB:def 7
 Tcircle (0.REAL a1),1;
coherence
Tcircle (0.REAL c9),1 is SubSpace of TOP-REAL c9 ;
end;

:: deftheorem Def7 defines Tunit_circle TOPREALB:def 7 :
for b1 being Nat holds Tunit_circle b1 = Tcircle (0.REAL b1),1;

set c9 = Tunit_circle 2;

set c10 = the carrier of (Tunit_circle 2);

Lemma23: the carrier of (Tunit_circle 2) = Sphere |[0,0]|,1
by Th9, EUCLID:58;

registration
let c11 be non empty Nat;
cluster Tunit_circle a1 -> non empty ;
coherence
not Tunit_circle c11 is empty ;
end;

theorem Th12: :: TOPREALB:12
for b1 being non empty Nat
for b2 being Point of (TOP-REAL b1) st b2 is Point of (Tunit_circle b1) holds
|.b2.| = 1
proof end;

theorem Th13: :: TOPREALB:13
for b1 being Point of (TOP-REAL 2) st b1 is Point of (Tunit_circle 2) holds
( - 1 <= b1 `1 & b1 `1 <= 1 & - 1 <= b1 `2 & b1 `2 <= 1 )
proof end;

theorem Th14: :: TOPREALB:14
for b1 being Point of (TOP-REAL 2) st b1 is Point of (Tunit_circle 2) & b1 `1 = 1 holds
b1 `2 = 0
proof end;

theorem Th15: :: TOPREALB:15
for b1 being Point of (TOP-REAL 2) st b1 is Point of (Tunit_circle 2) & b1 `1 = - 1 holds
b1 `2 = 0
proof end;

theorem Th16: :: TOPREALB:16
for b1 being Point of (TOP-REAL 2) st b1 is Point of (Tunit_circle 2) & b1 `2 = 1 holds
b1 `1 = 0
proof end;

theorem Th17: :: TOPREALB:17
for b1 being Point of (TOP-REAL 2) st b1 is Point of (Tunit_circle 2) & b1 `2 = - 1 holds
b1 `1 = 0
proof end;

set c11 = Trectangle c4,c5,c4,c5;

theorem Th18: :: TOPREALB:18
Tunit_circle 2 is SubSpace of Trectangle (- 1),1,(- 1),1 by Th10;

theorem Th19: :: TOPREALB:19
for b1 being non empty Nat
for b2 being real positive number
for b3 being Point of (TOP-REAL b1)
for b4 being Function of (Tunit_circle b1),(Tcircle b3,b2) st ( for b5 being Point of (Tunit_circle b1)
for b6 being Point of (TOP-REAL b1) st b5 = b6 holds
b4 . b5 = (b2 * b6) + b3 ) holds
b4 is_homeomorphism
proof end;

registration
cluster Tunit_circle 2 -> non empty compact arcwise_connected being_simple_closed_curve ;
coherence
Tunit_circle 2 is being_simple_closed_curve ;
end;

Lemma29: for b1 being non empty Nat
for b2 being real positive number
for b3 being Point of (TOP-REAL b1) holds Tunit_circle b1, Tcircle b3,b2 are_homeomorphic
proof end;

theorem Th20: :: TOPREALB:20
for b1 being non empty Nat
for b2, b3 being real positive number
for b4, b5 being Point of (TOP-REAL b1) holds Tcircle b4,b2, Tcircle b5,b3 are_homeomorphic
proof end;

registration
let c12 be Point of (TOP-REAL 2);
let c13 be real non negative number ;
cluster Tcircle a1,a2 -> non empty strict arcwise_connected ;
coherence
Tcircle c12,c13 is arcwise_connected
proof end;
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)
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;
end;

:: deftheorem Def8 defines c[10] TOPREALB:def 8 :
c[10] = |[1,0]|;

:: deftheorem Def9 defines c[-10] TOPREALB:def 9 :
c[-10] = |[(- 1),0]|;

theorem Th21: :: TOPREALB:21
c[10] <> c[-10] by SPPOL_2:1;

definition
let c12 be Point of (Tunit_circle 2);
func Topen_unit_circle c1 -> strict SubSpace of Tunit_circle 2 means :Def10: :: TOPREALB:def 10
the carrier of a2 = the carrier of (Tunit_circle 2) \ {a1};
existence
ex b1 being strict SubSpace of Tunit_circle 2 st the carrier of b1 = the carrier of (Tunit_circle 2) \ {c12}
proof end;
uniqueness
for b1, b2 being strict SubSpace of Tunit_circle 2 st the carrier of b1 = the carrier of (Tunit_circle 2) \ {c12} & the carrier of b2 = the carrier of (Tunit_circle 2) \ {c12} holds
b1 = b2 by TSEP_1:5;
end;

:: deftheorem Def10 defines Topen_unit_circle TOPREALB:def 10 :
for b1 being Point of (Tunit_circle 2)
for b2 being strict SubSpace of Tunit_circle 2 holds
( b2 = Topen_unit_circle b1 iff the carrier of b2 = the carrier of (Tunit_circle 2) \ {b1} );

registration
let c12 be Point of (Tunit_circle 2);
cluster Topen_unit_circle a1 -> non empty strict ;
coherence
not Topen_unit_circle c12 is empty
proof end;
end;

theorem Th22: :: TOPREALB:22
for b1 being Point of (Tunit_circle 2) holds b1 is not Point of (Topen_unit_circle b1)
proof end;

theorem Th23: :: TOPREALB:23
for b1 being Point of (Tunit_circle 2) holds Topen_unit_circle b1 = (Tunit_circle 2) | (([#] (Tunit_circle 2)) \ {b1})
proof end;

theorem Th24: :: TOPREALB:24
for b1, b2 being Point of (Tunit_circle 2) st b1 <> b2 holds
b2 is Point of (Topen_unit_circle b1)
proof end;

theorem Th25: :: TOPREALB:25
for b1 being Point of (TOP-REAL 2) st b1 is Point of (Topen_unit_circle c[10] ) & b1 `2 = 0 holds
b1 = c[-10]
proof end;

theorem Th26: :: TOPREALB:26
for b1 being Point of (TOP-REAL 2) st b1 is Point of (Topen_unit_circle c[-10] ) & b1 `2 = 0 holds
b1 = c[10]
proof end;

set c12 = Topen_unit_circle c[10] ;

set c13 = Topen_unit_circle c[-10] ;

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

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

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

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

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

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

theorem Th27: :: TOPREALB:27
for b1 being Point of (Tunit_circle 2)
for b2 being Point of (TOP-REAL 2) st b2 is Point of (Topen_unit_circle b1) holds
( - 1 <= b2 `1 & b2 `1 <= 1 & - 1 <= b2 `2 & b2 `2 <= 1 )
proof end;

theorem Th28: :: TOPREALB:28
for b1 being Point of (TOP-REAL 2) st b1 is Point of (Topen_unit_circle c[10] ) holds
( - 1 <= b1 `1 & b1 `1 < 1 )
proof end;

theorem Th29: :: TOPREALB:29
for b1 being Point of (TOP-REAL 2) st b1 is Point of (Topen_unit_circle c[-10] ) holds
( - 1 < b1 `1 & b1 `1 <= 1 )
proof end;

registration
let c18 be Point of (Tunit_circle 2);
cluster Topen_unit_circle a1 -> non empty strict open ;
coherence
Topen_unit_circle c18 is open
proof end;
end;

theorem Th30: :: TOPREALB:30
for b1 being Point of (Tunit_circle 2) holds Topen_unit_circle b1, I(01) are_homeomorphic
proof end;

theorem Th31: :: TOPREALB:31
for b1, b2 being Point of (Tunit_circle 2) holds Topen_unit_circle b1, Topen_unit_circle b2 are_homeomorphic
proof end;

definition
func CircleMap -> Function of R^1 ,(Tunit_circle 2) means :Def11: :: TOPREALB:def 11
for b1 being real number holds a1 . b1 = |[(cos ((2 * PI ) * b1)),(sin ((2 * PI ) * b1))]|;
existence
ex b1 being Function of R^1 ,(Tunit_circle 2) st
for b2 being real number holds b1 . b2 = |[(cos ((2 * PI ) * b2)),(sin ((2 * PI ) * b2))]|
proof end;
uniqueness
for b1, b2 being Function of R^1 ,(Tunit_circle 2) st ( for b3 being real number holds b1 . b3 = |[(cos ((2 * PI ) * b3)),(sin ((2 * PI ) * b3))]| ) & ( for b3 being real number holds b2 . b3 = |[(cos ((2 * PI ) * b3)),(sin ((2 * PI ) * b3))]| ) holds
b1 = b2
proof end;
end;

:: deftheorem Def11 defines CircleMap TOPREALB:def 11 :
for b1 being Function of R^1 ,(Tunit_circle 2) holds
( b1 = CircleMap iff for b2 being real number holds b1 . b2 = |[(cos ((2 * PI ) * b2)),(sin ((2 * PI ) * b2))]| );

Lemma43: dom CircleMap = REAL
by FUNCT_2:def 1, TOPMETR:24;

theorem Th32: :: TOPREALB:32
for b1 being Integer
for b2 being real number holds CircleMap . b2 = CircleMap . (b2 + b1)
proof end;

theorem Th33: :: TOPREALB:33
for b1 being Integer holds CircleMap . b1 = c[10]
proof end;

theorem Th34: :: TOPREALB:34
CircleMap " {c[10] } = INT
proof end;

Lemma47: CircleMap . (1 / 2) = |[(- 1),0]|
proof end;

Lemma48: CircleMap . 1 = |[1,0]|
by Th33;

theorem Th35: :: TOPREALB:35
for b1 being real number st frac b1 = 1 / 2 holds
CircleMap . b1 = |[(- 1),0]|
proof end;

theorem Th36: :: TOPREALB:36
for b1 being real number st frac b1 = 1 / 4 holds
CircleMap . b1 = |[0,1]|
proof end;

theorem Th37: :: TOPREALB:37
for b1 being real number st frac b1 = 3 / 4 holds
CircleMap . b1 = |[0,(- 1)]|
proof end;

Lemma50: for b1 being real number holds CircleMap . b1 = |[((cos * (AffineMap (2 * PI ),0)) . b1),((sin * (AffineMap (2 * PI ),0)) . b1)]|
proof end;

theorem Th38: :: TOPREALB:38
for b1 being real number
for b2, b3 being Integer holds CircleMap . b1 = |[((cos * (AffineMap (2 * PI ),((2 * PI ) * b2))) . b1),((sin * (AffineMap (2 * PI ),((2 * PI ) * b3))) . b1)]|
proof end;

registration
cluster CircleMap -> continuous ;
coherence
CircleMap is continuous
proof end;
end;

Lemma51: for b1 being Subset of R^1 holds CircleMap | b1 is Function of (R^1 | b1),(Tunit_circle 2)
proof end;

Lemma52: for b1 being real number st - 1 <= b1 & b1 <= 1 holds
( 0 <= (arccos b1) / (2 * PI ) & (arccos b1) / (2 * PI ) <= 1 / 2 )
proof end;

theorem Th39: :: TOPREALB:39
for b1 being Subset of R^1
for b2 being Function of (R^1 | b1),(Tunit_circle 2) st [.0,1.[ c= b1 & b2 = CircleMap | b1 holds
b2 is onto
proof end;

registration
cluster CircleMap -> onto continuous ;
coherence
CircleMap is onto
proof end;
end;

Lemma54: CircleMap | [.0,1.[ is one-to-one
proof end;

registration
let c18 be real number ;
cluster K16(CircleMap ,[.a1,(a1 + 1).[) -> one-to-one ;
coherence
CircleMap | [.c18,(c18 + 1).[ is one-to-one
proof end;
end;

registration
let c18 be real number ;
cluster K16(CircleMap ,].a1,(a1 + 1).[) -> one-to-one ;
coherence
CircleMap | ].c18,(c18 + 1).[ is one-to-one
proof end;
end;

theorem Th40: :: TOPREALB:40
for b1, b2 being real number st b1 - b2 <= 1 holds
for b3 being set st b3 in IntIntervals b2,b1 holds
CircleMap | b3 is one-to-one
proof end;

theorem Th41: :: TOPREALB:41
for b1, b2 being real number
for b3 being set st b3 in IntIntervals b1,b2 holds
CircleMap .: b3 = CircleMap .: (union (IntIntervals b1,b2))
proof end;

definition
let c18 be Point of R^1 ;
func CircleMap c1 -> Function of (R^1 | (R^1 ].a1,(a1 + 1).[)),(Topen_unit_circle (CircleMap . a1)) equals :: TOPREALB:def 12
CircleMap | ].a1,(a1 + 1).[;
coherence
CircleMap | ].c18,(c18 + 1).[ is Function of (R^1 | (R^1 ].c18,(c18 + 1).[)),(Topen_unit_circle (CircleMap . c18))
proof end;
end;

:: deftheorem Def12 defines CircleMap TOPREALB:def 12 :
for b1 being Point of R^1 holds CircleMap b1 = CircleMap | ].b1,(b1 + 1).[;

Lemma57: for b1, b2 being real number holds rng ((AffineMap 1,(- b1)) | ].(b2 + b1),((b2 + b1) + 1).[) = ].b2,(b2 + 1).[
proof end;

theorem Th42: :: TOPREALB:42
for b1 being Integer
for b2 being real number holds CircleMap (R^1 (b2 + b1)) = (CircleMap (R^1 b2)) * ((AffineMap 1,(- b1)) | ].(b2 + b1),((b2 + b1) + 1).[)
proof end;

registration
let c18 be Point of R^1 ;
cluster CircleMap a1 -> one-to-one onto continuous ;
coherence
( CircleMap c18 is one-to-one & CircleMap c18 is onto & CircleMap c18 is continuous )
proof end;
end;

definition
func Circle2IntervalR -> Function of (Topen_unit_circle c[10] ),(R^1 | (R^1 ].0,1.[)) means :Def13: :: TOPREALB:def 13
for b1 being Point of (Topen_unit_circle c[10] ) ex b2, b3 being real number st
( b1 = |[b2,b3]| & ( b3 >= 0 implies a1 . b1 = (arccos b2) / (2 * PI ) ) & ( b3 <= 0 implies a1 . b1 = 1 - ((arccos b2) / (2 * PI )) ) );
existence
ex b1 being Function of (Topen_unit_circle c[10] ),(R^1 | (R^1 ].0,1.[)) st
for b2 being Point of (Topen_unit_circle c[10] ) ex b3, b4 being real number st
( b2 = |[b3,b4]| & ( b4 >= 0 implies b1 . b2 = (arccos b3) / (2 * PI ) ) & ( b4 <= 0 implies b1 . b2 = 1 - ((arccos b3) / (2 * PI )) ) )
proof end;
uniqueness
for b1, b2 being Function of (Topen_unit_circle c[10] ),(R^1 | (R^1 ].0,1.[)) st ( for b3 being Point of (Topen_unit_circle c[10] ) ex b4, b5 being real number st
( b3 = |[b4,b5]| & ( b5 >= 0 implies b1 . b3 = (arccos b4) / (2 * PI ) ) & ( b5 <= 0 implies b1 . b3 = 1 - ((arccos b4) / (2 * PI )) ) ) ) & ( for b3 being Point of (Topen_unit_circle c[10] ) ex b4, b5 being real number st
( b3 = |[b4,b5]| & ( b5 >= 0 implies b2 . b3 = (arccos b4) / (2 * PI ) ) & ( b5 <= 0 implies b2 . b3 = 1 - ((arccos b4) / (2 * PI )) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def13 defines Circle2IntervalR TOPREALB:def 13 :
for b1 being Function of (Topen_unit_circle c[10] ),(R^1 | (R^1 ].0,1.[)) holds
( b1 = Circle2IntervalR iff for b2 being Point of (Topen_unit_circle c[10] ) ex b3, b4 being real number st
( b2 = |[b3,b4]| & ( b4 >= 0 implies b1 . b2 = (arccos b3) / (2 * PI ) ) & ( b4 <= 0 implies b1 . b2 = 1 - ((arccos b3) / (2 * PI )) ) ) );

set c18 = R^1 ].(1 / 2),((1 / 2) + c5).[;

definition
func Circle2IntervalL -> Function of (Topen_unit_circle c[-10] ),(R^1 | (R^1 ].(1 / 2),(3 / 2).[)) means :Def14: :: TOPREALB:def 14
for b1 being Point of (Topen_unit_circle c[-10] ) ex b2, b3 being real number st
( b1 = |[b2,b3]| & ( b3 >= 0 implies a1 . b1 = 1 + ((arccos b2) / (2 * PI )) ) & ( b3 <= 0 implies a1 . b1 = 1 - ((arccos b2) / (2 * PI )) ) );
existence
ex b1 being Function of (Topen_unit_circle c[-10] ),(R^1 | (R^1 ].(1 / 2),(3 / 2).[)) st
for b2 being Point of (Topen_unit_circle c[-10] ) ex b3, b4 being real number st
( b2 = |[b3,b4]| & ( b4 >= 0 implies b1 . b2 = 1 + ((arccos b3) / (2 * PI )) ) & ( b4 <= 0 implies b1 . b2 = 1 - ((arccos b3) / (2 * PI )) ) )
proof end;
uniqueness
for b1, b2 being Function of (Topen_unit_circle c[-10] ),(R^1 | (R^1 ].(1 / 2),(3 / 2).[)) st ( for b3 being Point of (Topen_unit_circle c[-10] ) ex b4, b5 being real number st
( b3 = |[b4,b5]| & ( b5 >= 0 implies b1 . b3 = 1 + ((arccos b4) / (2 * PI )) ) & ( b5 <= 0 implies b1 . b3 = 1 - ((arccos b4) / (2 * PI )) ) ) ) & ( for b3 being Point of (Topen_unit_circle c[-10] ) ex b4, b5 being real number st
( b3 = |[b4,b5]| & ( b5 >= 0 implies b2 . b3 = 1 + ((arccos b4) / (2 * PI )) ) & ( b5 <= 0 implies b2 . b3 = 1 - ((arccos b4) / (2 * PI )) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def14 defines Circle2IntervalL TOPREALB:def 14 :
for b1 being Function of (Topen_unit_circle c[-10] ),(R^1 | (R^1 ].(1 / 2),(3 / 2).[)) holds
( b1 = Circle2IntervalL iff for b2 being Point of (Topen_unit_circle c[-10] ) ex b3, b4 being real number st
( b2 = |[b3,b4]| & ( b4 >= 0 implies b1 . b2 = 1 + ((arccos b3) / (2 * PI )) ) & ( b4 <= 0 implies b1 . b2 = 1 - ((arccos b3) / (2 * PI )) ) ) );

set c19 = Circle2IntervalR ;

set c20 = Circle2IntervalL ;

theorem Th43: :: TOPREALB:43
(CircleMap (R^1 0)) " = Circle2IntervalR
proof end;

theorem Th44: :: TOPREALB:44
(CircleMap (R^1 (1 / 2))) " = Circle2IntervalL
proof end;

set c21 = ].0,1.[;

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

set c23 = ].0,PI .];

set c24 = 1 / (2 * PI );

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

Lemma63: the carrier of (R^1 | (R^1 c25)) = R^1 c25
by JORDAN1:1;

Lemma64: the carrier of (R^1 | (R^1 c26)) = R^1 c26
by JORDAN1:1;

Lemma65: the carrier of (R^1 | (R^1 ].0,1.[)) = R^1 ].0,1.[
by JORDAN1:1;

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

dom (AffineMap (1 / (2 * PI )),0) = the carrier of R^1
by FUNCT_2:def 1, TOPMETR:24;

then Lemma66: dom ((AffineMap (1 / (2 * PI )),0) | (R^1 c26)) = R^1 c26
by RELAT_1:91;

rng ((AffineMap (1 / (2 * PI )),0) | (R^1 c26)) c= ].0,1.[
proof end;

then reconsider c28 = (AffineMap (1 / (2 * PI )),0) | (R^1 c26) as Function of (R^1 | (R^1 c26)),(R^1 | (R^1 ].0,1.[)) by Lemma64, Lemma65, Lemma66, FUNCT_2:4;

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

Lemma68: dom (AffineMap (1 / (2 * PI )),0) = REAL
by FUNCT_2:def 1;

Lemma69: rng (AffineMap (1 / (2 * PI )),0) = REAL
by JORDAN16:32;

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

R^1 | ([#] R^1 ) = R^1
by TSEP_1:3;

then ( R^1 = R^1 | (R^1 (dom (AffineMap (1 / (2 * PI )),0))) & R^1 = R^1 | (R^1 (rng (AffineMap (1 / (2 * PI )),0))) )
by Lemma68, Lemma69, Lemma70;

then reconsider c29 = c28 as continuous Function of (R^1 | (R^1 c26)),(R^1 | (R^1 ].0,1.[)) by Lemma67, TOPREALA:29;

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

Lemma71: dom (AffineMap (- 1),1) = REAL
by FUNCT_2:def 1;

then Lemma72: 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 c31 = (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 Lemma65, Lemma72, FUNCT_2:4;

Lemma73: rng (AffineMap (- 1),1) = REAL
by JORDAN16:32;

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

Lemma75: R^1 | ([#] R^1 ) = R^1
by TSEP_1:3;

then ( R^1 = R^1 | (R^1 (dom (AffineMap (- 1),1))) & R^1 = R^1 | (R^1 (rng (AffineMap (- 1),1))) )
by Lemma71, Lemma73, Lemma74;

then reconsider c32 = c31 as continuous Function of (R^1 | (R^1 ].0,1.[)),(R^1 | (R^1 ].0,1.[)) by TOPREALA:29;

reconsider c33 = 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 c34 = c33 | (R^1 c25);

c25 c= [.(- 1),1.]
by TOPREALA:11;

then Lemma76: dom (c33 | (R^1 c25)) = c25
by RELAT_1:91, SIN_COS6:88;

Lemma77: rng (c33 | (R^1 c25)) c= c26
proof end;

then reconsider c35 = c33 | (R^1 c25) as Function of (R^1 | (R^1 c25)),(R^1 | (R^1 c26)) by Lemma63, Lemma64, Lemma76, FUNCT_2:4;

the carrier of (R^1 | (R^1 [.(- 1),1.])) = R^1 [.(- 1),1.] by JORDAN1:1
.= [.(- 1),1.] ;

then reconsider c36 = R^1 c25 as Subset of (R^1 | (R^1 [.(- 1),1.])) by TOPREALA:11;

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

then reconsider c37 = R^1 c26 as Subset of (R^1 | (R^1 [.0,PI .])) by TOPREALA:15;

( (R^1 | (R^1 [.(- 1),1.])) | c36 = R^1 | (R^1 c25) & (R^1 | (R^1 [.0,PI .])) | c37 = R^1 | (R^1 c26) )
by GOBOARD9:4;

then Lemma78: c35 is continuous
by TOPREALA:29;

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

Lemma79: dom c38 = the carrier of (TOP-REAL 2)
by FUNCT_2:def 1;

Lemma80: c38 is continuous
by TOPREAL6:83;

Lemma81: for b1 being Subset of (Topen_unit_circle c[10] ) st b1 = { b2 where B is Point of (TOP-REAL 2) : ( b2 in the carrier of (Topen_unit_circle c[10] ) & 0 <= b2 `2 ) } holds
Circle2IntervalR | ((Topen_unit_circle c[10] ) | b1) is continuous
proof end;

Lemma82: for b1 being Subset of (Topen_unit_circle c[10] ) st b1 = { b2 where B is Point of (TOP-REAL 2) : ( b2 in the carrier of (Topen_unit_circle c[10] ) & 0 >= b2 `2 ) } holds
Circle2IntervalR | ((Topen_unit_circle c[10] ) | b1) is continuous
proof end;

Lemma83: for b1 being Point of (Topen_unit_circle c[10] ) st b1 = c[-10] holds
Circle2IntervalR is_continuous_at b1
proof end;

set c39 = REAL --> 1;

Lemma84: dom (REAL --> 1) = REAL
by FUNCOP_1:19;

rng (REAL --> 1) c= REAL
by XBOOLE_1:1;

then reconsider c40 = REAL --> 1 as PartFunc of REAL , REAL by Lemma84, RELSET_1:11;

Lemma85: Circle2IntervalR is continuous
proof end;

set c41 = ].(1 / 2),((1 / 2) + c5).[;

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

set c43 = [.0,PI .[;

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

Lemma86: the carrier of (R^1 | (R^1 c44)) = R^1 c44
by JORDAN1:1;

Lemma87: the carrier of (R^1 | (R^1 c45)) = R^1 c45
by JORDAN1:1;

Lemma88: the carrier of (R^1 | (R^1 ].(1 / 2),((1 / 2) + c5).[)) = R^1 ].(1 / 2),((1 / 2) + c5).[
by JORDAN1:1;

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

dom (AffineMap (- (1 / (2 * PI ))),1) = the carrier of R^1
by FUNCT_2:def 1, TOPMETR:24;

then Lemma89: dom ((AffineMap (- (1 / (2 * PI ))),1) | (R^1 c45)) = R^1 c45
by RELAT_1:91;

rng ((AffineMap (- (1 / (2 * PI ))),1) | (R^1 c45)) c= ].(1 / 2),((1 / 2) + c5).[
proof end;

then reconsider c47 = (AffineMap (- (1 / (2 * PI ))),1) | (R^1 c45) as Function of (R^1 | (R^1 c45)),(R^1 | (R^1 ].(1 / 2),((1 / 2) + c5).[)) by Lemma87, Lemma88, Lemma89, FUNCT_2:4;

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

Lemma91: dom (AffineMap (- (1 / (2 * PI ))),1) = REAL
by FUNCT_2:def 1;

rng (AffineMap (- (1 / (2 * PI ))),1) = REAL
by JORDAN16:32;

then ( R^1 = R^1 | (R^1 (dom (AffineMap (- (1 / (2 * PI ))),1))) & R^1 = R^1 | (R^1 (rng (AffineMap (- (1 / (2 * PI ))),1))) )
by Lemma74, Lemma75, Lemma91;

then reconsider c48 = c47 as continuous Function of (R^1 | (R^1 c45)),(R^1 | (R^1 ].(1 / 2),((1 / 2) + c5).[)) by Lemma90, TOPREALA:29;

set c49 = (AffineMap (1 / (2 * PI )),1) | (R^1 c45);

dom (AffineMap (1 / (2 * PI )),1) = the carrier of R^1
by FUNCT_2:def 1, TOPMETR:24;

then Lemma92: dom ((AffineMap (1 / (2 * PI )),1) | (R^1 c45)) = R^1 c45
by RELAT_1:91;

rng ((AffineMap (1 / (2 * PI )),1) | (R^1 c45)) c= ].(1 / 2),((1 / 2) + c5).[
proof end;

then reconsider c50 = (AffineMap (1 / (2 * PI )),1) | (R^1 c45) as Function of (R^1 | (R^1 c45)),(R^1 | (R^1 ].(1 / 2),((1 / 2) + c5).[)) by Lemma87, Lemma88, Lemma92, FUNCT_2:4;

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

Lemma94: dom (AffineMap (1 / (2 * PI )),1) = REAL
by FUNCT_2:def 1;

rng (AffineMap (1 / (2 * PI )),1) = REAL
by JORDAN16:32;

then ( R^1 = R^1 | (R^1 (dom (AffineMap (1 / (2 * PI )),1))) & R^1 = R^1 | (R^1 (rng (AffineMap (1 / (2 * PI )),1))) )
by Lemma74, Lemma75, Lemma94;

then reconsider c51 = c50 as continuous Function of (R^1 | (R^1 c45)),(R^1 | (R^1 ].(1 / 2),((1 / 2) + c5).[)) by Lemma93, TOPREALA:29;

set c52 = c33 | (R^1 c44);

c44 c= [.(- 1),1.]
by TOPREALA:15;

then Lemma95: dom (c33 | (R^1 c44)) = c44
by RELAT_1:91, SIN_COS6:88;

Lemma96: rng (c33 | (R^1 c44)) c= c45
proof end;

then reconsider c53 = c33 | (R^1 c44) as Function of (R^1 | (R^1 c44)),(R^1 | (R^1 c45)) by Lemma86, Lemma87, Lemma95, FUNCT_2:4;

the carrier of (R^1 | (R^1 [.(- 1),1.])) = R^1 [.(- 1),1.] by JORDAN1:1
.= [.(- 1),1.] ;

then reconsider c54 = R^1 c44 as Subset of (R^1 | (R^1 [.(- 1),1.])) by TOPREALA:15;

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

then reconsider c55 = R^1 c45 as Subset of (R^1 | (R^1 [.0,PI .])) by TOPREALA:11;

( (R^1 | (R^1 [.(- 1),1.])) | c54 = R^1 | (R^1 c44) & (R^1 | (R^1 [.0,PI .])) | c55 = R^1 | (R^1 c45) )
by GOBOARD9:4;

then Lemma97: c53 is continuous
by TOPREALA:29;

Lemma98: for b1 being Subset of (Topen_unit_circle c[-10] ) st b1 = { b2 where B is Point of (TOP-REAL 2) : ( b2 in the carrier of (Topen_unit_circle c[-10] ) & 0 <= b2 `2 ) } holds
Circle2IntervalL | ((Topen_unit_circle c[-10] ) | b1) is continuous
proof end;

Lemma99: for b1 being Subset of (Topen_unit_circle c[-10] ) st b1 = { b2 where B is Point of (TOP-REAL 2) : ( b2 in the carrier of (Topen_unit_circle c[-10] ) & 0 >= b2 `2 ) } holds
Circle2IntervalL | ((Topen_unit_circle c[-10] ) | b1) is continuous
proof end;

Lemma100: for b1 being Point of (Topen_unit_circle c[-10] ) st b1 = c[10] holds
Circle2IntervalL is_continuous_at b1
proof end;

Lemma101: 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 )
proof end;
cluster Circle2IntervalL -> one-to-one onto continuous ;
coherence
( Circle2IntervalL is one-to-one & Circle2IntervalL is onto & Circle2IntervalL is continuous ) by Lemma101, Lemma47, Th44, WAYBEL29:1;
end;

Lemma102: CircleMap (R^1 0) is open
proof end;

Lemma103: CircleMap (R^1 (1 / 2)) is open
by Lemma47, Th44, TOPREALA:35;

registration
let c56 be Integer;
cluster CircleMap (R^1 a1) -> one-to-one onto continuous open ;
coherence
CircleMap (R^1 c56) is open
proof end;
cluster CircleMap (R^1 ((1 / 2) + a1)) -> one-to-one onto continuous open ;
coherence
CircleMap (R^1 ((1 / 2) + c56)) is open
proof end;
end;

registration
cluster Circle2IntervalR -> one-to-one onto continuous open ;
coherence
Circle2IntervalR is open
proof end;
cluster Circle2IntervalL -> one-to-one onto continuous open ;
coherence
Circle2IntervalL is open by Lemma47, Th44, TOPREALA:34;
end;

theorem Th45: :: TOPREALB:45
canceled;

theorem Th46: :: TOPREALB:46
CircleMap (R^1 (1 / 2)) is_homeomorphism
proof end;

theorem Th47: :: TOPREALB:47
canceled;

theorem Th48: :: TOPREALB:48
canceled;

theorem Th49: :: TOPREALB:49
ex b1 being Subset-Family of (Tunit_circle 2) st
( b1 = {(CircleMap .: ].0,1.[),(CircleMap .: ].(1 / 2),(3 / 2).[)} & b1 is_a_cover_of Tunit_circle 2 & b1 is open & ( for b2 being Subset of (Tunit_circle 2) holds
( ( b2 = CircleMap .: ].0,1.[ implies ( union (IntIntervals 0,1) = CircleMap " b2 & ( for b3 being Subset of R^1 st b3 in IntIntervals 0,1 holds
for b4 being Function of (R^1 | b3),((Tunit_circle 2) | b2) st b4 = CircleMap | b3 holds
b4 is_homeomorphism ) ) ) & ( b2 = CircleMap .: ].(1 / 2),(3 / 2).[ implies ( union (IntIntervals (1 / 2),(3 / 2)) = CircleMap " b2 & ( for b3 being Subset of R^1 st b3 in IntIntervals (1 / 2),(3 / 2) holds
for b4 being Function of (R^1 | b3),((Tunit_circle 2) | b2) st b4 = CircleMap | b3 holds
b4 is_homeomorphism ) ) ) ) ) )
proof end;