let A be Subset of R^1; :: thesis: for f being Function of (R^1 | A),() st [.0,1.[ c= A & f = CircleMap | A holds
f is onto

let f be Function of (R^1 | A),(); :: 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 ;
thus rng f c= the carrier of () ; :: according to XBOOLE_0:def 10,FUNCT_2:def 3 :: thesis: the carrier of () c= rng f
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in the carrier of () or y in rng f )
assume A4: y in the carrier of () ; :: thesis: y in rng f
then reconsider z = y as Point of () by PRE_TOPC:25;
set z1 = z `1 ;
set z2 = z `2 ;
A5: z `1 <= 1 by ;
set x = (arccos (z `1)) / (2 * PI);
A6: - 1 <= z `1 by ;
then A7: 0 <= (arccos (z `1)) / (2 * PI) by ;
(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 ;
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 ;
hence contradiction by A10, A9, A11; :: thesis: verum
end;
then A12: 1 - 0 > 1 - ((arccos (z `1)) / (2 * PI)) by ;
1 - ((arccos (z `1)) / (2 * PI)) > 1 - 1 by ;
then A13: 1 - ((arccos (z `1)) / (2 * PI)) in [.0,1.[ by ;
then f . (1 - ((arccos (z `1)) / (2 * PI))) = CircleMap . ((- ((arccos (z `1)) / (2 * PI))) + 1) by
.= 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
.= |[(z `1),(- (- (z `2)))]| by
.= y by EUCLID:53 ;
hence y in rng f by ; :: thesis: verum
end;
suppose A14: z `2 >= 0 ; :: thesis: y in rng f
A15: (arccos (z `1)) / (2 * PI) in [.0,1.[ by ;
then f . ((arccos (z `1)) / (2 * PI)) = CircleMap . ((arccos (z `1)) / (2 * PI)) by
.= |[(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
.= |[(z `1),(z `2)]| by
.= y by EUCLID:53 ;
hence y in rng f by ; :: thesis: verum
end;
end;