let x be Real; :: thesis: for n being Element of NAT holds sin (x + ((2 * n) * PI)) = sin x
let n be Element of NAT ; :: thesis: sin (x + ((2 * n) * PI)) = sin x
sin . x = sin . (((2 * PI) * n) + x) by SIN_COS2:10;
hence sin (x + ((2 * n) * PI)) = sin x ; :: thesis: verum