let r be real number ; :: thesis: for i being integer number holds cos . r = cos . (r + ((2 * PI ) * i))
let i be integer number ; :: thesis: cos . r = cos . (r + ((2 * PI ) * i))
thus cos . r = cos r by SIN_COS:def 23
.= cos (r + ((2 * PI ) * i)) by COMPLEX2:10
.= cos . (r + ((2 * PI ) * i)) by SIN_COS:def 23 ; :: thesis: verum