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