theorem Th57: :: SIN_COS6:57

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