thus CircleMap r is one-to-one ; :: thesis: ( CircleMap r is onto & CircleMap r is continuous )
thus CircleMap r is onto :: thesis: CircleMap r is continuous

proof

set A = ].r,(r + 1).[;
set f = CircleMap | ].r,(r + 1).[;
set TOUC = Topen_unit_circle (CircleMap . r);
set X = the carrier of (Topen_unit_circle (CircleMap . r));
thus rng (CircleMap r) c= the carrier of (Topen_unit_circle (CircleMap . r)) ; :: according to XBOOLE_0:def 10,FUNCT_2:def 3 :: thesis: the carrier of (Topen_unit_circle (CircleMap . r)) c= rng (CircleMap r)
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in the carrier of (Topen_unit_circle (CircleMap . r)) or y in rng (CircleMap r) )
assume A1: y in the carrier of (Topen_unit_circle (CircleMap . r)) ; :: thesis: y in rng (CircleMap r)
then reconsider z = y as Point of (TOP-REAL 2) by Lm9;
set z1 = z `1 ;
set z2 = z `2 ;
set x = (arccos (z `1 )) / (2 * PI );
A2: [\r/] <= r by INT_1:def 4;
A3: dom (CircleMap | ].r,(r + 1).[) = ].r,(r + 1).[ by Lm19, RELAT_1:91;
z is Point of (Tunit_circle 2) by A1, PRE_TOPC:55;
then A4: |.z.| = 1 by Th12;
A5: ((z `1 ) ^2 ) + ((z `2 ) ^2 ) = |.z.| ^2 by JGRAPH_1:46;
A6: ( - 1 <= z `1 & z `1 <= 1 ) by A1, Th27;
then A7: 0 <= (arccos (z `1 )) / (2 * PI ) by Lm24;
(arccos (z `1 )) / (2 * PI ) <= 1 / 2 by A6, Lm24;
then A8: (arccos (z `1 )) / (2 * PI ) < 1 by XXREAL_0:2;
then A9: ((arccos (z `1 )) / (2 * PI )) - ((arccos (z `1 )) / (2 * PI )) < 1 - ((arccos (z `1 )) / (2 * PI )) by XREAL_1:16;

per cases ( z `2 < 0 or z `2 >= 0 ) ;

suppose A10: z `2 < 0 ; :: thesis: y in rng (CircleMap r)

A11: CircleMap . (- ((arccos (z `1 )) / (2 * PI ))) = |[(cos (- ((2 * PI ) * ((arccos (z `1 )) / (2 * PI ))))),(sin ((2 * PI ) * (- ((arccos (z `1 )) / (2 * PI )))))]| by Def11
.= |[(cos ((2 * PI ) * ((arccos (z `1 )) / (2 * PI )))),(sin ((2 * PI ) * (- ((arccos (z `1 )) / (2 * PI )))))]| by SIN_COS:34
.= |[(cos (arccos (z `1 ))),(sin (- ((2 * PI ) * ((arccos (z `1 )) / (2 * PI )))))]| by XCMPLX_1:88
.= |[(cos (arccos (z `1 ))),(- (sin ((2 * PI ) * ((arccos (z `1 )) / (2 * PI )))))]| by SIN_COS:34
.= |[(cos (arccos (z `1 ))),(- (sin (arccos (z `1 ))))]| by XCMPLX_1:88
.= |[(z `1 ),(- (sin (arccos (z `1 ))))]| by A6, SIN_COS6:93
.= |[(z `1 ),(- (- (z `2 )))]| by A4, A5, A10, SIN_COS6:105
.= y by EUCLID:57 ;

per cases ( (1 - ((arccos (z `1 )) / (2 * PI ))) + [\r/] in ].r,(r + 1).[ or not (1 - ((arccos (z `1 )) / (2 * PI ))) + [\r/] in ].r,(r + 1).[ ) ;

suppose A12: (1 - ((arccos (z `1 )) / (2 * PI ))) + [\r/] in ].r,(r + 1).[ ; :: thesis: y in rng (CircleMap r)

then (CircleMap | ].r,(r + 1).[) . ((1 - ((arccos (z `1 )) / (2 * PI ))) + [\r/]) = CircleMap . ((- ((arccos (z `1 )) / (2 * PI ))) + ([\r/] + 1)) by FUNCT_1:72
.= CircleMap . (- ((arccos (z `1 )) / (2 * PI ))) by Th32 ;
hence y in rng (CircleMap r) by A3, A11, A12, FUNCT_1:def 5; :: thesis: verum

end;

suppose A13: not (1 - ((arccos (z `1 )) / (2 * PI ))) + [\r/] in ].r,(r + 1).[ ; :: thesis: y in rng (CircleMap r)

now

assume (arccos (z `1 )) / (2 * PI ) = 0 ; :: thesis: contradiction
then arccos (z `1 ) = 0 ;
then z `1 = 1 by A6, SIN_COS6:98;
hence contradiction by A4, A5, A10; :: thesis: verum

end;

then [\r/] - ((arccos (z `1 )) / (2 * PI )) < r - 0 by A2, A7, XREAL_1:17;
then ((- ((arccos (z `1 )) / (2 * PI ))) + [\r/]) + 1 < r + 1 by XREAL_1:8;
then A14: r >= (1 - ((arccos (z `1 )) / (2 * PI ))) + [\r/] by A13, XXREAL_1:4;

A15: now

assume ((- ((arccos (z `1 )) / (2 * PI ))) + [\r/]) + 1 = r ; :: thesis: contradiction
then CircleMap . r = CircleMap . ((- ((arccos (z `1 )) / (2 * PI ))) + ([\r/] + 1))
.= CircleMap . (- ((arccos (z `1 )) / (2 * PI ))) by Th32 ;
hence contradiction by A1, A11, Th22; :: thesis: verum

end;

([\r/] + 1) + 0 < ([\r/] + 1) + (1 - ((arccos (z `1 )) / (2 * PI ))) by A9, XREAL_1:8;
then A16: r < (2 - ((arccos (z `1 )) / (2 * PI ))) + [\r/] by INT_1:52, XXREAL_0:2;
(1 - ((arccos (z `1 )) / (2 * PI ))) + [\r/] < r by A14, A15, XXREAL_0:1;
then ((1 - ((arccos (z `1 )) / (2 * PI ))) + [\r/]) + 1 < r + 1 by XREAL_1:8;
then A17: ((- ((arccos (z `1 )) / (2 * PI ))) + [\r/]) + 2 in ].r,(r + 1).[ by A16, XXREAL_1:4;
then (CircleMap | ].r,(r + 1).[) . ((- ((arccos (z `1 )) / (2 * PI ))) + ([\r/] + 2)) = CircleMap . ((- ((arccos (z `1 )) / (2 * PI ))) + ([\r/] + 2)) by FUNCT_1:72
.= CircleMap . (- ((arccos (z `1 )) / (2 * PI ))) by Th32 ;
hence y in rng (CircleMap r) by A3, A11, A17, FUNCT_1:def 5; :: thesis: verum

end;

end;

end;

suppose A18: z `2 >= 0 ; :: thesis: y in rng (CircleMap r)

A19: CircleMap . ((arccos (z `1 )) / (2 * PI )) = |[(cos ((2 * PI ) * ((arccos (z `1 )) / (2 * PI )))),(sin ((2 * PI ) * ((arccos (z `1 )) / (2 * PI ))))]| by Def11
.= |[(cos (arccos (z `1 ))),(sin ((2 * PI ) * ((arccos (z `1 )) / (2 * PI ))))]| by XCMPLX_1:88
.= |[(cos (arccos (z `1 ))),(sin (arccos (z `1 )))]| by XCMPLX_1:88
.= |[(z `1 ),(sin (arccos (z `1 )))]| by A6, SIN_COS6:93
.= |[(z `1 ),(z `2 )]| by A4, A5, A18, SIN_COS6:104
.= y by EUCLID:57 ;

per cases ( ((arccos (z `1 )) / (2 * PI )) + [\r/] in ].r,(r + 1).[ or not ((arccos (z `1 )) / (2 * PI )) + [\r/] in ].r,(r + 1).[ ) ;

suppose A20: ((arccos (z `1 )) / (2 * PI )) + [\r/] in ].r,(r + 1).[ ; :: thesis: y in rng (CircleMap r)

then (CircleMap | ].r,(r + 1).[) . (((arccos (z `1 )) / (2 * PI )) + [\r/]) = CircleMap . (((arccos (z `1 )) / (2 * PI )) + [\r/]) by FUNCT_1:72
.= CircleMap . ((arccos (z `1 )) / (2 * PI )) by Th32 ;
hence y in rng (CircleMap r) by A3, A19, A20, FUNCT_1:def 5; :: thesis: verum

end;

suppose A21: not ((arccos (z `1 )) / (2 * PI )) + [\r/] in ].r,(r + 1).[ ; :: thesis: y in rng (CircleMap r)

0 + ([\r/] + 1) <= ((arccos (z `1 )) / (2 * PI )) + ([\r/] + 1) by A7, XREAL_1:8;
then A22: r < (((arccos (z `1 )) / (2 * PI )) + [\r/]) + 1 by INT_1:52, XXREAL_0:2;
((arccos (z `1 )) / (2 * PI )) + [\r/] < 1 + r by A2, A8, XREAL_1:10;
then ((arccos (z `1 )) / (2 * PI )) + [\r/] <= r by A21, XXREAL_1:4;
then A23: (((arccos (z `1 )) / (2 * PI )) + [\r/]) + 1 <= r + 1 by XREAL_1:8;

now

assume (((arccos (z `1 )) / (2 * PI )) + [\r/]) + 1 = r + 1 ; :: thesis: contradiction
then CircleMap . r = CircleMap . ((arccos (z `1 )) / (2 * PI )) by Th32;
hence contradiction by A1, A19, Th22; :: thesis: verum

end;

then (((arccos (z `1 )) / (2 * PI )) + [\r/]) + 1 < r + 1 by A23, XXREAL_0:1;
then A24: (((arccos (z `1 )) / (2 * PI )) + [\r/]) + 1 in ].r,(r + 1).[ by A22, XXREAL_1:4;
then (CircleMap | ].r,(r + 1).[) . ((((arccos (z `1 )) / (2 * PI )) + [\r/]) + 1) = CircleMap . (((arccos (z `1 )) / (2 * PI )) + ([\r/] + 1)) by FUNCT_1:72
.= CircleMap . ((arccos (z `1 )) / (2 * PI )) by Th32 ;
hence y in rng (CircleMap r) by A3, A19, A24, FUNCT_1:def 5; :: thesis: verum

end;

end;

end;

end;

end;

Topen_unit_circle (CircleMap . r) = (Tunit_circle 2) | (([#] (Tunit_circle 2)) \ {(CircleMap . r)}) by Th23;
hence CircleMap r is continuous by TOPREALA:29; :: thesis: verum