let f, g be Function of (Topen_unit_circle c[10] ),(R^1 | (R^1 ].0 ,1.[)); :: thesis: ( ( for p being Point of (Topen_unit_circle c[10] ) ex x, y being real number st
( p = |[x,y]| & ( y >= 0 implies f . p = (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 number st
( p = |[x,y]| & ( y >= 0 implies g . p = (arccos x) / (2 * PI ) ) & ( y <= 0 implies g . p = 1 - ((arccos x) / (2 * PI )) ) ) ) implies f = g )
assume that
A26: for p being Point of (Topen_unit_circle c[10] ) ex x, y being real number st
( p = |[x,y]| & ( y >= 0 implies f . p = (arccos x) / (2 * PI ) ) & ( y <= 0 implies f . p = 1 - ((arccos x) / (2 * PI )) ) ) and
A27: for p being Point of (Topen_unit_circle c[10] ) ex x, y being real number st
( p = |[x,y]| & ( y >= 0 implies g . p = (arccos x) / (2 * PI ) ) & ( y <= 0 implies g . p = 1 - ((arccos x) / (2 * PI )) ) ) ; :: thesis: f = g

now

let p be Point of (Topen_unit_circle c[10] ); :: thesis: f . p = g . p
A28: ex x2, y2 being real number st
( p = |[x2,y2]| & ( y2 >= 0 implies g . p = (arccos x2) / (2 * PI ) ) & ( y2 <= 0 implies g . p = 1 - ((arccos x2) / (2 * PI )) ) ) by A27;
ex x1, y1 being real number st
( p = |[x1,y1]| & ( y1 >= 0 implies f . p = (arccos x1) / (2 * PI ) ) & ( y1 <= 0 implies f . p = 1 - ((arccos x1) / (2 * PI )) ) ) by A26;
hence f . p = g . p by A28, SPPOL_2:1; :: thesis: verum

end;

hence f = g by FUNCT_2:113; :: thesis: verum