let r be Real; :: thesis: for i, j being Integer holds CircleMap . r = |[((cos * (AffineMap ((2 * PI),((2 * PI) * i)))) . r),((sin * (AffineMap ((2 * PI),((2 * PI) * j)))) . r)]|
let i, j be Integer; :: thesis: CircleMap . r = |[((cos * (AffineMap ((2 * PI),((2 * PI) * i)))) . r),((sin * (AffineMap ((2 * PI),((2 * PI) * j)))) . r)]|
thus CircleMap . r = |[(cos (((2 * PI) * r) + 0)),(sin ((2 * PI) * r))]| by Def11
.= |[(cos (((2 * PI) * r) + ((2 * PI) * i))),(sin (((2 * PI) * r) + 0))]| by COMPLEX2:9
.= |[(cos (((2 * PI) * r) + ((2 * PI) * i))),(sin (((2 * PI) * r) + ((2 * PI) * j)))]| by COMPLEX2:8
.= |[((cos * (AffineMap ((2 * PI),((2 * PI) * i)))) . r),(sin (((2 * PI) * r) + ((2 * PI) * j)))]| by Th2
.= |[((cos * (AffineMap ((2 * PI),((2 * PI) * i)))) . r),((sin * (AffineMap ((2 * PI),((2 * PI) * j)))) . r)]| by Th1 ; :: thesis: verum