theorem :: SIN_COS5:43
for x being Real holds sinh (3 * x) = (3 * (sinh x)) + (4 * ((sinh x) |^ 3))