let x be Real; :: thesis: for n being Element of NAT holds cos (x + ((2 * n) * PI)) = cos x
let n be Element of NAT ; :: thesis: cos (x + ((2 * n) * PI)) = cos x
cos . x = cos . (x + ((2 * PI) * n)) by SIN_COS6:10;
hence cos (x + ((2 * n) * PI)) = cos x ; :: thesis: verum