:: deftheorem Def6 defines SphereMap BORSUK_7:def 6 :
for b₁ being Function of R^1,(Tunit_circle 3) holds
( b₁ = SphereMap iff for x being Real holds b₁ . x = |[(cos ((2 * PI) * x)),(sin ((2 * PI) * x)),0]| );