for n being non zero Nat
for f being Function of (Tcircle ((0. (TOP-REAL (n + 1))),1)),(TOP-REAL n)
for x being Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)) st f is without_antipodals holds
(f . x) - (f . (- x)) <> 0. (TOP-REAL n)