let f, g be Function of ,(R^1 | (R^1 ].(1 / 2),(3 / 2).[)); :: thesis: ( ( for p being Point of ex x, y being Real st
( p = |[x,y]| & ( y >= 0 implies f . p = 1 + (() / (2 * PI)) ) & ( y <= 0 implies f . p = 1 - (() / (2 * PI)) ) ) ) & ( for p being Point of ex x, y being Real st
( p = |[x,y]| & ( y >= 0 implies g . p = 1 + (() / (2 * PI)) ) & ( y <= 0 implies g . p = 1 - (() / (2 * PI)) ) ) ) implies f = g )

assume that
A28: for p being Point of ex x, y being Real st
( p = |[x,y]| & ( y >= 0 implies f . p = 1 + (() / (2 * PI)) ) & ( y <= 0 implies f . p = 1 - (() / (2 * PI)) ) ) and
A29: for p being Point of ex x, y being Real st
( p = |[x,y]| & ( y >= 0 implies g . p = 1 + (() / (2 * PI)) ) & ( y <= 0 implies g . p = 1 - (() / (2 * PI)) ) ) ; :: thesis: f = g
now :: thesis: for p being Point of holds f . p = g . p
let p be Point of ; :: thesis: f . p = g . p
A30: ex x2, y2 being Real st
( p = |[x2,y2]| & ( y2 >= 0 implies g . p = 1 + ((arccos x2) / (2 * PI)) ) & ( y2 <= 0 implies g . p = 1 - ((arccos x2) / (2 * PI)) ) ) by A29;
ex x1, y1 being Real st
( p = |[x1,y1]| & ( y1 >= 0 implies f . p = 1 + ((arccos x1) / (2 * PI)) ) & ( y1 <= 0 implies f . p = 1 - ((arccos x1) / (2 * PI)) ) ) by A28;
hence f . p = g . p by ; :: thesis: verum
end;
hence f = g ; :: thesis: verum