for i being Integer
for r being Real holds CircleMap . r = CircleMap . (r + i)