let r be real number ; :: 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 6;
thus CircleMap . r = CircleMap . (r + (- [\r/])) by Th32
.= |[(cos ((2 * PI ) * (3 / 4))),(sin ((2 * PI ) * (3 / 4)))]| by A1, Def11
.= |[0 ,(- 1)]| by SIN_COS:82 ; :: thesis: verum