let r be Real; :: thesis: for i being Integer holds cos r = cos (((2 * PI) * i) + r)
let i be Integer; :: thesis: cos r = cos (((2 * PI) * i) + r)
A1: cos . r = cos r by SIN_COS:def 19;
A2: cos . (((2 * PI) * i) + r) = cos (((2 * PI) * i) + r) by SIN_COS:def 19;
A3: cos . (((2 * PI) * (- i)) + (((2 * PI) * i) + r)) = cos (((2 * PI) * (- i)) + (((2 * PI) * i) + r)) by SIN_COS:def 19;

per cases ( i >= 0 or i < 0 ) ;

suppose i >= 0 ; :: thesis: cos r = cos (((2 * PI) * i) + r)

then reconsider iN = i as Element of NAT by INT_1:3;
cos r = cos (((2 * PI) * iN) + r) by A1, A2, SIN_COS2:11;
hence cos r = cos (((2 * PI) * i) + r) ; :: thesis: verum

end;

suppose i < 0 ; :: thesis: cos r = cos (((2 * PI) * i) + r)

then reconsider iN = - i as Element of NAT by INT_1:3;
set aa = ((2 * PI) * i) + r;
cos (((2 * PI) * i) + r) = cos (((2 * PI) * iN) + (((2 * PI) * i) + r)) by A2, A3, SIN_COS2:11;
hence cos r = cos (((2 * PI) * i) + r) ; :: thesis: verum

end;

end;