for a being Real
for i being Integer holds sin a = sin (((2 * PI) * i) + a)