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;

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

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 :: thesis: 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).[))) . a

dom (Circle2IntervalL * f) = the carrier of (R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[))
by FUNCT_2:def 1;(Circle2IntervalL * f) . a = (id the carrier of (R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[))) . a

let a be object ; :: thesis: ( 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) ; :: thesis: (Circle2IntervalL * f) . a = (id the carrier of (R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[))) . a

then 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)) ;

.= (id the carrier of (R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[))) . a by A19 ; :: thesis: verum

end;assume A5: a in dom (Circle2IntervalL * f) ; :: thesis: (Circle2IntervalL * f) . a = (id the carrier of (R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[))) . a

then 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 :: thesis: Circle2IntervalL . (f . b) = bend;

thus (Circle2IntervalL * f) . a =
Circle2IntervalL . (f . b)
by A5, FUNCT_1:12
per cases
( c >= 1 or c < 1 )
;

end;

suppose A20:
c >= 1
; :: thesis: Circle2IntervalL . (f . b) = b

then A21:
1 - 1 <= c - 1
by XREAL_1:9;

(2 * PI) * c >= (2 * PI) * 1 by A20, XREAL_1:64;

hence Circle2IntervalL . (f . b) = 1 + (((2 * PI) * (c - 1)) / (2 * PI)) by A7, A18, A10, A14, A15, A21, SIN_COS6:16, SIN_COS6:92

.= 1 + (c - 1) by XCMPLX_1:89

.= b ;

:: thesis: verum

end;(2 * PI) * c >= (2 * PI) * 1 by A20, XREAL_1:64;

hence Circle2IntervalL . (f . b) = 1 + (((2 * PI) * (c - 1)) / (2 * PI)) by A7, A18, A10, A14, A15, A21, SIN_COS6:16, SIN_COS6:92

.= 1 + (c - 1) by XCMPLX_1:89

.= b ;

:: thesis: verum

suppose A22:
c < 1
; :: thesis: Circle2IntervalL . (f . b) = b

then
(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; :: thesis: verum

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

.= (id the carrier of (R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[))) . a by A19 ; :: thesis: verum

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