theorem Th59: :: SIN_COS6:59
for i being Integer holds cos | [.((2 * PI) * i),(PI + ((2 * PI) * i)).] is one-to-one