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 object ; :: 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 6;
A2: dom (CircleMap | ].r,(r + 1).[) = ].r,(r + 1).[ by Lm18, RELAT_1:62;
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, Th26;
set x = (arccos (z `1)) / (2 * PI);
A5: - 1 <= z `1 by A3, Th26;
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:14;
A9: ((z `1) ^2) + ((z `2) ^2) = |.z.| ^2 by JGRAPH_1:29;
z is Point of (Tunit_circle 2) by A3, PRE_TOPC:25;
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:31
.= |[(cos (arccos (z `1))),(sin (- ((2 * PI) * ((arccos (z `1)) / (2 * PI)))))]| by XCMPLX_1:87
.= |[(cos (arccos (z `1))),(- (sin ((2 * PI) * ((arccos (z `1)) / (2 * PI)))))]| by SIN_COS:31
.= |[(cos (arccos (z `1))),(- (sin (arccos (z `1))))]| by XCMPLX_1:87
.= |[(z `1),(- (sin (arccos (z `1))))]| by A5, A4, SIN_COS6:91
.= |[(z `1),(- (- (z `2)))]| by A10, A9, A11, SIN_COS6:103
.= y by EUCLID:53 ;

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:49
.= CircleMap . (- ((arccos (z `1)) / (2 * PI))) by Th31 ;
hence y in rng (CircleMap r) by A2, A12, A13, FUNCT_1:def 3; :: thesis: verum

end;

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

now :: thesis: not (arccos (z `1)) / (2 * PI) = 0

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

end;

then [\r/] - ((arccos (z `1)) / (2 * PI)) < r - 0 by A1, A6, XREAL_1:15;
then ((- ((arccos (z `1)) / (2 * PI))) + [\r/]) + 1 < r + 1 by XREAL_1:6;
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:6;
then A16: r < (2 - ((arccos (z `1)) / (2 * PI))) + [\r/] by INT_1:29, XXREAL_0:2;

now :: thesis: not ((- ((arccos (z `1)) / (2 * PI))) + [\r/]) + 1 = r

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 Th31 ;
hence contradiction by A3, A12, Th21; :: 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:6;
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:49
.= CircleMap . (- ((arccos (z `1)) / (2 * PI))) by Th31 ;
hence y in rng (CircleMap r) by A2, A12, A17, FUNCT_1:def 3; :: 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:87
.= |[(cos (arccos (z `1))),(sin (arccos (z `1)))]| by XCMPLX_1:87
.= |[(z `1),(sin (arccos (z `1)))]| by A5, A4, SIN_COS6:91
.= |[(z `1),(z `2)]| by A10, A9, A18, SIN_COS6:102
.= y by EUCLID:53 ;

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:49
.= CircleMap . ((arccos (z `1)) / (2 * PI)) by Th31 ;
hence y in rng (CircleMap r) by A2, A19, A20, FUNCT_1:def 3; :: 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:6;
then A22: r < (((arccos (z `1)) / (2 * PI)) + [\r/]) + 1 by INT_1:29, XXREAL_0:2;

A23: now :: thesis: not (((arccos (z `1)) / (2 * PI)) + [\r/]) + 1 = r + 1

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

end;

((arccos (z `1)) / (2 * PI)) + [\r/] < 1 + r by A1, A7, XREAL_1:8;
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:6;
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:49
.= CircleMap . ((arccos (z `1)) / (2 * PI)) by Th31 ;
hence y in rng (CircleMap r) by A2, A19, A24, FUNCT_1:def 3; :: thesis: verum

end;

end;

end;

end;

end;

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