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:10
.= c[10] by COMPLEX2:9, SIN_COS:34 ; :: thesis: verum