:: deftheorem Def4 defines cLoop TOPALG_5:def 4 :
for r being Real
for b₂ being Function of I[01],(Tunit_circle 2) holds
( b₂ = cLoop r iff for x being Point of I[01] holds b₂ . x = |[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x))]| );