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
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 set ; :: according to TARSKI:def 3 :: thesis: ( not y in the carrier of (Tunit_circle 2) or y in rng f )
assume A3: 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:55;
set z1 = z `1 ;
set z2 = z `2 ;
set x = (arccos (z `1 )) / (2 * PI );
A4: dom f = A by A2, Lm19, RELAT_1:91, TOPMETR:24;
A5: |.z.| = 1 by A3, Th12;
A6: ((z `1 ) ^2 ) + ((z `2 ) ^2 ) = |.z.| ^2 by JGRAPH_1:46;
A7: ( - 1 <= z `1 & z `1 <= 1 ) by A3, Th13;
then A8: 0 <= (arccos (z `1 )) / (2 * PI ) by Lm24;
(arccos (z `1 )) / (2 * PI ) <= 1 / 2 by A7, Lm24;
then A9: (arccos (z `1 )) / (2 * PI ) < 1 by XXREAL_0:2;

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

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

now

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

end;

then ( 1 - 0 > 1 - ((arccos (z `1 )) / (2 * PI )) & 1 - ((arccos (z `1 )) / (2 * PI )) > 1 - 1 ) by A8, A9, XREAL_1:17;
then A11: 1 - ((arccos (z `1 )) / (2 * PI )) in [.0 ,1.[ by XXREAL_1:3;
then f . (1 - ((arccos (z `1 )) / (2 * PI ))) = CircleMap . ((- ((arccos (z `1 )) / (2 * PI ))) + 1) by A1, A2, FUNCT_1:72
.= CircleMap . (- ((arccos (z `1 )) / (2 * PI ))) by Th32
.= |[(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 A7, SIN_COS6:93
.= |[(z `1 ),(- (- (z `2 )))]| by A5, A6, A10, SIN_COS6:105
.= y by EUCLID:57 ;
hence y in rng f by A1, A4, A11, FUNCT_1:def 5; :: thesis: verum

end;

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

A13: (arccos (z `1 )) / (2 * PI ) in [.0 ,1.[ by A8, A9, XXREAL_1:3;
then f . ((arccos (z `1 )) / (2 * PI )) = CircleMap . ((arccos (z `1 )) / (2 * PI )) by A1, A2, FUNCT_1:72
.= |[(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 A7, SIN_COS6:93
.= |[(z `1 ),(z `2 )]| by A5, A6, A12, SIN_COS6:104
.= y by EUCLID:57 ;
hence y in rng f by A1, A4, A13, FUNCT_1:def 5; :: thesis: verum

end;

end;