let r be Real; 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; 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
; verum