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