let r be Real; :: thesis: SphereMap . r = |[((cos * (AffineMap ((2 * PI),Q))) . r),((sin * (AffineMap ((2 * PI),0))) . r),0]|
SphereMap . r = |[(cos (((2 * PI) * r) + Q)),(sin ((2 * PI) * r)),0]| by Def6
.= |[((cos * (AffineMap ((2 * PI),0))) . r),(sin (((2 * PI) * r) + Q)),0]| by TOPREALB:2
.= |[((cos * (AffineMap ((2 * PI),0))) . r),((sin * (AffineMap ((2 * PI),0))) . r),0]| by TOPREALB:1 ;
hence SphereMap . r = |[((cos * (AffineMap ((2 * PI),Q))) . r),((sin * (AffineMap ((2 * PI),0))) . r),0]| ; :: thesis: verum