let i be non zero Integer; :: thesis: cos is (2 * PI) * i -periodic

i in INT by INT_1:def 2;

then consider k being Nat such that

A1: ( i = k or i = - k ) by INT_1:def 1;

i in INT by INT_1:def 2;

then consider k being Nat such that

A1: ( i = k or i = - k ) by INT_1:def 1;