let r be Real; :: thesis: ( frac r = 3 / 4 implies CircleMap . r = |[0,(- 1)]| )
assume frac r = 3 / 4 ; :: thesis: CircleMap . r = |[0,(- 1)]|
then A1: r - [\r/] = 3 / 4 by INT_1:def 8;
thus CircleMap . r = CircleMap . (r + (- [\r/])) by Th31
.= |[(cos ((2 * PI) * (3 / 4))),(sin ((2 * PI) * (3 / 4)))]| by A1, Def11
.= |[0,(- 1)]| by SIN_COS:77 ; :: thesis: verum