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

( 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

hence
f = g
; :: thesis: verumlet 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;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