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 Th33;
reconsider r0 = 0 as Point of R^1 by TOPMETR:24;
set F = AffineMap (2 * PI ),0 ;
A1: dom (id the carrier of (R^1 | A)) = the carrier of (R^1 | A) by RELAT_1:71;
A2: CircleMap . r0 = c[10] by Th33;
then A3: rng f = the carrier of (Topen_unit_circle c[10] ) by FUNCT_2:def 3;
A4: the carrier of (R^1 | A) = A by PRE_TOPC:29;

A5: now

let a be set ; :: thesis: ( a in dom (Circle2IntervalR * f) implies (Circle2IntervalR * f) . a = (id the carrier of (R^1 | A)) . a )
assume A6: 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 Real by XREAL_0:def 1;
consider x, y being real number such that
A7: f . b = |[x,y]| and
A8: ( y >= 0 implies Circle2IntervalR . (f . b) = (arccos x) / (2 * PI ) ) and
A9: ( y <= 0 implies Circle2IntervalR . (f . b) = 1 - ((arccos x) / (2 * PI )) ) by Def13;
A10: f . b = CircleMap . b by A4, FUNCT_1:72
.= |[((cos * (AffineMap (2 * PI ),0 )) . c),((sin * (AffineMap (2 * PI ),0 )) . c)]| by Lm20 ;
then y = (sin * (AffineMap (2 * PI ),0 )) . c by A7, SPPOL_2:1;
then A11: y = sin . ((AffineMap (2 * PI ),0 ) . c) by FUNCT_2:21;
x = (cos * (AffineMap (2 * PI ),0 )) . c by A7, A10, SPPOL_2:1;
then x = cos . ((AffineMap (2 * PI ),0 ) . c) by FUNCT_2:21;
then A12: x = cos ((AffineMap (2 * PI ),0 ) . c) by SIN_COS:def 23;
A13: c < 1 by A4, XXREAL_1:4;
A14: (AffineMap (2 * PI ),0 ) . c = ((2 * PI ) * c) + 0 by JORDAN16:def 3;
then A15: ((AffineMap (2 * PI ),0 ) . c) / ((2 * PI ) * 1) = c / 1 by XCMPLX_1:92;
A16: (AffineMap (2 * PI ),0 ) . (1 - c) = ((2 * PI ) * (1 - c)) + 0 by JORDAN16:def 3;
then A17: ((AffineMap (2 * PI ),0 ) . (1 - c)) / ((2 * PI ) * 1) = (1 - c) / 1 by XCMPLX_1:92;

A18: now

per cases ( y >= 0 or y < 0 ) ;

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

then not (AffineMap (2 * PI ),0 ) . c in ].PI ,(2 * PI ).[ by A11, COMPTRIG:25;
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:74;
then c <= 1 / 2 by A15, A13, XCMPLX_1:60, XCMPLX_1:92;
then A20: (2 * PI ) * c <= (2 * PI ) * (1 / 2) by XREAL_1:66;
0 <= c by A4, XXREAL_1:4;
hence Circle2IntervalR . (f . b) = ((AffineMap (2 * PI ),0 ) . c) / (2 * PI ) by A8, A12, A14, A19, A20, SIN_COS6:94
.= b by A14, XCMPLX_1:90 ;
:: thesis: verum

end;

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

then not (AffineMap (2 * PI ),0 ) . c in [.0 ,PI .] by A11, COMPTRIG:24;
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:76;
then ( c < 0 or c > 1 / 2 ) by A15, XCMPLX_1:92;
then 1 - c < 1 - (1 / 2) by A4, XREAL_1:17, XXREAL_1:4;
then A22: (2 * PI ) * (1 - c) <= (2 * PI ) * (1 / 2) by XREAL_1:66;
A23: 1 - c > 1 - 1 by A13, XREAL_1:17;
cos . ((AffineMap (2 * PI ),0 ) . (1 - c)) = cos ((- ((2 * PI ) * c)) + ((2 * PI ) * 1)) by A16, SIN_COS:def 23
.= cos (- ((2 * PI ) * c)) by COMPLEX2:10
.= cos ((2 * PI ) * c) by SIN_COS:34 ;
then arccos x = arccos (cos ((AffineMap (2 * PI ),0 ) . (1 - c))) by A12, A14, SIN_COS:def 23
.= (AffineMap (2 * PI ),0 ) . (1 - c) by A16, A23, A22, SIN_COS6:94 ;
hence Circle2IntervalR . (f . b) = b by A9, A17, A21; :: thesis: verum

end;

end;

end;

thus (Circle2IntervalR * f) . a = Circle2IntervalR . (f . b) by A6, FUNCT_1:22
.= (id the carrier of (R^1 | A)) . a by A18, FUNCT_1:35 ; :: thesis: verum

end;

dom (Circle2IntervalR * f) = the carrier of (R^1 | A) by FUNCT_2:def 1;
then Circle2IntervalR = f " by A3, A1, A5, FUNCT_1:9, FUNCT_2:36;
hence (CircleMap (R^1 0 )) " = Circle2IntervalR by A2, A3, TOPS_2:def 4; :: thesis: verum