reconsider A1 = R^1 ].(1 / 2),((1 / 2) + p1).[ as non empty Subset of R^1 ;
set f = CircleMap (R^1 (1 / 2));
set Y = the carrier of (R^1 | A1);
reconsider f = CircleMap (R^1 (1 / 2)) as Function of (R^1 | A1),(Topen_unit_circle c[-10]) by Lm19;
set G = AffineMap ((2 * PI),0);
A1:
dom (id the carrier of (R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[))) = the carrier of (R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[))
by RELAT_1:45;
A2:
rng f = the carrier of (Topen_unit_circle c[-10])
by Lm19, FUNCT_2:def 3;
A3:
the carrier of (R^1 | A1) = A1
by PRE_TOPC:8;
A4:
now for a being object st a in dom (Circle2IntervalL * f) holds
(Circle2IntervalL * f) . a = (id the carrier of (R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[))) . alet a be
object ;
( a in dom (Circle2IntervalL * f) implies (Circle2IntervalL * f) . a = (id the carrier of (R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[))) . a )assume A5:
a in dom (Circle2IntervalL * f)
;
(Circle2IntervalL * f) . a = (id the carrier of (R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[))) . athen reconsider b =
a as
Point of
(R^1 | A1) ;
reconsider c =
b as
Real ;
consider x,
y being
Real such that A6:
f . b = |[x,y]|
and A7:
(
y >= 0 implies
Circle2IntervalL . (f . b) = 1
+ ((arccos x) / (2 * PI)) )
and A8:
(
y <= 0 implies
Circle2IntervalL . (f . b) = 1
- ((arccos x) / (2 * PI)) )
by Def14;
A9:
f . b =
CircleMap . b
by A3, FUNCT_1:49
.=
|[(cos ((2 * PI) * c)),(sin ((2 * PI) * c))]|
by Def11
;
then A10:
y = sin ((2 * PI) * c)
by A6, SPPOL_2:1;
A11:
1
/ 2
< c
by A3, XXREAL_1:4;
then
(2 * PI) * (1 / 2) < (2 * PI) * c
by XREAL_1:68;
then A12:
PI + ((2 * PI) * 0) < (2 * PI) * c
;
A13:
c < 3
/ 2
by A3, XXREAL_1:4;
then
c - 1
< (3 / 2) - 1
by XREAL_1:9;
then A14:
(2 * PI) * (c - 1) <= (2 * PI) * (1 / 2)
by XREAL_1:64;
(2 * PI) * c <= (2 * PI) * ((1 / 2) + 1)
by A13, XREAL_1:64;
then A15:
(2 * PI) * c <= PI + ((2 * PI) * 1)
;
A16:
(AffineMap ((2 * PI),0)) . (1 - c) = ((2 * PI) * (1 - c)) + 0
by FCONT_1:def 4;
then A17:
((AffineMap ((2 * PI),0)) . (1 - c)) / ((2 * PI) * 1) = (1 - c) / 1
by XCMPLX_1:91;
A18:
x =
cos ((2 * PI) * c)
by A6, A9, SPPOL_2:1
.=
cos (((2 * PI) * c) + ((2 * PI) * (- 1)))
by COMPLEX2:9
.=
cos ((2 * PI) * (c - 1))
;
A19:
now Circle2IntervalL . (f . b) = bper cases
( c >= 1 or c < 1 )
;
suppose A22:
c < 1
;
Circle2IntervalL . (f . b) = bthen
(2 * PI) * c < (2 * PI) * 1
by XREAL_1:68;
then A23:
(2 * PI) * c < (2 * PI) + ((2 * PI) * 0)
;
1
- c < 1
- (1 / 2)
by A11, XREAL_1:15;
then A24:
(2 * PI) * (1 - c) <= (2 * PI) * (1 / 2)
by XREAL_1:64;
A25:
1
- 1
<= 1
- c
by A22, XREAL_1:15;
arccos x =
arccos (cos ((2 * PI) * c))
by A6, A9, SPPOL_2:1
.=
arccos (cos (- ((2 * PI) * c)))
by SIN_COS:31
.=
arccos (cos (((2 * PI) * (- c)) + ((2 * PI) * 1)))
by COMPLEX2:9
.=
(AffineMap ((2 * PI),0)) . (1 - c)
by A16, A25, A24, SIN_COS6:92
;
hence
Circle2IntervalL . (f . b) = b
by A8, A10, A17, A12, A23, SIN_COS6:12;
verum end; end; end; thus (Circle2IntervalL * f) . a =
Circle2IntervalL . (f . b)
by A5, FUNCT_1:12
.=
(id the carrier of (R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[))) . a
by A19
;
verum end;
dom (Circle2IntervalL * f) = the carrier of (R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[))
by FUNCT_2:def 1;
then
Circle2IntervalL = f "
by A2, A1, A4, FUNCT_1:2, FUNCT_2:30;
hence
(CircleMap (R^1 (1 / 2))) " = Circle2IntervalL
by TOPS_2:def 4; verum