theorem :: SIN_COS2:11
for th being Real
for n being Nat holds cos . th = cos . (((2 * PI) * n) + th)