let r be Real; :: 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 8;
thus CircleMap . r = CircleMap . (r + (- [\r/])) by Th31
.= |[(cos ((2 * PI) * (1 / 4))),(sin ((2 * PI) * (1 / 4)))]| by A1, Def11
.= |[0,1]| by SIN_COS:77 ; :: thesis: verum