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

now :: thesis: for p being Point of (Topen_unit_circle c[-10]) holds f . p = g . p

let p be Point of (Topen_unit_circle c[-10]); :: 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 A30, SPPOL_2:1; :: thesis: verum

end;

hence f = g ; :: thesis: verum