let r be Real; :: thesis: CircleMap . r = |[((cos * (AffineMap ((2 * PI),0))) . r),((sin * (AffineMap ((2 * PI),0))) . r)]|
thus CircleMap . r = |[(cos (((2 * PI) * r) + 0)),(sin ((2 * PI) * r))]| by Def11
.= |[((cos * (AffineMap ((2 * PI),0))) . r),(sin (((2 * PI) * r) + 0))]| by Th2
.= |[((cos * (AffineMap ((2 * PI),0))) . r),((sin * (AffineMap ((2 * PI),0))) . r)]| by Th1 ; :: thesis: verum