thus CircleMap . (1 / 2) = |[(cos ((2 * PI ) * (1 / 2))),(sin ((2 * PI ) * (1 / 2)))]| by Def11
.= |[(- 1),0 ]| by SIN_COS:82 ; :: thesis: verum