defpred S_{1}[ set , set ] means ex x, y being Real st

( $1 = |[x,y]| & ( y >= 0 implies $2 = (arccos x) / (2 * PI) ) & ( y <= 0 implies $2 = 1 - ((arccos x) / (2 * PI)) ) );

reconsider A = R^1 ].0,1.[ as non empty Subset of R^1 ;

A1: the carrier of (R^1 | (R^1 ].0,(0 + p1).[)) = A by PRE_TOPC:8;

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_{1}[x,y]

for p being Point of (Topen_unit_circle c[10]) holds S_{1}[p,G . p]
from FUNCT_2:sch 3(A2);

hence ex b_{1} 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 st

( p = |[x,y]| & ( y >= 0 implies b_{1} . p = (arccos x) / (2 * PI) ) & ( y <= 0 implies b_{1} . p = 1 - ((arccos x) / (2 * PI)) ) )
; :: thesis: verum

( $1 = |[x,y]| & ( y >= 0 implies $2 = (arccos x) / (2 * PI) ) & ( y <= 0 implies $2 = 1 - ((arccos x) / (2 * PI)) ) );

reconsider A = R^1 ].0,1.[ as non empty Subset of R^1 ;

A1: the carrier of (R^1 | (R^1 ].0,(0 + p1).[)) = A by PRE_TOPC:8;

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

proof

ex G being Function of (Topen_unit_circle c[10]),(R^1 | (R^1 ].0,(0 + p1).[)) st
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_{1}[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 Element of REAL such that

A6: x = <*a,b*> by A4, EUCLID:51;

reconsider x1 = x as Point of (TOP-REAL 2) by A4, A5;

A7: b = x1 `2 by A6, EUCLID:52;

set k = arccos a;

A8: a = x1 `1 by A6, EUCLID:52;

then A9: - 1 <= a by Th26;

A10: 1 ^2 = |.x1.| ^2 by A4, Th12

.= (a ^2) + (b ^2) by A8, A7, JGRAPH_3:1 ;

A11: a <= 1 by A8, Th26;

then A12: 0 <= arccos a by A9, SIN_COS6:99;

A13: (arccos a) / (2 * PI) <= 1 / 2 by A9, A11, Lm22;

A14: not x in {c[10]} by A3, XBOOLE_0:def 5;

A19: 0 <= (arccos a) / (2 * PI) by A9, A11, Lm22;

end;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 Element of REAL such that

A6: x = <*a,b*> by A4, EUCLID:51;

reconsider x1 = x as Point of (TOP-REAL 2) by A4, A5;

A7: b = x1 `2 by A6, EUCLID:52;

set k = arccos a;

A8: a = x1 `1 by A6, EUCLID:52;

then A9: - 1 <= a by Th26;

A10: 1 ^2 = |.x1.| ^2 by A4, Th12

.= (a ^2) + (b ^2) by A8, A7, JGRAPH_3:1 ;

A11: a <= 1 by A8, Th26;

then A12: 0 <= arccos a by A9, SIN_COS6:99;

A13: (arccos a) / (2 * PI) <= 1 / 2 by A9, A11, Lm22;

A14: not x in {c[10]} by A3, XBOOLE_0:def 5;

A15: now :: thesis: not arccos a = 0

A18:
arccos a <= PI
by A9, A11, SIN_COS6:99;assume A16:
arccos a = 0
; :: thesis: contradiction

then 1 - 1 = (1 + (b ^2)) - 1 by A9, A11, A10, SIN_COS6:96;

then A17: b = 0 ;

a = 1 by A9, A11, A16, SIN_COS6:96;

hence contradiction by A6, A14, A17, TARSKI:def 1; :: thesis: verum

end;then 1 - 1 = (1 + (b ^2)) - 1 by A9, A11, A10, SIN_COS6:96;

then A17: b = 0 ;

a = 1 by A9, A11, A16, SIN_COS6:96;

hence contradiction by A6, A14, A17, TARSKI:def 1; :: thesis: verum

A19: 0 <= (arccos a) / (2 * PI) by A9, A11, Lm22;

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

end;

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

set y = (arccos a) / (2 * PI);

(arccos a) / (2 * PI) < 1 by A13, 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, A19, A15, XXREAL_1:4;

take y ; :: thesis: S_{1}[x,y]

take a ; :: thesis: ex y being Real 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))

A21: a <> 1 by A6, A14, A20, TARSKI:def 1;

hence y = (1 * PI) / (2 * PI) by A10, A20, SIN_COS6:93, SQUARE_1:41

.= 1 - (1 / 2) by XCMPLX_1:91

.= 1 - ((1 * PI) / (2 * PI)) by XCMPLX_1:91

.= 1 - ((arccos a) / (2 * PI)) by A10, A20, A21, SIN_COS6:93, SQUARE_1:41 ;

:: thesis: verum

end;(arccos a) / (2 * PI) < 1 by A13, 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, A19, A15, XXREAL_1:4;

take y ; :: thesis: S

take a ; :: thesis: ex y being Real 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))

A21: a <> 1 by A6, A14, A20, TARSKI:def 1;

hence y = (1 * PI) / (2 * PI) by A10, A20, SIN_COS6:93, SQUARE_1:41

.= 1 - (1 / 2) by XCMPLX_1:91

.= 1 - ((1 * PI) / (2 * PI)) by XCMPLX_1:91

.= 1 - ((arccos a) / (2 * PI)) by A10, A20, A21, SIN_COS6:93, SQUARE_1:41 ;

:: thesis: verum

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

set y = (arccos a) / (2 * PI);

(arccos a) / (2 * PI) < 1 by A13, 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, A19, A15, XXREAL_1:4;

take y ; :: thesis: S_{1}[x,y]

take a ; :: thesis: ex y being Real 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, A22; :: thesis: verum

end;(arccos a) / (2 * PI) < 1 by A13, 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, A19, A15, XXREAL_1:4;

take y ; :: thesis: S

take a ; :: thesis: ex y being Real 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, A22; :: thesis: verum

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

set y = 1 - ((arccos a) / (2 * PI));

A24: ((2 * PI) - (arccos a)) / (2 * PI) = ((2 * PI) / (2 * PI)) - ((arccos a) / (2 * PI)) by XCMPLX_1:120

.= 1 - ((arccos a) / (2 * PI)) by XCMPLX_1:60 ;

(2 * PI) - (arccos a) < (2 * PI) - 0 by A12, A15, XREAL_1:15;

then 1 - ((arccos a) / (2 * PI)) < (2 * PI) / (2 * PI) by A24, XREAL_1:74;

then A25: 1 - ((arccos a) / (2 * PI)) < 1 by XCMPLX_1:60;

1 * (arccos a) < 2 * PI by A18, XREAL_1:98;

then (arccos a) - (arccos a) < (2 * PI) - (arccos a) by XREAL_1:14;

then reconsider y = 1 - ((arccos a) / (2 * PI)) as Element of the carrier of (R^1 | (R^1 ].0,(0 + p1).[)) by A1, A24, A25, XXREAL_1:4;

take y ; :: thesis: S_{1}[x,y]

take a ; :: thesis: ex y being Real 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, A23; :: thesis: verum

end;A24: ((2 * PI) - (arccos a)) / (2 * PI) = ((2 * PI) / (2 * PI)) - ((arccos a) / (2 * PI)) by XCMPLX_1:120

.= 1 - ((arccos a) / (2 * PI)) by XCMPLX_1:60 ;

(2 * PI) - (arccos a) < (2 * PI) - 0 by A12, A15, XREAL_1:15;

then 1 - ((arccos a) / (2 * PI)) < (2 * PI) / (2 * PI) by A24, XREAL_1:74;

then A25: 1 - ((arccos a) / (2 * PI)) < 1 by XCMPLX_1:60;

1 * (arccos a) < 2 * PI by A18, XREAL_1:98;

then (arccos a) - (arccos a) < (2 * PI) - (arccos a) by XREAL_1:14;

then reconsider y = 1 - ((arccos a) / (2 * PI)) as Element of the carrier of (R^1 | (R^1 ].0,(0 + p1).[)) by A1, A24, A25, XXREAL_1:4;

take y ; :: thesis: S

take a ; :: thesis: ex y being Real 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, A23; :: thesis: verum

for p being Point of (Topen_unit_circle c[10]) holds S

hence ex b

for p being Point of (Topen_unit_circle c[10]) ex x, y being Real st

( p = |[x,y]| & ( y >= 0 implies b