:: deftheorem Def5 defines CircleIso BORSUK_7:def 5 :
for n being non zero Nat
for p being Point of (TOP-REAL n)
for r being non negative Real
for b₄ being Function of (Tunit_circle n),(Tcircle (p,r)) holds
( b₄ = CircleIso (p,r) iff for a being Point of (Tunit_circle n)
for b being Point of (TOP-REAL n) st a = b holds
b₄ . a = (r * b) + p );