let r be Real; :: thesis: for i being Integer holds sin . r = sin . (r + ((2 * PI) * i))
let i be Integer; :: 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