sin | [.(PI / 2),((3 / 2) * PI ).] is one-to-one ;
hence sin | ].(PI / 2),((3 / 2) * PI ).[ is one-to-one by Th2, XXREAL_1:25; :: thesis: verum