theorem Th5: :: SIN_COS5:5

for x being Real holds sin (2 * x) = (2 * (sin x)) * (cos x)