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 21
.= sin (r + ((2 * PI ) * i)) by COMPLEX2:9
.= sin . (r + ((2 * PI ) * i)) by SIN_COS:def 21 ; :: thesis: verum