theorem Th58: :: SIN_COS6:58

for i being Integer holds sin | [.((PI / 2) + ((2 * PI) * i)),(((3 / 2) * PI) + ((2 * PI) * i)).] is one-to-one