for i being Integer holds sin (PI * i) = 0