theorem Th37: :: SIN_COS4:37

for th1, th2 being Real holds (sin (th1 + th2)) * (sin (th1 - th2)) = ((sin th1) * (sin th1)) - ((sin th2) * (sin th2))