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 TOUC = Topen_unit_circle (CircleMap . r);
set A = ].r,(r + 1).[;
set f = CircleMap | ].r,(r + 1).[;
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) )
A1: [\r/] <= r by INT_1:def 4;
A2: dom (CircleMap | ].r,(r + 1).[) = ].r,(r + 1).[ by Lm18, RELAT_1:91;
assume A3: 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 Lm8;
set z1 = z `1 ;
set z2 = z `2 ;
A4: z `1 <= 1 by A3, Th27;
set x = (arccos (z `1 )) / (2 * PI );
A5: - 1 <= z `1 by A3, Th27;
then A6: 0 <= (arccos (z `1 )) / (2 * PI ) by A4, Lm22;
(arccos (z `1 )) / (2 * PI ) <= 1 / 2 by A5, A4, Lm22;
then A7: (arccos (z `1 )) / (2 * PI ) < 1 by XXREAL_0:2;
then A8: ((arccos (z `1 )) / (2 * PI )) - ((arccos (z `1 )) / (2 * PI )) < 1 - ((arccos (z `1 )) / (2 * PI )) by XREAL_1:16;
A9: ((z `1 ) ^2 ) + ((z `2 ) ^2 ) = |.z.| ^2 by JGRAPH_1:46;
z is Point of (Tunit_circle 2) by A3, PRE_TOPC:55;
then A10: |.z.| = 1 by Th12;

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

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

A12: 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 A5, A4, SIN_COS6:93
.= |[(z `1 ),(- (- (z `2 )))]| by A10, A9, A11, 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 A13: (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 A2, A12, A13, FUNCT_1:def 5; :: thesis: verum

end;

suppose A14: 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 A5, A4, SIN_COS6:98;
hence contradiction by A10, A9, A11; :: thesis: verum

end;

then [\r/] - ((arccos (z `1 )) / (2 * PI )) < r - 0 by A1, A6, XREAL_1:17;
then ((- ((arccos (z `1 )) / (2 * PI ))) + [\r/]) + 1 < r + 1 by XREAL_1:8;
then A15: r >= (1 - ((arccos (z `1 )) / (2 * PI ))) + [\r/] by A14, XXREAL_1:4;
([\r/] + 1) + 0 < ([\r/] + 1) + (1 - ((arccos (z `1 )) / (2 * PI ))) by A8, XREAL_1:8;
then A16: r < (2 - ((arccos (z `1 )) / (2 * PI ))) + [\r/] by INT_1:52, XXREAL_0:2;

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 A3, A12, Th22; :: thesis: verum

end;

then (1 - ((arccos (z `1 )) / (2 * PI ))) + [\r/] < r by 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 A2, A12, 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 A5, A4, SIN_COS6:93
.= |[(z `1 ),(z `2 )]| by A10, A9, 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 A2, 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 A6, XREAL_1:8;
then A22: r < (((arccos (z `1 )) / (2 * PI )) + [\r/]) + 1 by INT_1:52, XXREAL_0:2;

A23: 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 A3, A19, Th22; :: thesis: verum

end;

((arccos (z `1 )) / (2 * PI )) + [\r/] < 1 + r by A1, A7, XREAL_1:10;
then ((arccos (z `1 )) / (2 * PI )) + [\r/] <= r by A21, XXREAL_1:4;
then (((arccos (z `1 )) / (2 * PI )) + [\r/]) + 1 <= r + 1 by XREAL_1:8;
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 A2, 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