let r be Real; :: thesis: for i being Integer holds cos . r = cos . (r + ((2 * PI) * i))
let i be Integer; :: thesis: cos . r = cos . (r + ((2 * PI) * i))
thus cos . r = cos r by SIN_COS:def 19
.= cos (r + ((2 * PI) * i)) by COMPLEX2:9
.= cos . (r + ((2 * PI) * i)) by SIN_COS:def 19 ; :: thesis: verum