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;