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 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 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 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 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 :: 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
A28: ex x2, y2 being Real 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 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 ; :: thesis: verum