:: deftheorem Def11 defines CircleMap TOPREALB:def 11 :
for b₁ being Function of R^1,(Tunit_circle 2) holds
( b₁ = CircleMap iff for x being Real holds b₁ . x = |[(cos ((2 * PI) * x)),(sin ((2 * PI) * x))]| );