theorem :: SIN_COS7:72

for x being Real holds sinh (5 * x) = ((5 * (sinh x)) + (20 * ((sinh x) |^ 3))) + (16 * ((sinh x) |^ 5))