theorem :: SIN_COS8:32

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