let a be Real; :: thesis: cos ((- (2 * PI)) + a) = cos a
cos ((- (2 * PI)) + a) = cos (a - (2 * PI))
.= ((cos a) * 1) + ((sin a) * (sin (2 * PI))) by SIN_COS:77, SIN_COS:83
.= cos a by SIN_COS:77 ;
hence cos ((- (2 * PI)) + a) = cos a ; :: thesis: verum