defpred S1[ set , set ] means ex x, y being Real st
( \$1 = |[x,y]| & ( y >= 0 implies \$2 = 1 + (() / (2 * PI)) ) & ( y <= 0 implies \$2 = 1 - (() / (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 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 ; :: 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 = the carrier of () \ by Def10;
then A4: x in the carrier of () by XBOOLE_0:def 5;
A5: not x in by ;
A6: the carrier of () is Subset of () by TSEP_1:1;
then consider a, b being Element of REAL such that
A7: x = <*a,b*> by ;
reconsider x1 = x as Point of () by A4, A6;
A8: b = x1 `2 by ;
set k = arccos a;
A9: a = x1 `1 by ;
then A10: - 1 <= a by Th26;
A11: a <= 1 by ;
then A12: (arccos a) / (2 * PI) <= 1 / 2 by ;
A13: 1 ^2 = |.x1.| ^2 by
.= (a ^2) + (b ^2) by ;
A14: now :: thesis: not arccos a = PI
assume A15: arccos a = PI ; :: thesis: contradiction
then 1 - 1 = (((- 1) ^2) + (b ^2)) - 1 by
.= ((1 ^2) + (b ^2)) - 1 ;
then A16: b = 0 ;
a = - 1 by ;
hence contradiction by A7, A5, A16, TARSKI:def 1; :: thesis: verum
end;
A17: now :: thesis: not () / (2 * PI) = 1 / 2
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;
A18: 0 <= () / (2 * PI) by ;
A19: now :: thesis: for y being Real st y = 1 + (() / (2 * PI)) holds
y is Element of the carrier of (R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[))
let y be Real; :: thesis: ( y = 1 + (() / (2 * PI)) implies y is Element of the carrier of (R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[)) )
assume A20: y = 1 + (() / (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 ;
then A22: 1 / 2 < y by XXREAL_0:2;
y <= 1 + (1 / 2) by ;
then y < 3 / 2 by ;
hence y is Element of the carrier of (R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[)) by ; :: thesis: verum
end;
per cases ( b = 0 or b > 0 or b < 0 ) ;
suppose A23: 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 + (() / (2 * PI)) as Element of the carrier of (R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[)) by A19;
take y ; :: thesis: S1[x,y]
take a ; :: thesis: ex y being Real st
( x = |[a,y]| & ( y >= 0 implies y = 1 + (() / (2 * PI)) ) & ( y <= 0 implies y = 1 - (() / (2 * PI)) ) )

take b ; :: thesis: ( x = |[a,b]| & ( b >= 0 implies y = 1 + (() / (2 * PI)) ) & ( b <= 0 implies y = 1 - (() / (2 * PI)) ) )
thus x = |[a,b]| by A7; :: thesis: ( ( b >= 0 implies y = 1 + (() / (2 * PI)) ) & ( b <= 0 implies y = 1 - (() / (2 * PI)) ) )
a <> - 1 by ;
then a = 1 by ;
hence ( ( b >= 0 implies y = 1 + (() / (2 * PI)) ) & ( b <= 0 implies y = 1 - (() / (2 * PI)) ) ) by SIN_COS6:95; :: thesis: verum
end;
suppose A24: 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 + (() / (2 * PI)) as Element of the carrier of (R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[)) by A19;
take y ; :: thesis: S1[x,y]
take a ; :: thesis: ex y being Real st
( x = |[a,y]| & ( y >= 0 implies y = 1 + (() / (2 * PI)) ) & ( y <= 0 implies y = 1 - (() / (2 * PI)) ) )

take b ; :: thesis: ( x = |[a,b]| & ( b >= 0 implies y = 1 + (() / (2 * PI)) ) & ( b <= 0 implies y = 1 - (() / (2 * PI)) ) )
thus ( x = |[a,b]| & ( b >= 0 implies y = 1 + (() / (2 * PI)) ) & ( b <= 0 implies y = 1 - (() / (2 * PI)) ) ) by ; :: thesis: verum
end;
suppose A25: 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 - (() / (2 * PI));
A26: 1 - (() / (2 * PI)) <> 1 / 2 by A17;
1 - (() / (2 * PI)) >= 1 - (1 / 2) by ;
then A27: 1 / 2 < 1 - (() / (2 * PI)) by ;
1 - 0 >= 1 - (() / (2 * PI)) by ;
then 1 - (() / (2 * PI)) < 3 / 2 by XXREAL_0:2;
then reconsider y = 1 - (() / (2 * PI)) as Element of the carrier of (R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[)) by ;
take y ; :: thesis: S1[x,y]
take a ; :: thesis: ex y being Real st
( x = |[a,y]| & ( y >= 0 implies y = 1 + (() / (2 * PI)) ) & ( y <= 0 implies y = 1 - (() / (2 * PI)) ) )

take b ; :: thesis: ( x = |[a,b]| & ( b >= 0 implies y = 1 + (() / (2 * PI)) ) & ( b <= 0 implies y = 1 - (() / (2 * PI)) ) )
thus ( x = |[a,b]| & ( b >= 0 implies y = 1 + (() / (2 * PI)) ) & ( b <= 0 implies y = 1 - (() / (2 * PI)) ) ) by ; :: thesis: verum
end;
end;
end;
ex G being Function of ,(R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[)) st
for p being Point of holds S1[p,G . p] from hence ex b1 being Function of ,(R^1 | (R^1 ].(1 / 2),(3 / 2).[)) st
for p being Point of ex x, y being Real st
( p = |[x,y]| & ( y >= 0 implies b1 . p = 1 + (() / (2 * PI)) ) & ( y <= 0 implies b1 . p = 1 - (() / (2 * PI)) ) ) ; :: thesis: verum