theorem :: SIN_COS7:73

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