let i be integer number ; :: thesis: sin | [.((PI / 2) + ((2 * PI ) * i)),(((3 / 2) * PI ) + ((2 * PI ) * i)).] is one-to-one
set Q = [.((PI / 2) + ((2 * PI ) * i)),(((3 / 2) * PI ) + ((2 * PI ) * i)).];
sin | [.((PI / 2) + ((2 * PI ) * i)),(((3 / 2) * PI ) + ((2 * PI ) * i)).] is decreasing by Th54;
hence sin | [.((PI / 2) + ((2 * PI ) * i)),(((3 / 2) * PI ) + ((2 * PI ) * i)).] is one-to-one by FCONT_3:16; :: thesis: verum