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 S₁[ Integer] means CircleMap . r = CircleMap . (r + $1);
A1: for i being Integer st S₁[i] holds
( S₁[i - 1] & S₁[i + 1] )

proof

let i be Integer; :: thesis: ( S₁[i] implies ( S₁[i - 1] & S₁[i + 1] ) )
assume A2: S₁[i] ; :: thesis: ( S₁[i - 1] & S₁[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: S₁[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: S₁[ 0 ] ;
for i being Integer holds S₁[i] from INT_1:sch 4(A3, A1);
hence CircleMap . r = CircleMap . (r + i) ; :: thesis: verum