let i be integer number ; :: 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;
then (cos | [.(PI + ((2 * PI ) * i)),((2 * PI ) + ((2 * PI ) * i)).]) | [.(PI + ((2 * PI ) * i)),((2 * PI ) + ((2 * PI ) * i)).] is increasing ;
then (cos | [.(PI + ((2 * PI ) * i)),((2 * PI ) + ((2 * PI ) * i)).]) | [.(PI + ((2 * PI ) * i)),((2 * PI ) + ((2 * PI ) * i)).] is one-to-one by FCONT_3:16;
hence cos | [.(PI + ((2 * PI ) * i)),((2 * PI ) + ((2 * PI ) * i)).] is one-to-one by RELAT_1:101; :: thesis: verum