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