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