let r be real number ; :: 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:10
.= |[(cos (((2 * PI ) * r) + ((2 * PI ) * i))),(sin (((2 * PI ) * r) + ((2 * PI ) * j)))]| by COMPLEX2:9
.= |[((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