theorem Th16: :: SIN_COS5:16

for x being Real holds sin (3 * x) = (- (4 * ((sin x) |^ 3))) + (3 * (sin x))