for x being real number st x in dom sin holds
( x + (2 * PI) in dom sin & x - (2 * PI) in dom sin & sin . x = sin . (x + (2 * PI)) ) by SIN_COS:27, SIN_COS:83;
hence sin is 2 * PI -periodic by Th1; :: thesis: verum