:: deftheorem Def8 defines Rn->S1 BORSUK_7:def 8 :
for n being Nat
for p being Point of (TOP-REAL n) st p <> 0. (TOP-REAL n) holds
Rn->S1 p = p (/) |.p.|;