let r be real number ; :: 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