theorem Th8: :: COMPLEX2:8

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