theorem Th29: :: SIN_COS4:29

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