let i be Integer; :: thesis: CircleMap . i = c[10]
thus CircleMap . i = |[(cos (((2 * PI) * i) + 0)),(sin ((2 * PI) * i))]| by Def11
.= |[(cos 0),(sin (((2 * PI) * i) + 0))]| by COMPLEX2:9
.= c[10] by COMPLEX2:8, SIN_COS:31 ; :: thesis: verum