reconsider A = R^1 ].0,1.[ as non empty Subset of R^1 ;

set f = CircleMap (R^1 0);

set Y = the carrier of (R^1 | A);

reconsider f = CircleMap (R^1 0) as Function of (R^1 | A),(Topen_unit_circle c[10]) by Th32;

reconsider r0 = In (0,REAL) as Point of R^1 by TOPMETR:17;

set F = AffineMap ((2 * PI),0);

A1: dom (id the carrier of (R^1 | A)) = the carrier of (R^1 | A) by RELAT_1:45;

CircleMap . r0 = c[10] by Th32;

then A2: rng f = the carrier of (Topen_unit_circle c[10]) by FUNCT_2:def 3;

A3: the carrier of (R^1 | A) = A by PRE_TOPC:8;

then Circle2IntervalR = f " by A2, A1, A4, FUNCT_1:2, FUNCT_2:30;

hence (CircleMap (R^1 0)) " = Circle2IntervalR by TOPS_2:def 4; :: thesis: verum

set f = CircleMap (R^1 0);

set Y = the carrier of (R^1 | A);

reconsider f = CircleMap (R^1 0) as Function of (R^1 | A),(Topen_unit_circle c[10]) by Th32;

reconsider r0 = In (0,REAL) as Point of R^1 by TOPMETR:17;

set F = AffineMap ((2 * PI),0);

A1: dom (id the carrier of (R^1 | A)) = the carrier of (R^1 | A) by RELAT_1:45;

CircleMap . r0 = c[10] by Th32;

then A2: rng f = the carrier of (Topen_unit_circle c[10]) by FUNCT_2:def 3;

A3: the carrier of (R^1 | A) = A by PRE_TOPC:8;

A4: now :: thesis: for a being object st a in dom (Circle2IntervalR * f) holds

(Circle2IntervalR * f) . a = (id the carrier of (R^1 | A)) . a

dom (Circle2IntervalR * f) = the carrier of (R^1 | A)
by FUNCT_2:def 1;(Circle2IntervalR * f) . a = (id the carrier of (R^1 | A)) . a

let a be object ; :: thesis: ( a in dom (Circle2IntervalR * f) implies (Circle2IntervalR * f) . a = (id the carrier of (R^1 | A)) . a )

assume A5: a in dom (Circle2IntervalR * f) ; :: thesis: (Circle2IntervalR * f) . a = (id the carrier of (R^1 | A)) . a

then reconsider b = a as Point of (R^1 | A) ;

reconsider c = b as Element of REAL by XREAL_0:def 1;

consider x, y being Real such that

A6: f . b = |[x,y]| and

A7: ( y >= 0 implies Circle2IntervalR . (f . b) = (arccos x) / (2 * PI) ) and

A8: ( y <= 0 implies Circle2IntervalR . (f . b) = 1 - ((arccos x) / (2 * PI)) ) by Def13;

A9: f . b = CircleMap . b by A3, FUNCT_1:49

.= |[((cos * (AffineMap ((2 * PI),0))) . c),((sin * (AffineMap ((2 * PI),0))) . c)]| by Lm20 ;

then y = (sin * (AffineMap ((2 * PI),0))) . c by A6, SPPOL_2:1;

then A10: y = sin . ((AffineMap ((2 * PI),0)) . c) by FUNCT_2:15;

x = (cos * (AffineMap ((2 * PI),0))) . c by A6, A9, SPPOL_2:1;

then x = cos . ((AffineMap ((2 * PI),0)) . c) by FUNCT_2:15;

then A11: x = cos ((AffineMap ((2 * PI),0)) . c) by SIN_COS:def 19;

A12: c < 1 by A3, XXREAL_1:4;

A13: (AffineMap ((2 * PI),0)) . c = ((2 * PI) * c) + 0 by FCONT_1:def 4;

then A14: ((AffineMap ((2 * PI),0)) . c) / ((2 * PI) * 1) = c / 1 by XCMPLX_1:91;

A15: (AffineMap ((2 * PI),0)) . (1 - c) = ((2 * PI) * (1 - c)) + 0 by FCONT_1:def 4;

then A16: ((AffineMap ((2 * PI),0)) . (1 - c)) / ((2 * PI) * 1) = (1 - c) / 1 by XCMPLX_1:91;

.= (id the carrier of (R^1 | A)) . a by A17 ; :: thesis: verum

end;assume A5: a in dom (Circle2IntervalR * f) ; :: thesis: (Circle2IntervalR * f) . a = (id the carrier of (R^1 | A)) . a

then reconsider b = a as Point of (R^1 | A) ;

reconsider c = b as Element of REAL by XREAL_0:def 1;

consider x, y being Real such that

A6: f . b = |[x,y]| and

A7: ( y >= 0 implies Circle2IntervalR . (f . b) = (arccos x) / (2 * PI) ) and

A8: ( y <= 0 implies Circle2IntervalR . (f . b) = 1 - ((arccos x) / (2 * PI)) ) by Def13;

A9: f . b = CircleMap . b by A3, FUNCT_1:49

.= |[((cos * (AffineMap ((2 * PI),0))) . c),((sin * (AffineMap ((2 * PI),0))) . c)]| by Lm20 ;

then y = (sin * (AffineMap ((2 * PI),0))) . c by A6, SPPOL_2:1;

then A10: y = sin . ((AffineMap ((2 * PI),0)) . c) by FUNCT_2:15;

x = (cos * (AffineMap ((2 * PI),0))) . c by A6, A9, SPPOL_2:1;

then x = cos . ((AffineMap ((2 * PI),0)) . c) by FUNCT_2:15;

then A11: x = cos ((AffineMap ((2 * PI),0)) . c) by SIN_COS:def 19;

A12: c < 1 by A3, XXREAL_1:4;

A13: (AffineMap ((2 * PI),0)) . c = ((2 * PI) * c) + 0 by FCONT_1:def 4;

then A14: ((AffineMap ((2 * PI),0)) . c) / ((2 * PI) * 1) = c / 1 by XCMPLX_1:91;

A15: (AffineMap ((2 * PI),0)) . (1 - c) = ((2 * PI) * (1 - c)) + 0 by FCONT_1:def 4;

then A16: ((AffineMap ((2 * PI),0)) . (1 - c)) / ((2 * PI) * 1) = (1 - c) / 1 by XCMPLX_1:91;

A17: now :: thesis: Circle2IntervalR . (f . b) = bend;

thus (Circle2IntervalR * f) . a =
Circle2IntervalR . (f . b)
by A5, FUNCT_1:12
per cases
( y >= 0 or y < 0 )
;

end;

suppose A18:
y >= 0
; :: thesis: Circle2IntervalR . (f . b) = b

then
not (AffineMap ((2 * PI),0)) . c in ].PI,(2 * PI).[
by A10, COMPTRIG:9;

then ( (AffineMap ((2 * PI),0)) . c <= PI or (AffineMap ((2 * PI),0)) . c >= 2 * PI ) by XXREAL_1:4;

then ( ((AffineMap ((2 * PI),0)) . c) / (2 * PI) <= (1 * PI) / (2 * PI) or ((AffineMap ((2 * PI),0)) . c) / (2 * PI) >= (2 * PI) / (2 * PI) ) by XREAL_1:72;

then c <= 1 / 2 by A14, A12, XCMPLX_1:60, XCMPLX_1:91;

then A19: (2 * PI) * c <= (2 * PI) * (1 / 2) by XREAL_1:64;

0 <= c by A3, XXREAL_1:4;

hence Circle2IntervalR . (f . b) = ((AffineMap ((2 * PI),0)) . c) / (2 * PI) by A7, A11, A13, A18, A19, SIN_COS6:92

.= b by A13, XCMPLX_1:89 ;

:: thesis: verum

end;then ( (AffineMap ((2 * PI),0)) . c <= PI or (AffineMap ((2 * PI),0)) . c >= 2 * PI ) by XXREAL_1:4;

then ( ((AffineMap ((2 * PI),0)) . c) / (2 * PI) <= (1 * PI) / (2 * PI) or ((AffineMap ((2 * PI),0)) . c) / (2 * PI) >= (2 * PI) / (2 * PI) ) by XREAL_1:72;

then c <= 1 / 2 by A14, A12, XCMPLX_1:60, XCMPLX_1:91;

then A19: (2 * PI) * c <= (2 * PI) * (1 / 2) by XREAL_1:64;

0 <= c by A3, XXREAL_1:4;

hence Circle2IntervalR . (f . b) = ((AffineMap ((2 * PI),0)) . c) / (2 * PI) by A7, A11, A13, A18, A19, SIN_COS6:92

.= b by A13, XCMPLX_1:89 ;

:: thesis: verum

suppose A20:
y < 0
; :: thesis: Circle2IntervalR . (f . b) = b

then
not (AffineMap ((2 * PI),0)) . c in [.0,PI.]
by A10, COMPTRIG:8;

then ( (AffineMap ((2 * PI),0)) . c < 0 or (AffineMap ((2 * PI),0)) . c > PI ) by XXREAL_1:1;

then ( ((AffineMap ((2 * PI),0)) . c) / (2 * PI) < 0 / (2 * PI) or ((AffineMap ((2 * PI),0)) . c) / (2 * PI) > (1 * PI) / (2 * PI) ) by XREAL_1:74;

then ( c < 0 or c > 1 / 2 ) by A14, XCMPLX_1:91;

then 1 - c < 1 - (1 / 2) by A3, XREAL_1:15, XXREAL_1:4;

then A21: (2 * PI) * (1 - c) <= (2 * PI) * (1 / 2) by XREAL_1:64;

A22: 1 - c > 1 - 1 by A12, XREAL_1:15;

cos . ((AffineMap ((2 * PI),0)) . (1 - c)) = cos ((- ((2 * PI) * c)) + ((2 * PI) * 1)) by A15, SIN_COS:def 19

.= cos (- ((2 * PI) * c)) by COMPLEX2:9

.= cos ((2 * PI) * c) by SIN_COS:31 ;

then arccos x = arccos (cos ((AffineMap ((2 * PI),0)) . (1 - c))) by A11, A13, SIN_COS:def 19

.= (AffineMap ((2 * PI),0)) . (1 - c) by A15, A22, A21, SIN_COS6:92 ;

hence Circle2IntervalR . (f . b) = b by A8, A16, A20; :: thesis: verum

end;then ( (AffineMap ((2 * PI),0)) . c < 0 or (AffineMap ((2 * PI),0)) . c > PI ) by XXREAL_1:1;

then ( ((AffineMap ((2 * PI),0)) . c) / (2 * PI) < 0 / (2 * PI) or ((AffineMap ((2 * PI),0)) . c) / (2 * PI) > (1 * PI) / (2 * PI) ) by XREAL_1:74;

then ( c < 0 or c > 1 / 2 ) by A14, XCMPLX_1:91;

then 1 - c < 1 - (1 / 2) by A3, XREAL_1:15, XXREAL_1:4;

then A21: (2 * PI) * (1 - c) <= (2 * PI) * (1 / 2) by XREAL_1:64;

A22: 1 - c > 1 - 1 by A12, XREAL_1:15;

cos . ((AffineMap ((2 * PI),0)) . (1 - c)) = cos ((- ((2 * PI) * c)) + ((2 * PI) * 1)) by A15, SIN_COS:def 19

.= cos (- ((2 * PI) * c)) by COMPLEX2:9

.= cos ((2 * PI) * c) by SIN_COS:31 ;

then arccos x = arccos (cos ((AffineMap ((2 * PI),0)) . (1 - c))) by A11, A13, SIN_COS:def 19

.= (AffineMap ((2 * PI),0)) . (1 - c) by A15, A22, A21, SIN_COS6:92 ;

hence Circle2IntervalR . (f . b) = b by A8, A16, A20; :: thesis: verum

.= (id the carrier of (R^1 | A)) . a by A17 ; :: thesis: verum

then Circle2IntervalR = f " by A2, A1, A4, FUNCT_1:2, FUNCT_2:30;

hence (CircleMap (R^1 0)) " = Circle2IntervalR by TOPS_2:def 4; :: thesis: verum