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

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

reconsider A1 = R^1 ].(1 / 2),((1 / 2) + p1).[ as non empty Subset of R^1 ;

A1: the carrier of (R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[)) = A1 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 ].(1 / 2),((1 / 2) + 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 ].(1 / 2),(3 / 2).[)) 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 = 1 + ((arccos x) / (2 * PI)) ) & ( y <= 0 implies b_{1} . p = 1 - ((arccos x) / (2 * PI)) ) )
; :: thesis: verum

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

reconsider A1 = R^1 ].(1 / 2),((1 / 2) + p1).[ as non empty Subset of R^1 ;

A1: the carrier of (R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[)) = A1 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 ].(1 / 2),((1 / 2) + p1).[)) st S

proof

ex G being Function of (Topen_unit_circle c[-10]),(R^1 | (R^1 ].(1 / 2),((1 / 2) + 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 ].(1 / 2),((1 / 2) + 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: not x in {c[-10]} by A3, XBOOLE_0:def 5;

A6: 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

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

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

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

set k = arccos a;

A9: a = x1 `1 by A7, EUCLID:52;

then A10: - 1 <= a by Th26;

A11: a <= 1 by A9, Th26;

then A12: (arccos a) / (2 * PI) <= 1 / 2 by A10, Lm22;

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

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

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: not x in {c[-10]} by A3, XBOOLE_0:def 5;

A6: 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

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

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

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

set k = arccos a;

A9: a = x1 `1 by A7, EUCLID:52;

then A10: - 1 <= a by Th26;

A11: a <= 1 by A9, Th26;

then A12: (arccos a) / (2 * PI) <= 1 / 2 by A10, Lm22;

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

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

A14: now :: thesis: not arccos a = PI

assume A15:
arccos a = PI
; :: thesis: contradiction

then 1 - 1 = (((- 1) ^2) + (b ^2)) - 1 by A10, A11, A13, SIN_COS6:98

.= ((1 ^2) + (b ^2)) - 1 ;

then A16: b = 0 ;

a = - 1 by A10, A11, A15, SIN_COS6:98;

hence contradiction by A7, A5, A16, TARSKI:def 1; :: thesis: verum

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

.= ((1 ^2) + (b ^2)) - 1 ;

then A16: b = 0 ;

a = - 1 by A10, A11, A15, SIN_COS6:98;

hence contradiction by A7, A5, A16, TARSKI:def 1; :: thesis: verum

A17: now :: thesis: not (arccos a) / (2 * PI) = 1 / 2

A18:
0 <= (arccos a) / (2 * PI)
by A10, A11, Lm22;assume
(arccos a) / (2 * PI) = 1 / 2
; :: thesis: contradiction

then ((arccos a) / (2 * PI)) * 2 = (1 / 2) * 2 ;

then (arccos a) / PI = 1 by XCMPLX_1:92;

hence contradiction by A14, XCMPLX_1:58; :: thesis: verum

end;then ((arccos a) / (2 * PI)) * 2 = (1 / 2) * 2 ;

then (arccos a) / PI = 1 by XCMPLX_1:92;

hence contradiction by A14, XCMPLX_1:58; :: thesis: verum

A19: now :: thesis: for y being Real st y = 1 + ((arccos a) / (2 * PI)) holds

y is Element of the carrier of (R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[))

y is Element of the carrier of (R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[))

let y be Real; :: thesis: ( y = 1 + ((arccos a) / (2 * PI)) implies y is Element of the carrier of (R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[)) )

assume A20: y = 1 + ((arccos a) / (2 * PI)) ; :: thesis: y is Element of the carrier of (R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[))

then A21: y <> 1 + (1 / 2) by A17;

1 + 0 <= y by A18, A20, XREAL_1:6;

then A22: 1 / 2 < y by XXREAL_0:2;

y <= 1 + (1 / 2) by A12, A20, XREAL_1:6;

then y < 3 / 2 by A21, XXREAL_0:1;

hence y is Element of the carrier of (R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[)) by A1, A22, XXREAL_1:4; :: thesis: verum

end;assume A20: y = 1 + ((arccos a) / (2 * PI)) ; :: thesis: y is Element of the carrier of (R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[))

then A21: y <> 1 + (1 / 2) by A17;

1 + 0 <= y by A18, A20, XREAL_1:6;

then A22: 1 / 2 < y by XXREAL_0:2;

y <= 1 + (1 / 2) by A12, A20, XREAL_1:6;

then y < 3 / 2 by A21, XXREAL_0:1;

hence y is Element of the carrier of (R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[)) by A1, A22, XXREAL_1:4; :: thesis: verum

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

end;

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

reconsider y = 1 + ((arccos a) / (2 * PI)) as Element of the carrier of (R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[)) by A19;

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

take a ; :: thesis: ex y being Real st

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

take b ; :: thesis: ( x = |[a,b]| & ( b >= 0 implies y = 1 + ((arccos a) / (2 * PI)) ) & ( b <= 0 implies y = 1 - ((arccos a) / (2 * PI)) ) )

thus x = |[a,b]| by A7; :: thesis: ( ( b >= 0 implies y = 1 + ((arccos a) / (2 * PI)) ) & ( b <= 0 implies y = 1 - ((arccos a) / (2 * PI)) ) )

a <> - 1 by A7, A5, A23, TARSKI:def 1;

then a = 1 by A13, A23, SQUARE_1:41;

hence ( ( b >= 0 implies y = 1 + ((arccos a) / (2 * PI)) ) & ( b <= 0 implies y = 1 - ((arccos a) / (2 * PI)) ) ) by SIN_COS6:95; :: thesis: verum

end;take y ; :: thesis: S

take a ; :: thesis: ex y being Real st

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

take b ; :: thesis: ( x = |[a,b]| & ( b >= 0 implies y = 1 + ((arccos a) / (2 * PI)) ) & ( b <= 0 implies y = 1 - ((arccos a) / (2 * PI)) ) )

thus x = |[a,b]| by A7; :: thesis: ( ( b >= 0 implies y = 1 + ((arccos a) / (2 * PI)) ) & ( b <= 0 implies y = 1 - ((arccos a) / (2 * PI)) ) )

a <> - 1 by A7, A5, A23, TARSKI:def 1;

then a = 1 by A13, A23, SQUARE_1:41;

hence ( ( b >= 0 implies y = 1 + ((arccos a) / (2 * PI)) ) & ( b <= 0 implies y = 1 - ((arccos a) / (2 * PI)) ) ) by SIN_COS6:95; :: thesis: verum

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

reconsider y = 1 + ((arccos a) / (2 * PI)) as Element of the carrier of (R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[)) by A19;

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

take a ; :: thesis: ex y being Real st

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

take b ; :: thesis: ( x = |[a,b]| & ( b >= 0 implies y = 1 + ((arccos a) / (2 * PI)) ) & ( b <= 0 implies y = 1 - ((arccos a) / (2 * PI)) ) )

thus ( x = |[a,b]| & ( b >= 0 implies y = 1 + ((arccos a) / (2 * PI)) ) & ( b <= 0 implies y = 1 - ((arccos a) / (2 * PI)) ) ) by A7, A24; :: thesis: verum

end;take y ; :: thesis: S

take a ; :: thesis: ex y being Real st

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

take b ; :: thesis: ( x = |[a,b]| & ( b >= 0 implies y = 1 + ((arccos a) / (2 * PI)) ) & ( b <= 0 implies y = 1 - ((arccos a) / (2 * PI)) ) )

thus ( x = |[a,b]| & ( b >= 0 implies y = 1 + ((arccos a) / (2 * PI)) ) & ( b <= 0 implies y = 1 - ((arccos a) / (2 * PI)) ) ) by A7, A24; :: thesis: verum

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

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

A26: 1 - ((arccos a) / (2 * PI)) <> 1 / 2 by A17;

1 - ((arccos a) / (2 * PI)) >= 1 - (1 / 2) by A12, XREAL_1:13;

then A27: 1 / 2 < 1 - ((arccos a) / (2 * PI)) by A26, XXREAL_0:1;

1 - 0 >= 1 - ((arccos a) / (2 * PI)) by A18, XREAL_1:13;

then 1 - ((arccos a) / (2 * PI)) < 3 / 2 by XXREAL_0:2;

then reconsider y = 1 - ((arccos a) / (2 * PI)) as Element of the carrier of (R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[)) by A1, A27, 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 = 1 + ((arccos a) / (2 * PI)) ) & ( y <= 0 implies y = 1 - ((arccos a) / (2 * PI)) ) )

take b ; :: thesis: ( x = |[a,b]| & ( b >= 0 implies y = 1 + ((arccos a) / (2 * PI)) ) & ( b <= 0 implies y = 1 - ((arccos a) / (2 * PI)) ) )

thus ( x = |[a,b]| & ( b >= 0 implies y = 1 + ((arccos a) / (2 * PI)) ) & ( b <= 0 implies y = 1 - ((arccos a) / (2 * PI)) ) ) by A7, A25; :: thesis: verum

end;A26: 1 - ((arccos a) / (2 * PI)) <> 1 / 2 by A17;

1 - ((arccos a) / (2 * PI)) >= 1 - (1 / 2) by A12, XREAL_1:13;

then A27: 1 / 2 < 1 - ((arccos a) / (2 * PI)) by A26, XXREAL_0:1;

1 - 0 >= 1 - ((arccos a) / (2 * PI)) by A18, XREAL_1:13;

then 1 - ((arccos a) / (2 * PI)) < 3 / 2 by XXREAL_0:2;

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

take y ; :: thesis: S

take a ; :: thesis: ex y being Real st

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

take b ; :: thesis: ( x = |[a,b]| & ( b >= 0 implies y = 1 + ((arccos a) / (2 * PI)) ) & ( b <= 0 implies y = 1 - ((arccos a) / (2 * PI)) ) )

thus ( x = |[a,b]| & ( b >= 0 implies y = 1 + ((arccos a) / (2 * PI)) ) & ( b <= 0 implies y = 1 - ((arccos a) / (2 * PI)) ) ) by A7, A25; :: 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