theorem Th31: :: SIN_COS4:31

for th1, th2 being Real holds (cos th1) * (sin th2) = (1 / 2) * ((sin (th1 + th2)) - (sin (th1 - th2)))