reconsider A = R^1 ].0 ,1.[ as non empty Subset of R^1 ;
defpred S₁[ set , set ] means ex x, y being real number st
( $1 = |[x,y]| & ( y >= 0 implies $2 = (arccos x) / (2 * PI ) ) & ( y <= 0 implies $2 = 1 - ((arccos x) / (2 * PI )) ) );
A1: the carrier of (R^1 | (R^1 ].0 ,(0 + p1).[)) = A by PRE_TOPC:29;
A2: for x being Element of the carrier of (Topen_unit_circle c[10] ) ex y being Element of the carrier of (R^1 | (R^1 ].0 ,(0 + p1).[)) st S₁[x,y]

proof

let x be Element of the carrier of (Topen_unit_circle c[10] ); :: thesis: ex y being Element of the carrier of (R^1 | (R^1 ].0 ,(0 + p1).[)) st S₁[x,y]
A3: the carrier of (Topen_unit_circle c[10] ) = the carrier of (Tunit_circle 2) \ {c[10] } by Def10;
then A4: x in the carrier of (Tunit_circle 2) by XBOOLE_0:def 5;
A5: the carrier of (Tunit_circle 2) is Subset of (TOP-REAL 2) by TSEP_1:1;
then consider a, b being Real such that
A6: x = <*a,b*> by A4, EUCLID:55;
A7: not x in {c[10] } by A3, XBOOLE_0:def 5;
set k = arccos a;
reconsider x1 = x as Point of (TOP-REAL 2) by A4, A5;
A8: ( a = x1 `1 & b = x1 `2 ) by A6, EUCLID:56;
then A9: ( - 1 <= a & a <= 1 ) by Th27;
then A10: ( 0 <= arccos a & arccos a <= PI ) by SIN_COS6:101;
A11: ( 0 <= (arccos a) / (2 * PI ) & (arccos a) / (2 * PI ) <= 1 / 2 ) by A9, Lm24;
A12: 1 ^2 = |.x1.| ^2 by A4, Th12
.= (a ^2 ) + (b ^2 ) by A8, JGRAPH_3:10 ;

A13: now

assume A14: arccos a = 0 ; :: thesis: contradiction
then A15: a = 1 by A9, SIN_COS6:98;
1 - 1 = (1 + (b ^2 )) - 1 by A9, A12, A14, SIN_COS6:98;
then b = 0 ;
hence contradiction by A6, A7, A15, TARSKI:def 1; :: thesis: verum

end;

per cases ( b = 0 or b > 0 or b < 0 ) ;

suppose A16: b = 0 ; :: thesis: ex y being Element of the carrier of (R^1 | (R^1 ].0 ,(0 + p1).[)) st S₁[x,y]

then A17: a <> 1 by A6, A7, TARSKI:def 1;
set y = (arccos a) / (2 * PI );
(arccos a) / (2 * PI ) <> 0 by A13;
then ( 0 < (arccos a) / (2 * PI ) & (arccos a) / (2 * PI ) < 1 ) by A11, XXREAL_0:2;
then reconsider y = (arccos a) / (2 * PI ) as Element of the carrier of (R^1 | (R^1 ].0 ,(0 + p1).[)) by A1, XXREAL_1:4;
take y ; :: thesis: S₁[x,y]
take a ; :: thesis: ex y being real number st
( x = |[a,y]| & ( y >= 0 implies y = (arccos a) / (2 * PI ) ) & ( y <= 0 implies y = 1 - ((arccos a) / (2 * PI )) ) )
take b ; :: thesis: ( x = |[a,b]| & ( b >= 0 implies y = (arccos a) / (2 * PI ) ) & ( b <= 0 implies y = 1 - ((arccos a) / (2 * PI )) ) )
thus x = |[a,b]| by A6; :: thesis: ( ( b >= 0 implies y = (arccos a) / (2 * PI ) ) & ( b <= 0 implies y = 1 - ((arccos a) / (2 * PI )) ) )
thus ( b >= 0 implies y = (arccos a) / (2 * PI ) ) ; :: thesis: ( b <= 0 implies y = 1 - ((arccos a) / (2 * PI )) )
assume b <= 0 ; :: thesis: y = 1 - ((arccos a) / (2 * PI ))
thus y = (1 * PI ) / (2 * PI ) by A12, A16, A17, SIN_COS6:95, SQUARE_1:110
.= 1 - (1 / 2) by XCMPLX_1:92
.= 1 - ((1 * PI ) / (2 * PI )) by XCMPLX_1:92
.= 1 - ((arccos a) / (2 * PI )) by A12, A16, A17, SIN_COS6:95, SQUARE_1:110 ; :: thesis: verum

end;

suppose A18: b > 0 ; :: thesis: ex y being Element of the carrier of (R^1 | (R^1 ].0 ,(0 + p1).[)) st S₁[x,y]

set y = (arccos a) / (2 * PI );
(arccos a) / (2 * PI ) <> 0 by A13;
then ( 0 < (arccos a) / (2 * PI ) & (arccos a) / (2 * PI ) < 1 ) by A11, XXREAL_0:2;
then reconsider y = (arccos a) / (2 * PI ) as Element of the carrier of (R^1 | (R^1 ].0 ,(0 + p1).[)) by A1, XXREAL_1:4;
take y ; :: thesis: S₁[x,y]
take a ; :: thesis: ex y being real number st
( x = |[a,y]| & ( y >= 0 implies y = (arccos a) / (2 * PI ) ) & ( y <= 0 implies y = 1 - ((arccos a) / (2 * PI )) ) )
take b ; :: thesis: ( x = |[a,b]| & ( b >= 0 implies y = (arccos a) / (2 * PI ) ) & ( b <= 0 implies y = 1 - ((arccos a) / (2 * PI )) ) )
thus ( x = |[a,b]| & ( b >= 0 implies y = (arccos a) / (2 * PI ) ) & ( b <= 0 implies y = 1 - ((arccos a) / (2 * PI )) ) ) by A6, A18; :: thesis: verum

end;

suppose A19: b < 0 ; :: thesis: ex y being Element of the carrier of (R^1 | (R^1 ].0 ,(0 + p1).[)) st S₁[x,y]

set y = 1 - ((arccos a) / (2 * PI ));
A20: ((2 * PI ) - (arccos a)) / (2 * PI ) = ((2 * PI ) / (2 * PI )) - ((arccos a) / (2 * PI )) by XCMPLX_1:121
.= 1 - ((arccos a) / (2 * PI )) by XCMPLX_1:60 ;
1 * (arccos a) < 2 * PI by A10, XREAL_1:100;
then ( (arccos a) - (arccos a) < (2 * PI ) - (arccos a) & (2 * PI ) - (arccos a) < (2 * PI ) - 0 ) by A10, A13, XREAL_1:16, XREAL_1:17;
then ( 0 / (2 * PI ) < 1 - ((arccos a) / (2 * PI )) & 1 - ((arccos a) / (2 * PI )) < (2 * PI ) / (2 * PI ) ) by A20, XREAL_1:76;
then ( 0 < 1 - ((arccos a) / (2 * PI )) & 1 - ((arccos a) / (2 * PI )) < 1 ) by XCMPLX_1:60;
then reconsider y = 1 - ((arccos a) / (2 * PI )) as Element of the carrier of (R^1 | (R^1 ].0 ,(0 + p1).[)) by A1, XXREAL_1:4;
take y ; :: thesis: S₁[x,y]
take a ; :: thesis: ex y being real number st
( x = |[a,y]| & ( y >= 0 implies y = (arccos a) / (2 * PI ) ) & ( y <= 0 implies y = 1 - ((arccos a) / (2 * PI )) ) )
take b ; :: thesis: ( x = |[a,b]| & ( b >= 0 implies y = (arccos a) / (2 * PI ) ) & ( b <= 0 implies y = 1 - ((arccos a) / (2 * PI )) ) )
thus ( x = |[a,b]| & ( b >= 0 implies y = (arccos a) / (2 * PI ) ) & ( b <= 0 implies y = 1 - ((arccos a) / (2 * PI )) ) ) by A6, A19; :: thesis: verum

end;

end;

end;

ex G being Function of (Topen_unit_circle c[10] ),(R^1 | (R^1 ].0 ,(0 + p1).[)) st
for p being Point of (Topen_unit_circle c[10] ) holds S₁[p,G . p] from FUNCT_2:sch 3(A2);
hence ex b₁ being Function of (Topen_unit_circle c[10] ),(R^1 | (R^1 ].0 ,1.[)) st
for p being Point of (Topen_unit_circle c[10] ) ex x, y being real number st
( p = |[x,y]| & ( y >= 0 implies b₁ . p = (arccos x) / (2 * PI ) ) & ( y <= 0 implies b₁ . p = 1 - ((arccos x) / (2 * PI )) ) ) ; :: thesis: verum