let i be Integer; :: thesis: for r being Real holds CircleMap . r = CircleMap . (r + i)
let r be Real; :: thesis: CircleMap . r = CircleMap . (r + i)
defpred S1[ Integer] means CircleMap . r = CircleMap . (r + $1);
A1: for i being Integer st S1[i] holds
( S1[i - 1] & S1[i + 1] )
proof
let i be Integer; :: thesis: ( S1[i] implies ( S1[i - 1] & S1[i + 1] ) )
assume A2: S1[i] ; :: thesis: ( S1[i - 1] & S1[i + 1] )
thus CircleMap . (r + (i - 1)) = |[(cos ((2 * PI) * ((r + i) - 1))),(sin ((2 * PI) * ((r + i) - 1)))]| by Def11
.= |[(cos ((2 * PI) * (r + i))),(sin (((2 * PI) * (r + i)) + ((2 * PI) * (- 1))))]| by COMPLEX2:9
.= |[(cos ((2 * PI) * (r + i))),(sin ((2 * PI) * (r + i)))]| by COMPLEX2:8
.= CircleMap . r by A2, Def11 ; :: thesis: S1[i + 1]
thus CircleMap . (r + (i + 1)) = |[(cos ((2 * PI) * ((r + i) + 1))),(sin ((2 * PI) * ((r + i) + 1)))]| by Def11
.= |[(cos ((2 * PI) * (r + i))),(sin (((2 * PI) * (r + i)) + ((2 * PI) * 1)))]| by COMPLEX2:9
.= |[(cos ((2 * PI) * (r + i))),(sin ((2 * PI) * (r + i)))]| by COMPLEX2:8
.= CircleMap . r by A2, Def11 ; :: thesis: verum
end;
A3: S1[ 0 ] ;
for i being Integer holds S1[i] from INT_1:sch 4(A3, A1);
 hence CircleMap . r = CircleMap . (r + i) ; :: thesis: verum