theorem Th1: :: INTEGRA8:1

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