theorem :: SIN_COS8:31

for x being Real holds
( (sinh x) |^ 3 = ((sinh (3 * x)) - (3 * (sinh x))) / 4 & (sinh x) |^ 4 = (((cosh (4 * x)) - (4 * (cosh (2 * x)))) + 3) / 8 & (sinh x) |^ 5 = (((sinh (5 * x)) - (5 * (sinh (3 * x)))) + (10 * (sinh x))) / 16 & (sinh x) |^ 6 = ((((cosh (6 * x)) - (6 * (cosh (4 * x)))) + (15 * (cosh (2 * x)))) - 10) / 32 & (sinh x) |^ 7 = ((((sinh (7 * x)) - (7 * (sinh (5 * x)))) + (21 * (sinh (3 * x)))) - (35 * (sinh x))) / 64 & (sinh x) |^ 8 = (((((cosh (8 * x)) - (8 * (cosh (6 * x)))) + (28 * (cosh (4 * x)))) - (56 * (cosh (2 * x)))) + 35) / 128 )