theorem Th3: :: INTEGRA8:3

for x being Real
for n being Element of NAT holds cos (x + ((2 * n) * PI)) = cos x