let i be Integer; :: thesis: cos | [.(PI + ((2 * PI) * i)),((2 * PI) + ((2 * PI) * i)).] is one-to-one
set Q1 = [.(PI + ((2 * PI) * i)),((2 * PI) + ((2 * PI) * i)).];
cos | [.(PI + ((2 * PI) * i)),((2 * PI) + ((2 * PI) * i)).] is increasing by Th56;
hence cos | [.(PI + ((2 * PI) * i)),((2 * PI) + ((2 * PI) * i)).] is one-to-one by FCONT_3:8; :: thesis: verum