for x being Real
for n being Element of NAT holds
( ((cosh x) + (sinh x)) |^ n = (cosh (n * x)) + (sinh (n * x)) & ((cosh x) - (sinh x)) |^ n = (cosh (n * x)) - (sinh (n * x)) )