let A be Subset of R^1; :: thesis: for f being Function of (R^1 | A),(Tunit_circle 2) st [.0,1.[ c= A & f = CircleMap | A holds
f is onto
let f be Function of (R^1 | A),(Tunit_circle 2); :: thesis: ( [.0,1.[ c= A & f = CircleMap | A implies f is onto )
assume that
A1: [.0,1.[ c= A and
A2: f = CircleMap | A ; :: thesis: f is onto
A3: dom f = A by A2, Lm18, RELAT_1:62, TOPMETR:17;
thus rng f c= the carrier of (Tunit_circle 2) ; :: according to XBOOLE_0:def 10,FUNCT_2:def 3 :: thesis: the carrier of (Tunit_circle 2) c= rng f
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in the carrier of (Tunit_circle 2) or y in rng f )
assume A4: y in the carrier of (Tunit_circle 2) ; :: thesis: y in rng f
then reconsider z = y as Point of (TOP-REAL 2) by PRE_TOPC:25;
set z1 = z `1 ;
set z2 = z `2 ;
A5: z `1 <= 1 by A4, Th13;
set x = (arccos (z `1)) / (2 * PI);
A6: - 1 <= z `1 by A4, Th13;
then A7: 0 <= (arccos (z `1)) / (2 * PI) by A5, Lm22;
(arccos (z `1)) / (2 * PI) <= 1 / 2 by A6, A5, Lm22;
then A8: (arccos (z `1)) / (2 * PI) < 1 by XXREAL_0:2;
A9: ((z `1) ^2) + ((z `2) ^2) = |.z.| ^2 by JGRAPH_1:29;
A10: |.z.| = 1 by A4, Th12;

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

suppose A11: z `2 < 0 ; :: thesis: y in rng f

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 A6, A5, SIN_COS6:96;
hence contradiction by A10, A9, A11; :: thesis: verum

end;

then A12: 1 - 0 > 1 - ((arccos (z `1)) / (2 * PI)) by A7, XREAL_1:15;
1 - ((arccos (z `1)) / (2 * PI)) > 1 - 1 by A8, XREAL_1:15;
then A13: 1 - ((arccos (z `1)) / (2 * PI)) in [.0,1.[ by A12, XXREAL_1:3;
then f . (1 - ((arccos (z `1)) / (2 * PI))) = CircleMap . ((- ((arccos (z `1)) / (2 * PI))) + 1) by A1, A2, FUNCT_1:49
.= CircleMap . (- ((arccos (z `1)) / (2 * PI))) by Th31
.= |[(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 A6, A5, SIN_COS6:91
.= |[(z `1),(- (- (z `2)))]| by A10, A9, A11, SIN_COS6:103
.= y by EUCLID:53 ;
hence y in rng f by A1, A3, A13, FUNCT_1:def 3; :: thesis: verum

end;

suppose A14: z `2 >= 0 ; :: thesis: y in rng f

A15: (arccos (z `1)) / (2 * PI) in [.0,1.[ by A7, A8, XXREAL_1:3;
then f . ((arccos (z `1)) / (2 * PI)) = CircleMap . ((arccos (z `1)) / (2 * PI)) by A1, A2, FUNCT_1:49
.= |[(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 A6, A5, SIN_COS6:91
.= |[(z `1),(z `2)]| by A10, A9, A14, SIN_COS6:102
.= y by EUCLID:53 ;
hence y in rng f by A1, A3, A15, FUNCT_1:def 3; :: thesis: verum

end;

end;