let r be real number ; :: thesis: ( frac r = 1 / 4 implies CircleMap . r = |[0 ,1]| )
assume frac r = 1 / 4 ; :: thesis: CircleMap . r = |[0 ,1]|
then A1: r - [\r/] = 1 / 4 by INT_1:def 6;
thus CircleMap . r = CircleMap . (r + (- [\r/])) by Th32
.= |[(cos ((2 * PI ) * (1 / 4))),(sin ((2 * PI ) * (1 / 4)))]| by A1, Def11
.= |[0 ,1]| by SIN_COS:82 ; :: thesis: verum