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