defpred S1[ 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 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 ].(1 / 2),((1 / 2) + 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:
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
;
A18:
0 <= (arccos a) / (2 * PI)
by A10, A11, Lm22;
A19:
now 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).[))let y be
Real;
( 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))
;
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;
verum end;
per cases
( b = 0 or b > 0 or b < 0 )
;
suppose A23:
b = 0
;
ex y being Element of the carrier of (R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[)) st S1[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
;
S1[x,y]take
a
;
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
;
( 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;
( ( 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;
verum end; suppose A25:
b < 0
;
ex y being Element of the carrier of (R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[)) st S1[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
;
S1[x,y]take
a
;
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
;
( 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;
verum end; end;
end;
ex G being Function of (Topen_unit_circle c[-10]),(R^1 | (R^1 ].(1 / 2),((1 / 2) + 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 ].(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 b1 . p = 1 + ((arccos x) / (2 * PI)) ) & ( y <= 0 implies b1 . p = 1 - ((arccos x) / (2 * PI)) ) )
; verum