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:91, TOPMETR:24;
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 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:55;
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:46;
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

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

end;

then A12: 1 - 0 > 1 - ((arccos (z `1 )) / (2 * PI )) by A7, XREAL_1:17;
1 - ((arccos (z `1 )) / (2 * PI )) > 1 - 1 by A8, XREAL_1:17;
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: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 A6, A5, SIN_COS6:93
.= |[(z `1 ),(- (- (z `2 )))]| by A10, A9, A11, SIN_COS6:105
.= y by EUCLID:57 ;
hence y in rng f by A1, A3, A13, FUNCT_1:def 5; :: 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: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 A6, A5, SIN_COS6:93
.= |[(z `1 ),(z `2 )]| by A10, A9, A14, SIN_COS6:104
.= y by EUCLID:57 ;
hence y in rng f by A1, A3, A15, FUNCT_1:def 5; :: thesis: verum

end;

end;