let a be Real; :: thesis: sin (((3 * PI) / 2) + a) = - (cos a)
sin (((3 * PI) / 2) + a) = ((sin ((3 * PI) / 2)) * (cos a)) + ((cos ((3 * PI) / 2)) * (sin a)) by SIN_COS:75
.= - (cos a) by SIN_COS:77 ;
hence sin (((3 * PI) / 2) + a) = - (cos a) ; :: thesis: verum