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