:: TOPREALB semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

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 ].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;

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

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

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

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

Lm9: 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;

Lm10: 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
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, r, b being real number holds sin ((a * r) + b) = (sin * (AffineMap a,b)) . r
proof end;

theorem Th2: :: TOPREALB:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, r, b being real number holds cos ((a * r) + b) = (cos * (AffineMap a,b)) . r
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 )
proof end;
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;

:: 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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).[ ) ;

registration
let a, b be real number ;
cluster IntIntervals a,b -> non empty ;
coherence
not IntIntervals a,b is empty
proof end;
end;

theorem :: TOPREALB:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for b, a being real number st b - a <= 1 holds
IntIntervals a,b is mutually-disjoint
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
proof end;
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
proof end;
end;

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;

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

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

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

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

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

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

registration
let A be closed Subset of REAL ;
cluster R^1 | (R^1 A) -> closed ;
coherence
R^1 | (R^1 A) is closed
proof end;
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)))
proof end;
end;

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

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

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

theorem Th5: :: TOPREALB:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
R^1 | (R^1 ([#] REAL )) = R^1
proof end;

theorem Th6: :: TOPREALB:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being PartFunc of REAL , REAL st dom f = REAL holds
R^1 | (R^1 (dom f)) = R^1
proof end;

theorem Th7: :: TOPREALB:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being Function of REAL , REAL holds f is Function of R^1 ,(R^1 | (R^1 (rng f)))
proof end;

theorem Th8: :: TOPREALB:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being Function of REAL , REAL holds f is Function of R^1 ,R^1
proof end;

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

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

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

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

Lm13: 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: dom (AffineMap a,b) = REAL by FUNCT_2:def 1;
A2: rng (AffineMap a,b) = REAL by JORDAN16:32;
A3: [#] 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 a,b))) & R^1 = R^1 | (R^1 (rng (AffineMap a,b))) ) by A1, A2, A3; :: thesis: verum
end;

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

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;

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

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

theorem Th9: :: TOPREALB:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
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
proof end;
end;

theorem Th10: :: TOPREALB:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r being real number holds Tcircle (0.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 -> non empty strict compact arcwise_connected being_simple_closed_curve ;
coherence
Tcircle x,r 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 :: TOPREALB:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S, T being being_simple_closed_curve SubSpace of TOP-REAL 2 holds S,T are_homeomorphic
proof end;

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

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

set TUC = Tunit_circle 2;

set cS1 = the carrier of (Tunit_circle 2);

Lm14: 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;

theorem Th12: :: TOPREALB:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being non empty Nat
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem Th14: :: TOPREALB:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being Point of (TOP-REAL 2) st x is Point of (Tunit_circle 2) & x `1 = 1 holds
x `2 = 0
proof end;

theorem Th15: :: TOPREALB:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being Point of (TOP-REAL 2) st x is Point of (Tunit_circle 2) & x `1 = - 1 holds
x `2 = 0
proof end;

theorem :: TOPREALB:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being Point of (TOP-REAL 2) st x is Point of (Tunit_circle 2) & x `2 = 1 holds
x `1 = 0
proof end;

theorem :: TOPREALB:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being Point of (TOP-REAL 2) st x is Point of (Tunit_circle 2) & x `2 = - 1 holds
x `1 = 0
proof end;

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

theorem :: TOPREALB:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
Tunit_circle 2 is SubSpace of Trectangle (- 1),1,(- 1),1 by Th10;

theorem Th19: :: TOPREALB:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being non empty 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_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;

Lm15: for n being non empty 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being non empty 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
proof end;

registration
let x be Point of (TOP-REAL 2);
let r be real non negative number ;
cluster Tcircle x,r -> non empty strict arcwise_connected ;
coherence
Tcircle x,r 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 defines c[10] TOPREALB:def 8 :
c[10] = |[1,0]|;

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

theorem Th21: :: TOPREALB:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 b1 being strict SubSpace of Tunit_circle 2 st the carrier of b1 = the carrier of (Tunit_circle 2) \ {p}
proof end;
uniqueness
for b1, b2 being strict SubSpace of Tunit_circle 2 st the carrier of b1 = the carrier of (Tunit_circle 2) \ {p} & the carrier of b2 = the carrier of (Tunit_circle 2) \ {p} holds
b1 = b2
by TSEP_1:5;
end;

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

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

theorem Th22: :: TOPREALB:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Point of (Tunit_circle 2) holds p is not Point of (Topen_unit_circle p)
proof end;

theorem Th23: :: TOPREALB:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Point of (Tunit_circle 2) st p <> q holds
q is Point of (Topen_unit_circle p)
proof end;

theorem Th25: :: TOPREALB:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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]
proof end;

theorem Th26: :: TOPREALB:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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]
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem Th28: :: TOPREALB:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem Th29: :: TOPREALB:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

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

theorem :: TOPREALB:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Point of (Tunit_circle 2) holds Topen_unit_circle p, I(01) are_homeomorphic
proof end;

theorem :: TOPREALB:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Point of (Tunit_circle 2) holds Topen_unit_circle p, Topen_unit_circle q are_homeomorphic
proof end;

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 b1 being Function of R^1 ,(Tunit_circle 2) st
for x being real number holds b1 . x = |[(cos ((2 * PI ) * x)),(sin ((2 * PI ) * x))]|
proof end;
uniqueness
for b1, b2 being Function of R^1 ,(Tunit_circle 2) st ( for x being real number holds b1 . x = |[(cos ((2 * PI ) * x)),(sin ((2 * PI ) * x))]| ) & ( for x being real number holds b2 . x = |[(cos ((2 * PI ) * x)),(sin ((2 * PI ) * x))]| ) 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 x being real number holds b1 . x = |[(cos ((2 * PI ) * x)),(sin ((2 * PI ) * x))]| );

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

theorem Th32: :: TOPREALB:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Integer
for r being real number holds CircleMap . r = CircleMap . (r + i)
proof end;

theorem Th33: :: TOPREALB:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Integer holds CircleMap . i = c[10]
proof end;

theorem Th34: :: TOPREALB:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
CircleMap " {c[10] } = INT
proof end;

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

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

theorem Th35: :: TOPREALB:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r being real number st frac r = 1 / 2 holds
CircleMap . r = |[(- 1),0]|
proof end;

theorem :: TOPREALB:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r being real number st frac r = 1 / 4 holds
CircleMap . r = |[0,1]|
proof end;

theorem :: TOPREALB:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r being real number st frac r = 3 / 4 holds
CircleMap . r = |[0,(- 1)]|
proof end;

Lm21: 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)]|
proof end;

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

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

Lm23: 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

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

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

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

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

theorem Th40: :: TOPREALB:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th41: :: TOPREALB:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being real number
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))
proof end;
end;

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

Lm25: 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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).[)
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 )
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 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 b1 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 b1 . p = (arccos x) / (2 * PI ) ) & ( y <= 0 implies b1 . p = 1 - ((arccos x) / (2 * PI )) ) )
proof end;
uniqueness
for b1, b2 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 b1 . p = (arccos x) / (2 * PI ) ) & ( y <= 0 implies b1 . 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 b2 . p = (arccos x) / (2 * PI ) ) & ( y <= 0 implies b2 . p = 1 - ((arccos x) / (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 p being Point of (Topen_unit_circle c[10] ) ex x, y being real number st
( p = |[x,y]| & ( y >= 0 implies b1 . p = (arccos x) / (2 * PI ) ) & ( y <= 0 implies b1 . p = 1 - ((arccos x) / (2 * PI )) ) ) );

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 b1 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 b1 . p = 1 + ((arccos x) / (2 * PI )) ) & ( y <= 0 implies b1 . p = 1 - ((arccos x) / (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 p being Point of (Topen_unit_circle c[-10] ) ex x, y being real number st
( p = |[x,y]| & ( y >= 0 implies b1 . p = 1 + ((arccos x) / (2 * PI )) ) & ( y <= 0 implies b1 . 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 b2 . p = 1 + ((arccos x) / (2 * PI )) ) & ( y <= 0 implies b2 . p = 1 - ((arccos x) / (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 p being Point of (Topen_unit_circle c[-10] ) ex x, y being real number st
( p = |[x,y]| & ( y >= 0 implies b1 . p = 1 + ((arccos x) / (2 * PI )) ) & ( y <= 0 implies b1 . p = 1 - ((arccos x) / (2 * PI )) ) ) );

set C = Circle2IntervalR ;

set Cm = Circle2IntervalL ;

theorem Th43: :: TOPREALB:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
(CircleMap (R^1 0)) " = Circle2IntervalR
proof end;

theorem Th44: :: TOPREALB:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
(CircleMap (R^1 (1 / 2))) " = Circle2IntervalL
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 ;

Lm26: the carrier of (R^1 | (R^1 Q)) = R^1 Q
by JORDAN1:1;

Lm27: the carrier of (R^1 | (R^1 E)) = R^1 E
by JORDAN1:1;

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

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 Lm29: 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 Lm27, Lm28, Lm29, FUNCT_2:4;

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

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

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

Lm33: [#] 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 Lm31, Lm32, Lm33;

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

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

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

then Lm35: 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 Lm28, Lm35, FUNCT_2:4;

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

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

Lm38: 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 Lm34, Lm36, Lm37;

then reconsider L = L as continuous Function of (R^1 | (R^1 ].0,1.[)),(R^1 | (R^1 ].0,1.[)) by 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);

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

then Lm39: dom (ac | (R^1 Q)) = Q
by RELAT_1:91, SIN_COS6:88;

Lm40: 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 Lm26, Lm27, Lm39, FUNCT_2:4;

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

then reconsider QQ = R^1 Q 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 EE = R^1 E as Subset of (R^1 | (R^1 [.0,PI .])) by TOPREALA:15;

( (R^1 | (R^1 [.(- 1),1.])) | QQ = R^1 | (R^1 Q) & (R^1 | (R^1 [.0,PI .])) | EE = R^1 | (R^1 E) )
by GOBOARD9:4;

then Lm41: c is continuous
by TOPREALA:29;

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

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

Lm43: p is continuous
by TOPREAL6:83;

Lm44: 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;

Lm45: 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;

Lm46: 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;

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

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

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

Lm48: 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 ;

Lm49: the carrier of (R^1 | (R^1 Q)) = R^1 Q
by JORDAN1:1;

Lm50: the carrier of (R^1 | (R^1 E)) = R^1 E
by JORDAN1:1;

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

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 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 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 Lm50, Lm51, 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 ( 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 Lm37, Lm38, Lm54;

then reconsider Af = Af as continuous Function of (R^1 | (R^1 E)),(R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[)) by Lm53, 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 Lm55: 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 Lm50, Lm51, Lm55, FUNCT_2:4;

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

Lm57: 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 Lm37, Lm38, Lm57;

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

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

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

then Lm58: dom (ac | (R^1 Q)) = Q
by RELAT_1:91, SIN_COS6:88;

Lm59: 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 Lm49, Lm50, Lm58, FUNCT_2:4;

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

then reconsider QQ = R^1 Q 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 EE = R^1 E as Subset of (R^1 | (R^1 [.0,PI .])) by TOPREALA:11;

( (R^1 | (R^1 [.(- 1),1.])) | QQ = R^1 | (R^1 Q) & (R^1 | (R^1 [.0,PI .])) | EE = R^1 | (R^1 E) )
by GOBOARD9:4;

then Lm60: c is continuous
by TOPREALA:29;

Lm61: 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;

Lm62: 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;

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

Lm64: 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 Lm64, Lm19, Th44, WAYBEL29:1;
end;

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

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

registration
let i be Integer;
cluster CircleMap (R^1 i) -> one-to-one onto continuous open ;
coherence
CircleMap (R^1 i) is open
proof end;
cluster CircleMap (R^1 ((1 / 2) + i)) -> one-to-one onto continuous open ;
coherence
CircleMap (R^1 ((1 / 2) + i)) 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 Lm19, Th44, TOPREALA:34;
end;

theorem :: TOPREALB:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: TOPREALB:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
CircleMap (R^1 (1 / 2)) is_homeomorphism
proof end;

theorem :: TOPREALB:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: TOPREALB:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: TOPREALB:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
ex F being Subset-Family of (Tunit_circle 2) st
( F = {(CircleMap .: ].0,1.[),(CircleMap .: ].(1 / 2),(3 / 2).[)} & F is_a_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_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_homeomorphism ) ) ) ) ) )
proof end;