let i be integer number ; :: thesis: cos | [.((2 * PI ) * i),(PI + ((2 * PI ) * i)).] is one-to-one
set Q1 = [.((2 * PI ) * i),(PI + ((2 * PI ) * i)).];
cos | [.((2 * PI ) * i),(PI + ((2 * PI ) * i)).] is decreasing by Th55;
hence cos | [.((2 * PI ) * i),(PI + ((2 * PI ) * i)).] is one-to-one by FCONT_3:16; :: thesis: verum