:: deftheorem Def9 defines Sn1->Sn BORSUK_7:def 9 :
for n being non zero Nat
for f being Function of (Tcircle ((0. (TOP-REAL (n + 1))),1)),(TOP-REAL n)
for b₃ being Function of (Tunit_circle (n + 1)),(Tunit_circle n) holds
( b₃ = Sn1->Sn f iff for x, y being Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)) st y = - x holds
b₃ . x = Rn->S1 ((f . x) - (f . y)) );