theorem :: COMPLEX2:4

for a being Real holds
( sin . (a - PI) = - (sin . a) & cos . (a - PI) = - (cos . a) )