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:24, SIN_COS:78;
hence cos is 2 * PI -periodic by Th1; :: thesis: verum