theorem Th9: :: COMPLEX2:9

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