for th being Real
for n being Nat holds sin . th = sin . (((2 * PI) * n) + th)