reconsider A1 = R^1 ].(1 / 2),((1 / 2) + p1).[ as non empty Subset of R^1 ;
defpred S1[ set , set ] means ex x, y being real number st
( $1 = |[x,y]| & ( y >= 0 implies $2 = 1 + ((arccos x) / (2 * PI )) ) & ( y <= 0 implies $2 = 1 - ((arccos x) / (2 * PI )) ) );
A1: the carrier of (R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[)) = A1 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 ].(1 / 2),((1 / 2) + p1).[)) st S1[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 ].(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: 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) / (2 * PI ) & (arccos a) / (2 * PI ) <= 1 / 2 ) by Lm24;
A11: 1 ^2 = |.x1.| ^2 by A4, Th12
.= (a ^2 ) + (b ^2 ) by A8, JGRAPH_3:10 ;
A12: now
assume A13: arccos a = PI ; :: thesis: contradiction
then A14: a = - 1 by A9, SIN_COS6:100;
1 - 1 = (((- 1) ^2 ) + (b ^2 )) - 1 by A9, A11, A13, SIN_COS6:100
.= ((1 ^2 ) + (b ^2 )) - 1 ;
then b = 0 ;
hence contradiction by A6, A7, A14, TARSKI:def 1; :: thesis: verum
end;
A15: now
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:93;
hence contradiction by A12, XCMPLX_1:58; :: thesis: verum
end;
A16: now
let y be real number ; :: 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 A17: y = 1 + ((arccos a) / (2 * PI )) ; :: thesis: y is Element of the carrier of (R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[))
then A18: ( 1 + 0 <= y & y <= 1 + (1 / 2) ) by A10, XREAL_1:8;
y <> 1 + (1 / 2) by A15, A17;
then ( 1 / 2 < y & y < 3 / 2 ) by A18, XXREAL_0:1, XXREAL_0:2;
hence y is Element of the carrier of (R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[)) by A1, XXREAL_1:4; :: thesis: verum
end;
per cases ( b = 0 or b > 0 or b < 0 ) ;
suppose A19: b = 0 ; :: thesis: ex y being Element of the carrier of (R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[)) st S1[x,y]
then a <> - 1 by A6, A7, TARSKI:def 1;
then A20: a = 1 by A11, A19, SQUARE_1:110;
reconsider y = 1 + ((arccos a) / (2 * PI )) as Element of the carrier of (R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[)) by A16;
take y ; :: thesis: S1[x,y]
take a ; :: thesis: ex y being real number 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 A6; :: thesis: ( ( b >= 0 implies y = 1 + ((arccos a) / (2 * PI )) ) & ( b <= 0 implies y = 1 - ((arccos a) / (2 * PI )) ) )
thus ( ( b >= 0 implies y = 1 + ((arccos a) / (2 * PI )) ) & ( b <= 0 implies y = 1 - ((arccos a) / (2 * PI )) ) ) by A20, SIN_COS6:97; :: thesis: verum
end;
suppose A21: b > 0 ; :: thesis: 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 A16;
take y ; :: thesis: S1[x,y]
take a ; :: thesis: ex y being real number 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 A6, A21; :: thesis: verum
end;
suppose A22: b < 0 ; :: thesis: 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 ));
A23: ( 1 - 0 >= 1 - ((arccos a) / (2 * PI )) & 1 - ((arccos a) / (2 * PI )) >= 1 - (1 / 2) ) by A10, XREAL_1:15;
1 - ((arccos a) / (2 * PI )) <> 1 / 2 by A15;
then ( 1 / 2 < 1 - ((arccos a) / (2 * PI )) & 1 - ((arccos a) / (2 * PI )) < 3 / 2 ) by A23, XXREAL_0:1, 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, XXREAL_1:4;
take y ; :: thesis: S1[x,y]
take a ; :: thesis: ex y being real number 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 A6, A22; :: thesis: 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 number st
( p = |[x,y]| & ( y >= 0 implies b1 . p = 1 + ((arccos x) / (2 * PI )) ) & ( y <= 0 implies b1 . p = 1 - ((arccos x) / (2 * PI )) ) ) ; :: thesis: verum