defpred S1[ 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 S1[x,y]
proof
let x be
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 S1[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;
A18:
arccos a <= PI
by A9, A11, SIN_COS6:99;
A19:
0 <= (arccos a) / (2 * PI)
by A9, A11, Lm22;
per cases
( b = 0 or b > 0 or b < 0 )
;
suppose A20:
b = 0
;
ex y being Element of the carrier of (R^1 | (R^1 ].0,(0 + p1).[)) st S1[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
;
S1[x,y]take
a
;
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
;
( 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;
( ( 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) )
;
( b <= 0 implies y = 1 - ((arccos a) / (2 * PI)) )assume
b <= 0
;
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
;
verum end; suppose A22:
b > 0
;
ex y being Element of the carrier of (R^1 | (R^1 ].0,(0 + p1).[)) st S1[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
;
S1[x,y]take
a
;
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
;
( 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;
verum end; suppose A23:
b < 0
;
ex y being Element of the carrier of (R^1 | (R^1 ].0,(0 + p1).[)) st S1[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
;
S1[x,y]take
a
;
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
;
( 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;
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 S1[p,G . p]
from FUNCT_2:sch 3(A2);
hence
ex b1 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 b1 . p = (arccos x) / (2 * PI) ) & ( y <= 0 implies b1 . p = 1 - ((arccos x) / (2 * PI)) ) )
; verum