theorem :: SIN_COS:75

for th1, th2 being Real holds
( sin (th1 + th2) = ((sin th1) * (cos th2)) + ((cos th1) * (sin th2)) & cos (th1 + th2) = ((cos th1) * (cos th2)) - ((sin th1) * (sin th2)) ) by Th73;